Descent for scalar extensions of algebra homomorphisms

A property of ring maps satisfying faithfully flat descent is reflected by faithfully flat extension of the common scalar ring. Use RingHom.CodescendsAlong.of_tensorProduct_map to deduce such a property of an algebra homomorphism from the corresponding property after extending scalars. In particular, it applies to finiteness and faithful flatness once their faithfully flat descent properties are supplied.

The rings share a universe because RingHom.CodescendsAlong is a descent condition for properties of maps between rings in one fixed universe. It does not supply a compatibility condition for transporting a property between universes.

theorem RingHom.CodescendsAlong.of_tensorProduct_map {P : {A B : Type u} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → Prop} (hP : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => P) fun {R S : Type u} [CommRing R] [CommRing S] => FaithfullyFlat) {R S A B : Type u} [CommRing R] [CommRing S] [CommRing A] [CommRing B] [Algebra R S] [Algebra R A] [Algebra R B] [Module.FaithfullyFlat R S] (f : A →ₐ[R] B) (hf : P (Algebra.TensorProduct.map (AlgHom.id R S) f).toRingHom) : P f.toRingHom

A property of ring maps with faithfully flat descent is reflected by faithfully flat extension of the common scalar ring of an algebra homomorphism.