From 3b220c587207ebfe48e7bcc3634b403756877e90 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 17 Sep 2024 21:38:31 +0000
Subject: [PATCH] feat(RingTheory/StandardSmooth): ring isomorphisms are
 standard smooth (#16869)

We show that any `R`-algebra `S` where `algebraMap R S` is bijective, is standard smooth by constructing an explicit submersive presentation.

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry"
in June 2024.
---
 Mathlib/Algebra/MvPolynomial/Equiv.lean       | 11 ++++
 Mathlib/RingTheory/AlgebraicIndependent.lean  |  6 +-
 Mathlib/RingTheory/Generators.lean            | 12 ++++
 Mathlib/RingTheory/Presentation.lean          | 33 ++++++++++
 Mathlib/RingTheory/Smooth/StandardSmooth.lean | 64 ++++++++++++++++++-
 5 files changed, 120 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/MvPolynomial/Equiv.lean b/Mathlib/Algebra/MvPolynomial/Equiv.lean
index a6350e2e62a69..7b6e4a464b071 100644
--- a/Mathlib/Algebra/MvPolynomial/Equiv.lean
+++ b/Mathlib/Algebra/MvPolynomial/Equiv.lean
@@ -196,6 +196,17 @@ def isEmptyAlgEquiv [he : IsEmpty σ] : MvPolynomial σ R ≃ₐ[R] R :=
       ext i m
       exact IsEmpty.elim' he i)
 
+variable {R S₁ σ} in
+@[simp]
+lemma aeval_injective_iff_of_isEmpty [IsEmpty σ] [CommSemiring S₁] [Algebra R S₁] {f : σ → S₁} :
+    Function.Injective (aeval f : MvPolynomial σ R →ₐ[R] S₁) ↔
+      Function.Injective (algebraMap R S₁) := by
+  have : aeval f = (Algebra.ofId R S₁).comp (@isEmptyAlgEquiv R σ _ _).toAlgHom := by
+    ext i
+    exact IsEmpty.elim' ‹IsEmpty σ› i
+  rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]
+  rfl
+
 /-- The ring isomorphism between multivariable polynomials in no variables
 and the ground ring. -/
 @[simps!]
diff --git a/Mathlib/RingTheory/AlgebraicIndependent.lean b/Mathlib/RingTheory/AlgebraicIndependent.lean
index b0e1db85e19c4..0e358adaa9418 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent.lean
@@ -82,11 +82,7 @@ theorem algebraicIndependent_iff_injective_aeval :
 @[simp]
 theorem algebraicIndependent_empty_type_iff [IsEmpty ι] :
     AlgebraicIndependent R x ↔ Injective (algebraMap R A) := by
-  have : aeval x = (Algebra.ofId R A).comp (@isEmptyAlgEquiv R ι _ _).toAlgHom := by
-    ext i
-    exact IsEmpty.elim' ‹IsEmpty ι› i
-  rw [AlgebraicIndependent, this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R ι _ _).bijective]
-  rfl
+  rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]
 
 namespace AlgebraicIndependent
 
diff --git a/Mathlib/RingTheory/Generators.lean b/Mathlib/RingTheory/Generators.lean
index 8cd1cdb774bff..3ded91b21c690 100644
--- a/Mathlib/RingTheory/Generators.lean
+++ b/Mathlib/RingTheory/Generators.lean
@@ -106,6 +106,18 @@ def ofSurjective {vars} (val : vars → S) (h : Function.Surjective (aeval (R :=
   σ' x := (h x).choose
   aeval_val_σ' x := (h x).choose_spec
 
+/-- If `algebraMap R S` is surjective, the empty type generates `S`. -/
+noncomputable def ofSurjectiveAlgebraMap (h : Function.Surjective (algebraMap R S)) :
+    Generators.{w} R S :=
+  ofSurjective PEmpty.elim <| fun s ↦ by
+    use C (h s).choose
+    simp [(h s).choose_spec]
+
+/-- The canonical generators for `R` as an `R`-algebra. -/
+noncomputable def id : Generators.{w} R R := ofSurjectiveAlgebraMap <| by
+  rw [id.map_eq_id]
+  exact RingHomSurjective.is_surjective
+
 /-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective. -/
 noncomputable
 def ofAlgHom {I} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective f) :
diff --git a/Mathlib/RingTheory/Presentation.lean b/Mathlib/RingTheory/Presentation.lean
index b7d31cd531382..6de568a38eb2b 100644
--- a/Mathlib/RingTheory/Presentation.lean
+++ b/Mathlib/RingTheory/Presentation.lean
@@ -123,6 +123,39 @@ lemma finitePresentation_of_isFinite [P.IsFinite] :
 
 section Construction
 
+/-- If `algebraMap R S` is bijective, the empty generators are a presentation with no relations. -/
+noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)) :
+    Presentation.{t, w} R S where
+  __ := Generators.ofSurjectiveAlgebraMap h.surjective
+  rels := PEmpty
+  relation := PEmpty.elim
+  span_range_relation_eq_ker := by
+    simp only [Set.range_eq_empty, Ideal.span_empty]
+    symm
+    rw [← RingHom.injective_iff_ker_eq_bot]
+    show Function.Injective (aeval PEmpty.elim)
+    rw [aeval_injective_iff_of_isEmpty]
+    exact h.injective
+
+instance ofBijectiveAlgebraMap_isFinite (h : Function.Bijective (algebraMap R S)) :
+    (ofBijectiveAlgebraMap.{t, w} h).IsFinite where
+  finite_vars := inferInstanceAs (Finite PEmpty.{w + 1})
+  finite_rels := inferInstanceAs (Finite PEmpty.{t + 1})
+
+lemma ofBijectiveAlgebraMap_dimension (h : Function.Bijective (algebraMap R S)) :
+    (ofBijectiveAlgebraMap h).dimension = 0 := by
+  show Nat.card PEmpty - Nat.card PEmpty = 0
+  simp only [Nat.card_eq_fintype_card, Fintype.card_ofIsEmpty, le_refl, tsub_eq_zero_of_le]
+
+variable (R) in
+/-- The canonical `R`-presentation of `R` with no generators and no relations. -/
+noncomputable def id : Presentation.{t, w} R R := ofBijectiveAlgebraMap Function.bijective_id
+
+instance : (id R).IsFinite := ofBijectiveAlgebraMap_isFinite (R := R) Function.bijective_id
+
+lemma id_dimension : (Presentation.id R).dimension = 0 :=
+  ofBijectiveAlgebraMap_dimension (R := R) Function.bijective_id
+
 section Localization
 
 variable (r : R) [IsLocalization.Away r S]
diff --git a/Mathlib/RingTheory/Smooth/StandardSmooth.lean b/Mathlib/RingTheory/Smooth/StandardSmooth.lean
index 33b0d6650afea..67da17a5eccf5 100644
--- a/Mathlib/RingTheory/Smooth/StandardSmooth.lean
+++ b/Mathlib/RingTheory/Smooth/StandardSmooth.lean
@@ -89,7 +89,7 @@ in June 2024.
 
 universe t t' w w' u v
 
-open TensorProduct
+open TensorProduct Classical
 
 variable (n : ℕ)
 
@@ -167,6 +167,33 @@ lemma jacobiMatrix_apply (i j : P.rels) :
 
 end Matrix
 
+section Constructions
+
+/-- If `algebraMap R S` is bijective, the empty generators are a pre-submersive
+presentation with no relations. -/
+noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)) :
+    PreSubmersivePresentation.{t, w} R S where
+  toPresentation := Presentation.ofBijectiveAlgebraMap.{t, w} h
+  map := PEmpty.elim
+  map_inj (a b : PEmpty) h := by contradiction
+  relations_finite := inferInstanceAs (Finite PEmpty.{t + 1})
+
+instance (h : Function.Bijective (algebraMap R S)) : Fintype (ofBijectiveAlgebraMap h).vars :=
+  inferInstanceAs (Fintype PEmpty)
+
+instance (h : Function.Bijective (algebraMap R S)) : Fintype (ofBijectiveAlgebraMap h).rels :=
+  inferInstanceAs (Fintype PEmpty)
+
+lemma ofBijectiveAlgebraMap_jacobian (h : Function.Bijective (algebraMap R S)) :
+    (ofBijectiveAlgebraMap h).jacobian = 1 := by
+  have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
+      (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
+    ext (i j : PEmpty)
+    contradiction
+  rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
+
+end Constructions
+
 end PreSubmersivePresentation
 
 /--
@@ -180,6 +207,31 @@ structure SubmersivePresentation extends PreSubmersivePresentation.{t, w} R S wh
 
 attribute [instance] SubmersivePresentation.isFinite
 
+namespace SubmersivePresentation
+
+open PreSubmersivePresentation
+
+section Constructions
+
+variable {R S} in
+/-- If `algebraMap R S` is bijective, the empty generators are a submersive
+presentation with no relations. -/
+noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)) :
+    SubmersivePresentation.{t, w} R S where
+  __ := PreSubmersivePresentation.ofBijectiveAlgebraMap.{t, w} h
+  jacobian_isUnit := by
+    rw [ofBijectiveAlgebraMap_jacobian]
+    exact isUnit_one
+  isFinite := Presentation.ofBijectiveAlgebraMap_isFinite h
+
+/-- The canonical submersive `R`-presentation of `R` with no generators and no relations. -/
+noncomputable def id : SubmersivePresentation.{t, w} R R :=
+  ofBijectiveAlgebraMap Function.bijective_id
+
+end Constructions
+
+end SubmersivePresentation
+
 /--
 An `R`-algebra `S` is called standard smooth, if there
 exists a submersive presentation.
@@ -211,6 +263,16 @@ lemma IsStandardSmoothOfRelativeDimension.isStandardSmooth
     IsStandardSmooth.{t, w} R S :=
   ⟨‹IsStandardSmoothOfRelativeDimension n R S›.out.nonempty⟩
 
+lemma IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective
+    (h : Function.Bijective (algebraMap R S)) :
+    IsStandardSmoothOfRelativeDimension.{t, w} 0 R S :=
+  ⟨SubmersivePresentation.ofBijectiveAlgebraMap h, Presentation.ofBijectiveAlgebraMap_dimension h⟩
+
+variable (R) in
+instance IsStandardSmoothOfRelativeDimension.id :
+    IsStandardSmoothOfRelativeDimension.{t, w} 0 R R :=
+  IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective Function.bijective_id
+
 end Algebra
 
 namespace RingHom