Documentation

Mathlib.RingTheory.RingHom.Flat

Flat ring homomorphisms #

In this file we define flat ring homomorphisms and show their meta properties.

source
def RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) :
Prop

A ring homomorphism f : R →+* S is flat if S is flat as an R module.

Equations
Instances For
    source
    theorem RingHom.Flat.id (R : Type u_1) [CommRing R] :
    (RingHom.id R).Flat

    The identity of a ring is flat.

    source
    theorem RingHom.Flat.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.Flat) (hg : g.Flat) :
    (g.comp f).Flat

    Composition of flat ring homomorphisms is flat.

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

    Bijective ring maps are flat.

    source
    theorem RingHom.Flat.containsIdentities :
    ContainsIdentities fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.stableUnderComposition :
    StableUnderComposition fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.respectsIso :
    RespectsIso fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.isStableUnderBaseChange :
    IsStableUnderBaseChange fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.holdsForLocalizationAway :
    HoldsForLocalizationAway fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.ofLocalizationSpanTarget :
    OfLocalizationSpanTarget fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.propertyIsLocal :
    PropertyIsLocal fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat

    Flat is a local property of ring homomorphisms.

    source
    theorem RingHom.Flat.ofLocalizationPrime :
    OfLocalizationPrime fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat
    source
    theorem RingHom.Flat.localRingHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Flat) (P : Ideal S) [P.IsPrime] (Q : Ideal R) [Q.IsPrime] (hQP : Q = Ideal.comap f P) :
    (Localization.localRingHom Q P f hQP).Flat