TameOrbitTransitivity.lean

1 import PaperXI.OrbitSpan
2 import PaperXI.GeneratedIrreducibility
3 
4 /-! The orbit-transitivity part of Theorem 3.2 for an actual irreducible group
5 representation with explicitly generating tame inertia and Frobenius. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TameOrbitTransitivity
9 open scoped BigOperators
10 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusOrbit
11 open PaperXI.OrbitSpan PaperXI.GeneratedIrreducibility
12 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
13 variable {M : ℕ} [NeZero M]
14 
15 abbrev tameRestriction (π : Representation ℂ G V)
16     (ι : Multiplicative (ZMod M) →* G) : Action (K := ℂ) (V := V) (M := M) := π.comp ι
17 
18 def generators (ι : Multiplicative (ZMod M) →* G) (φ : G) : Set G :=
19   Set.range ι ∪ {φ, φ⁻¹}
20 
21 omit [NeZero M] in
22 /-- The geometric group relation implies the checked operator relation. -/
23 theorem geometric_relation (π : Representation ℂ G V)
24     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
25     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
26       ι (Multiplicative.ofAdd (q : ZMod M))) :
27     (actionEquiv π φ).symm.conj (operator (tameRestriction π ι) 1) =
28       operator (tameRestriction π ι) (q : ZMod M) := by
29   apply LinearMap.ext
30   intro v
31   change π φ⁻¹ (π (ι (Multiplicative.ofAdd (1 : ZMod M))) (π φ v)) =
32     π (ι (Multiplicative.ofAdd (q : ZMod M))) v
33   calc
34     _ = π (φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ) v := by
35       simp [map_mul, Module.End.mul_apply]
36     _ = _ := by rw [hrel]
37 
38 theorem generators_preserve_orbitSpan (π : Representation ℂ G V)
39     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
40     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
41       ι (Multiplicative.ofAdd (q : ZMod M))) (j : ZMod M) :
42     ∀ g ∈ generators ι φ, ∀ v ∈ orbitSpan (tameRestriction π ι) q j,
43       π g v ∈ orbitSpan (tameRestriction π ι) q j := by
44   intro g hg v hv
45   rcases hg with ⟨a, rfl⟩ | hg
46   · exact inertia_stable (tameRestriction π ι) q j a.toAdd hv
47   · rcases hg with hg | hg
48     · have heq : g = φ := hg
49       subst g
50       exact forward_stable (tameRestriction π ι) (actionEquiv π φ) q
51         (geometric_relation π ι φ q hrel) j hv
52     · have heq : g = φ⁻¹ := hg
53       subst g
54       exact backward_stable (tameRestriction π ι) (actionEquiv π φ) q
55         (geometric_relation π ι φ q hrel) j hv
56 
57 /-- A packet orbit spans a genuine subrepresentation of the whole group. -/
58 def orbitSubrepresentation (π : Representation ℂ G V)
59     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
60     (hgen : Submonoid.closure (generators ι φ) = ⊤)
61     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
62       ι (Multiplicative.ofAdd (q : ZMod M))) (j : ZMod M) : Subrepresentation π where
63   toSubmodule := orbitSpan (tameRestriction π ι) q j
64   apply_mem_toSubmodule g _ hv :=
65     stable_of_generators π (generators ι φ) hgen _
66       (generators_preserve_orbitSpan π ι φ q hrel j) g hv
67 
68 theorem orbitSpan_eq_top (π : Representation ℂ G V) [Representation.IsIrreducible π]
69     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
70     (hgen : Submonoid.closure (generators ι φ) = ⊤)
71     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
72       ι (Multiplicative.ofAdd (q : ZMod M)))
73     {j : ZMod M} (hj : packet (tameRestriction π ι) j ≠ ⊥) :
74     orbitSpan (tameRestriction π ι) q j = ⊤ := by
75   exact (eq_bot_or_top π (generators ι φ) hgen _
76     (generators_preserve_orbitSpan π ι φ q hrel j)).resolve_left
77       (span_ne_bot (tameRestriction π ι) q hj)
78 
79 /-- Any two nonzero tame character packets lie in one Frobenius orbit. -/
80 theorem nonzero_packets_one_orbit (π : Representation ℂ G V)
81     [Representation.IsIrreducible π]
82     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
83     (hgen : Submonoid.closure (generators ι φ) = ⊤)
84     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
85       ι (Multiplicative.ofAdd (q : ZMod M)))
86     {j k : ZMod M} (hj : packet (tameRestriction π ι) j ≠ ⊥)
87     (hk : packet (tameRestriction π ι) k ≠ ⊥) :
88     ∃ n : ℤ, ((q ^ n : (ZMod M)ˣ) : ZMod M) * j = k :=
89   related_of_span_top (tameRestriction π ι) q (orbitSpan_eq_top π ι φ q hgen hrel hj) hk
90 
91 /-- Completeness ensures that the support of an irreducible representation is nonempty. -/
92 theorem exists_nonzero_packet (π : Representation ℂ G V) [Representation.IsIrreducible π]
93     (ι : Multiplicative (ZMod M) →* G) :
94     ∃ j : ZMod M, packet (tameRestriction π ι) j ≠ ⊥ := by
95   have : Nontrivial V := nontrivial_space π
96   obtain ⟨v, hv⟩ := exists_ne (0 : V)
97   by_contra hn
98   push Not at hn
99   have hp (j : ZMod M) : projector (tameRestriction π ι) j v = 0 := by
100     have h := PaperXI.FourierPackets.projector_mem_packet (tameRestriction π ι)
101       ZMod.stdAddChar j v
102     change projector (tameRestriction π ι) j v ∈ packet (tameRestriction π ι) j at h
103     simpa [hn j] using h
104   have hsum := PaperXI.FourierPackets.vector_reconstruction (tameRestriction π ι)
105     ZMod.stdAddChar (ZMod.isPrimitive_stdAddChar M) (NeZero.ne (M : ℂ)) v
106   change (∑ j : ZMod M, projector (tameRestriction π ι) j v) = v at hsum
107   have hz : v = 0 := by simpa only [hp, Finset.sum_const_zero] using hsum.symm
108   exact hv hz
109 
110 end PaperXI.TameOrbitTransitivity

Back to source controls