Descent of faithful flatness

Faithful flatness of an algebra descends along a faithfully flat extension of the base. Thus faithful flatness can be established after extending scalars to a faithfully flat algebra. The ring-homomorphism formulation supplies the descent property used to descend finite faithfully flat morphisms, such as isogenies of affine group schemes.

theorem Module.FaithfullyFlat.of_tensorProduct (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [FaithfullyFlat R S] [FaithfullyFlat S (TensorProduct R S T)] : FaithfullyFlat R T

Faithful flatness of an algebra descends along faithfully flat scalar extension.

theorem RingHom.FaithfullyFlat.codescendsAlong_faithfullyFlat : CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat) fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat

Faithfully flat ring maps descend along faithfully flat base change.