Theorems · Theorem · commutative algebra

Algebra.Generators.map_comp_cotangentCompAwaySec

∀ {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},
  (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g →
    Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom ∘ₗ
        Algebra.Generators.cotangentCompAwaySec g P x =
      LinearMap.id

The section cotangentCompAwaySec is indeed a section of the canonical map J/J² → K/K².

Defined in

Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization.Away