feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation (#31034)

Let `S` be a finitely presented `R`-algebra and suppose `P : R[X] → S` generates `S` with
kernel `I`. In this PR we show that 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'`.

From Pi1.

Author: chrisflav

Mathlib.lean

@@ -5847,6 +5847,7 @@ public import Mathlib.RingTheory.EuclideanDomain
 public import Mathlib.RingTheory.Extension
 public import Mathlib.RingTheory.Extension.Basic
 public import Mathlib.RingTheory.Extension.Cotangent.Basic
+public import Mathlib.RingTheory.Extension.Cotangent.Basis
 public import Mathlib.RingTheory.Extension.Cotangent.Free
 public import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
 public import Mathlib.RingTheory.Extension.Generators

Mathlib/RingTheory/Extension/Cotangent/Basis.lean

@@ -0,0 +1,321 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.RingTheory.Extension.Cotangent.Basic
+public import Mathlib.RingTheory.Smooth.StandardSmoothCotangent
+public import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
+
+/-!
+# 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
+-/
+
+open Pointwise MvPolynomial TensorProduct
+namespace Algebra.Generators
+
+variable {R : Type*} {S : Type*} [CommRing R] [CommRing S] [Algebra R S] {σ : Type*}
+
+noncomputable section
+
+namespace PresentationOfFreeCotangent
+
+variable {ι : Type*} (P : Generators R S ι) {σ : Type*}
+  (b : Module.Basis σ S P.toExtension.Cotangent)
+
+/-- An auxiliary structure containing the data to construct the presentation in
+`Generators.exists_presentation_of_free`. -/
+structure Aux where
+  /-- A section of the projection `I → I/I²`. -/
+  f : P.toExtension.Cotangent → P.toExtension.ker
+  hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
+  /-- An element `g` that becomes invertible in `S = R[X₁, ..., Xₙ] / I`. -/
+  g : P.Ring
+  hgmem : g - 1 ∈ P.ker
+  hg : g • P.ker ≤ Ideal.span (Set.range <| Subtype.val ∘ f ∘ b)
+
+namespace Aux
+
+variable {P} {b}
+variable (D : Aux P b)
+
+/-- `T = R[X₁, ..., Xₙ] / (b₁, ..., bᵣ)` where the `bᵢ` are lifts of the basis elements
+of `I/I²` in `I`. -/
+abbrev T :=
+  MvPolynomial ι R ⧸ (Ideal.span <| Set.range <| Subtype.val ∘ D.f ∘ b)
+
+/-- The map `R[X₁, ..., Xₙ] → S` factors via `T`, because the `bᵢ` are in `I`. -/
+def hom : D.T →ₐ[R] S := Ideal.Quotient.liftₐ _ (aeval P.val) <| by
+  simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
+  intro i
+  simpa only [Generators.toExtension_Ring, Generators.toExtension_commRing, Function.comp_apply,
+    SetLike.mem_coe, RingHom.mem_ker, ← P.algebraMap_apply] using (D.f _).property
+
+instance : Algebra D.T S := D.hom.toAlgebra
+instance [Nontrivial S] : Nontrivial D.T := RingHom.domain_nontrivial (algebraMap D.T S)
+instance : IsScalarTower P.Ring D.T S := by
+  refine ⟨fun x y z ↦ ?_⟩
+  obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
+  obtain ⟨z, rfl⟩ := P.algebraMap_surjective z
+  simp only [Algebra.smul_def, map_mul, Generators.algebraMap_apply, ← mul_assoc]
+  rfl
+
+/-- The image of `g : R[X₁, ..., Xₙ]` in `T`. -/
+abbrev gbar : D.T := D.g
+
+/-- `S` is the localization of `T` away from `S`. -/
+instance : IsLocalization.Away D.gbar S := by
+  refine .of_surjective_of_isScalarTower (n := 1) ?_ ?_ _ ?_ (by simpa using D.hg)
+  · refine .of_comp (g := algebraMap P.Ring D.T) ?_
+    convert P.algebraMap_surjective
+    ext x
+    exact (IsScalarTower.algebraMap_apply _ D.T S x).symm
+  · simp [T, Ideal.Quotient.mk_surjective]
+  · suffices h : (algebraMap P.Ring S) D.g = 1 by simp [h]
+    rw [← map_one (algebraMap P.Ring S), ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
+    exact D.hgmem
+
+open Classical in
+/-- The "naive" presentation of `T = R[X₁, ..., Xₙ] / (b₁, ..., bᵣ)` over `R`.
+We make sure the section `T → R[X₁, ..., Xₙ]` maps `-1` to `-1` and `0` to `0`. -/
+def presLeft : Presentation R D.T ι σ :=
+  .naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else
+      Function.surjInv Ideal.Quotient.mk_surjective x) fun x ↦ by
+    dsimp only; split_ifs
+    · next h => subst h; rfl
+    · next h => subst h; rfl
+    · simp [Function.surjInv_eq]
+
+/-- The `i`-th generator of the kernel `(b₁, ..., bᵣ)` of the naive presentation of `T`. -/
+def kerGen (i : σ) : D.presLeft.toExtension.ker :=
+  ⟨(D.f (b i)).val, Presentation.mem_ker_naive _ _ i⟩
+
+/-- The identity on `R[X₁, ..., Xₙ]` as a map of presentations of `T` to `S`. -/
+def fhom : D.presLeft.Hom P where
+  val i := X i
+  aeval_val i := by simp [RingHom.algebraMap_toAlgebra, presLeft, hom, T]
+
+@[simp]
+lemma toAlgHom_fhom : D.fhom.toAlgHom = AlgHom.id R P.Ring := by
+  ext : 1
+  simp [fhom]
+
+lemma ker_presLeft_le : D.presLeft.ker ≤ P.ker := by
+  intro x hx
+  simpa only [toExtension_commRing, toExtension_Ring, RingHom.mem_ker,
+    toExtension_algebra₂, algebraMap_apply, Ideal.Quotient.algebraMap_eq,
+    map_zero] using (algebraMap D.T S).congr_arg hx
+
+/-- The forward direction of the isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`. -/
+def tensorCotangentHom : S ⊗[D.T] D.presLeft.toExtension.Cotangent →ₗ[S] P.toExtension.Cotangent :=
+  LinearMap.liftBaseChange _ (Extension.Cotangent.map D.fhom.toExtensionHom)
+
+lemma tensorCotangentHom_tmul (x : D.presLeft.toExtension.ker) :
+    D.tensorCotangentHom (1 ⊗ₜ[D.T] Extension.Cotangent.mk x) =
+      .mk ⟨x.val, D.ker_presLeft_le x.2⟩ := by
+  simp only [tensorCotangentHom, LinearMap.liftBaseChange_tmul, one_smul, presLeft,
+    Extension.Cotangent.map_mk, Extension.Hom.toAlgHom_apply, Hom.toExtensionHom_toRingHom,
+    toAlgHom_fhom, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]
+  rfl
+
+/-- The backwards direction of the isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`. -/
+def tensorCotangentInv : P.toExtension.Cotangent →ₗ[S] S ⊗[D.T] D.presLeft.toExtension.Cotangent :=
+  b.constr S fun i : σ ↦ 1 ⊗ₜ Extension.Cotangent.mk (D.kerGen i)
+
+@[simp]
+lemma tensorCotangentInv_apply (i : σ) :
+    D.tensorCotangentInv (b i) = 1 ⊗ₜ Extension.Cotangent.mk (D.kerGen i) :=
+  Module.Basis.constr_basis _ _ _ _
+
+lemma span_range_mk_kerGen : Submodule.span D.T
+    (Set.range fun i ↦ Extension.Cotangent.mk (D.kerGen i)) = ⊤ := by
+  refine Extension.Cotangent.span_eq_top_of_span_eq_ker _ ?_
+  dsimp only [presLeft, Presentation.naive_toGenerators]
+  exact (Generators.ker_naive _ _).symm
+
+/-- The linear isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`. -/
+def tensorCotangentEquiv :
+    S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent := by
+  refine LinearEquiv.ofLinear D.tensorCotangentHom D.tensorCotangentInv ?_ ?_
+  · refine b.ext fun i ↦ ?_
+    simpa only [LinearMap.coe_comp, Function.comp_apply, tensorCotangentInv_apply,
+      tensorCotangentHom_tmul] using D.hf (b i)
+  · ext : 2
+    refine LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_
+    simp [-toExtension_commRing, -toExtension_Ring, -toExtension_algebra₂, tensorCotangentHom_tmul,
+      kerGen, D.hf]
+
+lemma tensorCotangentEquiv_symm_apply (i : σ) :
+    D.tensorCotangentEquiv.symm (b i) = 1 ⊗ₜ Extension.Cotangent.mk (D.kerGen i) :=
+  D.tensorCotangentInv_apply i
+
+/-- The canonical presentation of `S` as the localization of `T` away from `g`. -/
+def presRight : Presentation D.T S Unit Unit :=
+  Presentation.localizationAway S D.gbar
+
+/-- The presentation of `S` over `R` obtained from composing the naive presentation of
+`T = R[X₁, ..., Xₙ]/(b₁, ..., bᵣ)` with the presentation of the localization away from `g`. -/
+def pres : Presentation R S (Unit ⊕ ι) (Unit ⊕ σ) :=
+  D.presRight.comp D.presLeft
+
+lemma map_ofComp_mk [Nontrivial S] :
+    (Extension.Cotangent.map
+      ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toExtensionHom)
+      (Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl ()), D.pres.relation_mem_ker _⟩) =
+      Generators.cMulXSubOneCotangent S D.gbar := by
+  simp_rw [Extension.Cotangent.map_mk, Generators.Hom.toExtensionHom_toAlgHom_apply]
+  congr 2
+  have : Nontrivial D.T := inferInstance
+  dsimp only [T, Generators.toExtension_Ring, Generators.toExtension_commRing] at this
+  rw [pres, presLeft, presRight, Presentation.relation_comp_localizationAway_inl]
+  · exact Generators.toAlgHom_ofComp_localizationAway _ _
+  · rw [Presentation.naive, Generators.naive_σ];
+    simp
+  · rw [Presentation.naive, Generators.naive_σ]
+    simp
+
+/-- The cotangent space of the constructed presentation is isomorphic
+to `(g X - 1)/(g X - 1)² × S ⊗[T] J/J²`. -/
+def cotangentEquivProd [Nontrivial S] : D.pres.toExtension.Cotangent ≃ₗ[S]
+    D.presRight.toExtension.Cotangent × S ⊗[D.T] D.presLeft.toExtension.Cotangent :=
+  (D.presLeft.cotangentCompLocalizationAwayEquiv (T := S) D.gbar D.map_ofComp_mk) ≪≫ₗ
+    LinearEquiv.prodComm _ _ _
+
+lemma cotangentEquivProd_symm_apply [Nontrivial S] (x : D.presRight.toExtension.Cotangent)
+      (y : S ⊗[D.T] D.presLeft.toExtension.Cotangent) :
+    D.cotangentEquivProd.symm (x, y) =
+      (D.presLeft.cotangentCompLocalizationAwayEquiv (T := S) D.gbar D.map_ofComp_mk).symm (y, x) :=
+  rfl
+
+/-- The basis of `S ⊗[T] J/J²` induced from the basis on `I/I²`. -/
+def basisLeft : Module.Basis σ S (S ⊗[D.T] D.presLeft.toExtension.Cotangent) :=
+  b.map D.tensorCotangentEquiv.symm
+
+/-- The canonical basis on `(g X - 1)/(g X - 1)²`. -/
+def basisRight : Module.Basis Unit S D.presRight.toExtension.Cotangent :=
+  Generators.basisCotangentAway S D.gbar
+
+/-- The basis on the cotangent space of the constructed presentation. -/
+def basis [Nontrivial S] : Module.Basis (Unit ⊕ σ) S D.pres.toExtension.Cotangent :=
+  (Module.Basis.prod D.basisRight D.basisLeft).map D.cotangentEquivProd.symm
+
+lemma basis_inl [Nontrivial S] :
+    D.basis (.inl ()) =
+      D.cotangentEquivProd.symm (Generators.cMulXSubOneCotangent S D.gbar, 0) := by
+  simpa [basis] using Generators.basisCotangentAway_apply _ _
+
+lemma basis_inr [Nontrivial S] (i : σ) :
+    D.basis (.inr i) = D.cotangentEquivProd.symm (0, D.basisLeft i) := by
+  simp [basis]
+
+lemma pres_val_comp_inr : D.pres.val ∘ Sum.inr = P.val := funext (aeval_X _)
+
+/-- The constructed basis indeed is given by the images of the relations. -/
+lemma basis_apply [Nontrivial S] (r : Unit ⊕ σ) :
+    D.basis r = Extension.Cotangent.mk ⟨D.pres.relation r, D.pres.relation_mem_ker r⟩ := by
+  obtain (r | r) := r
+  · rw [basis_inl, cotangentEquivProd_symm_apply]
+    exact cotangentCompLocalizationAwayEquiv_symm_inr _ _ _
+  · rw [basis_inr, cotangentEquivProd_symm_apply, cotangentCompLocalizationAwayEquiv_symm_inl,
+      basisLeft, Module.Basis.map_apply, tensorCotangentEquiv_symm_apply,
+      LinearMap.liftBaseChange_tmul, one_smul, Extension.Cotangent.map_mk]
+    rfl
+
+end PresentationOfFreeCotangent.Aux
+
+end
+
+open PresentationOfFreeCotangent in
+/--
+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.
+-/
+@[stacks 07CF]
+public lemma exists_presentation_of_basis_cotangent [Algebra.FinitePresentation R S]
+    {α : Type*} (P : Generators R S α) [Finite α] {σ : Type*}
+    (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, b r = Extension.Cotangent.mk ⟨P'.relation r, P'.relation_mem_ker r⟩ := by
+  cases subsingleton_or_nontrivial S
+  · let P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
+      { toGenerators := .ofSurjective (fun i : Unit ⊕ α ↦ 0) (Function.surjective_to_subsingleton _)
+        relation _ := 1
+        span_range_relation_eq_ker := by simpa using (RingHom.ker_eq_top_of_subsingleton _).symm }
+    have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
+    exact ⟨P', default, by subsingleton, by subsingleton⟩
+  classical
+  choose f hf using Extension.Cotangent.mk_surjective (P := P.toExtension)
+  let v (i : σ) : P.ker := f (b₀ i)
+  let J : Ideal P.Ring := Ideal.span (Set.range <| Subtype.val ∘ v)
+  have hJfg : P.ker.FG := by
+    rw [P.ker_eq_ker_aeval_val]
+    apply FinitePresentation.ker_fG_of_surjective
+    convert P.algebraMap_surjective
+    simp [P.algebraMap_eq]
+  have hJ : J ≤ P.ker := by simp [J, Ideal.span_le, Set.range_subset_iff]
+  suffices hJ : P.ker ≤ J ⊔ P.ker • P.ker by
+    obtain ⟨g, hgmem, hg⟩ := Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup hJfg le_rfl hJ
+    let D : Aux P b₀ := { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg }
+    exact ⟨D.pres, D.basis, D.pres_val_comp_inr, D.basis_apply⟩
+  rw [← Submodule.comap_le_comap_iff_of_le_range (f := P.ker.subtype) (by simp),
+    Submodule.comap_subtype_self,
+    Submodule.comap_sup_of_injective P.ker.subtype_injective (by simpa using hJ)
+    (by simp [Ideal.mul_le_left]),
+    Submodule.comap_smul'' P.ker.subtype_injective (by simp)]
+  simp only [Submodule.comap_subtype_self, J]
+  rw [← Submodule.coe_subtype, Ideal.span, Set.range_comp, ← Submodule.map_span,
+    Submodule.comap_map_eq_of_injective P.ker.subtype_injective,
+    ← Extension.Cotangent.ker_mk]
+  dsimp
+  simp only [← LinearMap.map_le_map_iff, Submodule.map_span, ← Set.range_comp,
+    Function.comp_def, ← Submodule.restrictScalars_span P.Ring S P.algebraMap_surjective]
+  refine le_trans le_top (top_le_iff.mpr ?_)
+  rw [Submodule.restrictScalars_eq_top_iff]
+  convert b₀.span_eq
+  exact hf _
+
+open PresentationOfFreeCotangent in
+/-- 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. -/
+@[stacks 07CF]
+public lemma exists_presentation_of_free_cotangent [Algebra.FinitePresentation R S]
+    {α : Type*} (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, b r = Extension.Cotangent.mk ⟨P'.relation r, P'.relation_mem_ker r⟩ := by
+  cases subsingleton_or_nontrivial S
+  · let P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
+      { toGenerators := .ofSurjective (fun i : Unit ⊕ α ↦ 0) (Function.surjective_to_subsingleton _)
+        relation _ := 1
+        span_range_relation_eq_ker := by simpa using (RingHom.ker_eq_top_of_subsingleton _).symm }
+    have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
+    exact ⟨P', default, by subsingleton, by subsingleton⟩
+  have : Module.Finite S P.toExtension.Cotangent :=
+    Algebra.Extension.Cotangent.finite P.fg_ker_of_finitePresentation
+  exact exists_presentation_of_basis_cotangent _ <| Module.finBasis S P.toExtension.Cotangent
+
+end Algebra.Generators

Mathlib/RingTheory/Extension/Generators.lean

@@ -110,6 +110,9 @@ lemma σ_injective : P.σ.Injective := by
   intro x y e
   rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]
 
+lemma aeval_val_surjective : Function.Surjective (aeval (R := R) P.val) :=
+  fun x ↦ ⟨P.σ x, by simp⟩
+
 lemma algebraMap_surjective : Function.Surjective (algebraMap P.Ring S) :=
   (⟨_, P.algebraMap_apply _ ▸ P.aeval_val_σ ·⟩)
 

Mathlib/RingTheory/Extension/Presentation/Basic.lean

@@ -509,10 +509,17 @@ lemma naive_relation : (naive s hs).relation = v := rfl
 
 @[simp] lemma naive_relation_apply (i : ι) : (naive s hs).relation i = v i := rfl
 
+lemma mem_ker_naive (i : ι) : v i ∈ (naive s hs).ker := relation_mem_ker _ i
+
 end
 
 end Construction
 
 end Presentation
 
+lemma Generators.fg_ker_of_finitePresentation [Algebra.FinitePresentation R S] {α : Type*}
+    (P : Generators R S α) [Finite α] : P.ker.FG := by
+  rw [Generators.ker_eq_ker_aeval_val]
+  exact Algebra.FinitePresentation.ker_fG_of_surjective _ P.aeval_val_surjective
+
 end Algebra