feat(RingTheory/Smooth/StandardSmooth): transport IsStandardSmooth along algebra isomorphisms (#32925)

Author: chrisflav

Mathlib/RingTheory/Extension/Generators.lean

@@ -169,6 +169,20 @@ def toExtension : Extension R S where
   σ := P.σ
   algebraMap_σ := by simp
 
+/-- Transport generators along an algebra isomorphism. -/
+def ofAlgEquiv (P : Generators R S ι) {T : Type*} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
+    Generators R T ι where
+  val := e ∘ P.val
+  σ' := P.σ ∘ e.symm
+  aeval_val_σ' t := by
+    rw [Function.comp_def, ← AlgHom.coe_coe e, ← MvPolynomial.comp_aeval_apply]
+    simp
+
+@[simp]
+lemma ofAlgEquiv_val (P : Generators R S ι) {T : Type*} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
+    (P.ofAlgEquiv e).val = e ∘ P.val :=
+  rfl
+
 section Localization
 
 variable (r : R) [IsLocalization.Away r S]
@@ -567,6 +581,14 @@ lemma ker_ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.
   congr
   exact MvPolynomial.ringHom_ext (by simp) (by simp [ofAlgHom])
 
+@[simp]
+lemma ker_ofAlgEquiv (P : Generators R S ι) {T : Type*} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
+    (P.ofAlgEquiv e).ker = P.ker := by
+  rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,
+    ← MvPolynomial.comp_aeval, ← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom,
+    AlgHomClass.toRingHom_toAlgHom, AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot,
+    ← ker_eq_ker_aeval_val]
+
 lemma map_toComp_ker (Q : Generators S T ι') (P : Generators R S ι) :
     P.ker.map (Q.toComp P).toAlgHom = RingHom.ker (Q.ofComp P).toAlgHom := by
   letI : DecidableEq (ι' →₀ ℕ) := Classical.decEq _

Mathlib/RingTheory/Extension/Presentation/Basic.lean

@@ -160,6 +160,20 @@ def ofFinitePresentation [FinitePresentation R S] :
 
 section Construction
 
+/-- Transport a presentation along an algebra isomorphism. -/
+@[simps toGenerators relation]
+def ofAlgEquiv (P : Presentation R S ι σ) {T : Type*} [CommRing T] [Algebra R T]
+    (e : S ≃ₐ[R] T) :
+    Presentation R T ι σ where
+  __ := Generators.ofAlgEquiv P.toGenerators e
+  relation i := P.relation i
+  span_range_relation_eq_ker := by simp [P.span_range_relation_eq_ker]
+
+@[simp]
+lemma dimension_ofAlgEquiv (P : Presentation R S ι σ) {T : Type*} [CommRing T] [Algebra R T]
+    (e : S ≃ₐ[R] T) : (P.ofAlgEquiv e).dimension = P.dimension :=
+  rfl
+
 /-- 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 R S PEmpty.{w + 1} PEmpty.{t + 1} where

Mathlib/RingTheory/Extension/Presentation/Submersive.lean

@@ -177,6 +177,33 @@ end
 
 section Constructions
 
+/-- Transport a pre-submersive presentation along an algebra isomorphism. -/
+@[simps toPresentation map]
+def ofAlgEquiv (P : PreSubmersivePresentation R S ι σ) {T : Type*} [CommRing T] [Algebra R T]
+    (e : S ≃ₐ[R] T) :
+    PreSubmersivePresentation R T ι σ where
+  __ := P.toPresentation.ofAlgEquiv e
+  map := P.map
+  map_inj := P.map_inj
+
+@[simp]
+lemma jacobiMatrix_ofAlgEquiv (P : PreSubmersivePresentation R S ι σ) {T : Type*} [CommRing T]
+    [Algebra R T] (e : S ≃ₐ[R] T) [Fintype σ] [DecidableEq σ] :
+    (P.ofAlgEquiv e).jacobiMatrix = P.jacobiMatrix :=
+  rfl
+
+@[simp]
+lemma jacobian_ofAlgEquiv (P : PreSubmersivePresentation R S ι σ) {T : Type*} [CommRing T]
+    [Algebra R T] (e : S ≃ₐ[R] T) [Finite σ] :
+    (P.ofAlgEquiv e).jacobian = e P.jacobian := by
+  classical
+  cases nonempty_fintype σ
+  rw [jacobian_eq_jacobiMatrix_det, jacobian_eq_jacobiMatrix_det]
+  simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
+    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
+    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_apply]
+  simp [Function.comp_def]
+
 /-- 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)) :
@@ -479,6 +506,15 @@ open PreSubmersivePresentation
 
 section Constructions
 
+variable {R S ι σ} in
+/-- Transport a submersive presentation along an algebra isomorphism. -/
+@[simps toPreSubmersivePresentation]
+def ofAlgEquiv (P : SubmersivePresentation R S ι σ) {T : Type*} [CommRing T] [Algebra R T]
+    (e : S ≃ₐ[R] T) :
+    SubmersivePresentation R T ι σ where
+  __ := P.toPreSubmersivePresentation.ofAlgEquiv e
+  jacobian_isUnit := by simp [P.jacobian_isUnit]
+
 variable {R S} in
 /-- If `algebraMap R S` is bijective, the empty generators are a submersive
 presentation with no relations. -/

Mathlib/RingTheory/Smooth/StandardSmooth.lean

@@ -64,6 +64,7 @@ class IsStandardSmooth : Prop where
 
 variable [Finite σ]
 
+variable {R S ι σ} in
 lemma SubmersivePresentation.isStandardSmooth [Finite ι] (P : SubmersivePresentation R S ι σ) :
     IsStandardSmooth R S := by
   exact ⟨_, _, _, inferInstance, ⟨P.reindex (Fintype.equivFin _).symm (Fintype.equivFin _).symm⟩⟩
@@ -88,6 +89,7 @@ class IsStandardSmoothOfRelativeDimension : Prop where
   out : ∃ (ι σ : Type) (_ : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R S ι σ),
     P.dimension = n
 
+variable {R S ι σ n} in
 lemma SubmersivePresentation.isStandardSmoothOfRelativeDimension [Finite ι]
     (P : SubmersivePresentation R S ι σ) (hP : P.dimension = n) :
     IsStandardSmoothOfRelativeDimension n R S := by
@@ -118,6 +120,17 @@ instance (priority := 100) IsStandardSmooth.finitePresentation [IsStandardSmooth
   obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
   exact P.finitePresentation_of_isFinite
 
+lemma IsStandardSmooth.of_algEquiv {T : Type*} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T)
+    [IsStandardSmooth R S] : IsStandardSmooth R T := by
+  obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
+  exact (P.ofAlgEquiv e).isStandardSmooth
+
+lemma IsStandardSmoothOfRelativeDimension.of_algEquiv {T : Type*} [CommRing T] [Algebra R T]
+    (e : S ≃ₐ[R] T) [IsStandardSmoothOfRelativeDimension n R S] :
+    IsStandardSmoothOfRelativeDimension n R T := by
+  obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
+  exact (P.ofAlgEquiv e).isStandardSmoothOfRelativeDimension (by simpa)
+
 section Composition
 
 variable (R S T) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]