English
The cokernel solution provides a presentation of the quotient module, i.e. the map to the quotient induces an isomorphism with the target.
Русский
Решение коконеллы задаёт презентацию фактор-модуля: полученная карта на поэтому фактор-модуль индуцирует изоморфизм с целевым модулем.
LaTeX
$$isPresentation : (pres₂.cokernelSolution data).IsPresentation$$
Lean4
/-- The `S`-module `Ω[S⁄R]` contains an obvious solution to the system of linear
equations `pres.differentialsRelations.Solution` when `pres` is a presentation
of `S` as an `R`-algebra. -/
noncomputable def differentialsSolution : pres.differentialsRelations.Solution Ω[S⁄R]
where
var g := D _ _ (pres.val g)
linearCombination_var_relation
r :=
by
simp only [differentialsRelations_G, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← comm₂₃',
← comm₁₂_single]
apply DFunLike.congr_fun (Function.Exact.linearMap_comp_eq_zero (pres.toExtension.exact_cotangentComplex_toKaehler))
