PacketBasis.lean

1 import PaperXI.PacketLines
2 import Mathlib.LinearAlgebra.Basis.Basic
3 
4 /-! The finite Frobenius orbit is a proved basis, giving the exact ambient
5 dimension and the action of inertia and Frobenius on the basis vectors. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.PacketBasis
9 open scoped BigOperators
10 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusPeriod
11 open PaperXI.CycleSpan PaperXI.PacketLines
12 open PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
13 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
14 variable {M : ℕ} [NeZero M]
15 
16 theorem cycleVector_ne_zero (F : V ≃ₗ[ℂ] V) {v : V} (hv : v ≠ 0)
17     {f : ℕ} (a : Fin f) : cycleVector F v a ≠ 0 := by
18   intro h
19   exact hv ((F ^ (a : ℕ)).injective (h.trans (map_zero _).symm))
20 
21 /-- Distinct packet projectors extract coefficients from any linear relation. -/
22 theorem cycle_linearIndependent (ρ : 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) (hv0 : v ≠ 0) :
26     LinearIndependent ℂ (cycleVector (f := period q j) F v) := by
27   classical
28   apply Fintype.linearIndependent_iff.mpr
29   intro c hc a
30   have hp := congrArg (projector ρ (orbitLabel q j a)) hc
31   simp only [map_sum, map_smul, map_zero] at hp
32   simp_rw [projector_cycle ρ F q h j hv] at hp
33   have hs : c a • cycleVector F v a = 0 := by simpa using hp
34   exact (smul_eq_zero.mp hs).resolve_right (cycleVector_ne_zero F hv0 a)
35 
36 variable {G : Type*} [Group G]
37 
38 /-- An explicit basis whose a-th vector is F^a v. -/
39 def orbitBasis (π : Representation ℂ G V) [Representation.IsIrreducible π]
40     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
41     (hgen : Submonoid.closure (generators ι φ) = ⊤)
42     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
43       ι (Multiplicative.ofAdd (q : ZMod M)))
44     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
45     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
46     Module.Basis (Fin (period q j)) ℂ V :=
47   Module.Basis.mk
48     (cycle_linearIndependent (tameRestriction π ι) (actionEquiv π φ) q
49       (geometric_relation π ι φ q hrel) j hv hv0)
50     (cycleSpan_eq_top π ι φ q hgen hrel j hv hv0 hc hclose).ge
51 
52 theorem orbitBasis_apply (π : Representation ℂ G V) [Representation.IsIrreducible π]
53     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
54     (hgen : Submonoid.closure (generators ι φ) = ⊤)
55     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
56       ι (Multiplicative.ofAdd (q : ZMod M)))
57     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
58     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v)
59     (a : Fin (period q j)) :
60     orbitBasis π ι φ q hgen hrel j hv hv0 hc hclose a = (actionEquiv π φ ^ (a : ℕ)) v :=
61   Module.Basis.mk_apply _ _ a
62 
63 theorem finrank_eq_period_of_return (π : Representation ℂ G V) [Representation.IsIrreducible π]
64     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
65     (hgen : Submonoid.closure (generators ι φ) = ⊤)
66     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
67       ι (Multiplicative.ofAdd (q : ZMod M)))
68     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
69     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
70     Module.finrank ℂ V = period q j := by
71   simpa using Module.finrank_eq_card_basis (orbitBasis π ι φ q hgen hrel j hv hv0 hc hclose)
72 
73 /-- The algebraic dimension formula in Corollary 3.3. -/
74 theorem finrank_eq_period [FiniteDimensional ℂ V]
75     (π : Representation ℂ G V) [Representation.IsIrreducible π]
76     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
77     (hgen : Submonoid.closure (generators ι φ) = ⊤)
78     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
79       ι (Multiplicative.ofAdd (q : ZMod M)))
80     {j : ZMod M} (hj : packet (tameRestriction π ι) j ≠ ⊥) :
81     Module.finrank ℂ V = period q j := by
82   obtain ⟨c, v, hc, hv, hv0, hclose⟩ := PaperXI.PacketReturn.exists_closing_eigenvector
83     (tameRestriction π ι) (actionEquiv π φ) q (geometric_relation π ι φ q hrel) hj
84   exact finrank_eq_period_of_return π ι φ q hgen hrel j hv hv0 hc hclose
85 
86 theorem finrank_eq_orbit_card [FiniteDimensional ℂ V]
87     (π : Representation ℂ G V) [Representation.IsIrreducible π]
88     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
89     (hgen : Submonoid.closure (generators ι φ) = ⊤)
90     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
91       ι (Multiplicative.ofAdd (q : ZMod M)))
92     {j : ZMod M} (hj : packet (tameRestriction π ι) j ≠ ⊥) :
93     Module.finrank ℂ V = Nat.card {k : ZMod M // PaperXI.FrobeniusOrbit.Related q j k} := by
94   rw [orbit_card]
95   exact finrank_eq_period π ι φ q hgen hrel hj
96 
97 end PaperXI.PacketBasis

Back to source controls