FiniteModels.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.SectionCycles
7 import Mathlib.RingTheory.AdjoinRoot
8 import Mathlib.Analysis.Normed.Algebra.MatrixExponential
9 
10 /-!
11 # Finite algebra and companion-matrix models
12 
13 This file formalizes the finite models from Section 6 of Paper IV.  The
14 quotient-algebra exponential identities are identities of formal power series.
15 The companion matrix is treated both algebraically, through an exact formula
16 for every matrix power, and analytically through the finite-dimensional matrix
17 exponential.
18 
19 No determinant-of-exponential theorem is assumed here.  The pinned Mathlib
20 matrix-exponential API explicitly leaves that general theorem as future work.
21 -/
22 
23 namespace Komorebi.PaperIV
24 
25 open Polynomial NormedSpace
26 open scoped PowerSeries
27 
28 noncomputable section
29 
30 /-! ## The two finite quotient algebras -/
31 
32 /-- The polynomial defining the cyclic algebra `R[xi] / (xi^N - 1)`. -/
33 def cyclicAlgebraPolynomial (R : Type*) [CommRing R] (N : ℕ) : R[X] :=
34   X ^ N - 1
35 
36 /-- The polynomial defining the signed cyclic algebra `R[xi] / (xi^N + 1)`. -/
37 def signedCyclicAlgebraPolynomial (R : Type*) [CommRing R] (N : ℕ) : R[X] :=
38   X ^ N + 1
39 
40 /-- The finite cyclic quotient algebra `R[xi] / (xi^N - 1)`. -/
41 abbrev CyclicAlgebra (R : Type*) [CommRing R] (N : ℕ) :=
42   AdjoinRoot (cyclicAlgebraPolynomial R N)
43 
44 /-- The finite signed quotient algebra `R[xi] / (xi^N + 1)`. -/
45 abbrev SignedCyclicAlgebra (R : Type*) [CommRing R] (N : ℕ) :=
46   AdjoinRoot (signedCyclicAlgebraPolynomial R N)
47 
48 /-- The distinguished generator of the cyclic quotient algebra. -/
49 def cyclicGenerator (R : Type*) [CommRing R] (N : ℕ) : CyclicAlgebra R N :=
50   AdjoinRoot.root (cyclicAlgebraPolynomial R N)
51 
52 /-- The distinguished generator of the signed quotient algebra. -/
53 def signedCyclicGenerator (R : Type*) [CommRing R] (N : ℕ) : SignedCyclicAlgebra R N :=
54   AdjoinRoot.root (signedCyclicAlgebraPolynomial R N)
55 
56 @[simp]
57 theorem cyclicGenerator_pow (R : Type*) [CommRing R] (N : ℕ) :
58     cyclicGenerator R N ^ N = 1 := by
59   have h := AdjoinRoot.eval₂_root (cyclicAlgebraPolynomial R N)
60   rw [cyclicAlgebraPolynomial, Polynomial.eval₂_sub, Polynomial.eval₂_pow,
61     Polynomial.eval₂_X, Polynomial.eval₂_one] at h
62   exact sub_eq_zero.mp h
63 
64 @[simp]
65 theorem signedCyclicGenerator_pow (R : Type*) [CommRing R] (N : ℕ) :
66     signedCyclicGenerator R N ^ N = -1 := by
67   have h := AdjoinRoot.eval₂_root (signedCyclicAlgebraPolynomial R N)
68   rw [signedCyclicAlgebraPolynomial, Polynomial.eval₂_add, Polynomial.eval₂_pow,
69     Polynomial.eval₂_X, Polynomial.eval₂_one] at h
70   exact eq_neg_of_add_eq_zero_left h
71 
72 /-- Reduction of powers in the cyclic quotient algebra. -/
73 theorem cyclicGenerator_pow_eq_mod (R : Type*) [CommRing R] (N m : ℕ) :
74     cyclicGenerator R N ^ m = cyclicGenerator R N ^ (m % N) := by
75   calc
76     cyclicGenerator R N ^ m =
77         cyclicGenerator R N ^ (m % N + N * (m / N)) := by
78           rw [Nat.mod_add_div]
79     _ = cyclicGenerator R N ^ (m % N) *
80         (cyclicGenerator R N ^ N) ^ (m / N) := by
81           rw [pow_add, pow_mul]
82     _ = cyclicGenerator R N ^ (m % N) := by simp
83 
84 /-- Reduction of powers in the signed quotient algebra, including every
85 wraparound sign. -/
86 theorem signedCyclicGenerator_pow_eq_mod (R : Type*) [CommRing R] (N m : ℕ) :
87     signedCyclicGenerator R N ^ m =
88       (-1 : SignedCyclicAlgebra R N) ^ (m / N) *
89         signedCyclicGenerator R N ^ (m % N) := by
90   calc
91     signedCyclicGenerator R N ^ m =
92         signedCyclicGenerator R N ^ (m % N + N * (m / N)) := by
93           rw [Nat.mod_add_div]
94     _ = signedCyclicGenerator R N ^ (m % N) *
95         (signedCyclicGenerator R N ^ N) ^ (m / N) := by
96           rw [pow_add, pow_mul]
97     _ = signedCyclicGenerator R N ^ (m % N) *
98         (-1 : SignedCyclicAlgebra R N) ^ (m / N) := by
99           rw [signedCyclicGenerator_pow]
100     _ = _ := by ring
101 
102 /-- A power basis witnessing the unique representative of degree below `N`
103 in the cyclic quotient algebra. -/
104 def cyclicAlgebraPowerBasis (R : Type*) [CommRing R] (N : ℕ) (hN : 0 < N) :
105     PowerBasis R (CyclicAlgebra R N) :=
106   AdjoinRoot.powerBasis'
107     (by simpa [cyclicAlgebraPolynomial] using
108       (Polynomial.monic_X_pow_sub_C (1 : R) hN.ne'))
109 
110 /-- A power basis witnessing the unique representative of degree below `N`
111 in the signed quotient algebra. -/
112 def signedCyclicAlgebraPowerBasis (R : Type*) [CommRing R] (N : ℕ) (hN : 0 < N) :
113     PowerBasis R (SignedCyclicAlgebra R N) :=
114   AdjoinRoot.powerBasis'
115     (by simpa [signedCyclicAlgebraPolynomial] using
116       (Polynomial.monic_X_pow_add_C (1 : R) hN.ne'))
117 
118 @[simp]
119 theorem cyclicAlgebraPowerBasis_dim (R : Type*) [CommRing R] [Nontrivial R]
120     (N : ℕ) (hN : 0 < N) :
121     (cyclicAlgebraPowerBasis R N hN).dim = N := by
122   rw [cyclicAlgebraPowerBasis, AdjoinRoot.powerBasis'_dim]
123   simpa [cyclicAlgebraPolynomial] using
124     (Polynomial.natDegree_X_pow_sub_C (R := R) (n := N) (r := 1))
125 
126 @[simp]
127 theorem signedCyclicAlgebraPowerBasis_dim (R : Type*) [CommRing R] [Nontrivial R]
128     (N : ℕ) (hN : 0 < N) :
129     (signedCyclicAlgebraPowerBasis R N hN).dim = N := by
130   rw [signedCyclicAlgebraPowerBasis, AdjoinRoot.powerBasis'_dim]
131   simp [signedCyclicAlgebraPolynomial]
132 
133 section FormalAlgebraExponential
134 
135 variable (R : Type*) [CommRing R] [Algebra ℚ R]
136 
137 /-- The formal exponential `exp(lambda X xi)` in the cyclic quotient algebra. -/
138 def cyclicAlgebraExponentialSeries (N : ℕ) (lambda : R) :
139     (CyclicAlgebra R N)⟦X⟧ :=
140   PowerSeries.rescale
141     (algebraMap R (CyclicAlgebra R N) lambda * cyclicGenerator R N)
142     (PowerSeries.exp (CyclicAlgebra R N))
143 
144 /-- The formal exponential `exp(X xi)` in the signed quotient algebra. -/
145 def signedCyclicAlgebraExponentialSeries (N : ℕ) :
146     (SignedCyclicAlgebra R N)⟦X⟧ :=
147   PowerSeries.rescale (signedCyclicGenerator R N)
148     (PowerSeries.exp (SignedCyclicAlgebra R N))
149 
150 /-- Exact formal version of
151 `exp(lambda z xi) = sum_j E_{N,j}(lambda z) xi^j` in `xi^N = 1`. -/
152 theorem cyclicAlgebra_exponential_eq_sections (N : ℕ) (hN : 0 < N) (lambda : R) :
153     cyclicAlgebraExponentialSeries R N lambda =
154       ∑ j : Fin N,
155         PowerSeries.C (cyclicGenerator R N ^ j.val) *
156           transferSection N j.val (algebraMap R (CyclicAlgebra R N) lambda) := by
157   classical
158   ext m
159   rw [cyclicAlgebraExponentialSeries, PowerSeries.coeff_rescale, map_sum]
160   simp only [PowerSeries.coeff_exp, PowerSeries.coeff_C_mul, coeff_transferSection,
161     transferSectionCoeff]
162   rw [mul_pow, cyclicGenerator_pow_eq_mod]
163   have hm : m % N < N := Nat.mod_lt m hN
164   rw [Finset.sum_eq_single (⟨m % N, hm⟩ : Fin N)]
165   · simp only [ite_true]
166     ring
167   · intro b _hb hne
168     have hval : m % N ≠ b.val := by
169       intro heq
170       apply hne
171       apply Fin.ext
172       simpa using heq.symm
173     simp [hval]
174   · simp
175 
176 /-- Exact formal version of
177 `exp(z xi) = sum_j D_{N,j}(z) xi^j` in `xi^N = -1`. -/
178 theorem signedCyclicAlgebra_exponential_eq_sections (N : ℕ) (hN : 0 < N) :
179     signedCyclicAlgebraExponentialSeries R N =
180       ∑ j : Fin N,
181         PowerSeries.C (signedCyclicGenerator R N ^ j.val) *
182           signedSection (R := SignedCyclicAlgebra R N) N j.val := by
183   classical
184   ext m
185   rw [signedCyclicAlgebraExponentialSeries, PowerSeries.coeff_rescale, map_sum]
186   simp only [PowerSeries.coeff_exp, PowerSeries.coeff_C_mul, coeff_signedSection,
187     signedSectionCoeff]
188   rw [signedCyclicGenerator_pow_eq_mod]
189   have hm : m % N < N := Nat.mod_lt m hN
190   rw [Finset.sum_eq_single (⟨m % N, hm⟩ : Fin N)]
191   · simp only [ite_true]
192     ring
193   · intro b _hb hne
194     have hval : m % N ≠ b.val := by
195       intro heq
196       apply hne
197       apply Fin.ext
198       simpa using heq.symm
199     simp [hval]
200   · simp
201 
202 end FormalAlgebraExponential
203 
204 /-! ## The signed cyclic shift and all of its powers -/
205 
206 section SignedShift
207 
208 variable {R : Type*} [CommRing R]
209 
210 /-- Closed form for the `k`th signed cyclic shift.  There is one nonzero entry
211 in each column, and its sign records the number of crossings of the signed
212 edge. -/
213 def signedShiftPowerMatrix (N k : ℕ) : Matrix (Fin N) (Fin N) R :=
214   fun p q =>
215     if p.val = (q.val + k) % N then
216       (-1 : R) ^ ((q.val + k) / N)
217     else 0
218 
219 /-- The signed cyclic shift `J_N`; column `q` is sent to column `q+1`, with a
220 minus sign at the wraparound. -/
221 def signedShiftMatrix (N : ℕ) : Matrix (Fin N) (Fin N) R :=
222   signedShiftPowerMatrix N 1
223 
224 @[simp]
225 theorem signedShiftPowerMatrix_apply (N k : ℕ) (p q : Fin N) :
226     signedShiftPowerMatrix (R := R) N k p q =
227       if p.val = (q.val + k) % N then
228         (-1 : R) ^ ((q.val + k) / N)
229       else 0 := rfl
230 
231 @[simp]
232 theorem signedShiftPowerMatrix_zero (N : ℕ) :
233     signedShiftPowerMatrix (R := R) N 0 = 1 := by
234   ext p q
235   rw [Matrix.one_apply]
236   by_cases hpq : p = q
237   · subst p
238     simp [signedShiftPowerMatrix, Nat.mod_eq_of_lt q.isLt, Nat.div_eq_of_lt q.isLt]
239   · have hval : p.val ≠ q.val := fun h => hpq (Fin.ext h)
240     simp [signedShiftPowerMatrix, Nat.mod_eq_of_lt q.isLt, hpq, hval]
241 
242 private theorem add_mod_after_mod (N t a : ℕ) :
243     (t % N + a) % N = (t + a) % N := by
244   calc
245     (t % N + a) % N = (t % N % N + a % N) % N := Nat.add_mod _ _ _
246     _ = (t % N + a % N) % N := by rw [Nat.mod_mod]
247     _ = (t + a) % N := (Nat.add_mod _ _ _).symm
248 
249 private theorem add_div_after_mod (N t a : ℕ) (hN : 0 < N) :
250     (t % N + a) / N + t / N = (t + a) / N := by
251   rw [← Nat.add_mul_div_left (t % N + a) (t / N) hN]
252   congr 1
253   calc
254     t % N + a + N * (t / N) = (t % N + N * (t / N)) + a := by omega
255     _ = t + a := by rw [Nat.mod_add_div]
256 
257 /-- The closed signed shifts form an additive one-parameter semigroup. -/
258 theorem signedShiftPowerMatrix_mul (N a b : ℕ) (hN : 0 < N) :
259     signedShiftPowerMatrix (R := R) N a * signedShiftPowerMatrix N b =
260       signedShiftPowerMatrix N (a + b) := by
261   classical
262   ext p q
263   rw [Matrix.mul_apply]
264   let x : Fin N := ⟨(q.val + b) % N, Nat.mod_lt _ hN⟩
265   rw [Finset.sum_eq_single x]
266   · simp only [signedShiftPowerMatrix]
267     have hmod : (x.val + a) % N = (q.val + (a + b)) % N := by
268       change ((q.val + b) % N + a) % N = _
269       rw [add_mod_after_mod]
270       congr 1
271       omega
272     have hdiv :
273         (x.val + a) / N + (q.val + b) / N =
274           (q.val + (a + b)) / N := by
275       change ((q.val + b) % N + a) / N + (q.val + b) / N = _
276       rw [add_div_after_mod N (q.val + b) a hN]
277       congr 1
278       omega
279     rw [show x.val = (q.val + b) % N by rfl]
280     simp only [ite_true]
281     rw [hmod]
282     by_cases hp : p.val = (q.val + (a + b)) % N
283     · simp only [hp, ite_true]
284       rw [← pow_add, hdiv]
285     · simp [hp]
286   · intro y _hy hyx
287     simp only [signedShiftPowerMatrix]
288     have hval : y.val ≠ (q.val + b) % N := by
289       intro h
290       apply hyx
291       apply Fin.ext
292       exact h
293     simp [hval]
294   · simp
295 
296 /-- Every matrix power of `J_N` has the closed signed-shift form. -/
297 theorem signedShiftMatrix_pow (N k : ℕ) (hN : 0 < N) :
298     signedShiftMatrix (R := R) N ^ k = signedShiftPowerMatrix N k := by
299   induction k with
300   | zero => simp
301   | succ k ih =>
302       rw [pow_succ, ih, signedShiftMatrix, signedShiftPowerMatrix_mul N k 1 hN]
303 
304 /-- Exact entry formula for every power of the signed shift. -/
305 theorem signedShiftMatrix_pow_apply (N k : ℕ) (hN : 0 < N) (p q : Fin N) :
306     (signedShiftMatrix (R := R) N ^ k) p q =
307       if p.val = (q.val + k) % N then
308         (-1 : R) ^ ((q.val + k) / N)
309       else 0 := by
310   rw [signedShiftMatrix_pow N k hN]
311   rfl
312 
313 private theorem signedShiftPowerMatrix_period (N : ℕ) (hN : 0 < N) :
314     signedShiftPowerMatrix (R := R) N N = -1 := by
315   ext p q
316   rw [Matrix.neg_apply, Matrix.one_apply]
317   have hmod : (q.val + N) % N = q.val := by
318     rw [Nat.add_mod_right, Nat.mod_eq_of_lt q.isLt]
319   have hdiv : (q.val + N) / N = 1 := by
320     simpa [Nat.div_eq_of_lt q.isLt] using Nat.add_mul_div_left q.val 1 hN
321   by_cases hpq : p = q
322   · subst p
323     simp [signedShiftPowerMatrix, hmod, hdiv]
324   · have hval : p.val ≠ q.val := fun h => hpq (Fin.ext h)
325     simp [signedShiftPowerMatrix, hmod, hpq, hval]
326 
327 /-- The companion relation `J_N^N = -I`. -/
328 theorem signedShiftMatrix_pow_order (N : ℕ) (hN : 0 < N) :
329     signedShiftMatrix (R := R) N ^ N = -1 := by
330   rw [signedShiftMatrix_pow N N hN, signedShiftPowerMatrix_period N hN]
331 
332 end SignedShift
333 
334 /-! ## The analytic finite-dimensional fundamental matrix -/
335 
336 /-- The fundamental matrix `U_N(z) = exp(z J_N)`. -/
337 def signedFundamentalMatrix (N : ℕ) (z : ℂ) : Matrix (Fin N) (Fin N) ℂ :=
338   exp (z • signedShiftMatrix (R := ℂ) N)
339 
340 /-- The matrix exponential obeys the addition law. -/
341 theorem signedFundamentalMatrix_add (N : ℕ) (z w : ℂ) :
342     signedFundamentalMatrix N (z + w) =
343       signedFundamentalMatrix N z * signedFundamentalMatrix N w := by
344   rw [signedFundamentalMatrix, add_smul]
345   exact Matrix.exp_add_of_commute _ _
346     (((Commute.refl (signedShiftMatrix (R := ℂ) N)).smul_left z).smul_right w)
347 
348 /-- Negating the parameter gives the matrix inverse. -/
349 theorem signedFundamentalMatrix_neg (N : ℕ) (z : ℂ) :
350     signedFundamentalMatrix N (-z) = (signedFundamentalMatrix N z)⁻¹ := by
351   rw [signedFundamentalMatrix, signedFundamentalMatrix, neg_smul]
352   exact Matrix.exp_neg _
353 
354 /-- Two opposite parameters multiply to the identity matrix. -/
355 theorem signedFundamentalMatrix_mul_neg (N : ℕ) (z : ℂ) :
356     signedFundamentalMatrix N z * signedFundamentalMatrix N (-z) = 1 := by
357   rw [← signedFundamentalMatrix_add, add_neg_cancel]
358   simp [signedFundamentalMatrix]
359 
360 /-- The fundamental matrix is a unit for every parameter. -/
361 theorem signedFundamentalMatrix_isUnit (N : ℕ) (z : ℂ) :
362     IsUnit (signedFundamentalMatrix N z) := by
363   exact Matrix.isUnit_exp _
364 
365 end
366 
367 end Komorebi.PaperIV

Back to source controls