Theorems · Theorem · commutative algebra

Algebra.Generators.comp_localizationAway_ker

∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι) (f : P.Ring),
  (algebraMap P.Ring S) f = g →
    ((Algebra.Generators.localizationAway T g).comp P).ker =
      Ideal.map ((Algebra.Generators.localizationAway T g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(MvPolynomial.rename Sum.inr) f * MvPolynomial.X (Sum.inl ()) - 1}

Defined in: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Cited by: 1 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra CommRing Algebra Algebra IsScalarTower IsLocalization.Away

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites45

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
Finsuppstatement · cited by 5,255
Idealstatement and proof · cited by 4,748
Algebra.algebraMapstatement and proof · cited by 4,706
IsScalarTowerstatement and proof · cited by 3,896
AlgHomstatement · cited by 3,236
MvPolynomialstatement · cited by 2,140
map_mulproof · cited by 1,137

Cited by1

Results whose statement or proof uses this declaration.

Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHomproof · cited by 1