feat(RingTheory/StandardSmooth): presentation independent characterization (leanprover-community#31081)

We show that if `S` is of finite presentation over `R` such that `H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`, then `S` is `R`-standard smooth. The converse of this is already in mathlib.

In the next PR, we will deduce from this that smooth is equivalent to locally standard smooth.

From Pi1.

Author: chrisflav

Mathlib.lean

@@ -6247,6 +6247,7 @@ public import Mathlib.RingTheory.Smooth.NoetherianDescent
 public import Mathlib.RingTheory.Smooth.Pi
 public import Mathlib.RingTheory.Smooth.StandardSmooth
 public import Mathlib.RingTheory.Smooth.StandardSmoothCotangent
+public import Mathlib.RingTheory.Smooth.StandardSmoothOfFree
 public import Mathlib.RingTheory.Spectrum.Maximal.Basic
 public import Mathlib.RingTheory.Spectrum.Maximal.Defs
 public import Mathlib.RingTheory.Spectrum.Maximal.Localization

Mathlib/LinearAlgebra/Basis/Exact.lean

@@ -99,6 +99,14 @@ noncomputable def Module.Basis.ofSplitExact (hg : Function.Surjective g) (v : Ba
   .mk (v.linearIndependent.linearIndependent_of_exact_of_retraction hs hfg hainj hsa)
     (Submodule.top_le_span_of_exact_of_retraction hs hfg hg hsa hlib hab (by rw [v.span_eq]))
 
+@[simp]
+lemma Module.Basis.ofSplitExact_apply (hg : Function.Surjective g) (v : Basis ι R M)
+    (hainj : Function.Injective a) (hsa : ∀ i, s (v (a i)) = 0)
+    (hlib : LinearIndependent R (s ∘ v ∘ b))
+    (hab : Codisjoint (Set.range a) (Set.range b)) (k : κ) :
+    ofSplitExact hs hfg hg v hainj hsa hlib hab k = g (v (a k)) := by
+  simp [ofSplitExact]
+
 end
 
 section

Mathlib/RingTheory/Extension/Cotangent/Free.lean

@@ -91,6 +91,17 @@ lemma disjoint_ker_toKaehler_of_linearIndependent
   obtain rfl := (linearIndependent_iff.mp h) c hx
   simp
 
+lemma cotangentRestrict_bijective_of_basis_kaehlerDifferential
+    (huv : IsCompl (Set.range v) (Set.range u)) (b : Module.Basis κ S (Ω[S⁄R]))
+    (hb : ∀ k, b k = (D R S) (P.val (v k))) [Subsingleton (H1Cotangent R S)] :
+    Function.Bijective (cotangentRestrict P hu) := by
+  refine P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_
+  · simp_rw [← hb]
+    exact b.span_eq
+  · apply disjoint_ker_toKaehler_of_linearIndependent
+    simp_rw [← hb]
+    exact b.linearIndependent
+
 end Generators
 
 namespace PreSubmersivePresentation

Mathlib/RingTheory/Extension/Generators.lean

@@ -251,6 +251,20 @@ def baseChange (T) [CommRing T] [Algebra R T] (P : Generators R S ι) :
     use (a + b)
     rw [map_add, ha, hb]
 
+/-- Extend generators by more variables. -/
+noncomputable def extend (P : Generators R S ι) (b : ι' → S) : Generators R S (ι ⊕ ι') :=
+  .ofSurjective (Sum.elim P.val b) fun s ↦ by
+    use rename Sum.inl (P.σ s)
+    simp [aeval_rename]
+
+@[simp]
+lemma extend_val_inl (P : Generators R S ι) (b : ι' → S) (i : ι) :
+    (P.extend b).val (.inl i) = P.val i := rfl
+
+@[simp]
+lemma extend_val_inr (P : Generators R S ι) (b : ι' → S) (i : ι') :
+    (P.extend b).val (.inr i) = b i := rfl
+
 /-- Given generators `P` and an equivalence `ι ≃ P.vars`, these
 are the induced generators indexed by `ι`. -/
 noncomputable def reindex (P : Generators R S ι') (e : ι ≃ ι') :

Mathlib/RingTheory/Smooth/StandardSmooth.lean

@@ -168,9 +168,11 @@ instance IsStandardSmoothOfRelativeDimension.baseChange
 
 end BaseChange
 
+@[nontriviality]
 instance (priority := 100) [Subsingleton S] : IsStandardSmooth R S :=
   ⟨Unit, Unit, inferInstance, inferInstance, ⟨.ofSubsingleton R S⟩⟩
 
+@[nontriviality]
 instance (priority := 100) [Subsingleton S] : IsStandardSmoothOfRelativeDimension 0 R S :=
   ⟨Unit, Unit, inferInstance, inferInstance, .ofSubsingleton R S, by simp [Presentation.dimension]⟩
 

Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

@@ -214,6 +214,12 @@ noncomputable def basisKaehlerOfIsCompl {κ : Type*} {f : κ → ι}
     simp [Finsupp.single_eq_pi_single]
   · exact hcompl.2
 
+@[simp]
+lemma basisKaehlerOfIsCompl_apply {κ : Type*} {f : κ → ι}
+    (hf : Function.Injective f) (hcompl : IsCompl (Set.range f) (Set.range P.map)) (k : κ) :
+    P.basisKaehlerOfIsCompl hf hcompl k = KaehlerDifferential.D _ _ (P.val (f k)) := by
+  simp [basisKaehlerOfIsCompl]
+
 /-- Given a submersive presentation of `S` as `R`-algebra, the images of `dxᵢ`
 for `i` in the complement of `σ` in `ι` form a basis of `Ω[S⁄R]`. -/
 @[stacks 00T7 "(2)"]
@@ -223,6 +229,11 @@ noncomputable def basisKaehler :
     rw [Subtype.range_coe_subtype]
     exact IsCompl.symm isCompl_compl
 
+@[simp]
+lemma basisKaehler_apply (k : ((Set.range P.map)ᶜ : Set _)) :
+    P.basisKaehler k = KaehlerDifferential.D _ _ (P.val k) := by
+  simp [basisKaehler]
+
 /-- If `P` is a submersive presentation of `S` as an `R`-algebra, `Ω[S⁄R]` is free. -/
 @[stacks 00T7 "(2)"]
 theorem free_kaehlerDifferential (P : SubmersivePresentation R S ι σ) :
@@ -306,6 +317,15 @@ theorem IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential [Nontrivial
   obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
   rw [P.rank_kaehlerDifferential, hP]
 
+lemma IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth [Nontrivial S]
+    [IsStandardSmooth R S] (n : ℕ) :
+    IsStandardSmoothOfRelativeDimension n R S ↔ Module.rank S Ω[S⁄R] = n := by
+  refine ⟨fun h ↦ IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential _, fun h ↦ ?_⟩
+  obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
+  refine ⟨_, _, _, ‹_›, ⟨P, ?_⟩⟩
+  apply Nat.cast_injective (R := Cardinal)
+  rwa [← P.rank_kaehlerDifferential]
+
 instance IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential
     [IsStandardSmoothOfRelativeDimension 0 R S] : Subsingleton Ω[S⁄R] := by
   cases subsingleton_or_nontrivial S

Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean

@@ -0,0 +1,100 @@
+/-
+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.Basis
+public import Mathlib.RingTheory.Extension.Cotangent.Free
+
+/-!
+# Standard smooth of free Kaehler differentials
+
+In this file we show a presentation independent characterization of being
+standard smooth: An `R`-algebra `S` of finite presentation is standard smooth if and only if
+`H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`.
+
+From this we deduce relations of standard smooth with other local properties.
+
+## Main results
+
+- `IsStandardSmooth.iff_exists_basis_kaehlerDifferential`: An `R`-algebra `S` of finite
+  presentation is standard smooth if and only if `H¹(S/R) = 0` and `Ω[S⁄R]` is free on
+  `{d sᵢ}ᵢ` for some `sᵢ : S`.
+- `Etale.iff_isStandardSmoothOfRelativeDimension_zero`: An `R`-algebra `S` is
+  étale if and only if it is standard smooth of relative dimension zero.
+
+## Notes
+
+For an example of an algebra with `H¹(S/R) = 0` and `Ω[S⁄R]` finite and free, but
+`S` not standard smooth over `R`, consider `R = ℝ` and `S = R[x,y]/(x² + y² - 1)` the
+coordinate ring of the circle. One can show that then `Ω[S⁄R]` is `S`-free on `ω = xdy - ydx`,
+but there are no `f g : S` such that `ω = g df`.
+
+## TODOs
+
+- Deduce from this that smooth is equivalent to locally standard smooth (TODO @chrisflav).
+-/
+
+@[expose] public section
+
+namespace Algebra
+
+open KaehlerDifferential
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+
+/-- If `H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`, then `S`
+is `R`-standard smooth. -/
+theorem IsStandardSmooth.of_basis_kaehlerDifferential [FinitePresentation R S]
+    [Subsingleton (H1Cotangent R S)]
+    {I : Type*} (b : Module.Basis I S (Ω[S⁄R])) (hb : Set.range b ⊆ Set.range (D R S)) :
+    IsStandardSmooth R S := by
+  nontriviality S
+  obtain ⟨n, ⟨P⟩⟩ := (FiniteType.iff_exists_generators (R := R) (S := S)).mp inferInstance
+  choose f' hf' using hb
+  let P := P.extend fun i ↦ f' ⟨i, rfl⟩
+  have hb (i : I) : b i = D R S (P.val (Sum.inr i)) := by simp [P, hf']
+  have : Function.Bijective (P.cotangentRestrict _) :=
+    P.cotangentRestrict_bijective_of_basis_kaehlerDifferential Sum.inl_injective
+      Set.isCompl_range_inl_range_inr.symm b hb
+  let bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
+    .ofRepr (.ofBijective (P.cotangentRestrict _) this)
+  have : Finite I := Module.Finite.finite_basis b
+  obtain ⟨Q, bcot, hcomp, hbcot⟩ := P.exists_presentation_of_basis_cotangent bcot'
+  let P' : PreSubmersivePresentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
+    { __ := Q
+      map := Sum.map _root_.id Sum.inl
+      map_inj := Sum.map_injective.mpr ⟨fun _ _ h ↦ h, Sum.inl_injective⟩ }
+  have hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map) := by
+    simp [P', ← eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff]
+  have hbij : Function.Bijective (P'.cotangentRestrict P'.map_inj) := by
+    apply P'.cotangentRestrict_bijective_of_basis_kaehlerDifferential P'.map_inj hcompl b
+    intro k
+    simp only [hb, ← hcomp, P', Function.comp_def]
+  let P'' : SubmersivePresentation R S _ _ :=
+    ⟨P', P'.isUnit_jacobian_of_cotangentRestrict_bijective bcot hbcot hbij⟩
+  exact P''.isStandardSmooth
+
+/-- An `R`-algebra `S` of finite presentation is standard smooth if and only if
+`H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`. -/
+theorem IsStandardSmooth.iff_exists_basis_kaehlerDifferential [FinitePresentation R S] :
+    IsStandardSmooth R S ↔ Subsingleton (H1Cotangent R S) ∧
+      ∃ (I : Type) (b : Module.Basis I S (Ω[S⁄R])), Set.range b ⊆ Set.range (D R S) := by
+  refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩
+  obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := Algebra.IsStandardSmooth.out (R := R) (S := S)
+  exact ⟨_, P.basisKaehler, by simp [Set.range_subset_iff]⟩
+
+/-- `S` is an étale `R`-algebra if and only if it is standard smooth of relative dimension `0`. -/
+theorem Etale.iff_isStandardSmoothOfRelativeDimension_zero :
+    Etale R S ↔ IsStandardSmoothOfRelativeDimension 0 R S := by
+  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
+  nontriviality S
+  suffices h : IsStandardSmooth R S by
+    simp [IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth]
+  rw [IsStandardSmooth.iff_exists_basis_kaehlerDifferential]
+  refine ⟨inferInstance, ⟨Empty, Module.Basis.empty Ω[S⁄R], ?_⟩⟩
+  simp [Set.range_subset_iff]
+
+end Algebra