CycleFixed.lean

1 import PaperXI.CycleCoordinates
2 import Mathlib.LinearAlgebra.Eigenspace.Basic
3 
4 /-! Fixed vectors of an actual cyclic basis, valid in every characteristic. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CycleFixed
8 open scoped BigOperators Classical
9 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
10 
11 def fixedSpace (F : Module.End K V) : Submodule K V := LinearMap.ker (F - LinearMap.id)
12 
13 @[simp] theorem mem_fixedSpace (F : Module.End K V) (x : V) :
14     x ∈ fixedSpace F ↔ F x = x := by simp [fixedSpace, sub_eq_zero]
15 
16 theorem coordinate_step (F : Module.End K V) {n : ℕ} (hn : 0 < n)
17     (b : Module.Basis (Fin n) K V)
18     (hstep : ∀ (k : Fin n) (hk : (k : ℕ) + 1 < n), F (b k) = b ⟨k + 1, hk⟩)
19     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩)
20     (i : Fin n) (hi : (i : ℕ) + 1 < n) (x : V) :
21     b.repr (F x) ⟨i + 1, hi⟩ = b.repr x i := by
22   have he : (b.coord ⟨i + 1, hi⟩).comp F = b.coord i := by
23     apply b.ext
24     intro k
25     by_cases hk : (k : ℕ) + 1 < n
26     · simp only [LinearMap.comp_apply, hstep k hk, Module.Basis.coord_apply,
27         Module.Basis.repr_self, Finsupp.single_apply]
28       have heq : (⟨(k : ℕ) + 1, hk⟩ : Fin n) = ⟨i + 1, hi⟩ ↔ k = i := by
29         simp only [Fin.ext_iff]
30         omega
31       simp only [heq]
32     · have hkl : k = ⟨n - 1, by omega⟩ := by
33         apply Fin.ext
34         change (k : ℕ) = n - 1
35         omega
36       have hki : k ≠ i := by intro he; have := congrArg Fin.val he; omega
37       simp only [LinearMap.comp_apply]
38       rw [show F (b k) = c • b ⟨0, hn⟩ by rw [hkl, hlast]]
39       simp [Module.Basis.coord_apply, Module.Basis.repr_self, hki]
40   exact LinearMap.congr_fun he x
41 
42 theorem fixed_coordinates_constant (F : Module.End K V) {n : ℕ} (hn : 0 < n)
43     (b : Module.Basis (Fin n) K V)
44     (hstep : ∀ (k : Fin n) (hk : (k : ℕ) + 1 < n), F (b k) = b ⟨k + 1, hk⟩)
45     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩)
46     {x : V} (hx : F x = x) : ∀ i : Fin n, b.repr x i = b.repr x ⟨0, hn⟩ := by
47   have aux : ∀ k (hk : k < n), b.repr x ⟨k, hk⟩ = b.repr x ⟨0, hn⟩ := by
48     intro k
49     induction k with
50     | zero => intro hk; rfl
51     | succ k ih =>
52       intro hk
53       have h := coordinate_step F hn b hstep c hlast ⟨k, by omega⟩ hk x
54       rw [hx] at h
55       exact h.trans (ih (by omega))
56   intro i
57   exact aux i i.isLt
58 
59 theorem basis_sum_ne_zero {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) K V) :
60     (∑ i, b i) ≠ 0 := by
61   intro h
62   have he := congrArg (fun x => b.repr x ⟨0, hn⟩) h
63   simp at he
64 
65 theorem fixed_eq_smul_sum (F : Module.End K V) {n : ℕ} (hn : 0 < n)
66     (b : Module.Basis (Fin n) K V)
67     (hstep : ∀ (k : Fin n) (hk : (k : ℕ) + 1 < n), F (b k) = b ⟨k + 1, hk⟩)
68     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩)
69     {x : V} (hx : F x = x) : x = (b.repr x ⟨0, hn⟩) • ∑ i, b i := by
70   apply b.repr.injective
71   ext i
72   simpa using fixed_coordinates_constant F hn b hstep c hlast hx i
73 
74 
75 theorem map_basis_sum (F : Module.End K V) {n : ℕ} (hn : 0 < n)
76     (b : Module.Basis (Fin n) K V)
77     (hstep : ∀ (k : Fin n) (hk : (k : ℕ) + 1 < n), F (b k) = b ⟨k + 1, hk⟩)
78     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩) :
79     F (∑ i, b i) = (∑ i, b i) + (c - 1) • b ⟨0, hn⟩ := by
80   cases n with
81   | zero => omega
82   | succ n =>
83     rw [map_sum, Fin.sum_univ_castSucc, Fin.sum_univ_succ]
84     have hs (i : Fin n) : F (b i.castSucc) = b i.succ := hstep i.castSucc (Nat.succ_lt_succ i.isLt)
85     simp_rw [hs]
86     have hl : F (b (Fin.last n)) = c • b 0 := hlast
87     rw [hl, show (⟨0, hn⟩ : Fin (n + 1)) = 0 from rfl, sub_smul, one_smul]
88     abel
89 
90 theorem fixedSpace_eq (F : Module.End K V) {n : ℕ} (hn : 0 < n)
91     (b : Module.Basis (Fin n) K V)
92     (hstep : ∀ (k : Fin n) (hk : (k : ℕ) + 1 < n), F (b k) = b ⟨k + 1, hk⟩)
93     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩) :
94     fixedSpace F = if c = 1 then Submodule.span K {∑ i, b i} else ⊥ := by
95   classical
96   have hm := map_basis_sum F hn b hstep c hlast
97   by_cases hc : c = 1
98   · rw [ite_eq_left hc]
99     apply le_antisymm
100     · intro x hx
101       rw [fixed_eq_smul_sum F hn b hstep c hlast ((mem_fixedSpace F x).mp hx)]
102       exact Submodule.smul_mem _ _ (Submodule.subset_span (Set.mem_singleton _))
103     · apply Submodule.span_le.mpr
104       intro x hx
105       have he : x = ∑ i, b i := hx
106       subst x
107       apply (mem_fixedSpace F _).mpr
108       simpa [hc] using hm
109   · rw [ite_eq_right hc]
110     apply le_antisymm _ bot_le
111     intro x hx
112     have hx' := (mem_fixedSpace F x).mp hx
113     have he := fixed_eq_smul_sum F hn b hstep c hlast hx'
114     have hz : (b.repr x ⟨0, hn⟩ * (c - 1)) • b ⟨0, hn⟩ = 0 := by
115       have h := hx'
116       conv_lhs at h => rw [he, map_smul, hm, smul_add, ← he]
117       have hh := add_left_cancel (h.trans (add_zero x).symm)
118       simpa only [smul_smul] using hh
119     have hz' : b.repr x ⟨0, hn⟩ = 0 := by
120       rcases (smul_eq_zero.mp hz) with hs | hb
121       · exact (mul_eq_zero.mp hs).resolve_right (sub_ne_zero.mpr hc)
122       · exact False.elim (b.ne_zero _ hb)
123     change x = 0
124     rw [he, hz', zero_smul]
125 
126 theorem fixedSpace_finrank (F : Module.End K V) {n : ℕ} (hn : 0 < n)
127     (b : Module.Basis (Fin n) K V)
128     (hstep : ∀ (k : Fin n) (hk : (k : ℕ) + 1 < n), F (b k) = b ⟨k + 1, hk⟩)
129     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩) :
130     Module.finrank K (fixedSpace F) = if c = 1 then 1 else 0 := by
131   classical
132   by_cases hc : c = 1
133   · rw [fixedSpace_eq F hn b hstep c hlast, ite_eq_left hc, ite_eq_left hc]
134     exact finrank_span_singleton (K := K) (basis_sum_ne_zero hn b)
135   · rw [fixedSpace_eq F hn b hstep c hlast, ite_eq_right hc, ite_eq_right hc]
136     exact finrank_bot K V
137 
138 end PaperXI.CycleFixed

Back to source controls