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 :
    RingHom.ContainsIdentities fun {R S : Type u_4} [CommRing R] [CommRing S] => RingHom.Flat
    source
    theorem RingHom.Flat.stableUnderComposition :
    RingHom.StableUnderComposition fun {R S : Type u_4} [CommRing R] [CommRing S] => RingHom.Flat
    source
    theorem RingHom.Flat.respectsIso :
    RingHom.RespectsIso fun {R S : Type u_4} [CommRing R] [CommRing S] => RingHom.Flat
    source
    theorem RingHom.Flat.isStableUnderBaseChange :
    RingHom.IsStableUnderBaseChange fun {R S : Type u_4} [CommRing R] [CommRing S] => RingHom.Flat
    source
    theorem RingHom.Flat.holdsForLocalizationAway :
    RingHom.HoldsForLocalizationAway fun {R S : Type u_4} [CommRing R] [CommRing S] => RingHom.Flat