Theorems · Theorem · commutative algebra

Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (A : Type u_1) [inst_3 : CommRing A] [inst_4 : Algebra S A] [inst_5 : Algebra P.Ring A]
  [inst_6 : IsScalarTower P.Ring S A],
  KaehlerDifferential.cotangentComplexBaseChange R S P.Ring A =
    ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ
      LinearMap.baseChange A P.cotangentComplex ∘ₗ
        ↑((TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
            LinearEquiv.baseChange S A (TensorProduct P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv)

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTower