Flat ring homomorphisms

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

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.

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

theorem RingHom.Flat.id (R : Type u_1) [CommRing R] : (RingHom.id R).Flat

The identity of a ring is flat.

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.

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.

theorem RingHom.Flat.containsIdentities : ContainsIdentities fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat

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

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

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

theorem RingHom.Flat.holdsForLocalizationAway : HoldsForLocalizationAway fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat

theorem RingHom.Flat.ofLocalizationSpanTarget : OfLocalizationSpanTarget fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat

theorem RingHom.Flat.propertyIsLocal : PropertyIsLocal fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat

Flat is a local property of ring homomorphisms.

theorem RingHom.Flat.ofLocalizationPrime : OfLocalizationPrime fun {R S : Type u_4} [CommRing R] [CommRing S] => Flat

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

theorem RingHom.Flat.generalizingMap_comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Flat) : GeneralizingMap (PrimeSpectrum.comap f)

Spec S → Spec R is generalizing if R →+* S is flat.

theorem RingHom.Flat.of_isField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (hR : IsField R) (f : R →+* S) : f.Flat

theorem CommRingCat.inr_injective_of_flat {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T) (hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hg : (Hom.hom g).Flat) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g))

theorem CommRingCat.inl_injective_of_flat {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T) (hf : (Hom.hom f).Flat) (hg : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom g)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inl f g))