CycleSpan.lean

1 import PaperXI.PacketReturn
2 
3 /-! The span of a finite Frobenius cycle with a nonzero closing scalar. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CycleSpan
7 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
8 variable {f : ℕ}
9 
10 def cycleVector (F : V ≃ₗ[K] V) (v : V) (a : Fin f) : V := (F ^ (a : ℕ)) v
11 
12 def cycleSpan (F : V ≃ₗ[K] V) (v : V) (f : ℕ) : Submodule K V :=
13   Submodule.span K (Set.range (cycleVector (f := f) F v))
14 
15 theorem power_mem (F : V ≃ₗ[K] V) (v : V) {n : ℕ} (hn : n < f) :
16     (F ^ n) v ∈ cycleSpan F v f := Submodule.subset_span ⟨⟨n, hn⟩, rfl⟩
17 
18 theorem base_mem (F : V ≃ₗ[K] V) (v : V) (hf : 0 < f) : v ∈ cycleSpan F v f := by
19   simpa using power_mem F v hf
20 
21 theorem map_mem (F : V ≃ₗ[K] V) (v : V) (f : ℕ) (A : Module.End K V)
22     (hA : ∀ a : Fin f, A (cycleVector F v a) ∈ cycleSpan F v f)
23     {w : V} (hw : w ∈ cycleSpan F v f) : A w ∈ cycleSpan F v f := by
24   induction hw using Submodule.span_induction with
25   | mem w hw => obtain ⟨a, rfl⟩ := hw; exact hA a
26   | zero => simp
27   | add x y _ _ hx hy => simpa using (cycleSpan F v f).add_mem hx hy
28   | smul c x _ hx => simpa using (cycleSpan F v f).smul_mem c hx
29 
30 theorem forward_power (F : V ≃ₗ[K] V) (v : V) (n : ℕ) :
31     F ((F ^ n) v) = (F ^ (n + 1)) v := by simp [pow_succ']
32 
33 theorem backward_power (F : V ≃ₗ[K] V) (v : V) (n : ℕ) :
34     F.symm ((F ^ (n + 1)) v) = (F ^ n) v := by simp [pow_succ']
35 
36 /-- The inverse wrap uses the inverse of the actual closing scalar. -/
37 theorem inverse_wrap (F : V ≃ₗ[K] V) (v : V) (hf : 0 < f) {c : K} (hc : c ≠ 0)
38     (hclose : (F ^ f) v = c • v) : F.symm v = c⁻¹ • (F ^ (f - 1)) v := by
39   apply F.injective
40   rw [F.apply_symm_apply, map_smul, forward_power, Nat.sub_add_cancel (by omega), hclose,
41     smul_smul, inv_mul_cancel₀ hc, one_smul]
42 
43 theorem forward_stable (F : V ≃ₗ[K] V) (v : V) (hf : 0 < f) {c : K}
44     (hclose : (F ^ f) v = c • v) {w : V} (hw : w ∈ cycleSpan F v f) :
45     F w ∈ cycleSpan F v f := by
46   apply map_mem F v f F.toLinearMap (fun a => ?_) hw
47   change F ((F ^ (a : ℕ)) v) ∈ _
48   rw [forward_power]
49   by_cases ha : (a : ℕ) + 1 < f
50   · exact power_mem F v ha
51   · have heq : (a : ℕ) + 1 = f := by have := a.isLt; omega
52     rw [heq, hclose]
53     exact (cycleSpan F v f).smul_mem c (base_mem F v hf)
54 
55 theorem backward_stable (F : V ≃ₗ[K] V) (v : V) (hf : 0 < f) {c : K} (hc : c ≠ 0)
56     (hclose : (F ^ f) v = c • v) {w : V} (hw : w ∈ cycleSpan F v f) :
57     F.symm w ∈ cycleSpan F v f := by
58   apply map_mem F v f F.symm.toLinearMap (fun a => ?_) hw
59   change F.symm ((F ^ (a : ℕ)) v) ∈ _
60   by_cases ha : (a : ℕ) = 0
61   · rw [ha, pow_zero]
62     change F.symm v ∈ _
63     rw [inverse_wrap F v hf hc hclose]
64     exact (cycleSpan F v f).smul_mem _ (power_mem F v (by omega))
65   · have heq : (a : ℕ) = ((a : ℕ) - 1) + 1 := by omega
66     rw [heq, backward_power]
67     exact power_mem F v (by have := a.isLt; omega)
68 
69 theorem span_ne_bot (F : V ≃ₗ[K] V) {v : V} (hv : v ≠ 0) (hf : 0 < f) :
70     cycleSpan F v f ≠ ⊥ := by
71   intro h
72   have hm := base_mem F v hf
73   rw [h] at hm
74   exact hv (by simpa using hm)
75 
76 end PaperXI.CycleSpan

Back to source controls