English
If R ⟶ S is finitely presented and S is such that the Kaehler differential modules are projective, then H1Cotangent R S is finitely presented as an S-module.
Русский
Если отображение R ⟶ S имеет конечную презентацию и модуль дифференциал Kaehler проектен как S-модуль, то H1Cotangent R S является конечной презентацией как S-модуль.
LaTeX
$$$[Algebra.FinitePresentation R S] \\Rightarrow [Module.FinitePresentation S (\\Omega[S\\! /\\! R])]$$$
Lean4
instance [FinitePresentation R S] [Module.Projective S Ω[S⁄R]] : Module.Finite S (H1Cotangent R S) :=
by
let P := Algebra.Presentation.ofFinitePresentation R S
have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
suffices Module.Finite S P.toExtension.H1Cotangent from
.of_surjective P.equivH1Cotangent.toLinearMap P.equivH1Cotangent.surjective
rw [Module.finite_def, Submodule.fg_top, ← LinearMap.ker_rangeRestrict]
have := Extension.Cotangent.finite P.fg_ker
have : Module.FinitePresentation S (LinearMap.range P.toExtension.cotangentComplex) :=
by
rw [← LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler]
exact
Module.finitePresentation_of_projective_of_exact _ _ (Subtype.val_injective) P.toExtension.toKaehler_surjective
(LinearMap.exact_subtype_ker_map _)
exact
Module.FinitePresentation.fg_ker (N := LinearMap.range P.toExtension.cotangentComplex) _
P.toExtension.cotangentComplex.surjective_rangeRestrict
