RegularCyclic.lean

1 import PaperXI.TameProjectors
2 
3 /-! A concrete regular cyclic model. Every character packet is nonzero, and
4 the erroneous forward-label rule has an actual complex representation counterexample. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.RegularCyclic
8 open PaperXI.CyclicAction
9 variable {K : Type*} [Field K]
10 variable {M : ℕ}
11 
12 def translation (a : ZMod M) : Module.End K (ZMod M → K) where
13   toFun f x := f (x + a)
14   map_add' _ _ := rfl
15   map_smul' _ _ := rfl
16 
17 def regular : Action (K := K) (V := ZMod M → K) (M := M) where
18   toFun a := translation a.toAdd
19   map_one' := by
20     apply LinearMap.ext
21     intro f
22     funext x
23     simp [translation]
24   map_mul' a b := by
25     apply LinearMap.ext
26     intro f
27     funext x
28     simp [translation, Module.End.mul_apply, add_assoc]
29 
30 @[simp] theorem operator_apply (a x : ZMod M) (f : ZMod M → K) :
31     operator (regular (K := K)) a f x = f (x + a) := rfl
32 
33 def frobenius (q : (ZMod M)ˣ) : (ZMod M → K) ≃ₗ[K] (ZMod M → K) where
34   toFun f x := f (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * x)
35   invFun f x := f ((q : ZMod M) * x)
36   left_inv f := by funext x; simp [← mul_assoc]
37   right_inv f := by funext x; simp [← mul_assoc]
38   map_add' _ _ := rfl
39   map_smul' _ _ := rfl
40 
41 theorem generator_relation (q : (ZMod M)ˣ) :
42     (frobenius (K := K) q).conj (operator regular 1) = operator regular (q : ZMod M) := by
43   apply LinearMap.ext
44   intro f
45   funext x
46   change f ((q : ZMod M) * (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * x + 1)) =
47     f (x + (q : ZMod M))
48   simp [mul_add, ← mul_assoc]
49 
50 theorem character_vector_mem (ψ : AddChar (ZMod M) K) (j : ZMod M) :
51     (fun x => ψ (j * x)) ∈ PaperXI.FourierPackets.packet regular ψ j := by
52   intro a
53   funext x
54   change ψ (j * (x + a)) = ψ (j * a) * ψ (j * x)
55   rw [mul_add, AddChar.map_add_eq_mul, mul_comm]
56 
57 variable [NeZero M]
58 
59 theorem projector_nonzero (ψ : AddChar (ZMod M) K) (hM : (M : K) ≠ 0) (j : ZMod M) :
60     PaperXI.FourierProjectors.projector regular ψ j ≠ 0 := by
61   intro h
62   have hp := PaperXI.FourierPackets.projector_on_packet regular ψ hM j
63     (character_vector_mem ψ j)
64   have hh := congrArg (fun f : ZMod M → K => f 0) hp
65   simp [h] at hh
66 
67 theorem projectors_distinct (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive)
68     (hM : (M : K) ≠ 0) {i j : ZMod M} (hij : i ≠ j) :
69     PaperXI.FourierProjectors.projector regular ψ i ≠
70       PaperXI.FourierProjectors.projector regular ψ j := by
71   intro h
72   have hp := PaperXI.FourierProjectors.projector_orthogonal regular ψ hψ hM hij
73   rw [h, ← pow_two, PaperXI.FourierProjectors.projector_idempotent regular ψ hψ hM] at hp
74   exact projector_nonzero ψ hM j hp
75 
76 def twoModFive : (ZMod 5)ˣ := ⟨2, 3, by decide, by decide⟩
77 
78 /-- Actual counterexample over C: F t F^-1 = t^2 but F P_1 F^-1 is not P_2. -/
79 theorem wrong_forward_label :
80     (frobenius (K := ℂ) twoModFive).conj
81       (PaperXI.TameProjectors.projector (regular (K := ℂ) (M := 5)) 1) ≠
82         PaperXI.TameProjectors.projector (regular (K := ℂ) (M := 5)) 2 := by
83   rw [PaperXI.TameProjectors.forward_generator_covariance regular (frobenius twoModFive)
84     twoModFive (generator_relation twoModFive)]
85   apply projectors_distinct ZMod.stdAddChar (ZMod.isPrimitive_stdAddChar 5)
86     (by norm_num : (5 : ℂ) ≠ 0)
87   change (3 : ZMod 5) * 1 ≠ 2
88   decide
89 
90 end PaperXI.RegularCyclic

Back to source controls