refactor(Algebra/MvPolynomial): generalize pUnitAlgEquiv to Unique (leanprover-community#37801)

## Summary

Generalizes `MvPolynomial.pUnitAlgEquiv` from `PUnit` to any uniquely inhabited index type as `MvPolynomial.uniqueAlgEquiv`.

The old `pUnitAlgEquiv` API is kept as deprecated compatibility aliases, and downstream uses are migrated where appropriate.

This PR adds proofs autoformalised by @Aristotle-Harmonic.

## Motivation

The equivalence `MvPolynomial σ R ≃ₐ[R] R[X]` only needs `[Unique σ]`, not the specific index type `PUnit`.

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <efw@google.com>

Author: 3 people

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -1,15 +1,15 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
+Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro, Elias Judin
 -/
 module
 
 public import Mathlib.Algebra.BigOperators.Finsupp.Fin
+public import Mathlib.Algebra.MonoidAlgebra.Basic
 public import Mathlib.Algebra.MvPolynomial.Degrees
 public import Mathlib.Algebra.MvPolynomial.Rename
 public import Mathlib.Algebra.Polynomial.AlgebraMap
-public import Mathlib.Algebra.MonoidAlgebra.Basic
 public import Mathlib.Algebra.Polynomial.Degree.Lemmas
 public import Mathlib.Data.Finsupp.Option
 public import Mathlib.Logic.Equiv.Fin.Basic
@@ -62,24 +62,24 @@ section Equiv
 
 variable (R) [CommSemiring R]
 
-/-- The ring isomorphism between multivariable polynomials in a single variable and
-polynomials over the ground ring.
--/
+/-- The algebra isomorphism between multivariable polynomials indexed by a type with a unique
+element and polynomials over the ground ring. -/
 @[simps]
-def pUnitAlgEquiv : MvPolynomial PUnit R ≃ₐ[R] R[X] where
+def uniqueAlgEquiv (σ : Type*) [Unique σ] : MvPolynomial σ R ≃ₐ[R] R[X] where
   toFun := eval₂ Polynomial.C fun _ => Polynomial.X
-  invFun := Polynomial.eval₂ MvPolynomial.C (X PUnit.unit)
+  invFun := Polynomial.eval₂ MvPolynomial.C (X default)
   left_inv := by
-    let f : R[X] →+* MvPolynomial PUnit R := Polynomial.eval₂RingHom MvPolynomial.C (X PUnit.unit)
-    let g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X
+    let f : R[X] →+* MvPolynomial σ R := Polynomial.eval₂RingHom MvPolynomial.C (X default)
+    let g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X
     change ∀ p, f.comp g p = p
     apply is_id
     · ext a
       dsimp [f, g]
       rw [eval₂_C, Polynomial.eval₂_C]
-    · rintro ⟨⟩
+    · intro i
       dsimp [f, g]
       rw [eval₂_X, Polynomial.eval₂_X]
+      rw [← Unique.eq_default i]
   right_inv p :=
     Polynomial.induction_on p (fun a => by rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C])
     (fun p q hp hq => by rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]) fun p n _ => by
@@ -89,15 +89,34 @@ def pUnitAlgEquiv : MvPolynomial PUnit R ≃ₐ[R] R[X] where
   map_add' _ _ := eval₂_add _ _
   commutes' _ := eval₂_C _ _ _
 
+theorem uniqueAlgEquiv_monomial [Unique σ] {d : σ →₀ ℕ} {r : R} :
+    (MvPolynomial.uniqueAlgEquiv R σ) (MvPolynomial.monomial d r)
+      = Polynomial.monomial (d default) r := by
+  simp [Polynomial.C_mul_X_pow_eq_monomial]
+
+theorem uniqueAlgEquiv_symm_monomial [Unique σ] {d : σ →₀ ℕ} {r : R} :
+    (MvPolynomial.uniqueAlgEquiv R σ).symm (Polynomial.monomial (d default) r)
+      = MvPolynomial.monomial d r := by
+  simp [MvPolynomial.monomial_eq]
+
+/-- The algebra isomorphism between multivariable polynomials in a single variable and
+polynomials over the ground ring. -/
+@[deprecated uniqueAlgEquiv (since := "2026-04-15")]
+abbrev pUnitAlgEquiv := uniqueAlgEquiv (R := R) PUnit
+
+set_option linter.deprecated false in
+@[deprecated uniqueAlgEquiv_monomial (since := "2026-04-15")]
 theorem pUnitAlgEquiv_monomial {d : PUnit →₀ ℕ} {r : R} :
     MvPolynomial.pUnitAlgEquiv R (MvPolynomial.monomial d r)
-      = Polynomial.monomial (d ()) r := by
-  simp [Polynomial.C_mul_X_pow_eq_monomial]
+      = Polynomial.monomial (d ()) r :=
+  uniqueAlgEquiv_monomial _
 
+set_option linter.deprecated false in
+@[deprecated uniqueAlgEquiv_symm_monomial (since := "2026-04-15")]
 theorem pUnitAlgEquiv_symm_monomial {d : PUnit →₀ ℕ} {r : R} :
     (MvPolynomial.pUnitAlgEquiv R).symm (Polynomial.monomial (d ()) r)
-      = MvPolynomial.monomial d r := by
-  simp [MvPolynomial.monomial_eq]
+      = MvPolynomial.monomial d r :=
+  uniqueAlgEquiv_symm_monomial _
 
 section Map
 
@@ -109,7 +128,8 @@ def mapEquiv [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :
   AddMonoidAlgebra.mapRingEquiv _ e
 
 @[simp]
-lemma mapEquiv_apply [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) (x : MvPolynomial σ S₁) :
+lemma mapEquiv_apply [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂)
+    (x : MvPolynomial σ S₁) :
     mapEquiv σ e x = map e x := rfl
 
 @[simp]
@@ -134,7 +154,8 @@ def mapAlgEquiv (e : A₁ ≃ₐ[R] A₂) : MvPolynomial σ A₁ ≃ₐ[R] MvPol
   AddMonoidAlgebra.mapAlgEquiv _ _ e
 
 @[simp]
-lemma mapAlgEquiv_apply (e : A₁ ≃ₐ[R] A₂) (x : MvPolynomial σ A₁) : mapAlgEquiv σ e x = map e x :=
+lemma mapAlgEquiv_apply (e : A₁ ≃ₐ[R] A₂) (x : MvPolynomial σ A₁) :
+    mapAlgEquiv σ e x = map e x :=
   rfl
 
 @[simp]
@@ -156,29 +177,65 @@ section Eval
 
 variable {R S : Type*} [CommSemiring R] [CommSemiring S]
 
+theorem eval₂_uniqueAlgEquiv [Unique σ] {f : MvPolynomial σ R} {φ : R →+* S}
+    {a : σ → S} :
+    ((MvPolynomial.uniqueAlgEquiv R σ) f : Polynomial R).eval₂ φ (a default) =
+      f.eval₂ φ a := by
+  simp only [MvPolynomial.uniqueAlgEquiv_apply]
+  induction f using MvPolynomial.induction_on' with
+  | monomial d r =>
+    rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
+    simp only [Polynomial.eval₂_monomial, eval₂_monomial]
+    rw [Finsupp.unique_single d, Finsupp.prod_single_index]
+    · simp
+    · simp only [pow_zero]
+  | add f g hf hg => simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]
+
+theorem eval₂_uniqueAlgEquiv_symm [Unique σ] {f : Polynomial R} {φ : R →+* S}
+    {a : σ → S} :
+    ((MvPolynomial.uniqueAlgEquiv R σ).symm f : MvPolynomial σ R).eval₂ φ a =
+      f.eval₂ φ (a default) := by
+  rw [(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
+    (φ := φ) (a := a)).symm]
+  rw [AlgEquiv.apply_symm_apply]
+
+theorem eval₂_const_uniqueAlgEquiv_symm [Unique σ] {f : Polynomial R}
+    {φ : R →+* S} {a : S} :
+    ((MvPolynomial.uniqueAlgEquiv R σ).symm f : MvPolynomial σ R).eval₂ φ (fun _ ↦ a) =
+      f.eval₂ φ a := by
+  rw [eval₂_uniqueAlgEquiv_symm]
+
+theorem eval₂_const_uniqueAlgEquiv [Unique σ] {f : MvPolynomial σ R}
+    {φ : R →+* S} {a : S} :
+    ((MvPolynomial.uniqueAlgEquiv R σ) f : Polynomial R).eval₂ φ a =
+      f.eval₂ φ (fun _ ↦ a) := by
+  rw [← eval₂_uniqueAlgEquiv]
+
+set_option linter.deprecated false in
+@[deprecated eval₂_uniqueAlgEquiv_symm (since := "2026-04-15")]
 theorem eval₂_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : Unit → S} :
     ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ a =
-      f.eval₂ φ (a ()) := by
-  simp only [MvPolynomial.pUnitAlgEquiv_symm_apply]
-  induction f using Polynomial.induction_on' with
-  | add f g hf hg => simp [hf, hg]
-  | monomial n r => simp
+      f.eval₂ φ (a ()) :=
+  eval₂_uniqueAlgEquiv_symm
 
+set_option linter.deprecated false in
+@[deprecated eval₂_const_uniqueAlgEquiv_symm (since := "2026-04-15")]
 theorem eval₂_const_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : S} :
     ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ (fun _ ↦ a) =
-      f.eval₂ φ a := by
-  rw [eval₂_pUnitAlgEquiv_symm]
+      f.eval₂ φ a :=
+  eval₂_const_uniqueAlgEquiv_symm
 
+set_option linter.deprecated false in
+@[deprecated eval₂_uniqueAlgEquiv (since := "2026-04-15")]
 theorem eval₂_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : PUnit → S} :
-    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ (a default) = f.eval₂ φ a := by
-  simp only [MvPolynomial.pUnitAlgEquiv_apply]
-  induction f using MvPolynomial.induction_on' with
-  | monomial d r => simp
-  | add f g hf hg => simp [hf, hg]
+    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ (a default) = f.eval₂ φ a :=
+  eval₂_uniqueAlgEquiv
 
+set_option linter.deprecated false in
+@[deprecated eval₂_const_uniqueAlgEquiv (since := "2026-04-15")]
 theorem eval₂_const_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : S} :
-    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ a = f.eval₂ φ (fun _ ↦ a) := by
-  rw [← eval₂_pUnitAlgEquiv]
+    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ a = f.eval₂ φ (fun _ ↦ a) :=
+  eval₂_const_uniqueAlgEquiv
 
 end Eval
 
@@ -788,7 +845,7 @@ lemma Polynomial.toMvPolynomial_X (i : σ) : X.toMvPolynomial i = MvPolynomial.X
 
 lemma Polynomial.toMvPolynomial_eq_rename_comp (i : σ) :
     toMvPolynomial (R := R) i =
-      (MvPolynomial.rename (fun _ : Unit ↦ i)).comp (MvPolynomial.pUnitAlgEquiv R).symm := by
+      (MvPolynomial.rename (fun _ : Unit ↦ i)).comp (MvPolynomial.uniqueAlgEquiv R Unit).symm := by
   ext
   simp
 

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -424,7 +424,7 @@ lemma isIntegralHom_over_iff_isEmpty : IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEm
     obtain ⟨p : Polynomial R, hp, hp'⟩ :=
       (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
         (arrowIsoΓSpecOfIsAffine _)).mpr h.2 (X i)
-    have : (rename fun _ ↦ i).comp (pUnitAlgEquiv.{_, v} _).symm.toAlgHom p = 0 := by
+    have : (rename fun _ ↦ i).comp (uniqueAlgEquiv.{_, v} _ PUnit).symm.toAlgHom p = 0 := by
       simp [← hp', ← algebraMap_eq]
     rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this
     simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe, EmbeddingLike.map_eq_zero_iff] at this

Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

@@ -184,7 +184,7 @@ theorem IsTranscendenceBasis.polynomial [Nonempty ι] [Subsingleton ι] :
   nontriviality R
   have := (nonempty_unique ι).some
   refine (isTranscendenceBasis_equiv (Equiv.equivPUnit.{_, 1} _).symm).mp <|
-    (MvPolynomial.pUnitAlgEquiv R).symm.isTranscendenceBasis_iff.mp ?_
+    (MvPolynomial.uniqueAlgEquiv R PUnit).symm.isTranscendenceBasis_iff.mp ?_
   convert IsTranscendenceBasis.mvPolynomial PUnit R
   ext; simp
 

Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean

@@ -41,7 +41,7 @@ its element is transcendental. -/
 theorem algebraicIndependent_unique_type_iff [Unique ι] :
     AlgebraicIndependent R x ↔ Transcendental R (x default) := by
   rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]
-  let i := (renameEquiv R (Equiv.equivPUnit.{_, 1} ι)).trans (pUnitAlgEquiv R)
+  let i := uniqueAlgEquiv R ι
   have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
     ext y
     simp [i, Subsingleton.elim y default]

Mathlib/RingTheory/FinitePresentation.lean

@@ -200,7 +200,7 @@ instance self : FinitePresentation R R :=
 /-- `R[X]` is finitely presented as `R`-algebra. -/
 instance polynomial [FinitePresentation R A] : FinitePresentation R A[X] :=
   letI := FinitePresentation.mvPolynomial R A Unit
-  have := equiv (MvPolynomial.pUnitAlgEquiv.{_, 0} A)
+  have := equiv (MvPolynomial.uniqueAlgEquiv.{_, 0} A PUnit)
   .trans _ A _
 
 open MvPolynomial

Mathlib/RingTheory/FreeCommRing.lean

@@ -410,7 +410,7 @@ noncomputable alias freeCommRingPemptyEquivInt := freeCommRingPEmptyEquivInt
 
 /-- The free commutative ring on a type with one term is isomorphic to `ℤ[X]`. -/
 def freeCommRingPUnitEquivPolynomialInt : FreeCommRing PUnit.{u + 1} ≃+* ℤ[X] :=
-  (freeCommRingEquivMvPolynomialInt _).trans (MvPolynomial.pUnitAlgEquiv ℤ).toRingEquiv
+  (freeCommRingEquivMvPolynomialInt _).trans (MvPolynomial.uniqueAlgEquiv ℤ PUnit).toRingEquiv
 
 @[deprecated (since := "2026-02-08")]
 noncomputable alias freeCommRingPunitEquivPolynomialInt := freeCommRingPUnitEquivPolynomialInt

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -858,21 +858,22 @@ section CommSemiring
 variable {R : Type*} [CommSemiring R] (φ ψ : R[X])
 
 theorem _root_.MvPolynomial.toMvPowerSeries_pUnitAlgEquiv {f : MvPolynomial PUnit R} :
-    (f.toMvPowerSeries : PowerSeries R) = (f.pUnitAlgEquiv R).toPowerSeries := by
+    (f.toMvPowerSeries : PowerSeries R) =
+      (MvPolynomial.uniqueAlgEquiv R PUnit f).toPowerSeries := by
   induction f using MvPolynomial.induction_on' with
   | monomial d r =>
     --Note: this `have` should be a generic `simp` lemma for a `Unique` type with `()` replaced
     --by any element.
     have : single () (d ()) = d := by ext; simp
-    simp only [MvPolynomial.coe_monomial, MvPolynomial.pUnitAlgEquiv_monomial,
+    simp only [MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial,
       Polynomial.coe_monomial, PowerSeries.monomial, this]
   | add f g hf hg => simp [hf, hg]
 
 theorem pUnitAlgEquiv_symm_toPowerSeries {f : Polynomial R} :
     ((f.toPowerSeries) : MvPowerSeries PUnit R)
-      = ((MvPolynomial.pUnitAlgEquiv R).symm f).toMvPowerSeries := by
-  set g := (MvPolynomial.pUnitAlgEquiv R).symm f
-  have : f = MvPolynomial.pUnitAlgEquiv R g := by simp only [g, AlgEquiv.apply_symm_apply]
+      = ((MvPolynomial.uniqueAlgEquiv R PUnit).symm f).toMvPowerSeries := by
+  set g := (MvPolynomial.uniqueAlgEquiv R PUnit).symm f
+  have : f = MvPolynomial.uniqueAlgEquiv R PUnit g := by simp only [g, AlgEquiv.apply_symm_apply]
   rw [this, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv]
 
 variable (A : Type*) [Semiring A] [Algebra R A]

Mathlib/RingTheory/PowerSeries/Evaluation.lean

@@ -134,10 +134,8 @@ noncomputable def eval₂ : PowerSeries R → S :=
 
 @[simp]
 theorem eval₂_coe (f : Polynomial R) : eval₂ φ a f = f.eval₂ φ a := by
-  let g : MvPolynomial Unit R := (MvPolynomial.pUnitAlgEquiv R).symm f
-  have : f = MvPolynomial.pUnitAlgEquiv R g := by
-    simp only [g, ← AlgEquiv.symm_apply_eq]
-  simp only [this, PowerSeries.eval₂, MvPolynomial.eval₂_const_pUnitAlgEquiv]
+  rw [← (MvPolynomial.uniqueAlgEquiv R Unit).apply_symm_apply f]
+  simp only [PowerSeries.eval₂, MvPolynomial.eval₂_const_uniqueAlgEquiv]
   rw [← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPowerSeries.eval₂_coe]
 
 @[simp]
@@ -194,21 +192,17 @@ theorem eval₂_unique (hφ : Continuous φ) (ha : HasEval a)
     {ε : PowerSeries R → S} (hε : Continuous ε)
     (h : ∀ p : Polynomial R, ε p = Polynomial.eval₂ φ a p) :
     ε = eval₂ φ a := by
-  apply MvPowerSeries.eval₂_unique hφ (hasEval ha) hε
-  intro p
-  rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_pUnitAlgEquiv]
+  refine MvPowerSeries.eval₂_unique hφ (hasEval ha) hε (fun p ↦ ?_)
+  rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_uniqueAlgEquiv]
 
 theorem comp_eval₂ (hφ : Continuous φ) (ha : HasEval a)
     {T : Type*} [UniformSpace T] [CompleteSpace T] [T2Space T]
     [CommRing T] [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T]
     {ε : S →+* T} (hε : Continuous ε) :
     ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (ε a) := by
-  apply eval₂_unique _ (ha.map hε)
-  · exact Continuous.comp hε (continuous_eval₂ hφ ha)
-  · intro p
-    simp only [Function.comp_apply, eval₂_coe]
-    exact Polynomial.hom_eval₂ p φ ε a
-  · simp only [RingHom.coe_comp, Continuous.comp hε hφ]
+  refine eval₂_unique (by simp only [RingHom.coe_comp, hε.comp hφ]) (ha.map hε)
+    (hε.comp (continuous_eval₂ hφ ha)) (fun p ↦ ?_)
+  simpa [Function.comp_apply, eval₂_coe] using p.hom_eval₂ φ ε a
 
 variable [Algebra R S] [ContinuousSMul R S]
 

Mathlib/RingTheory/Smooth/Basic.lean

@@ -394,7 +394,7 @@ section Polynomial
 
 open scoped Polynomial in
 instance polynomial (R : Type*) [CommRing R] :
-  FormallySmooth R R[X] := .of_equiv (MvPolynomial.pUnitAlgEquiv.{_, 0} R)
+  FormallySmooth R R[X] := .of_equiv (MvPolynomial.uniqueAlgEquiv.{_, 0} R PUnit)
 
 instance : FormallySmooth R R := .of_equiv (MvPolynomial.isEmptyAlgEquiv R Empty)