Documentation

Mathlib.RingTheory.RingHom.FaithfullyFlat

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.

source
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.

Stacks Tag 00HB (Part (4))

Equations
Instances For
    source
    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
    source
    theorem RingHom.FaithfullyFlat.flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FaithfullyFlat) :
    f.Flat
    source
    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 f.specComap
    source
    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 f.specComap
    source
    theorem RingHom.FaithfullyFlat.stableUnderComposition :
    StableUnderComposition fun {R S : Type u_3} [CommRing R] [CommRing S] => FaithfullyFlat
    source
    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
    source
    theorem RingHom.FaithfullyFlat.respectsIso :
    RespectsIso fun {R S : Type u_3} [CommRing R] [CommRing S] => FaithfullyFlat
    source
    theorem RingHom.FaithfullyFlat.isStableUnderBaseChange :
    IsStableUnderBaseChange fun {R S : Type u_3} [CommRing R] [CommRing S] => FaithfullyFlat