Theorems · Definition · commutative algebra

KaehlerDifferential

(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type v

The module of Kähler differentials (Kahler differentials, Kaehler differentials). This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S. To view elements as a linear combination of the form s • D s', use KaehlerDifferential.tensorProductTo_surjective and Derivation.tensorProductTo_tmul. We also provide the notation Ω[S⁄R] for KaehlerDifferential R S. Note that the slash is \textfractionsolidus.

Defined in

Mathlib.RingTheory.Kaehler.Basic

Cited by

204 results in Mathlib

Foundations

Depth 81 from the axioms, rests on 1,631 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra