Theorems · Theorem · commutative algebra

Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv

∀ {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 ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g)
  (a : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent),
  ((Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx) a).2 =
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) a

Defined in

Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Cited by

0 results in Mathlib

Foundations

Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization.Away