feat(RingTheory/): MvPolynomial is standard smooth

Mathlib/RingTheory/Extension/Presentation/Basic.lean

@@ -198,6 +198,20 @@ noncomputable def id : Presentation R R PEmpty.{w + 1} PEmpty.{t + 1} :=
 lemma id_dimension : (Presentation.id R).dimension = 0 :=
   ofBijectiveAlgebraMap_dimension (R := R) Function.bijective_id
 
+variable (R ι) in
+/-- The canonical `R`-presentation of the polynomial algebra `MvPolynomial ι R`,
+with generators `X` indexed by `ι` and no relations. -/
+@[simps -fullyApplied relation]
+noncomputable def mvPolynomial : Presentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where
+  relation := PEmpty.elim
+  span_range_relation_eq_ker := by
+    simpa only [Generators.ker_mvPolynomial, Set.range_eq_empty] using Ideal.span_empty
+  __ := Generators.mvPolynomial R ι
+
+@[simp]
+lemma dimension_mvPolynomial : (mvPolynomial R ι).dimension = Nat.card ι := by
+  simp [dimension]
+
 section Localization
 
 variable (r : R) [IsLocalization.Away r S]

Mathlib/RingTheory/Extension/Presentation/Submersive.lean

@@ -222,6 +222,20 @@ lemma ofBijectiveAlgebraMap_jacobian (h : Function.Bijective (algebraMap R S)) :
     contradiction
   rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
 
+variable (R ι) in
+/-- The canonical pre-submersive `R`-presentation of the polynomial algebra `MvPolynomial ι R`,
+with generators `X` indexed by `ι` and no relations. -/
+@[simps -fullyApplied map]
+noncomputable def mvPolynomial :
+    PreSubmersivePresentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where
+  map := PEmpty.elim
+  map_inj := PEmpty.elim.injective_of_subsingleton
+  __ := Presentation.mvPolynomial R ι
+
+@[simp]
+lemma jacobian_mvPolynomial : (mvPolynomial R ι).jacobian = 1 := by
+  rw [jacobian_eq_jacobiMatrix_det, Matrix.det_isEmpty, map_one]
+
 section Localization
 
 variable (r : R) [IsLocalization.Away r S]
@@ -528,6 +542,11 @@ noncomputable def ofBijectiveAlgebraMap (h : Function.Bijective (algebraMap R S)
 noncomputable def id : SubmersivePresentation R R PEmpty.{w + 1} PEmpty.{t + 1} :=
   ofBijectiveAlgebraMap Function.bijective_id
 
+/-- The canonical submersive `R`-presentation of the polynomial algebra `MvPolynomial ι R`. -/
+noncomputable def mvPolynomial : SubmersivePresentation R (MvPolynomial ι R) ι PEmpty.{t + 1} where
+  __ := PreSubmersivePresentation.mvPolynomial R ι
+  jacobian_isUnit := by simp
+
 section Composition
 variable {R S ι σ}
 variable {T ι' σ' : Type*} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]

Mathlib/RingTheory/Smooth/StandardSmooth.lean

@@ -115,6 +115,20 @@ instance IsStandardSmoothOfRelativeDimension.id :
     IsStandardSmoothOfRelativeDimension 0 R R :=
   IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective Function.bijective_id
 
+variable (R) in
+/-- The polynomial algebra `MvPolynomial ι R` is standard smooth over `R` of relative
+dimension `Nat.card ι`. -/
+lemma IsStandardSmoothOfRelativeDimension.mvPolynomial [Finite ι] :
+    IsStandardSmoothOfRelativeDimension (Nat.card ι) R (MvPolynomial ι R) :=
+  (SubmersivePresentation.mvPolynomial.{0} R ι).isStandardSmoothOfRelativeDimension
+    (Presentation.dimension_mvPolynomial)
+
+/-- The polynomial algebra `MvPolynomial (Fin n) R` is standard smooth over `R` of relative
+dimension `n`. -/
+instance IsStandardSmoothOfRelativeDimension.mvPolynomial_fin {n : ℕ} :
+    IsStandardSmoothOfRelativeDimension n R (MvPolynomial (Fin n) R) := by
+  simpa using IsStandardSmoothOfRelativeDimension.mvPolynomial R (Fin n)
+
 instance (priority := 100) IsStandardSmooth.finitePresentation [IsStandardSmooth R S] :
     FinitePresentation R S := by
   obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›