PacketSupport.lean

1 import PaperXI.TameOrbitTransitivity
2 
3 /-! Exact support, and constant packet dimension along the Frobenius orbit. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.PacketSupport
7 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusOrbit
8 open PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
9 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
10 variable {M : ℕ} [NeZero M]
11 
12 theorem nonzero_step_iff (ρ : Action (K := ℂ) (V := V) (M := M))
13     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
14     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
15     packet ρ j ≠ ⊥ ↔ packet ρ ((q : ZMod M) * j) ≠ ⊥ := by
16   rw [← Submodule.nontrivial_iff_ne_bot, ← Submodule.nontrivial_iff_ne_bot]
17   exact (packetEquiv ρ F q h j).toEquiv.nontrivial_congr
18 
19 theorem nonzero_back_iff (ρ : Action (K := ℂ) (V := V) (M := M))
20     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
21     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
22     packet ρ j ≠ ⊥ ↔ packet ρ (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) ≠ ⊥ := by
23   simpa only [← mul_assoc, Units.mul_inv, one_mul] using
24     (nonzero_step_iff ρ F q h (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j)).symm
25 
26 theorem nonzero_zpow_iff (ρ : Action (K := ℂ) (V := V) (M := M))
27     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
28     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) (n : ℤ) :
29     packet ρ j ≠ ⊥ ↔ packet ρ (((q ^ n : (ZMod M)ˣ) : ZMod M) * j) ≠ ⊥ := by
30   induction n using Int.induction_on with
31   | zero => simp
32   | succ n ih =>
33     simpa [zpow_add_one, mul_assoc, mul_left_comm] using
34       ih.trans (nonzero_step_iff ρ F q h (((q ^ (n : ℤ) : (ZMod M)ˣ) : ZMod M) * j))
35   | pred n ih =>
36     simpa [zpow_sub_one, mul_assoc, mul_left_comm] using
37       ih.trans (nonzero_back_iff ρ F q h (((q ^ (-(n : ℤ)) : (ZMod M)ˣ) : ZMod M) * j))
38 
39 theorem finrank_zpow (ρ : Action (K := ℂ) (V := V) (M := M))
40     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
41     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) (n : ℤ) :
42     Module.finrank ℂ (packet ρ j) =
43       Module.finrank ℂ (packet ρ (((q ^ n : (ZMod M)ˣ) : ZMod M) * j)) := by
44   induction n using Int.induction_on with
45   | zero => rw [zpow_zero, Units.val_one, one_mul]
46   | succ n ih =>
47     have hi : ((q ^ ((n : ℤ) + 1) : (ZMod M)ˣ) : ZMod M) * j =
48         (q : ZMod M) * (((q ^ (n : ℤ) : (ZMod M)ˣ) : ZMod M) * j) := by
49       simp [zpow_add_one, mul_assoc, mul_left_comm]
50     rw [hi]
51     exact ih.trans (packet_finrank_step ρ F q h _)
52   | pred n ih =>
53     have hb (k : ZMod M) : Module.finrank ℂ (packet ρ k) =
54         Module.finrank ℂ (packet ρ (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * k)) := by
55       have hi : (q : ZMod M) * (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * k) = k := by
56         simp [← mul_assoc]
57       have hs := packet_finrank_step ρ F q h (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * k)
58       rw [hi] at hs
59       exact hs.symm
60     have hi : ((q ^ (-(n : ℤ) - 1) : (ZMod M)ˣ) : ZMod M) * j =
61         ((q⁻¹ : (ZMod M)ˣ) : ZMod M) * (((q ^ (-(n : ℤ)) : (ZMod M)ˣ) : ZMod M) * j) := by
62       simp [zpow_sub_one, mul_assoc, mul_left_comm]
63     rw [hi]
64     exact ih.trans (hb _)
65 
66 variable {G : Type*} [Group G]
67 
68 theorem support_iff_orbit (π : 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 ≠ ⊥) (k : ZMod M) :
74     packet (tameRestriction π ι) k ≠ ⊥ ↔ Related q j k := by
75   constructor
76   · exact nonzero_packets_one_orbit π ι φ q hgen hrel hj
77   · rintro ⟨n, rfl⟩
78     exact (nonzero_zpow_iff (tameRestriction π ι) (actionEquiv π φ) q
79       (geometric_relation π ι φ q hrel) j n).mp hj
80 
81 /-- Nonempty support is exactly one full orbit, including the converse direction. -/
82 theorem support_is_one_orbit (π : Representation ℂ G V) [Representation.IsIrreducible π]
83     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
84     (hgen : Submonoid.closure (generators ι φ) = ⊤)
85     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
86       ι (Multiplicative.ofAdd (q : ZMod M))) :
87     ∃ j : ZMod M, packet (tameRestriction π ι) j ≠ ⊥ ∧
88       ∀ k, packet (tameRestriction π ι) k ≠ ⊥ ↔ Related q j k := by
89   obtain ⟨j, hj⟩ := exists_nonzero_packet π ι
90   exact ⟨j, hj, support_iff_orbit π ι φ q hgen hrel hj⟩
91 
92 theorem equal_packet_dimensions (π : Representation ℂ G V) [Representation.IsIrreducible π]
93     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
94     (hgen : Submonoid.closure (generators ι φ) = ⊤)
95     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
96       ι (Multiplicative.ofAdd (q : ZMod M)))
97     {j k : ZMod M} (hj : packet (tameRestriction π ι) j ≠ ⊥)
98     (hk : packet (tameRestriction π ι) k ≠ ⊥) :
99     Module.finrank ℂ (packet (tameRestriction π ι) j) =
100       Module.finrank ℂ (packet (tameRestriction π ι) k) := by
101   obtain ⟨n, rfl⟩ := nonzero_packets_one_orbit π ι φ q hgen hrel hj hk
102   exact finrank_zpow (tameRestriction π ι) (actionEquiv π φ) q
103     (geometric_relation π ι φ q hrel) j n
104 
105 end PaperXI.PacketSupport

Back to source controls