QuotientExponential.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FiniteModels
6 import KomorebiPaperIV.EntireBridge
7 import Mathlib.Analysis.Normed.Module.FiniteDimension
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 
12 /-- The ordinary exponential power series in a finite-dimensional algebra. -/
13 def finiteAlgebraExponential {A : Type*} [Ring A] [Algebra ℂ A]
14     [TopologicalSpace A] (x : A) (z : ℂ) : A :=
15   ∑' m : ℕ, (z^m / (m.factorial : ℂ)) • x^m
16 
17 section General
18 variable {A : Type*} [CommRing A] [Algebra ℂ A]
19   [TopologicalSpace A] [ContinuousAdd A] [ContinuousSMul ℂ A]
20 
21 /-- Pointwise convergence and section coordinates when `x^N = 1`. -/
22 theorem hasSum_cyclicAlgebra_exponential {N : ℕ} (hN : 0 < N)
23     {omega : ℂ} (ho : IsPrimitiveRoot omega N) (x : A) (hx : x^N = 1)
24     (lambda z : ℂ) :
25     HasSum (fun m : ℕ => ((lambda*z)^m / (m.factorial : ℂ)) • x^m)
26       (∑ j : Fin N, entireTransfer N j.val omega lambda z • x^j.val) := by
27   have h := hasSum_sum (s := Finset.univ) (fun j (_ : j ∈ (Finset.univ : Finset (Fin N))) =>
28     (hasSum_entireTransfer hN j.isLt ho lambda z).smul_const (x^j.val))
29   apply h.congr_fun
30   intro m
31   have hxmod : x^m = x^(m%N) := by
32     calc
33       x^m = x^(m%N + N*(m/N)) := by rw [Nat.mod_add_div]
34       _ = x^(m%N) := by rw [pow_add, pow_mul, hx]; simp
35   rw [hxmod, Finset.sum_eq_single (⟨m%N, Nat.mod_lt m hN⟩ : Fin N)]
36   · simp only [coeff_transferSection, transferSectionCoeff, ite_true]
37     congr 1
38     simp [mul_pow, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
39   · intro j _ hj
40     have hne : m%N ≠ j.val := by intro he; apply hj; exact Fin.ext he.symm
41     simp [coeff_transferSection, transferSectionCoeff, hne]
42   · simp
43 
44 /-- Pointwise convergence and section coordinates when `x^N = -1`. -/
45 theorem hasSum_signedAlgebra_exponential {N : ℕ} (hN : 0 < N)
46     {omega rho : ℂ} (ho : IsPrimitiveRoot omega N) (hr : rho^N = -1)
47     (x : A) (hx : x^N = -1) (z : ℂ) :
48     HasSum (fun m : ℕ => (z^m / (m.factorial : ℂ)) • x^m)
49       (∑ j : Fin N, entireSigned N j.val omega rho z • x^j.val) := by
50   have h := hasSum_sum (s := Finset.univ) (fun j (_ : j ∈ (Finset.univ : Finset (Fin N))) =>
51     (hasSum_entireSigned hN j.isLt ho hr z).smul_const (x^j.val))
52   apply h.congr_fun
53   intro m
54   have hxmod : x^m = (-1 : A)^(m/N) * x^(m%N) := by
55     calc
56       x^m = x^(m%N + N*(m/N)) := by rw [Nat.mod_add_div]
57       _ = _ := by rw [pow_add, pow_mul, hx]; ring
58   rw [hxmod, Finset.sum_eq_single (⟨m%N, Nat.mod_lt m hN⟩ : Fin N)]
59   · simp only [coeff_signedSection, signedSectionCoeff, ite_true]
60     simp only [Algebra.smul_def, div_eq_mul_inv, map_mul, map_pow, map_neg, map_one, map_inv₀, map_natCast]
61     ring
62   · intro j _ hj
63     have hne : m%N ≠ j.val := by intro he; apply hj; exact Fin.ext he.symm
64     simp [coeff_signedSection, signedSectionCoeff, hne]
65   · simp
66 
67 end General
68 
69 /-- The coefficient sup norm supplies the canonical finite-dimensional quotient topology. -/
70 instance cyclicAlgebraNormedAddCommGroup (N : ℕ) [NeZero N] :
71     NormedAddCommGroup (CyclicAlgebra ℂ N) :=
72   NormedAddCommGroup.induced _ _
73     (cyclicAlgebraPowerBasis ℂ N (Nat.pos_of_ne_zero (NeZero.ne N))).basis.equivFun
74     (cyclicAlgebraPowerBasis ℂ N (Nat.pos_of_ne_zero (NeZero.ne N))).basis.equivFun.injective
75 
76 instance cyclicAlgebraNormedSpace (N : ℕ) [NeZero N] : NormedSpace ℂ (CyclicAlgebra ℂ N) :=
77   NormedSpace.induced ℂ _ _
78     (cyclicAlgebraPowerBasis ℂ N (Nat.pos_of_ne_zero (NeZero.ne N))).basis.equivFun
79 
80 instance signedAlgebraNormedAddCommGroup (N : ℕ) [NeZero N] :
81     NormedAddCommGroup (SignedCyclicAlgebra ℂ N) :=
82   NormedAddCommGroup.induced _ _
83     (signedCyclicAlgebraPowerBasis ℂ N (Nat.pos_of_ne_zero (NeZero.ne N))).basis.equivFun
84     (signedCyclicAlgebraPowerBasis ℂ N (Nat.pos_of_ne_zero (NeZero.ne N))).basis.equivFun.injective
85 
86 instance signedAlgebraNormedSpace (N : ℕ) [NeZero N] : NormedSpace ℂ (SignedCyclicAlgebra ℂ N) :=
87   NormedSpace.induced ℂ _ _
88     (signedCyclicAlgebraPowerBasis ℂ N (Nat.pos_of_ne_zero (NeZero.ne N))).basis.equivFun
89 
90 /-- Theorem 6.2 in the actual cyclic quotient algebra, at every complex argument. -/
91 theorem cyclicAlgebra_pointwise_exponential {N : ℕ} [NeZero N]
92     {omega : ℂ} (ho : IsPrimitiveRoot omega N) (lambda z : ℂ) :
93     finiteAlgebraExponential (cyclicGenerator ℂ N) (lambda*z) =
94       ∑ j : Fin N, entireTransfer N j.val omega lambda z • (cyclicGenerator ℂ N)^j.val := by
95   exact (hasSum_cyclicAlgebra_exponential (Nat.pos_of_ne_zero (NeZero.ne N)) ho
96     (cyclicGenerator ℂ N) (cyclicGenerator_pow ℂ N) lambda z).tsum_eq
97 
98 /-- Theorem 6.2 in the actual signed quotient algebra, at every complex argument. -/
99 theorem signedAlgebra_pointwise_exponential {N : ℕ} [NeZero N]
100     {omega rho : ℂ} (ho : IsPrimitiveRoot omega N) (hr : rho^N = -1) (z : ℂ) :
101     finiteAlgebraExponential (signedCyclicGenerator ℂ N) z =
102       ∑ j : Fin N, entireSigned N j.val omega rho z • (signedCyclicGenerator ℂ N)^j.val := by
103   exact (hasSum_signedAlgebra_exponential (Nat.pos_of_ne_zero (NeZero.ne N)) ho hr
104     (signedCyclicGenerator ℂ N) (signedCyclicGenerator_pow ℂ N) z).tsum_eq
105 
106 end
107 end Komorebi.PaperIV

Back to source controls