Documentation

Mathlib.RingTheory.RingHom.Flat

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) :

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

Equations

f.Flat = Module.Flat R S

Instances For

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) :

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) :

theorem RingHom.Flat.lTensor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (A : Type u_4) {B : Type u_5} {D : Type u_7} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [CommRing B] [Algebra R B] [CommRing D] [Algebra R D] {f : B →ₐ[R] D} (hf : f.Flat) :

(Algebra.TensorProduct.lTensor A f).Flat

theorem RingHom.Flat.tensorProductMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [CommRing D] [Algebra R D] {f : A →ₐ[S] C} {g : B →ₐ[R] D} (hf : f.Flat) (hg : g.Flat) :

(Algebra.TensorProduct.map f g).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))