English
The module of differentials Ω[S/R] admits a canonical solution arising from a presentation of S as an R-algebra, mapping generators to their differentials.
Русский
Модуль дифференциалов Ω[S/R] обладает каноническим решением, полученным из презентации S как R-алгебры, отображающим генераторы в их дифференциалы.
LaTeX
$$$\\text{differentialsSolution}: pres.differentialsRelations.Solution(\\Omega[S/R])$ with $\\text{var } g := D(\\cdot, \\cdot, (pres.val\; g))$ and appropriate linear relations.$$
Lean4
/-- The canonical map `(σ →₀ S) →ₗ[S] pres.toExtension.Cotangent`. -/
noncomputable def hom₁ : (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent :=
Finsupp.linearCombination S (fun r ↦ Extension.Cotangent.mk ⟨pres.relation r, by simp⟩)