Theorems · Definition · commutative algebra

KaehlerDifferential.endEquivAuxEquiv

(R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          { f //
              (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f =
                IsScalarTower.toAlgHom R S
                  ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸
                    (KaehlerDifferential.ideal R S).cotangentIdeal) } ≃
            { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }

(Implementation) An Equiv version of KaehlerDifferential.End_equiv_aux. Used in KaehlerDifferential.endEquiv.

Defined in

Mathlib.RingTheory.Kaehler.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra