Faithfully flat ring maps

A ring map f : R →+* S is faithfully flat if S is faithfully flat as an R-algebra. This is the same as being flat and a surjection on prime spectra.

def RingHom.FaithfullyFlat {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) : Prop

A ring map f : R →+* S is faithfully flat if S is faithfully flat as an R-algebra.

theorem RingHom.faithfullyFlat_algebraMap_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S

theorem RingHom.FaithfullyFlat.flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FaithfullyFlat) : f.Flat

theorem RingHom.FaithfullyFlat.iff_flat_and_comap_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} : f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

theorem RingHom.FaithfullyFlat.eq_and {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] : FaithfullyFlat = fun (f : R →+* S) => f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

theorem RingHom.FaithfullyFlat.stableUnderComposition : StableUnderComposition fun {R S : Type u_3} [CommRing R] [CommRing S] => FaithfullyFlat

theorem RingHom.FaithfullyFlat.of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Bijective ⇑f) : f.FaithfullyFlat

theorem RingHom.FaithfullyFlat.injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FaithfullyFlat) : Function.Injective ⇑f

theorem RingHom.FaithfullyFlat.respectsIso : RespectsIso fun {R S : Type u_3} [CommRing R] [CommRing S] => FaithfullyFlat

theorem RingHom.FaithfullyFlat.isStableUnderBaseChange : IsStableUnderBaseChange fun {R S : Type u_3} [CommRing R] [CommRing S] => FaithfullyFlat