differentials — Mathlib

English

From a presentation of S as an R-algebra one obtains a presentation of the module of differentials Ω[S/R].

Русский

Из презентации S как R-алгебры следует презентация модуля дифференциалов Ω[S/R].

LaTeX

$$$\\text{differentials pres: }\\text{Presentation } S\\, \\Omega[S/R]$$$

Lean4

/-- The presentation of the `S`-module `Ω[S⁄R]` deduced from a presentation
of `S` as a `R`-algebra. -/
noncomputable def differentials : Module.Presentation S Ω[S⁄R]
    where
  G := ι
  R := σ
  relation := _
  toSolution := differentialsSolution pres
  toIsPresentation := pres.differentialsSolution_isPresentation

Похожие утверждения