def kaehlerDifferentialsModule (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] : Type v

The module Ω[A⁄k] of Kähler differentials of the k-algebra A.

theorem goal135_leibniz (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] (a b : A) : (KaehlerDifferential.D k A) (a * b) = a • (KaehlerDifferential.D k A) b + b • (KaehlerDifferential.D k A) a

The universal derivation D : A → Ω[A⁄k] satisfies the Leibniz rule D(ab) = a · D b + b · D a.

theorem goal135_map_algebraMap (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] (r : k) : (KaehlerDifferential.D k A) ((algebraMap k A) r) = 0

The universal derivation kills elements coming from the base ring k.

theorem goal135_span_range (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] : Submodule.span A (Set.range ⇑(KaehlerDifferential.D k A)) = ⊤

The image of the universal derivation spans Ω[A⁄k] as an A-module.

noncomputable def goal136_universalProperty (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] {M : Type u_1} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] : (Ω[A⁄k] →ₗ[A] M) ≃ₗ[A] Derivation k A M

The universal property of Ω[A⁄k]: A-linear maps Ω[A⁄k] → M correspond naturally to k-derivations A → M.

theorem goal136_lift_comp (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] {M : Type u_1} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (D' : Derivation k A M) : D'.liftKaehlerDifferential.compDer (KaehlerDifferential.D k A) = D'

The lift of a k-derivation D' through the universal derivation recovers D'.

theorem goal136_lift_unique (k : Type u) (A : Type v) [CommRing k] [CommRing A] [Algebra k A] {M : Type u_1} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (f g : Ω[A⁄k] →ₗ[A] M) (hfg : f.compDer (KaehlerDifferential.D k A) = g.compDer (KaehlerDifferential.D k A)) : f = g

Uniqueness in the universal property: two A-linear maps Ω[A⁄k] → M that compose to the same derivation with D must be equal.