PacketReturn.lean

1 import PaperXI.FrobeniusPeriod
2 import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
3 
4 /-! The actual return operator on a packet and its nonzero eigenline. The
5 claim that this line is the whole packet is deliberately not assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.PacketReturn
9 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusPeriod
10 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
11 variable {M : ℕ} [NeZero M]
12 
13 theorem power_mem (ρ : Action (K := ℂ) (V := V) (M := M))
14     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
15     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
16     (j : ZMod M) (n : ℕ) {v : V} (hv : v ∈ packet ρ j) :
17     (F ^ n) v ∈ packet ρ (((q ^ n : (ZMod M)ˣ) : ZMod M) * j) := by
18   induction n with
19   | zero => simpa using hv
20   | succ n ih =>
21     simpa [pow_succ', mul_assoc] using forward_mem ρ F q h _ ih
22 
23 theorem return_mem (ρ : Action (K := ℂ) (V := V) (M := M))
24     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
25     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
26     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) :
27     (F ^ period q j) v ∈ packet ρ j := by
28   simpa only [return_label] using power_mem ρ F q h j (period q j) hv
29 
30 def closingOperator (ρ : Action (K := ℂ) (V := V) (M := M))
31     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
32     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
33     Module.End ℂ (packet ρ j) where
34   toFun v := ⟨(F ^ period q j) v, return_mem ρ F q h j v.property⟩
35   map_add' v w := by ext; simp
36   map_smul' c v := by ext; simp
37 
38 /-- Every nonzero finite-dimensional packet contains a return eigenvector,
39 with nonzero closing scalar because Frobenius is invertible. -/
40 theorem exists_closing_eigenvector [FiniteDimensional ℂ V]
41     (ρ : Action (K := ℂ) (V := V) (M := M)) (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
42     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
43     {j : ZMod M} (hj : packet ρ j ≠ ⊥) :
44     ∃ (c : ℂ) (v : V), c ≠ 0 ∧ v ∈ packet ρ j ∧ v ≠ 0 ∧
45       (F ^ period q j) v = c • v := by
46   have : Nontrivial (packet ρ j) := Submodule.nontrivial_iff_ne_bot.mpr hj
47   obtain ⟨c, hc⟩ := (closingOperator ρ F q h j).exists_eigenvalue
48   obtain ⟨w, hw⟩ := hc.exists_hasEigenvector
49   have hne : (w : V) ≠ 0 := by
50     intro hz
51     apply hw.2
52     exact Subtype.ext hz
53   have heq : (F ^ period q j) (w : V) = c • (w : V) :=
54     congrArg Subtype.val hw.apply_eq_smul
55   have hc0 : c ≠ 0 := by
56     intro hz
57     rw [hz, zero_smul] at heq
58     exact hne ((F ^ period q j).injective (heq.trans (map_zero _).symm))
59   exact ⟨c, w, hc0, w.property, hne, heq⟩
60 
61 end PaperXI.PacketReturn

Back to source controls