Theorems · Theorem · commutative algebra

Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl

∀ {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),
  ↑(Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm ∘ₗ
      LinearMap.inl T (TensorProduct S T P.toExtension.Cotangent)
        (Algebra.Generators.localizationAway T g).toExtension.Cotangent =
    LinearMap.liftBaseChange T
      (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).toComp P).toExtensionHom)

Defined in

Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalization.Away