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

    source
    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
    source
    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
    source
    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
    source
    theorem RingHom.Flat.comp_iff_of_bijective_left {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hg : Function.Bijective ⇑g) :
    (g.comp f).Flat ↔ f.Flat
    source
    theorem RingHom.Flat.comp_iff_of_bijective_right {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : T →+* R} (hg : Function.Bijective ⇑g) :
    (f.comp g).Flat ↔ f.Flat
    source
    @[simp]
    theorem RingHom.Flat.ulift_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} :
    (ulift.{u₁, u₂, u_1, u_2} f).Flat ↔ f.Flat
    source
    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))
    source
    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))
    source
    def CommRingCat.flat :
    CategoryTheory.MorphismProperty CommRingCat

    The morphism property of flat ring maps.

    Equations
    Instances For
      source
      @[simp]
      theorem CommRingCat.flat_iff {R S : CommRingCat} (f : R ⟶ S) :
      flat f ↔ (Hom.hom f).Flat
      source
      theorem CommRingCat.flat_ofHom_iff {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
      flat (ofHom f) ↔ f.Flat
      source
      instance CommRingCat.instIsStableUnderCobaseChangeFlat :
      flat.IsStableUnderCobaseChange
      source
      theorem RingHom.Flat.mapOfCompatibleSMul {R S : Type u} (T A : Type u) [CommRing R] [CommRing S] [CommRing T] [CommRing A] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (h : (Algebra.TensorProduct.lmul' R).Flat) :
      (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).Flat

      If S ⊗[R] S → S is flat, then also T ⊗[R] A → T ⊗[S] A is flat.