PacketCycle.lean

1 import PaperXI.CycleCoordinates
2 import PaperXI.PacketBasis
3 
4 /-! Cycle invariants of the actual irreducible tame algebraic group action. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.PacketCycle
8 open Polynomial
9 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusPeriod
10 open PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
11 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
12 
13 theorem linear_power (F : V ≃ₗ[ℂ] V) (n : ℕ) (v : V) :
14     (F.toLinearMap ^ n) v = (F ^ n) v := by
15   induction n with
16   | zero => rfl
17   | succ n ih =>
18     rw [pow_succ', pow_succ']
19     change F ((F.toLinearMap ^ n) v) = F ((F ^ n) v)
20     rw [ih]
21 
22 variable {G : Type*} [Group G] {M : ℕ} [NeZero M]
23 variable (π : Representation ℂ G V) [Representation.IsIrreducible π]
24 variable (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
25 variable (hgen : Submonoid.closure (generators ι φ) = ⊤)
26 variable (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
27   ι (Multiplicative.ofAdd (q : ZMod M)))
28 
29 include hgen hrel
30 
31 /-- The characteristic polynomial of the actual Frobenius action. -/
32 theorem charpoly [FiniteDimensional ℂ V] (j : ZMod M) {v : V}
33     (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
34     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
35     (actionEquiv π φ).toLinearMap.charpoly = X ^ period q j - C c := by
36   let b := PaperXI.PacketBasis.orbitBasis π ι φ q hgen hrel j hv hv0 hc hclose
37   apply PaperXI.CyclicPolynomial.charpoly_of_orbit_basis _ (period_pos q j) b v
38   · intro a
39     rw [linear_power]
40     exact PaperXI.PacketBasis.orbitBasis_apply π ι φ q hgen hrel j hv hv0 hc hclose a
41   · simpa only [linear_power] using hclose
42 
43 theorem det [FiniteDimensional ℂ V] (j : ZMod M) {v : V}
44     (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
45     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
46     (actionEquiv π φ).toLinearMap.det = (-1) ^ (period q j - 1) * c := by
47   let b := PaperXI.PacketBasis.orbitBasis π ι φ q hgen hrel j hv hv0 hc hclose
48   apply PaperXI.CyclicPolynomial.det_of_orbit_basis _ (period_pos q j) b v
49   · intro a
50     rw [linear_power]
51     exact PaperXI.PacketBasis.orbitBasis_apply π ι φ q hgen hrel j hv hv0 hc hclose a
52   · simpa only [linear_power] using hclose
53 
54 theorem ambient_polynomial [FiniteDimensional ℂ V] (j : ZMod M) {v : V}
55     (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
56     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
57     (LinearMap.toMatrix
58       (PaperXI.PacketBasis.orbitBasis π ι φ q hgen hrel j hv hv0 hc hclose)
59       (PaperXI.PacketBasis.orbitBasis π ι φ q hgen hrel j hv hv0 hc hclose)
60       (actionEquiv π φ).toLinearMap).charpolyRev = 1 - C c * X ^ period q j := by
61   rw [← Matrix.reverse_charpoly, LinearMap.charpoly_toMatrix,
62     charpoly π ι φ q hgen hrel j hv hv0 hc hclose,
63     PaperXI.CyclicPolynomial.reverse_cycle_polynomial]
64 
65 /-- Every nonzero packet supplies a nonzero closing scalar with these invariants. -/
66 theorem exists_cycle_invariants [FiniteDimensional ℂ V] {j : ZMod M}
67     (hj : packet (tameRestriction π ι) j ≠ ⊥) :
68     ∃ c : ℂ, c ≠ 0 ∧
69       (actionEquiv π φ).toLinearMap.charpoly = X ^ period q j - C c ∧
70       (actionEquiv π φ).toLinearMap.det = (-1) ^ (period q j - 1) * c := by
71   obtain ⟨c, v, hc, hv, hv0, hclose⟩ := PaperXI.PacketReturn.exists_closing_eigenvector
72     (tameRestriction π ι) (actionEquiv π φ) q (geometric_relation π ι φ q hrel) hj
73   exact ⟨c, hc, charpoly π ι φ q hgen hrel j hv hv0 hc hclose,
74     det π ι φ q hgen hrel j hv hv0 hc hclose⟩
75 
76 end PaperXI.PacketCycle

Back to source controls