PacketLines.lean

1 import PaperXI.CycleSpan
2 
3 /-! A return eigenline exhausts its packet in an actual irreducible
4 representation. No packet dimension or spanning conclusion is assumed. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.PacketLines
8 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusPeriod
9 open PaperXI.CycleSpan PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
10 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
11 variable {M : ℕ} [NeZero M]
12 
13 def orbitLabel (q : (ZMod M)ˣ) (j : ZMod M) (a : Fin (period q j)) : ZMod M :=
14   ((q ^ (a : ℕ) : (ZMod M)ˣ) : ZMod M) * j
15 
16 theorem orbitLabel_injective (q : (ZMod M)ˣ) (j : ZMod M) :
17     Function.Injective (orbitLabel q j) := by
18   intro a b h
19   apply (orbitEquiv q j).injective
20   exact Subtype.ext h
21 
22 theorem cycle_mem_packet (ρ : Action (K := ℂ) (V := V) (M := M))
23     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
24     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
25     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) (a : Fin (period q j)) :
26     cycleVector F v a ∈ packet ρ (orbitLabel q j a) :=
27   PaperXI.PacketReturn.power_mem ρ F q h j a hv
28 
29 theorem inertia_cycle (ρ : Action (K := ℂ) (V := V) (M := M))
30     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
31     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
32     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j)
33     (a : Fin (period q j)) (b : ZMod M) :
34     operator ρ b (cycleVector F v a) =
35       ZMod.stdAddChar (orbitLabel q j a * b) • cycleVector F v a :=
36   cycle_mem_packet ρ F q h j hv a b
37 
38 theorem inertia_stable (ρ : Action (K := ℂ) (V := V) (M := M))
39     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
40     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
41     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) (b : ZMod M)
42     {w : V} (hw : w ∈ cycleSpan F v (period q j)) :
43     operator ρ b w ∈ cycleSpan F v (period q j) := by
44   apply CycleSpan.map_mem F v (period q j) (operator ρ b) (fun a => ?_) hw
45   rw [inertia_cycle ρ F q h j hv]
46   exact (cycleSpan F v (period q j)).smul_mem _ (CycleSpan.power_mem F v a.isLt)
47 
48 /-- Fourier projectors extract exactly one vector of the finite orbit. -/
49 theorem projector_cycle (ρ : Action (K := ℂ) (V := V) (M := M))
50     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
51     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
52     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) (a b : Fin (period q j)) :
53     projector ρ (orbitLabel q j a) (cycleVector F v b) =
54       if b = a then cycleVector F v a else 0 := by
55   classical
56   by_cases hab : b = a
57   · subst b
58     simp only [ite_true]
59     exact (mem_iff_projector ρ _ _).mp (cycle_mem_packet ρ F q h j hv a)
60   · rw [ite_eq_right hab]
61     apply projector_on_other_packet ρ _ (cycle_mem_packet ρ F q h j hv b)
62     intro heq
63     exact hab ((orbitLabel_injective q j heq).symm)
64 
65 /-- Projecting the finite cycle span onto its initial packet leaves just the chosen line. -/
66 theorem projection_to_line (ρ : Action (K := ℂ) (V := V) (M := M))
67     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
68     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
69     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) :
70     cycleSpan F v (period q j) ≤ (Submodule.span ℂ {v}).comap (projector ρ j) := by
71   apply Submodule.span_le.mpr
72   rintro w ⟨a, rfl⟩
73   change projector ρ j (cycleVector F v a) ∈ Submodule.span ℂ {v}
74   by_cases ha : (a : ℕ) = 0
75   · have heq : cycleVector F v a = v := by simp [cycleVector, ha]
76     rw [heq, (mem_iff_projector ρ j v).mp hv]
77     exact Submodule.subset_span (Set.mem_singleton v)
78   · have hne : j ≠ orbitLabel q j a :=
79       (no_short_return q j (Nat.pos_of_ne_zero ha) a.isLt).symm
80     rw [projector_on_other_packet ρ hne (cycle_mem_packet ρ F q h j hv a)]
81     exact Submodule.zero_mem _
82 
83 theorem packet_eq_line_of_span_top (ρ : Action (K := ℂ) (V := V) (M := M))
84     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
85     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
86     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j)
87     (htop : cycleSpan F v (period q j) = ⊤) : packet ρ j = Submodule.span ℂ {v} := by
88   apply le_antisymm
89   · intro w hw
90     have ht : w ∈ cycleSpan F v (period q j) := by simp [htop]
91     have hm := projection_to_line ρ F q h j hv ht
92     change projector ρ j w ∈ Submodule.span ℂ {v} at hm
93     rwa [(mem_iff_projector ρ j w).mp hw] at hm
94   · exact Submodule.span_le.mpr (by simpa using hv)
95 
96 variable {G : Type*} [Group G]
97 
98 theorem generators_preserve_cycleSpan (π : Representation ℂ G V)
99     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
100     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
101       ι (Multiplicative.ofAdd (q : ZMod M)))
102     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j)
103     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
104     ∀ g ∈ generators ι φ, ∀ w ∈ cycleSpan (actionEquiv π φ) v (period q j),
105       π g w ∈ cycleSpan (actionEquiv π φ) v (period q j) := by
106   intro g hg w hw
107   rcases hg with ⟨a, rfl⟩ | hg
108   · exact inertia_stable (tameRestriction π ι) (actionEquiv π φ) q
109       (geometric_relation π ι φ q hrel) j hv a.toAdd hw
110   · rcases hg with hg | hg
111     · have heq : g = φ := hg
112       subst g
113       exact CycleSpan.forward_stable (actionEquiv π φ) v (period_pos q j) hclose hw
114     · have heq : g = φ⁻¹ := hg
115       subst g
116       exact CycleSpan.backward_stable (actionEquiv π φ) v (period_pos q j) hc hclose hw
117 
118 theorem cycleSpan_eq_top (π : Representation ℂ G V) [Representation.IsIrreducible π]
119     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
120     (hgen : Submonoid.closure (generators ι φ) = ⊤)
121     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
122       ι (Multiplicative.ofAdd (q : ZMod M)))
123     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
124     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
125     cycleSpan (actionEquiv π φ) v (period q j) = ⊤ :=
126   (eq_bot_or_top π (generators ι φ) hgen _
127     (generators_preserve_cycleSpan π ι φ q hrel j hv hc hclose)).resolve_left
128       (CycleSpan.span_ne_bot (actionEquiv π φ) hv0 (period_pos q j))
129 
130 /-- Every nonzero packet is one-dimensional; this is a conclusion of irreducibility. -/
131 theorem nonzero_packet_finrank_one [FiniteDimensional ℂ V]
132     (π : Representation ℂ G V) [Representation.IsIrreducible π]
133     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
134     (hgen : Submonoid.closure (generators ι φ) = ⊤)
135     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
136       ι (Multiplicative.ofAdd (q : ZMod M)))
137     {j : ZMod M} (hj : packet (tameRestriction π ι) j ≠ ⊥) :
138     Module.finrank ℂ (packet (tameRestriction π ι) j) = 1 := by
139   obtain ⟨c, v, hc, hv, hv0, hclose⟩ := PaperXI.PacketReturn.exists_closing_eigenvector
140     (tameRestriction π ι) (actionEquiv π φ) q (geometric_relation π ι φ q hrel) hj
141   have htop := cycleSpan_eq_top π ι φ q hgen hrel j hv hv0 hc hclose
142   have hline := packet_eq_line_of_span_top (tameRestriction π ι) (actionEquiv π φ) q
143     (geometric_relation π ι φ q hrel) j hv htop
144   rw [hline]
145   exact finrank_span_singleton hv0
146 
147 end PaperXI.PacketLines

Back to source controls