CyclicAction.lean

1 import PaperXI.FourierCovariance
2 import Mathlib.RepresentationTheory.Basic
3 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
4 
5 /-! Actual representations of the additive finite cyclic group. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CyclicAction
9 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
10 variable {M : ℕ}
11 
12 abbrev Action := Representation K (Multiplicative (ZMod M)) V
13 
14 def operator (ρ : Action (K := K) (V := V) (M := M)) (a : ZMod M) : Module.End K V :=
15   ρ (Multiplicative.ofAdd a)
16 
17 @[simp] theorem operator_zero (ρ : Action (K := K) (V := V) (M := M)) :
18     operator ρ 0 = 1 := map_one ρ
19 
20 theorem operator_add (ρ : Action (K := K) (V := V) (M := M)) (a b : ZMod M) :
21     operator ρ (a + b) = operator ρ a * operator ρ b := map_mul ρ _ _
22 
23 theorem operator_nsmul (ρ : Action (K := K) (V := V) (M := M)) (a : ZMod M) (n : ℕ) :
24     operator ρ (n • a) = operator ρ a ^ n := by
25   induction n with
26   | zero => simp
27   | succ n ih => rw [succ_nsmul, operator_add, ih, pow_succ]
28 
29 variable [NeZero M]
30 
31 theorem operator_mul (ρ : Action (K := K) (V := V) (M := M)) (a b : ZMod M) :
32     operator ρ (a * b) = operator ρ a ^ b.val := by
33   have h : a * b = b.val • a := by simp [nsmul_eq_mul, mul_comm]
34   rw [h, operator_nsmul]
35 
36 theorem operator_eq_generator_pow (ρ : Action (K := K) (V := V) (M := M)) (a : ZMod M) :
37     operator ρ a = operator ρ 1 ^ a.val := by simpa using operator_mul ρ 1 a
38 
39 omit [NeZero M] in
40 theorem generator_period (ρ : Action (K := K) (V := V) (M := M)) :
41     operator ρ 1 ^ M = 1 := by
42   rw [← operator_nsmul]
43   simp [nsmul_eq_mul]
44 
45 /-- The generator conjugation relation implies every cyclic action relation. -/
46 theorem conjugation_from_generator (ρ : Action (K := K) (V := V) (M := M))
47     (F : V ≃ₗ[K] V) (q : ZMod M)
48     (h : F.conj (operator ρ 1) = operator ρ q) (a : ZMod M) :
49     F.conj (operator ρ a) = operator ρ (q * a) := by
50   rw [operator_eq_generator_pow ρ a, operator_mul]
51   have hp : F.conj (operator ρ 1 ^ a.val) = F.conj (operator ρ 1) ^ a.val :=
52     map_pow F.conjRingEquiv _ _
53   rw [hp, h]
54 
55 end PaperXI.CyclicAction

Back to source controls