feat(RingTheory/Smooth/Basic): add Generators.mvPolynomial (leanprover-community#39708)

Define trivial `Generators` for `MvPolynomial` and use it to golf `FormallySmooth.mvPolynomial` (where they were previously defined inline). This also removes a `set_option backward.isDefEq.respectTransparency false`.

- [x] depends on: leanprover-community#39706

Author: justus-springer

Mathlib/RingTheory/Extension/Generators.lean

@@ -35,6 +35,9 @@ public import Mathlib.RingTheory.Extension.Basic
 - `Algebra.Generators.Cotangent`: The cotangent space w.r.t. `P = R[X] → S`, i.e. the
   space `I/I²` with `I` being the kernel of the presentation.
 
+- `Algebra.Generators.mvPolynomial`: The canonical `R`-generators of the polynomial algebra
+  `MvPolynomial ι R`, indexed by `ι` via the variables `X`.
+
 ## TODOs
 
 Currently, Lean does not see through the `ι` field of terms of `Generators R S` obtained
@@ -139,6 +142,15 @@ noncomputable def id : Generators R R PEmpty.{w + 1} := ofSurjectiveAlgebraMap <
   rw [algebraMap_self]
   exact RingHomSurjective.is_surjective
 
+variable (R ι) in
+/-- The canonical `R`-generators of the polynomial algebra `MvPolynomial ι R`,
+indexed by `ι` via the variables `X`. -/
+@[simps σ, simps -fullyApplied val]
+noncomputable def mvPolynomial : Generators R (MvPolynomial ι R) ι where
+  val := X
+  σ' f := f
+  aeval_val_σ' := aeval_X_left_apply
+
 /-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective. -/
 noncomputable
 def ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective f) :
@@ -606,6 +618,9 @@ lemma ker_eq_ker_aeval_val : P.ker = RingHom.ker (aeval P.val) := by
   simp only [ker, Extension.ker, toExtension_Ring, algebraMap_eq]
   rfl
 
+lemma ker_mvPolynomial : (mvPolynomial R ι).ker = ⊥ := by
+  simp [ker_eq_ker_aeval_val, SetLike.ext_iff, aeval_X_left]
+
 variable {P} in
 lemma aeval_val_eq_zero {x} (hx : x ∈ P.ker) : aeval P.val x = 0 := by rwa [← algebraMap_apply]
 

Mathlib/RingTheory/Smooth/Basic.lean

@@ -107,13 +107,10 @@ lemma FormallySmooth.comp_surjective [FormallySmooth R A] (I : Ideal B) (hI : I
     simpa using (Function.surjInv_eq _ _).symm
   exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩
 
-set_option backward.isDefEq.respectTransparency false in
 instance instFormallySmoothMvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by
-  let P : Generators R (MvPolynomial σ R) σ :=
-    .ofSurjective X (by simp [aeval_X_left, Function.Surjective])
+  let P := Generators.mvPolynomial R σ
   have : Subsingleton ↥P.toExtension.ker :=
-    Submodule.subsingleton_iff_eq_bot.mpr <| by
-      simp [SetLike.ext_iff, P, Generators.ofSurjective, aeval_X_left]
+    Submodule.subsingleton_iff_eq_bot.mpr Generators.ker_mvPolynomial
   have : Subsingleton P.toExtension.Cotangent := Cotangent.mk_surjective.subsingleton
   have := P.toExtension.h1Cotangentι_injective.subsingleton
   exact ⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩