Theorems · Definition · commutative algebra

KaehlerDifferential.cotangentComplexBaseChange

(R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (P : Type u_2) →
          (A : Type u_3) →
            [inst_2 : CommRing P] →
              [inst_3 : CommRing A] →
                [inst_4 : Algebra P S] →
                  [inst_5 : Algebra P A] →
                    [inst_6 : Algebra R P] →
                      [inst_7 : Algebra S A] →
                        [IsScalarTower P S A] →
                          TensorProduct P A ↥(RingHom.ker (algebraMap P S)) →ₗ[A] TensorProduct P A Ω[P⁄R]

This is (isomorphic to) the base change of the cotangent complex to A, but the domain and codomains of this are more manageable.

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTower