instFinitePresentationKaehlerDifferentialOfFinitePresentation

English

If R ⟶ S is finitely presented, then the Kaehler differential Ω[S/R] is finitely presented as an S-module.

Русский

Если отображение R ⟶ S конечной презентации, то дифференциал Кеидера Ω[S/R] является конечной презентацией как S-модуль.

LaTeX

$$$[Algebra.FinitePresentation R S] \\Rightarrow [Module.FinitePresentation S \\Omega[S\\! /\\! R]]$$$

Lean4

instance [Algebra.FinitePresentation R S] : Module.FinitePresentation S Ω[S⁄R] :=
  by
  let P := Algebra.Presentation.ofFinitePresentation R S
  have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
  refine Module.finitePresentation_of_surjective _ P.toExtension.toKaehler_surjective ?_
  rw [LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler, ← Submodule.map_top]
  exact (Extension.Cotangent.finite P.fg_ker).1.map P.toExtension.cotangentComplex

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