TameProjectors.lean

1 import PaperXI.FourierPackets
2 import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
3 
4 /-! Proposition 3.1 over C, with primitivity and the nonzero denominator proved.
5 Both Frobenius conventions are stated explicitly, without changing the operators. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TameProjectors
9 open scoped BigOperators
10 open PaperXI.CyclicAction
11 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
12 variable {M : ℕ} [NeZero M]
13 
14 def projector (ρ : Action (K := ℂ) (V := V) (M := M)) (j : ZMod M) : Module.End ℂ V :=
15   PaperXI.FourierProjectors.projector ρ ZMod.stdAddChar j
16 
17 theorem idempotent (ρ : Action (K := ℂ) (V := V) (M := M)) (j : ZMod M) :
18     projector ρ j ^ 2 = projector ρ j :=
19   PaperXI.FourierProjectors.projector_idempotent ρ _ (ZMod.isPrimitive_stdAddChar M)
20     (NeZero.ne (M : ℂ)) j
21 
22 theorem orthogonal (ρ : Action (K := ℂ) (V := V) (M := M))
23     {i j : ZMod M} (h : i ≠ j) : projector ρ i * projector ρ j = 0 :=
24   PaperXI.FourierProjectors.projector_orthogonal ρ _ (ZMod.isPrimitive_stdAddChar M)
25     (NeZero.ne (M : ℂ)) h
26 
27 theorem complete (ρ : Action (K := ℂ) (V := V) (M := M)) :
28     (∑ j : ZMod M, projector ρ j) = 1 :=
29   PaperXI.FourierProjectors.projector_complete ρ _ (ZMod.isPrimitive_stdAddChar M)
30     (NeZero.ne (M : ℂ))
31 
32 theorem range_eq_character_space (ρ : Action (K := ℂ) (V := V) (M := M)) (j : ZMod M) :
33     LinearMap.range (projector ρ j) = PaperXI.FourierPackets.packet ρ ZMod.stdAddChar j :=
34   PaperXI.FourierPackets.projector_range ρ _ (NeZero.ne (M : ℂ)) j
35 
36 /-- Under F t F^-1 = t^q the projector label changes by q^-1. -/
37 theorem forward_generator_covariance (ρ : Action (K := ℂ) (V := V) (M := M))
38     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
39     (h : F.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
40     F.conj (projector ρ j) = projector ρ (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) :=
41   PaperXI.FourierCovariance.inverse_exponent_covariance q F (operator ρ) ZMod.stdAddChar j
42     (conjugation_from_generator ρ F q h)
43 
44 /-- Under F^-1 t F = t^q the projector label changes by q. -/
45 theorem geometric_covariance (ρ : Action (K := ℂ) (V := V) (M := M))
46     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
47     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
48     F.conj (projector ρ j) = projector ρ ((q : ZMod M) * j) := by
49   have hs := forward_generator_covariance ρ F.symm q h ((q : ZMod M) * j)
50   simp only [← mul_assoc, Units.inv_mul, one_mul] at hs
51   have hh := congrArg F.conj hs
52   simpa only [LinearEquiv.conj_conj_symm] using hh.symm
53 
54 theorem character_weight (j a : ZMod M) :
55     (ZMod.stdAddChar (N := M)) (-j * a) =
56       (ZMod.stdAddChar (N := M) 1) ^ (-((j.val : ℤ) * (a.val : ℤ))) := by
57   have h : (-((j.val : ℤ) * (a.val : ℤ))) • (1 : ZMod M) = -j * a := by
58     simp [zsmul_eq_mul]
59   rw [← h, AddChar.map_zsmul_eq_zpow]
60 
61 theorem standard_root : (ZMod.stdAddChar (N := M)) 1 =
62     Complex.exp (2 * Real.pi * Complex.I / M) := by
63   simpa using (ZMod.stdAddChar_coe (N := M) (1 : ℤ))
64 
65 /-- The computed operator is exactly the manuscript's root-of-unity sum. -/
66 theorem manuscript_formula (ρ : Action (K := ℂ) (V := V) (M := M)) (j : ZMod M) :
67     projector ρ j = (M : ℂ)⁻¹ • ∑ a : ZMod M,
68       (Complex.exp (2 * Real.pi * Complex.I / M)) ^ (-((j.val : ℤ) * (a.val : ℤ))) •
69         (operator ρ 1 ^ a.val) := by
70   rw [projector, PaperXI.FourierProjectors.projector_formula]
71   congr 1
72   apply Finset.sum_congr rfl
73   intro a _
74   rw [character_weight, standard_root, operator_eq_generator_pow ρ a]
75 
76 /-- The complete finite statement in Proposition 3.1 with the geometric relation. -/
77 theorem tame_projector_theorem (ρ : Action (K := ℂ) (V := V) (M := M))
78     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
79     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) :
80     (∀ j, projector ρ j ^ 2 = projector ρ j) ∧
81     (∀ i j, i ≠ j → projector ρ i * projector ρ j = 0) ∧
82     (∑ j : ZMod M, projector ρ j) = 1 ∧
83     (∀ j, F.conj (projector ρ j) = projector ρ ((q : ZMod M) * j)) :=
84   ⟨idempotent ρ, fun _ _ hij => orthogonal ρ hij, complete ρ, geometric_covariance ρ F q h⟩
85 
86 end PaperXI.TameProjectors

Back to source controls