CycleCoordinates.lean

1 import PaperXI.CyclicPolynomial
2 import Mathlib.LinearAlgebra.Basis.SMul
3 import Mathlib.GroupTheory.Perm.Fin
4 
5 /-! Transfer formulas in an actual basis, including independent rescalings. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CycleCoordinates
9 open Polynomial
10 open PaperXI.CyclicPolynomial
11 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
12 
13 theorem basis_eq_powers (F : Module.End K V) {n : ℕ} (hn : 0 < n)
14     (b : Module.Basis (Fin n) K V)
15     (hstep : ∀ (i : Fin n) (hi : (i : ℕ) + 1 < n), F (b i) = b ⟨i + 1, hi⟩) :
16     ∀ i : Fin n, b i = (F ^ (i : ℕ)) (b ⟨0, hn⟩) := by
17   have aux : ∀ k (hk : k < n), b ⟨k, hk⟩ = (F ^ k) (b ⟨0, hn⟩) := by
18     intro k
19     induction k with
20     | zero => intro hk; simp
21     | succ k ih =>
22       intro hk
23       rw [← hstep ⟨k, by omega⟩ hk, ih (by omega), pow_succ']
24       rfl
25   intro i
26   exact aux i i.isLt
27 
28 theorem closing_of_last_step (F : Module.End K V) {n : ℕ} (hn : 0 < n)
29     (b : Module.Basis (Fin n) K V)
30     (hstep : ∀ (i : Fin n) (hi : (i : ℕ) + 1 < n), F (b i) = b ⟨i + 1, hi⟩)
31     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩) :
32     (F ^ n) (b ⟨0, hn⟩) = c • b ⟨0, hn⟩ := by
33   have hb := basis_eq_powers F hn b hstep ⟨n - 1, by omega⟩
34   have he : n = (n - 1) + 1 := by omega
35   calc
36     (F ^ n) (b ⟨0, hn⟩) = F ((F ^ (n - 1)) (b ⟨0, hn⟩)) := by
37       have hp : F ^ n = F * F ^ (n - 1) := by
38         conv_lhs => rw [he, pow_succ']
39       rw [hp]
40       rfl
41     _ = F (b ⟨n - 1, by omega⟩) := congrArg F hb.symm
42     _ = c • b ⟨0, hn⟩ := hlast
43 
44 /-- Proposition 4.4 in its stated cyclic-coordinate form. -/
45 theorem cycle_formula [FiniteDimensional K V] (F : Module.End K V) {n : ℕ}
46     (hn : 0 < n) (b : Module.Basis (Fin n) K V)
47     (hstep : ∀ (i : Fin n) (hi : (i : ℕ) + 1 < n), F (b i) = b ⟨i + 1, hi⟩)
48     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩) :
49     F.charpoly = X ^ n - C c ∧ F.det = (-1) ^ (n - 1) * c := by
50   have hb := basis_eq_powers F hn b hstep
51   have hc := closing_of_last_step F hn b hstep c hlast
52   exact ⟨charpoly_of_orbit_basis F hn b _ hb c hc,
53     det_of_orbit_basis F hn b _ hb c hc⟩
54 
55 theorem rescaled_entry {ι : Type*} [Fintype ι] [DecidableEq ι]
56     (F : Module.End K V) (b : Module.Basis ι K V) (w : ι → Kˣ) (i j : ι) :
57     LinearMap.toMatrix (b.unitsSMul w) (b.unitsSMul w) F i j =
58       (w i : K)⁻¹ * LinearMap.toMatrix b b F i j * (w j : K) := by
59   simp [LinearMap.toMatrix_apply, Module.Basis.unitsSMul_apply,
60     Module.Basis.repr_unitsSMul, Units.smul_def, mul_comm]
61 
62 theorem rescaled_charpoly [FiniteDimensional K V]
63     {ι : Type*} [Fintype ι] [DecidableEq ι]
64     (F : Module.End K V) (b : Module.Basis ι K V) (w : ι → Kˣ) :
65     (LinearMap.toMatrix (b.unitsSMul w) (b.unitsSMul w) F).charpoly =
66       (LinearMap.toMatrix b b F).charpoly := by simp
67 
68 theorem rescaled_det {ι : Type*} [Fintype ι] [DecidableEq ι]
69     (F : Module.End K V) (b : Module.Basis ι K V) (w : ι → Kˣ) :
70     (LinearMap.toMatrix (b.unitsSMul w) (b.unitsSMul w) F).det =
71       (LinearMap.toMatrix b b F).det := by
72   rw [LinearMap.det_toMatrix, LinearMap.det_toMatrix]
73 
74 theorem cycle_orientation (n : ℕ) : Equiv.Perm.sign (finRotate n) = (-1) ^ (n - 1) :=
75   sign_finRotate n
76 
77 theorem cycle_local_polynomial [FiniteDimensional K V] (F : Module.End K V) {n : ℕ}
78     (hn : 0 < n) (b : Module.Basis (Fin n) K V)
79     (hstep : ∀ (i : Fin n) (hi : (i : ℕ) + 1 < n), F (b i) = b ⟨i + 1, hi⟩)
80     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩) :
81     Matrix.det (1 - (X : K[X]) • (LinearMap.toMatrix b b F).map C) =
82       1 - C c * X ^ n := by
83   change (LinearMap.toMatrix b b F).charpolyRev = _
84   exact local_polynomial_of_orbit_basis F hn b _ (basis_eq_powers F hn b hstep) c
85     (closing_of_last_step F hn b hstep c hlast)
86 
87 theorem rescaled_cycle_formula [FiniteDimensional K V] (F : Module.End K V) {n : ℕ}
88     (hn : 0 < n) (b : Module.Basis (Fin n) K V)
89     (hstep : ∀ (i : Fin n) (hi : (i : ℕ) + 1 < n), F (b i) = b ⟨i + 1, hi⟩)
90     (c : K) (hlast : F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩)
91     (w : Fin n → Kˣ) :
92     (LinearMap.toMatrix (b.unitsSMul w) (b.unitsSMul w) F).charpoly = X ^ n - C c ∧
93     (LinearMap.toMatrix (b.unitsSMul w) (b.unitsSMul w) F).det = (-1) ^ (n - 1) * c := by
94   rw [LinearMap.charpoly_toMatrix, LinearMap.det_toMatrix]
95   exact cycle_formula F hn b hstep c hlast
96 
97 end PaperXI.CycleCoordinates

Back to source controls