InertiaFixed.lean

1 import PaperXI.PacketReturn
2 import Mathlib.RepresentationTheory.Invariants
3 
4 /-! Actual inertia invariants of a cyclic packet, without irreducibility or
5 an assumption that its inertia labels are distinct. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.InertiaFixed
9 open PaperXI.CyclicAction PaperXI.PacketTransport
10 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
11 variable {M : ℕ} [NeZero M]
12 
13 theorem invariants_eq_packet_zero (ρ : Action (K := ℂ) (V := V) (M := M)) :
14     ρ.invariants = packet ρ 0 := by
15   ext v
16   constructor
17   · intro hv a
18     simpa [operator] using hv (Multiplicative.ofAdd a)
19   · intro hv a
20     simpa [operator] using hv a.toAdd
21 
22 omit [NeZero M] in
23 theorem orbit_label_eq_zero_iff (q : (ZMod M)ˣ) (j : ZMod M) (n : ℕ) :
24     ((q ^ n : (ZMod M)ˣ) : ZMod M) * j = 0 ↔ j = 0 := by
25   constructor
26   · intro h
27     have h' := congrArg (fun x : ZMod M => (((q ^ n)⁻¹ : (ZMod M)ˣ) : ZMod M) * x) h
28     simpa only [← mul_assoc, Units.inv_mul, one_mul, mul_zero] using h'
29   · rintro rfl
30     simp
31 
32 theorem invariants_eq_top_of_basis (ρ : Action (K := ℂ) (V := V) (M := M))
33     {ι : Type*} (b : Module.Basis ι ℂ V) (hb : ∀ i, b i ∈ packet ρ 0) :
34     ρ.invariants = ⊤ := by
35   rw [invariants_eq_packet_zero]
36   apply top_unique
37   rw [← b.span_eq]
38   exact Submodule.span_le.mpr (by rintro _ ⟨i, rfl⟩; exact hb i)
39 
40 theorem invariants_eq_bot_of_basis (ρ : Action (K := ℂ) (V := V) (M := M))
41     {ι : Type*} (b : Module.Basis ι ℂ V) (labels : ι → ZMod M)
42     (hlabels : ∀ i, labels i ≠ 0) (hb : ∀ i, b i ∈ packet ρ (labels i)) :
43     ρ.invariants = ⊥ := by
44   have hp : projector ρ 0 = 0 := by
45     apply b.ext
46     intro i
47     exact projector_on_other_packet ρ (Ne.symm (hlabels i)) (hb i)
48   rw [invariants_eq_packet_zero]
49   apply le_antisymm
50   · intro v hv
51     have he := (mem_iff_projector ρ 0 v).mp hv
52     rw [hp] at he
53     exact he.symm
54   · exact bot_le
55 
56 theorem fixed_forward (ρ : Action (K := ℂ) (V := V) (M := M))
57     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
58     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
59     {v : V} (hv : v ∈ ρ.invariants) : F v ∈ ρ.invariants := by
60   rw [invariants_eq_packet_zero] at hv ⊢
61   simpa using forward_mem ρ F q h 0 hv
62 
63 theorem fixed_backward (ρ : Action (K := ℂ) (V := V) (M := M))
64     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
65     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
66     {v : V} (hv : v ∈ ρ.invariants) : F.symm v ∈ ρ.invariants := by
67   rw [invariants_eq_packet_zero] at hv ⊢
68   simpa using backward_mem ρ F q h 0 hv
69 
70 theorem invariants_of_cycle_basis (ρ : Action (K := ℂ) (V := V) (M := M))
71     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
72     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
73     {n : ℕ} (b : Module.Basis (Fin n) ℂ V) (j : ZMod M) {v : V}
74     (hv : v ∈ packet ρ j) (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v) :
75     ρ.invariants = if j = 0 then ⊤ else ⊥ := by
76   classical
77   have hmem (i : Fin n) : b i ∈ packet ρ (((q ^ (i : ℕ) : (ZMod M)ˣ) : ZMod M) * j) := by
78     rw [hb]
79     exact PaperXI.PacketReturn.power_mem ρ F q h j i hv
80   by_cases hj : j = 0
81   · rw [ite_eq_left hj]
82     apply invariants_eq_top_of_basis ρ b
83     intro i
84     simpa [hj] using hmem i
85   · rw [ite_eq_right hj]
86     apply invariants_eq_bot_of_basis ρ b _ _ hmem
87     intro i hz
88     exact hj ((orbit_label_eq_zero_iff q j i).mp hz)
89 
90 end PaperXI.InertiaFixed

Back to source controls