Theorems · Definition · commutative algebra

KaehlerDifferential.endEquiv

(R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Module.End S Ω[S⁄R] ≃ { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }

The endomorphisms of Ω[S⁄R] corresponds to sections of the surjection S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S, with J being the kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

Defined in

Mathlib.RingTheory.Kaehler.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra