CyclicProjectors.lean

1 module
2 public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
3 public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
4 public import Mathlib.LinearAlgebra.Matrix.Hermitian
5 public import Mathlib.Algebra.Star.Unitary
6 public import Mathlib.Tactic
7 /-! Author: Komorebi P. Paper VII, checked third block.
8 This module is independently compilable using the pinned portable Lean kit. -/
9 public section
10 set_option autoImplicit false
11 set_option linter.unusedSectionVars false
12 set_option backward.isDefEq.respectTransparency false
13 set_option backward.isDefEq.respectTransparency.types false
14 namespace KomorebiPaperVII.CyclicProjectors
15 open Finset ZMod AddChar
16 variable {N : ℕ} [NeZero N]
17 variable {A : Type*} [Ring A] [Algebra ℂ A]
18 
19 noncomputable def packet (rho : ZMod N → A) (j : ZMod N) : A :=
20   (N : ℂ)⁻¹ • ∑ r : ZMod N, stdAddChar (-(r*j)) • rho r
21 
22 theorem character_sum (t : ZMod N) :
23     ∑ r : ZMod N, stdAddChar (t*r) = if t=0 then (N : ℂ) else 0 := by
24   split_ifs with h
25   · simp [h]
26   · exact sum_eq_zero_of_ne_one (isPrimitive_stdAddChar N h)
27 
28 theorem packet_eigen (rho : ZMod N → A)
29     (hadd : ∀ a b, rho (a+b) = rho a * rho b) (a j : ZMod N) :
30     rho a * packet rho j = stdAddChar (a*j) • packet rho j := by
31   unfold packet
32   rw [Algebra.mul_smul_comm, Finset.mul_sum]
33   simp only [Algebra.mul_smul_comm, ← hadd]
34   have hs : (∑ r : ZMod N, stdAddChar (-(r*j)) • rho (a+r)) =
35       ∑ r : ZMod N, stdAddChar (-((r-a)*j)) • rho r := by
36     apply Fintype.sum_equiv (Equiv.addLeft a)
37     intro r
38     simp
39   rw [hs]
40   have hf (r : ZMod N) : -((r-a)*j) = a*j + -(r*j) := by ring
41   simp only [hf, map_add_eq_mul, mul_smul]
42   rw [← Finset.smul_sum, smul_comm]
43 
44 theorem packet_mul (rho : ZMod N → A)
45     (hadd : ∀ a b, rho (a+b) = rho a * rho b) (j k : ZMod N) :
46     packet rho j * packet rho k = if j=k then packet rho j else 0 := by
47   conv_lhs => lhs; unfold packet
48   rw [Algebra.smul_mul_assoc, Finset.sum_mul]
49   simp only [Algebra.smul_mul_assoc, packet_eigen rho hadd, smul_smul,
50     ← map_add_eq_mul]
51   have hf (r : ZMod N) : -(r*j) + r*k = (k-j)*r := by ring
52   simp only [hf]
53   rw [← Finset.sum_smul, character_sum]
54   by_cases h : j=k
55   · subst k
56     simp [NeZero.ne N]
57   · have hk : k-j ≠ 0 := sub_ne_zero.mpr (Ne.symm h)
58     simp [hk, h]
59 
60 theorem packet_idempotent (rho : ZMod N → A)
61     (hadd : ∀ a b, rho (a+b) = rho a * rho b) (j : ZMod N) :
62     packet rho j * packet rho j = packet rho j := by
63   simp [packet_mul rho hadd]
64 
65 theorem packet_complete (rho : ZMod N → A) (hzero : rho 0 = 1) :
66     ∑ j : ZMod N, packet rho j = 1 := by
67   simp only [packet, ← Finset.smul_sum]
68   rw [Finset.sum_comm]
69   simp only [← Finset.sum_smul, ← neg_mul, character_sum, neg_eq_zero,
70     ite_smul, zero_smul, Finset.sum_ite_eq', Finset.mem_univ, ite_true, hzero]
71   simp [NeZero.ne N]
72 
73 /-- The representation is constructed from actual powers of the finite-order symmetry. -/
74 noncomputable def cyclicPowers (S : A) (r : ZMod N) : A := S ^ r.val
75 
76 theorem powers_zero (S : A) : cyclicPowers (N := N) S 0 = 1 := by
77   simp [cyclicPowers]
78 
79 theorem powers_add (S : A) (hS : S^N=1) (r s : ZMod N) :
80     cyclicPowers S (r+s) = cyclicPowers S r * cyclicPowers S s := by
81   rw [cyclicPowers, ZMod.val_add, ← pow_eq_pow_mod _ hS, pow_add]
82   rfl
83 
84 theorem powers_one (S : A) (hS : S^N=1) : cyclicPowers (N := N) S 1 = S := by
85   rw [cyclicPowers, show (1 : ZMod N).val = 1 % N from by simpa using ZMod.val_natCast N 1, ← pow_eq_pow_mod _ hS, pow_one]
86 
87 theorem cyclic_quantum_projectors (S : A) (hS : S^N=1) :
88     (∀ j k : ZMod N, packet (cyclicPowers S) j * packet (cyclicPowers S) k =
89       if j=k then packet (cyclicPowers S) j else 0) ∧
90     (∑ j : ZMod N, packet (cyclicPowers S) j) = 1 ∧
91     ∀ j : ZMod N, S * packet (cyclicPowers S) j =
92       stdAddChar j • packet (cyclicPowers S) j := by
93   refine ⟨packet_mul _ (powers_add S hS), packet_complete _ (powers_zero S), ?_⟩
94   intro j
95   simpa only [powers_one S hS, one_mul] using packet_eigen _ (powers_add S hS) 1 j
96 
97 theorem star_character (x : ZMod N) : star (stdAddChar x) = stdAddChar (-x) := by
98   simpa only [stdAddChar_apply, map_neg_eq_inv, Circle.coe_inv, starRingEnd_apply] using
99     (Circle.coe_inv_eq_conj (toCircle x)).symm
100 
101 section Star
102 variable [StarRing A] [StarModule ℂ A]
103 
104 theorem packet_selfAdjoint (rho : ZMod N → A)
105     (hstar : ∀ r, star (rho r) = rho (-r)) (j : ZMod N) :
106     star (packet rho j) = packet rho j := by
107   unfold packet
108   simp only [star_smul, star_sum, star_character, hstar, neg_neg]
109   have hn : star ((N : ℂ)⁻¹) = (N : ℂ)⁻¹ := by simp
110   rw [hn]
111   congr 1
112   apply Fintype.sum_equiv (Equiv.neg (ZMod N))
113   intro r
114   simp
115 
116 theorem powers_star (S : A) (hS : S^N=1) (hU : S ∈ unitary A)
117     (r : ZMod N) : star (cyclicPowers S r) = cyclicPowers S (-r) := by
118   have hleft : star (cyclicPowers S r) * cyclicPowers S r = 1 := by
119     exact Unitary.star_mul_self_of_mem ((unitary A).pow_mem hU r.val)
120   have hright : cyclicPowers S r * cyclicPowers S (-r) = 1 := by
121     rw [← powers_add S hS, add_neg_cancel, powers_zero]
122   calc
123     star (cyclicPowers S r) = star (cyclicPowers S r) *
124       (cyclicPowers S r * cyclicPowers S (-r)) := by rw [hright, mul_one]
125     _ = cyclicPowers S (-r) := by rw [← mul_assoc, hleft, one_mul]
126 
127 theorem cyclic_packet_selfAdjoint (S : A) (hS : S^N=1) (hU : S ∈ unitary A)
128     (j : ZMod N) : star (packet (cyclicPowers S) j) = packet (cyclicPowers S) j := by
129   exact packet_selfAdjoint _ (powers_star S hS hU) j
130 
131 end Star
132 
133 /-- The standard complex Nth root, identified with its exponential expression. -/
134 noncomputable def omega : ℂ := stdAddChar (1 : ZMod N)
135 
136 theorem omega_exponential : omega (N := N) =
137     Complex.exp (2 * Real.pi * Complex.I / (N : ℂ)) := by
138   simpa [omega] using (ZMod.stdAddChar_coe (N := N) (1 : ℤ))
139 
140 theorem character_as_power (r : ZMod N) : stdAddChar r = omega (N := N) ^ r.val := by
141   simpa [omega, nsmul_eq_mul] using (stdAddChar (N := N)).map_nsmul_eq_pow r.val (1 : ZMod N)
142 
143 theorem packet_coefficient (r j : ZMod N) :
144     stdAddChar (-(r*j)) = (omega (N := N) ^ (r.val * j.val))⁻¹ := by
145   rw [map_neg_eq_inv]
146   congr 1
147   have h : r*j = (r.val * j.val) • (1 : ZMod N) := by simp [nsmul_eq_mul]
148   rw [h, map_nsmul_eq_pow]
149   rfl
150 
151 theorem cyclic_projector_formula (S : A) (j : ZMod N) :
152     packet (cyclicPowers S) j = (N : ℂ)⁻¹ •
153       ∑ r : ZMod N, ((omega (N := N)) ^ (r.val*j.val))⁻¹ • S^r.val := by
154   simp only [packet, packet_coefficient, cyclicPowers]
155 
156 /-- Concrete complex-matrix version, including the Hermitian projector condition. -/
157 theorem finite_cyclic_projectors {n : Type*} [Fintype n] [DecidableEq n]
158     (S : Matrix n n ℂ) (hS : S^N=1) (hU : S ∈ unitary (Matrix n n ℂ)) :
159     (∀ j k : ZMod N, packet (cyclicPowers S) j * packet (cyclicPowers S) k =
160       if j=k then packet (cyclicPowers S) j else 0) ∧
161     (∑ j : ZMod N, packet (cyclicPowers S) j) = 1 ∧
162     (∀ j : ZMod N, S * packet (cyclicPowers S) j =
163       omega (N := N)^j.val • packet (cyclicPowers S) j) ∧
164     ∀ j : ZMod N, (packet (cyclicPowers S) j).IsHermitian := by
165   obtain ⟨hp, hs, he⟩ := cyclic_quantum_projectors S hS
166   refine ⟨hp, hs, ?_, ?_⟩
167   · intro j
168     simpa only [character_as_power] using he j
169   · intro j
170     exact cyclic_packet_selfAdjoint S hS hU j
171 
172 end KomorebiPaperVII.CyclicProjectors
173 
174 /-! Complete declaration-level trust audit. -/
175 #print axioms KomorebiPaperVII.CyclicProjectors.character_sum
176 #print axioms KomorebiPaperVII.CyclicProjectors.packet_eigen
177 #print axioms KomorebiPaperVII.CyclicProjectors.packet_mul
178 #print axioms KomorebiPaperVII.CyclicProjectors.packet_idempotent
179 #print axioms KomorebiPaperVII.CyclicProjectors.packet_complete
180 #print axioms KomorebiPaperVII.CyclicProjectors.powers_zero
181 #print axioms KomorebiPaperVII.CyclicProjectors.powers_add
182 #print axioms KomorebiPaperVII.CyclicProjectors.powers_one
183 #print axioms KomorebiPaperVII.CyclicProjectors.cyclic_quantum_projectors
184 #print axioms KomorebiPaperVII.CyclicProjectors.star_character
185 #print axioms KomorebiPaperVII.CyclicProjectors.packet_selfAdjoint
186 #print axioms KomorebiPaperVII.CyclicProjectors.powers_star
187 #print axioms KomorebiPaperVII.CyclicProjectors.cyclic_packet_selfAdjoint
188 #print axioms KomorebiPaperVII.CyclicProjectors.omega_exponential
189 #print axioms KomorebiPaperVII.CyclicProjectors.character_as_power
190 #print axioms KomorebiPaperVII.CyclicProjectors.packet_coefficient
191 #print axioms KomorebiPaperVII.CyclicProjectors.cyclic_projector_formula
192 #print axioms KomorebiPaperVII.CyclicProjectors.finite_cyclic_projectors

Back to source controls