English
The differentials solution provides a presentation of the module of Kaehler differentials Ω[S/R].
Русский
Решение дифференциалов обеспечивает презентацию модуля Kaehler дифференциалов Ω[S/R].
LaTeX
$$$pres.differentialsSolution.IsPresentation$$$
Lean4
theorem differentialsSolution_isPresentation : pres.differentialsSolution.IsPresentation :=
by
rw [Module.Relations.Solution.isPresentation_iff]
constructor
· rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]
exact Extension.toKaehler_surjective.comp pres.cotangentSpaceBasis.repr.symm.surjective
· rw [← Module.Relations.range_map]
exact
Function.Exact.linearMap_ker_eq
((LinearMap.exact_iff_of_surjective_of_bijective_of_injective _ _ _ _ (hom₁ pres)
pres.cotangentSpaceBasis.repr.symm.toLinearMap .id (comm₁₂ pres) (by simpa using comm₂₃ pres)
(surjective_hom₁ pres) (LinearEquiv.bijective _) (Equiv.refl _).injective).2
pres.toExtension.exact_cotangentComplex_toKaehler)
