English
An identity of differential commutator maps: the map from the extension’s cotangent complex composed with hom₁ equals a linear combination built from the differentials of the presentation relations.
Русский
Идентичность композиции дифференциальных отображений: композиция cottangentComplex и hom₁ равна линейной комбинации производных от реляций презентации.
LaTeX
$$$pres.toExtension.toKaehler.\\circ pres.cotangentSpaceBasis.repr.symm.toLinearMap = Finsupp.linearCombination S (\\lambda g \\, D _ _ (pres.val g))$$$
Lean4
/-- The shape of the presentation by generators and relations of the `S`-module `Ω[S⁄R]`
that is obtained from a presentation of `S` as an `R`-algebra. -/
@[simps G R]
noncomputable def differentialsRelations : Module.Relations S
where
G := ι
R := σ
relation
r := Finsupp.mapRange (algebraMap pres.Ring S) (by simp) ((mvPolynomialBasis R ι).repr (D _ _ (pres.relation r)))
