Skip to content

Commit 311784a

Browse files
DimitriosMitsiosDimitriosMitsios
authored
feat: Implement variable renaming: rename and renameEquiv (#83)
* implementation of rename * All properties of rename proven, renameEquiv also completed * Rename.lean file added * Removed private lemma and added some cleaning. * comments cleaned up * Authors field added
1 parent 258fa03 commit 311784a

3 files changed

Lines changed: 308 additions & 9 deletions

File tree

‎CompPoly.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import CompPoly.Multivariate.CMvPolynomial
1010
import CompPoly.Multivariate.CMvPolynomialEvalLemmas
1111
import CompPoly.Multivariate.Lawful
1212
import CompPoly.Multivariate.MvPolyEquiv
13+
import CompPoly.Multivariate.Rename
1314
import CompPoly.Multivariate.Unlawful
1415
import CompPoly.Multivariate.Wheels
1516
import CompPoly.Univariate.Raw

‎CompPoly/Multivariate/CMvPolynomial.lean‎

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -222,16 +222,11 @@ def bind₁ {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
222222
-/
223223
def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
224224
(f : Fin n → Fin m) (p : CMvPolynomial n R) : CMvPolynomial m R :=
225-
sorry
226-
227-
/-- Ring equivalence for variable renaming when the function is a bijection.
225+
let renameMonomial (mono : CMvMonomial n) : CMvMonomial m :=
226+
Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i))
227+
ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1
228228

229-
Given `f : Fin n ≃ Fin m`, provides a ring isomorphism between
230-
`CMvPolynomial n R` and `CMvPolynomial m R`.
231-
-/
232-
def renameEquiv {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
233-
(f : Fin n ≃ Fin m) : CMvPolynomial n R ≃+* CMvPolynomial m R :=
234-
sorry
229+
-- `renameEquiv` is defined in `CompPoly.Multivariate.Rename`
235230

236231
/-- Scalar multiplication with zero handling.
237232

‎CompPoly/Multivariate/Rename.lean‎

Lines changed: 303 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,303 @@
1+
/-
2+
Copyright (c) 2025 CompPoly. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Dimitris Mitsios
5+
-/
6+
import CompPoly.Multivariate.MvPolyEquiv
7+
import Mathlib.Algebra.MvPolynomial.Rename
8+
9+
/-!
10+
# Properties of variable renaming for `CMvPolynomial`
11+
12+
This file proves properties of the `rename` function defined in `CMvPolynomial.lean`,
13+
by transferring results from Mathlib's `MvPolynomial.rename` through the
14+
`polyRingEquiv : CMvPolynomial n R ≃+* MvPolynomial (Fin n) R` equivalence.
15+
16+
## Main results
17+
18+
* `fromCMvPolynomial_rename` — correspondence between `CMvPolynomial.rename` and
19+
`MvPolynomial.rename`
20+
* `rename_C`, `rename_X`, `rename_add`, `rename_mul`, `rename_id`, `rename_rename`
21+
— algebraic properties
22+
* `CMvPolynomial.renameEquiv` — ring isomorphism for bijective variable renaming
23+
24+
-/
25+
26+
namespace CPoly
27+
28+
open Std CMvPolynomial
29+
30+
variable {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
31+
32+
/-! ### Helper lemmas for `fromCMvPolynomial_rename` -/
33+
34+
/-- In a commutative additive monoid, the order of addition in a list fold
35+
does not matter. -/
36+
lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
37+
(g : K → V → β) (l : List (K × V)) (init : β) :
38+
List.foldl (fun acc pair => acc + g pair.1 pair.2) init l =
39+
List.foldl (fun acc pair => g pair.1 pair.2 + acc) init l := by
40+
induction l generalizing init with
41+
| nil => rfl
42+
| cons h t ih =>
43+
simp only [List.foldl_cons]
44+
rw [show init + g h.1 h.2 = g h.1 h.2 + init from add_comm _ _]
45+
exact ih _
46+
47+
/-- Swapping addition order in `ExtTreeMap.foldl` does not change the result. -/
48+
lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ}
49+
{R' : Type} (g : CMvMonomial k → R' → β)
50+
(t : Std.ExtTreeMap (CMvMonomial k) R') :
51+
Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t =
52+
Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by
53+
simp only [Std.ExtTreeMap.foldl_eq_foldl_toList]
54+
exact list_foldl_add_comm g t.toList 0
55+
56+
/-- Applying `CMvMonomial.toFinsupp` at index `i` equals `Vector.get`. -/
57+
lemma toFinsupp_apply (mono : CMvMonomial n) (i : Fin n) :
58+
(CMvMonomial.toFinsupp mono) i = mono.get i := rfl
59+
60+
/-- Monomial renaming via `Vector.ofFn` corresponds to `Finsupp.mapDomain`
61+
on the `Finsupp` side. -/
62+
lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) :
63+
(Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum
64+
(fun i => mono.get i)) : CMvMonomial m) =
65+
CMvMonomial.ofFinsupp
66+
(Finsupp.mapDomain f (CMvMonomial.toFinsupp mono)) := by
67+
unfold CMvMonomial.ofFinsupp
68+
congr 1; funext j
69+
simp only [Finsupp.mapDomain, Finsupp.sum_apply, Finsupp.single_apply]
70+
rw [Finset.sum_filter]
71+
rw [Finsupp.sum]
72+
-- Extend the sum from `support` to `Finset.univ`
73+
symm
74+
apply Finset.sum_subset (Finset.subset_univ _)
75+
intro x _ hxs
76+
rw [Finsupp.notMem_support_iff] at hxs
77+
simp [hxs]
78+
79+
/-- `fromCMvPolynomial` maps `CMvPolynomial.monomial` to
80+
`MvPolynomial.monomial`. -/
81+
lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
82+
fromCMvPolynomial (CMvPolynomial.monomial mono c) =
83+
MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by
84+
by_cases hc : c = 0
85+
· subst hc; simp [CMvPolynomial.monomial, map_zero]
86+
· ext μ
87+
rw [coeff_eq, MvPolynomial.coeff_monomial]
88+
unfold CMvPolynomial.coeff CMvPolynomial.monomial
89+
simp only [show (c == (0 : R)) = false from by simp [hc]]
90+
unfold Lawful.fromUnlawful
91+
erw [Unlawful.filter_get]
92+
simp only [Unlawful.ofList]
93+
by_cases hm : CMvMonomial.toFinsupp mono = μ
94+
· subst hm; rw [if_pos rfl, CMvMonomial.ofFinsupp_toFinsupp]
95+
erw [ExtTreeMap.getElem?_ofList_of_mem
96+
(k := mono) (k_eq := compare_self) (v := c)
97+
(mem := by simp) (distinct := ?distinct)]
98+
· simp
99+
case distinct => simp
100+
· rw [if_neg hm]
101+
have hne : CMvMonomial.ofFinsupp μ ≠ mono :=
102+
fun h => hm (h ▸ CMvMonomial.toFinsupp_ofFinsupp)
103+
erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false
104+
(by simp [hne])]
105+
rfl
106+
107+
/-- `fromCMvPolynomial` distributes over `Finsupp.sum`. -/
108+
lemma fromCMvPolynomial_finsupp_sum {k : ℕ}
109+
(g : (Fin n →₀ ℕ) → R → CMvPolynomial k R)
110+
(a : CMvPolynomial n R) :
111+
fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) =
112+
Finsupp.sum (fromCMvPolynomial a)
113+
(fun μ c => fromCMvPolynomial (g μ c)) := by
114+
unfold Finsupp.sum; ext
115+
simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
116+
117+
/-! ### Main correspondence lemma -/
118+
119+
/-- `CMvPolynomial.rename` agrees with `MvPolynomial.rename` under the
120+
`fromCMvPolynomial` equivalence. -/
121+
lemma fromCMvPolynomial_rename (f : Fin n → Fin m)
122+
(p : CMvPolynomial n R) :
123+
fromCMvPolynomial (CMvPolynomial.rename f p) =
124+
MvPolynomial.rename f (fromCMvPolynomial p) := by
125+
-- Express rename as a `Finsupp.sum` via `foldl_eq_sum`
126+
have step1 : CMvPolynomial.rename f p =
127+
Finsupp.sum (fromCMvPolynomial p) (fun μ c =>
128+
CMvPolynomial.monomial
129+
(CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by
130+
show Std.ExtTreeMap.foldl
131+
(fun acc mono c => acc + CMvPolynomial.monomial
132+
(Vector.ofFn fun j =>
133+
(Finset.univ.filter fun i => f i = j).sum
134+
fun i => mono.get i) c)
135+
0 p.1 = _
136+
simp_rw [renameMonomial_eq f]
137+
rw [foldl_add_comm' (fun mono c =>
138+
CMvPolynomial.monomial (CMvMonomial.ofFinsupp
139+
(Finsupp.mapDomain f (CMvMonomial.toFinsupp mono))) c)]
140+
rw [foldl_eq_sum]
141+
congr 1; ext μ c
142+
simp only [Function.comp_def, CMvMonomial.toFinsupp_ofFinsupp]
143+
rw [step1]
144+
rw [fromCMvPolynomial_finsupp_sum]
145+
simp only [fromCMvPolynomial_monomial,
146+
CMvMonomial.toFinsupp_ofFinsupp]
147+
-- Conclude using Mathlib's `MvPolynomial.rename_monomial`
148+
conv_rhs =>
149+
rw [← MvPolynomial.support_sum_monomial_coeff
150+
(fromCMvPolynomial p)]
151+
rw [map_sum (MvPolynomial.rename f)]
152+
simp only [MvPolynomial.rename_monomial]
153+
rfl
154+
155+
/-! ### Bridging lemmas for `C` and `X` -/
156+
157+
/-- `CMvPolynomial.C c` equals `CMvPolynomial.monomial 0 c`. -/
158+
lemma C_eq_monomial {k : ℕ} (c : R) :
159+
CMvPolynomial.C (n := k) c = CMvPolynomial.monomial 0 c := by
160+
by_cases hc : c = 0
161+
· subst hc; ext m
162+
unfold CMvPolynomial.coeff CMvPolynomial.C CMvPolynomial.monomial
163+
Lawful.C Unlawful.C
164+
grind
165+
· ext m
166+
show (CMvPolynomial.C c).coeff m =
167+
(CMvPolynomial.monomial (0 : CMvMonomial k) c).coeff m
168+
unfold CMvPolynomial.coeff CMvPolynomial.C Lawful.C
169+
CMvPolynomial.monomial Unlawful.C
170+
simp only [show (c == (0 : R)) = false from by simp [hc],
171+
hc, ite_false, MonoR.C]
172+
show (Unlawful.ofList [(CMvMonomial.zero, c)])[m]?.getD 0 =
173+
(Lawful.fromUnlawful
174+
(Unlawful.ofList [(CMvMonomial.zero, c)])).1[m]?.getD 0
175+
unfold Lawful.fromUnlawful
176+
erw [Unlawful.filter_get]
177+
178+
/-- The `Finsupp` of the zero monomial is zero. -/
179+
lemma toFinsupp_zero {k : ℕ} :
180+
CMvMonomial.toFinsupp (0 : CMvMonomial k) = 0 := by
181+
ext i
182+
simp [CMvMonomial.toFinsupp, Vector.get]
183+
184+
/-- `fromCMvPolynomial` maps `CMvPolynomial.C` to `MvPolynomial.C`. -/
185+
lemma fromCMvPolynomial_C {k : ℕ} (c : R) :
186+
fromCMvPolynomial (CMvPolynomial.C (n := k) c) =
187+
MvPolynomial.C c := by
188+
rw [C_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_zero,
189+
← MvPolynomial.C_apply]
190+
191+
/-! ### Algebraic properties of rename -/
192+
193+
/-- Constants are unchanged under renaming. -/
194+
@[simp]
195+
lemma rename_C (f : Fin n → Fin m) (c : R) :
196+
CMvPolynomial.rename f (CMvPolynomial.C c) =
197+
CMvPolynomial.C (n := m) c := by
198+
apply fromCMvPolynomial_injective
199+
rw [fromCMvPolynomial_rename, fromCMvPolynomial_C,
200+
fromCMvPolynomial_C]
201+
exact MvPolynomial.rename_C f c
202+
203+
/-- `CMvPolynomial.X i` equals `CMvPolynomial.monomial eᵢ 1`
204+
where `eᵢ` is the `i`-th standard basis vector. -/
205+
lemma X_eq_monomial {k : ℕ} (i : Fin k) :
206+
CMvPolynomial.X (R := R) i = CMvPolynomial.monomial
207+
(Vector.ofFn (fun j => if j = i then 1 else 0))
208+
(1 : R) := by
209+
unfold CMvPolynomial.X CMvPolynomial.monomial
210+
by_cases h : (1 : R) = 0
211+
· ext m; unfold CMvPolynomial.coeff Lawful.fromUnlawful
212+
erw [Unlawful.filter_get]; simp [h]; grind
213+
· simp only [show ((1 : R) == 0) = false from by simp [h]]
214+
exact (if_neg (by decide)).symm
215+
216+
/-- The `Finsupp` of the `i`-th standard basis monomial is
217+
`Finsupp.single i 1`. -/
218+
lemma toFinsupp_unitMono {k : ℕ} (i : Fin k) :
219+
CMvMonomial.toFinsupp
220+
(Vector.ofFn (fun j : Fin k =>
221+
if j = i then 1 else 0)) =
222+
Finsupp.single i 1 := by
223+
ext j
224+
simp [CMvMonomial.toFinsupp, Vector.get,
225+
Finsupp.single_apply, eq_comm]
226+
227+
/-- `fromCMvPolynomial` maps `CMvPolynomial.X i` to
228+
`MvPolynomial.X i`. -/
229+
lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) :
230+
fromCMvPolynomial (CMvPolynomial.X (R := R) i) =
231+
MvPolynomial.X i := by
232+
rw [X_eq_monomial, fromCMvPolynomial_monomial,
233+
toFinsupp_unitMono]
234+
rfl
235+
236+
/-- Renaming maps variable `X i` to `X (f i)`. -/
237+
@[simp]
238+
lemma rename_X (f : Fin n → Fin m) (i : Fin n) :
239+
CMvPolynomial.rename f (CMvPolynomial.X (R := R) i) =
240+
CMvPolynomial.X (f i) := by
241+
apply fromCMvPolynomial_injective
242+
rw [fromCMvPolynomial_rename, fromCMvPolynomial_X,
243+
fromCMvPolynomial_X]
244+
exact MvPolynomial.rename_X f i
245+
246+
/-- Renaming preserves addition. -/
247+
@[simp]
248+
lemma rename_add (f : Fin n → Fin m)
249+
(p q : CMvPolynomial n R) :
250+
CMvPolynomial.rename f (p + q) =
251+
CMvPolynomial.rename f p +
252+
CMvPolynomial.rename f q := by
253+
apply fromCMvPolynomial_injective
254+
simp only [fromCMvPolynomial_rename, CPoly.map_add]
255+
exact _root_.map_add (MvPolynomial.rename f)
256+
(fromCMvPolynomial p) (fromCMvPolynomial q)
257+
258+
/-- Renaming preserves multiplication. -/
259+
@[simp]
260+
lemma rename_mul (f : Fin n → Fin m)
261+
(p q : CMvPolynomial n R) :
262+
CMvPolynomial.rename f (p * q) =
263+
CMvPolynomial.rename f p *
264+
CMvPolynomial.rename f q := by
265+
apply fromCMvPolynomial_injective
266+
simp only [fromCMvPolynomial_rename, CPoly.map_mul]
267+
exact _root_.map_mul (MvPolynomial.rename f)
268+
(fromCMvPolynomial p) (fromCMvPolynomial q)
269+
270+
/-- Renaming by the identity function is the identity. -/
271+
@[simp]
272+
lemma rename_id (p : CMvPolynomial n R) :
273+
CMvPolynomial.rename id p = p := by
274+
apply fromCMvPolynomial_injective
275+
rw [fromCMvPolynomial_rename]
276+
exact MvPolynomial.rename_id_apply (fromCMvPolynomial p)
277+
278+
/-- Composing two renamings equals renaming by the composition. -/
279+
@[simp]
280+
lemma rename_rename {k : ℕ} (f : Fin n → Fin m)
281+
(g : Fin m → Fin k) (p : CMvPolynomial n R) :
282+
CMvPolynomial.rename g (CMvPolynomial.rename f p) =
283+
CMvPolynomial.rename (g ∘ f) p := by
284+
apply fromCMvPolynomial_injective
285+
rw [fromCMvPolynomial_rename, fromCMvPolynomial_rename,
286+
fromCMvPolynomial_rename]
287+
exact MvPolynomial.rename_rename f g (fromCMvPolynomial p)
288+
289+
/-- Ring equivalence for variable renaming when the function is
290+
a bijection. -/
291+
noncomputable def CMvPolynomial.renameEquiv
292+
(f : Fin n ≃ Fin m) :
293+
CMvPolynomial n R ≃+* CMvPolynomial m R where
294+
toFun := CMvPolynomial.rename f
295+
invFun := CMvPolynomial.rename f.symm
296+
left_inv p := by
297+
rw [rename_rename, f.symm_comp_self, rename_id]
298+
right_inv q := by
299+
rw [rename_rename, f.self_comp_symm, rename_id]
300+
map_add' p q := rename_add f p q
301+
map_mul' p q := rename_mul f p q
302+
303+
end CPoly

0 commit comments

Comments
 (0)