Basis of cotangent space can be realized as a presentation

Let S be a finitely presented R-algebra and suppose P : R[X] → S generates S with kernel I.

In this file we show Algebra.Generators.exists_presentation_of_free: If I/I² is free, there exists an R-presentation P' of S extending P with kernel I', such that I'/I'² is free on the images of the relations of P'.

References

• https://stacks.math.columbia.edu/tag/07CF

theorem Algebra.Generators.exists_presentation_of_basis_cotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] {α : Type u_4} (P : Generators R S α) [Finite α] {σ : Type u_5} (b₀ : Module.Basis σ S P.toExtension.Cotangent) : ∃ (P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ)) (b : Module.Basis (Unit ⊕ σ) S P'.toExtension.Cotangent), P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Version of Algebra.Generators.exists_presentation_of_free_cotangent taking a basis instead of a Module.Free assumption. Note that the basis b₀ only serves as a way of saying that I/I² is free of rank σ, which gives more definitional control over σ. If this does not matter, use Algebra.Generators.exists_presentation_of_free_cotangent instead.

theorem Algebra.Generators.exists_presentation_of_free_cotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] {α : Type u_4} (P : Generators R S α) [Finite α] [Module.Free S P.toExtension.Cotangent] : ∃ (P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b : Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent), P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Let S be a finitely presented R-algebra and suppose P : R[X] → S generates S with kernel I. If I/I² is free, there exists an R-presentation P' of S extending P with kernel I', such that I'/I'² is free on the images of the relations of P'. See Algebra.Generators.exists_presentation_of_basis_cotangent for a version taking a basis of I/I² instead.