OrbitSpan.lean

1 import PaperXI.FrobeniusOrbit
2 
3 /-! The span of a Frobenius orbit of actual character spaces. Its stability and
4 separation from other packets are proved, not assumed. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.OrbitSpan
8 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusOrbit
9 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
10 variable {M : ℕ} [NeZero M]
11 
12 def orbitSpan (ρ : Action (K := ℂ) (V := V) (M := M))
13     (q : (ZMod M)ˣ) (j : ZMod M) : Submodule ℂ V :=
14   Submodule.span ℂ {v | ∃ k, Related q j k ∧ v ∈ packet ρ k}
15 
16 theorem packet_le (ρ : Action (K := ℂ) (V := V) (M := M))
17     (q : (ZMod M)ˣ) {j k : ZMod M} (hk : Related q j k) :
18     packet ρ k ≤ orbitSpan ρ q j := by
19   intro v hv
20   exact Submodule.subset_span ⟨k, hk, hv⟩
21 
22 theorem self_packet_le (ρ : Action (K := ℂ) (V := V) (M := M))
23     (q : (ZMod M)ˣ) (j : ZMod M) : packet ρ j ≤ orbitSpan ρ q j :=
24   packet_le ρ q (FrobeniusOrbit.refl q j)
25 
26 theorem map_mem (ρ : Action (K := ℂ) (V := V) (M := M))
27     (q : (ZMod M)ˣ) (j : ZMod M) (A : Module.End ℂ V)
28     (hA : ∀ k, Related q j k → ∀ v, v ∈ packet ρ k → A v ∈ orbitSpan ρ q j)
29     {v : V} (hv : v ∈ orbitSpan ρ q j) : A v ∈ orbitSpan ρ q j := by
30   induction hv using Submodule.span_induction with
31   | mem v hv => obtain ⟨k, hk, hvk⟩ := hv; exact hA k hk v hvk
32   | zero => simp
33   | add x y _ _ hx hy => simpa using (orbitSpan ρ q j).add_mem hx hy
34   | smul c x _ hx => simpa using (orbitSpan ρ q j).smul_mem c hx
35 
36 theorem inertia_stable (ρ : Action (K := ℂ) (V := V) (M := M))
37     (q : (ZMod M)ˣ) (j a : ZMod M) {v : V} (hv : v ∈ orbitSpan ρ q j) :
38     operator ρ a v ∈ orbitSpan ρ q j :=
39   map_mem ρ q j (operator ρ a)
40     (fun k hk _ hvk => packet_le ρ q hk (inertia_mem ρ a k hvk)) hv
41 
42 theorem forward_stable (ρ : Action (K := ℂ) (V := V) (M := M))
43     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
44     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
45     (j : ZMod M) {v : V} (hv : v ∈ orbitSpan ρ q j) : F v ∈ orbitSpan ρ q j :=
46   map_mem ρ q j F.toLinearMap
47     (fun k hk _ hvk => packet_le ρ q (step_mem q hk) (forward_mem ρ F q h k hvk)) hv
48 
49 theorem backward_stable (ρ : 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 ∈ orbitSpan ρ q j) : F.symm v ∈ orbitSpan ρ q j :=
53   map_mem ρ q j F.symm.toLinearMap
54     (fun k hk _ hvk => packet_le ρ q (back_mem q hk) (backward_mem ρ F q h k hvk)) hv
55 
56 theorem outside_projector_zero (ρ : Action (K := ℂ) (V := V) (M := M))
57     (q : (ZMod M)ˣ) {j k : ZMod M} (hk : ¬Related q j k)
58     {v : V} (hv : v ∈ orbitSpan ρ q j) : projector ρ k v = 0 := by
59   have hle : orbitSpan ρ q j ≤ LinearMap.ker (projector ρ k) := by
60     apply Submodule.span_le.mpr
61     rintro w ⟨i, hi, hwi⟩
62     have hki : k ≠ i := by rintro rfl; exact hk hi
63     exact projector_on_other_packet ρ hki hwi
64   exact hle hv
65 
66 theorem span_ne_bot (ρ : Action (K := ℂ) (V := V) (M := M))
67     (q : (ZMod M)ˣ) {j : ZMod M} (hj : packet ρ j ≠ ⊥) : orbitSpan ρ q j ≠ ⊥ := by
68   intro h
69   exact hj (eq_bot_iff.mpr (h ▸ self_packet_le ρ q j))
70 
71 theorem outside_packet_eq_bot (ρ : Action (K := ℂ) (V := V) (M := M))
72     (q : (ZMod M)ˣ) {j k : ZMod M} (hk : ¬Related q j k)
73     (htop : orbitSpan ρ q j = ⊤) : packet ρ k = ⊥ := by
74   apply eq_bot_iff.mpr
75   intro v hv
76   have hz := outside_projector_zero ρ q hk (v := v) (by simp [htop])
77   rw [(mem_iff_projector ρ k v).mp hv] at hz
78   simpa using hz
79 
80 theorem related_of_span_top (ρ : Action (K := ℂ) (V := V) (M := M))
81     (q : (ZMod M)ˣ) {j k : ZMod M} (htop : orbitSpan ρ q j = ⊤)
82     (hk : packet ρ k ≠ ⊥) : Related q j k := by
83   by_contra hn
84   exact hk (outside_packet_eq_bot ρ q hn htop)
85 
86 end PaperXI.OrbitSpan

Back to source controls