refactor(multivariate): place renameEquiv and finSuccEquiv under CMvPolynomial namespace (#206)

* fix: dot notation in defs and duplicate defs removed

* fix: added a comma

Author: DimitriosMitsios

CompPoly/Multivariate/FinSuccEquiv.lean

@@ -1,51 +1,58 @@
 /-
 Copyright (c) 2025 CompPoly. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Elias Judin, Aristotle (Harmonic)
+Authors: Elias Judin, Aristotle (Harmonic), Dimitris Mitsios
 -/
 import CompPoly.Multivariate.MvPolyEquiv
 import Mathlib.Algebra.MvPolynomial.Equiv
 import Mathlib.RingTheory.Polynomial.Basic
 
 /-!
-# `finSuccEquiv` and `optionEquivLeft` for `CMvPolynomial`
+# `finSuccEquiv` for `CMvPolynomial`
 
-This file defines computable multivariate polynomial equivalences for splitting off one variable,
-mirroring `MvPolynomial.finSuccEquiv` and `MvPolynomial.optionEquivLeft` from Mathlib.
+This file defines the computable multivariate polynomial equivalence for
+splitting off one variable, mirroring `MvPolynomial.finSuccEquiv` from Mathlib.
+
+In Mathlib, `MvPolynomial` accepts a general type `σ` for the index set of the
+variables. Then, `optionEquivLeft` provides the algebra isomorphism
+`MvPolynomial (Option σ) R ≃ₐ[R] Polynomial (MvPolynomial σ R)`. Finally,
+`finSuccEquiv` is defined as the composition of the rename step
+(`Fin (n+1) ≃ Option (Fin n)`) with `optionEquivLeft`. There is no such
+distinction in `CMvPolynomial` because the variables are of type `Fin n` by
+definition. Therefore, only `CMvPolynomial.finSuccEquiv` applies.
 
 ## Main definitions
 
 * `CMvPolynomial.finSuccEquiv` — ring equivalence
     `CMvPolynomial (n+1) R ≃+* Polynomial (CMvPolynomial n R)`,
     viewing a polynomial in `n+1` variables as a univariate polynomial over `n` variables.
-* `CMvPolynomial.optionEquivLeft` — ring equivalence
-    `CMvPolynomial (n+1) R ≃+* Polynomial (CMvPolynomial n R)`,
-    defined as the composition of the variable renaming `Fin (n+1) ≃ Option (Fin n)` with
-    the Mathlib `MvPolynomial.optionEquivLeft` equivalence.  This mirrors the way
-    `MvPolynomial.finSuccEquiv` is built from `MvPolynomial.optionEquivLeft`.
 
 ## Implementation notes
 
-Both equivalences are `noncomputable` because they go through the `polyRingEquiv`
+The equivalence is `noncomputable` because it goes through the `polyRingEquiv`
 bridge between `CMvPolynomial` and `MvPolynomial`.
 
 The forward/inverse correctness is obtained structurally from the underlying
 Mathlib `AlgEquiv` via `RingEquiv.trans`.
 -/
 
-namespace CPoly
-
-open Std CMvPolynomial
+open Std CPoly CMvPolynomial
 
 variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R]
 
+namespace CPoly
+
 /-! ### Polynomial-level ring equivalence -/
 
 /-- `Polynomial.mapEquiv` through the CMvPolynomial ↔ MvPolynomial bridge. -/
 noncomputable def polynomialCMvPolyEquiv :
     Polynomial (CMvPolynomial n R) ≃+* Polynomial (MvPolynomial (Fin n) R) :=
   Polynomial.mapEquiv polyRingEquiv
 
+end CPoly
+
+namespace CMvPolynomial
+
 /-! ### `finSuccEquiv` -/
 
 /-- Ring equivalence splitting off the first variable:
@@ -54,85 +61,46 @@ noncomputable def polynomialCMvPolyEquiv :
     This mirrors `MvPolynomial.finSuccEquiv R n`. The 0-th variable becomes
     the univariate indeterminate `Polynomial.X`, and variables `1, …, n` become
     the multivariate variables of the coefficient ring `CMvPolynomial n R`. -/
-noncomputable def CMvPolynomial.finSuccEquiv :
+noncomputable def finSuccEquiv :
     CMvPolynomial (n + 1) R ≃+* Polynomial (CMvPolynomial n R) :=
   (polyRingEquiv (n := n + 1)).trans <|
     (MvPolynomial.finSuccEquiv R n).toRingEquiv.trans polynomialCMvPolyEquiv.symm
 
 /-- The equivalence is a left inverse: applying the inverse then forward is the identity. -/
 @[simp]
-theorem CMvPolynomial.finSuccEquiv_symm_apply_apply (p : CMvPolynomial (n + 1) R) :
-    CMvPolynomial.finSuccEquiv.symm (CMvPolynomial.finSuccEquiv p) = p :=
-  CMvPolynomial.finSuccEquiv.symm_apply_apply p
+theorem finSuccEquiv_symm_apply_apply (p : CMvPolynomial (n + 1) R) :
+    finSuccEquiv.symm (finSuccEquiv p) = p :=
+  finSuccEquiv.symm_apply_apply p
 
 /-- The equivalence is a right inverse: applying forward then the inverse is the identity. -/
 @[simp]
-theorem CMvPolynomial.finSuccEquiv_apply_symm_apply
+theorem finSuccEquiv_apply_symm_apply
     (q : Polynomial (CMvPolynomial n R)) :
-    CMvPolynomial.finSuccEquiv (CMvPolynomial.finSuccEquiv.symm q) = q :=
-  CMvPolynomial.finSuccEquiv.apply_symm_apply q
+    finSuccEquiv (finSuccEquiv.symm q) = q :=
+  finSuccEquiv.apply_symm_apply q
 
 /-- `finSuccEquiv` preserves addition. -/
-theorem CMvPolynomial.finSuccEquiv_add (p q : CMvPolynomial (n + 1) R) :
-    CMvPolynomial.finSuccEquiv (p + q) =
-      CMvPolynomial.finSuccEquiv p + CMvPolynomial.finSuccEquiv q :=
-  CMvPolynomial.finSuccEquiv.map_add p q
+theorem finSuccEquiv_add (p q : CMvPolynomial (n + 1) R) :
+    finSuccEquiv (p + q) =
+      finSuccEquiv p + finSuccEquiv q :=
+  finSuccEquiv.map_add p q
 
 /-- `finSuccEquiv` preserves multiplication. -/
-theorem CMvPolynomial.finSuccEquiv_mul (p q : CMvPolynomial (n + 1) R) :
-    CMvPolynomial.finSuccEquiv (p * q) =
-      CMvPolynomial.finSuccEquiv p * CMvPolynomial.finSuccEquiv q :=
-  CMvPolynomial.finSuccEquiv.map_mul p q
+theorem finSuccEquiv_mul (p q : CMvPolynomial (n + 1) R) :
+    finSuccEquiv (p * q) =
+      finSuccEquiv p * finSuccEquiv q :=
+  finSuccEquiv.map_mul p q
 
 /-- `finSuccEquiv` maps zero to zero. -/
 @[simp]
-theorem CMvPolynomial.finSuccEquiv_zero :
-    CMvPolynomial.finSuccEquiv (0 : CMvPolynomial (n + 1) R) = 0 :=
-  RingEquiv.map_zero (CMvPolynomial.finSuccEquiv (n := n) (R := R))
+theorem finSuccEquiv_zero :
+    finSuccEquiv (0 : CMvPolynomial (n + 1) R) = 0 :=
+  RingEquiv.map_zero (finSuccEquiv (n := n) (R := R))
 
 /-- `finSuccEquiv` maps one to one. -/
 @[simp]
-theorem CMvPolynomial.finSuccEquiv_one :
-    CMvPolynomial.finSuccEquiv (1 : CMvPolynomial (n + 1) R) = 1 :=
-  RingEquiv.map_one (CMvPolynomial.finSuccEquiv (n := n) (R := R))
-
-/-! ### `optionEquivLeft` -/
-
-/-- Ring equivalence mirroring `MvPolynomial.optionEquivLeft` for `CMvPolynomial`.
-
-    Since `CMvPolynomial` is indexed by `Fin n`, the `Option`-indexed analogue
-    of `MvPolynomial.optionEquivLeft R (Fin n)` is an equivalence
-    `CMvPolynomial (n+1) R ≃+* Polynomial (CMvPolynomial n R)`.
-    We define it by composing the `polyRingEquiv` bridge with the Mathlib
-    `MvPolynomial.optionEquivLeft` (after renaming `Fin (n+1) ≃ Option (Fin n)`
-    via `finSuccEquiv'`), matching how `MvPolynomial.finSuccEquiv` is built. -/
-noncomputable def CMvPolynomial.optionEquivLeft :
-    CMvPolynomial (n + 1) R ≃+* Polynomial (CMvPolynomial n R) :=
-  CMvPolynomial.finSuccEquiv
-
-/-- `optionEquivLeft` is a left inverse. -/
-@[simp]
-theorem CMvPolynomial.optionEquivLeft_symm_apply_apply (p : CMvPolynomial (n + 1) R) :
-    CMvPolynomial.optionEquivLeft.symm (CMvPolynomial.optionEquivLeft p) = p :=
-  CMvPolynomial.optionEquivLeft.symm_apply_apply p
+theorem finSuccEquiv_one :
+    finSuccEquiv (1 : CMvPolynomial (n + 1) R) = 1 :=
+  RingEquiv.map_one (finSuccEquiv (n := n) (R := R))
 
-/-- `optionEquivLeft` is a right inverse. -/
-@[simp]
-theorem CMvPolynomial.optionEquivLeft_apply_symm_apply
-    (q : Polynomial (CMvPolynomial n R)) :
-    CMvPolynomial.optionEquivLeft (CMvPolynomial.optionEquivLeft.symm q) = q :=
-  CMvPolynomial.optionEquivLeft.apply_symm_apply q
-
-/-- `optionEquivLeft` preserves addition. -/
-theorem CMvPolynomial.optionEquivLeft_add (p q : CMvPolynomial (n + 1) R) :
-    CMvPolynomial.optionEquivLeft (p + q) =
-      CMvPolynomial.optionEquivLeft p + CMvPolynomial.optionEquivLeft q :=
-  CMvPolynomial.optionEquivLeft.map_add p q
-
-/-- `optionEquivLeft` preserves multiplication. -/
-theorem CMvPolynomial.optionEquivLeft_mul (p q : CMvPolynomial (n + 1) R) :
-    CMvPolynomial.optionEquivLeft (p * q) =
-      CMvPolynomial.optionEquivLeft p * CMvPolynomial.optionEquivLeft q :=
-  CMvPolynomial.optionEquivLeft.map_mul p q
-
-end CPoly
+end CMvPolynomial

CompPoly/Multivariate/Rename.lean

@@ -287,9 +287,17 @@ lemma rename_rename {k : ℕ} (f : Fin n → Fin m)
     fromCMvPolynomial_rename]
   exact MvPolynomial.rename_rename f g (fromCMvPolynomial p)
 
+end CPoly
+
+namespace CMvPolynomial
+
+open CPoly
+
+variable {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R]
+
 /-- Ring equivalence for variable renaming when the function is
 a bijection. -/
-noncomputable def CMvPolynomial.renameEquiv
+noncomputable def renameEquiv
     (f : Fin n ≃ Fin m) :
     CMvPolynomial n R ≃+* CMvPolynomial m R where
   toFun := CMvPolynomial.rename f
@@ -301,4 +309,4 @@ noncomputable def CMvPolynomial.renameEquiv
   map_add' p q := rename_add f p q
   map_mul' p q := rename_mul f p q
 
-end CPoly
+end CMvPolynomial

ROADMAP.md

@@ -42,7 +42,7 @@ CompPoly aims to be the premier formally verified library for computable polynom
    - ✅ `aeval`, `bind₁`: Algebra evaluation and substitution
    - ✅ `algebra`, `module`: Algebra and module structures
    - ✅ `degrees`; ✅ `eval₂Hom`: Degree utilities and evaluation homomorphisms
-   - ✅ `finSuccEquiv`, `optionEquivLeft`: Variable manipulation equivalences (for `CMvPolynomial`)
+   - ✅ `finSuccEquiv`: Variable manipulation equivalences (for `CMvPolynomial`)
    - ✅ `isEmptyRingEquiv` for `CMvPolynomial 0 R`
    - ✅ `smulZeroClass`: Scalar multiplication with zero behavior
    - ✅ `sumToIter`: Iteration utility with reconstruction/API lemmas
@@ -69,7 +69,7 @@ CompPoly aims to be the premier formally verified library for computable polynom
    - Implement FFT/NTT-based multiplication (O(n log n) vs current O(n²))
    - Focus on NTT for finite field arithmetic
    - Maintain correctness proofs alongside optimizations
-   
+
 **Note**: [erdkocak](https://github.com/erdkocak) and [doran2728](https://github.com/doran2728) have communicated they will be working on this.
 
 3. **Exponentiation optimization**
@@ -105,7 +105,7 @@ CompPoly aims to be the premier formally verified library for computable polynom
 
 **Goal**: Turn CompPoly into an integration-ready, downstream-friendly library by adding interoperability layers, serialization, proof automation, and extraction compatibility.
 
-#### Priorities 
+#### Priorities
 
 1. **Lowering / interop with LLZK / PrimeIR polynomial dialects**
 	- Explore representing CompPoly structures in the MLIR pipeline