SpecialMonodromy.lean

1 import PaperX.MonodromyKernels
2 import Mathlib.Tactic.Ring
3 
4 /-! Exact version of Komorebi's special monodromy chain.
5 Coordinates are 0,...,n-1; N e_j=e_(j-1), and F e_j=a q^(-j)e_j.
6 The length-zero case is included as a zero-dimensional space. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.SpecialMonodromy
10 open scoped BigOperators Matrix
11 open Polynomial
12 open PaperX.MonodromyData
13 
14 variable {K : Type*} [Field K]
15 
16 def shift (n : ℕ) : Module.End K (Fin n → K) where
17   toFun x i := if h : i.val + 1 < n then x ⟨i.val + 1, h⟩ else 0
18   map_add' := by intro x y; funext i; dsimp; split <;> simp
19   map_smul' := by intro a x; funext i; dsimp; split <;> simp
20 
21 @[simp] theorem shift_apply (n : ℕ) (x : Fin n → K) (i : Fin n) :
22     shift n x i = if h : i.val + 1 < n then x ⟨i.val + 1, h⟩ else 0 := rfl
23 
24 theorem shift_pow_apply (n k : ℕ) (x : Fin n → K) (i : Fin n) :
25     (shift n ^ k) x i = if h : i.val + k < n then x ⟨i.val + k, h⟩ else 0 := by
26   induction k generalizing x i with
27   | zero => simp [i.isLt]
28   | succ k ih =>
29       rw [pow_succ', Module.End.mul_apply, shift_apply]
30       by_cases h : i.val + 1 < n
31       · rw [dite_eq_left h, ih]
32         by_cases h' : i.val + (k + 1) < n
33         · have hh : (i.val + 1) + k < n := by omega
34           rw [dite_eq_left hh, dite_eq_left h']
35           congr 1
36           apply Fin.ext
37           dsimp
38           omega
39         · have hh : ¬ (i.val + 1) + k < n := by omega
40           rw [dite_eq_right hh, dite_eq_right h']
41       · have h' : ¬ i.val + (k + 1) < n := by omega
42         rw [dite_eq_right h, dite_eq_right h']
43 
44 theorem shift_nilpotent (n : ℕ) : shift (K := K) n ^ n = 0 := by
45   apply LinearMap.ext
46   intro x
47   funext i
48   rw [shift_pow_apply, dite_eq_right (by omega)]
49   rfl
50 
51 theorem shift_previous_power_nonzero (n : ℕ) (hn : 0 < n) :
52     shift (K := K) n ^ (n - 1) ≠ 0 := by
53   intro h
54   have hh := congrFun (LinearMap.congr_fun h (fun _ => (1 : K))) (⟨0, hn⟩ : Fin n)
55   simp [shift_pow_apply, Nat.ne_of_gt hn] at hh
56 
57 /-- Diagonal linear automorphism; inverses are actual coordinatewise inverses. -/
58 def diagonalF (q a : Kˣ) (n : ℕ) : (Fin n → K) ≃ₗ[K] (Fin n → K) where
59   toFun x i := ((a * q⁻¹ ^ i.val : Kˣ) : K) * x i
60   invFun x i := (((a * q⁻¹ ^ i.val)⁻¹ : Kˣ) : K) * x i
61   left_inv x := by funext i; simp [← mul_assoc]
62   right_inv x := by funext i; simp [← mul_assoc]
63   map_add' x y := by funext i; exact mul_add _ _ _
64   map_smul' c x := by funext i; simp [mul_left_comm]
65 
66 @[simp] theorem diagonalF_apply (q a : Kˣ) (n : ℕ) (x : Fin n → K) (i : Fin n) :
67     diagonalF q a n x i = ((a * q⁻¹ ^ i.val : Kˣ) : K) * x i := rfl
68 
69 theorem chain_relation (q a : Kˣ) (n : ℕ) (x : Fin n → K) :
70     diagonalF q a n (shift n x) = (q : K) • shift n (diagonalF q a n x) := by
71   funext i
72   simp only [diagonalF_apply, shift_apply, Pi.smul_apply, smul_eq_mul]
73   split_ifs with h
74   · simp only [Units.val_mul, Units.val_pow_eq_pow_val, Units.val_inv_eq_inv_val, pow_succ]
75     field_simp
76   · simp
77 
78 def specialDatum (q a : Kˣ) (n : ℕ) : Datum q (Fin n → K) where
79   F := diagonalF q a n
80   N := shift n
81   nilpotent := ⟨n, shift_nilpotent n⟩
82   relation := chain_relation q a n
83 
84 /-- The kernel is precisely the first-coordinate line when n is positive. -/
85 theorem shift_kernel_iff (n : ℕ) (x : Fin n → K) :
86     shift n x = 0 ↔ ∀ j : Fin n, j.val ≠ 0 → x j = 0 := by
87   constructor
88   · intro hx j hj
89     have hi : j.val - 1 < n := by omega
90     have hn : j.val - 1 + 1 < n := by omega
91     have hidx : (⟨j.val - 1 + 1, hn⟩ : Fin n) = j := by apply Fin.ext; dsimp; omega
92     have hh := congrFun hx (⟨j.val - 1, hi⟩ : Fin n)
93     simpa [shift_apply, hn, hidx] using hh
94   · intro hx
95     funext i
96     by_cases h : i.val + 1 < n
97     · simpa [shift_apply, h] using hx (⟨i.val + 1, h⟩ : Fin n) (by dsimp; omega)
98     · simp [shift_apply, h]
99 
100 def kernelLine (n : ℕ) (hn : 0 < n) : LinearMap.ker (shift (K := K) n) ≃ₗ[K] K where
101   toFun x := x.val ⟨0, hn⟩
102   invFun c := ⟨fun j => if j.val = 0 then c else 0, by
103     apply (shift_kernel_iff n _).2
104     intro j hj
105     simp [hj]⟩
106   left_inv x := by
107     apply Subtype.ext
108     funext j
109     by_cases hj : j.val = 0
110     · have hidx : j = (⟨0, hn⟩ : Fin n) := by apply Fin.ext; exact hj
111       simp [hidx]
112     · simp [hj, (shift_kernel_iff n x.val).1 x.property j hj]
113   right_inv c := by simp
114   map_add' x y := rfl
115   map_smul' a x := rfl
116 
117 theorem kernelLine_conjugate (q a : Kˣ) (n : ℕ) (hn : 0 < n) :
118     (kernelLine n hn).conj (kernelF (specialDatum q a n)).toLinearMap =
119       (a : K) • (LinearMap.id : K →ₗ[K] K) := by
120   apply LinearMap.ext
121   intro c
122   change ((a * q⁻¹ ^ 0 : Kˣ) : K) * c = (a : K) * c
123   simp
124 
125 theorem scalar_charpoly (a : K) :
126     (a • (LinearMap.id : K →ₗ[K] K)).charpoly = X - C a := by
127   rw [← LinearMap.charpoly_toMatrix _ (Module.Basis.singleton Unit K)]
128   have h : LinearMap.toMatrix (Module.Basis.singleton Unit K) (Module.Basis.singleton Unit K)
129       (a • (LinearMap.id : K →ₗ[K] K)) = Matrix.diagonal (fun _ : Unit => a) := by
130     ext i j
131     cases i; cases j
132     simp [LinearMap.toMatrix_apply]
133   rw [h, Matrix.charpoly_diagonal]
134   simp
135 
136 theorem special_kernel_charpoly (q a : Kˣ) (n : ℕ) (hn : 0 < n) :
137     kernelCharpoly (specialDatum q a n) = X - C (a : K) := by
138   let e : LinearMap.ker (specialDatum q a n).N ≃ₗ[K] K := kernelLine n hn
139   unfold kernelCharpoly
140   calc
141     _ = (e.conj (kernelF (specialDatum q a n)).toLinearMap).charpoly :=
142       (e.charpoly_conj _).symm
143     _ = ((a : K) • (LinearMap.id : K →ₗ[K] K)).charpoly := by
144       congr 1
145       exact kernelLine_conjugate q a n hn
146     _ = X - C (a : K) := scalar_charpoly _
147 
148 theorem special_kernel_dimension (q a : Kˣ) (n : ℕ) (hn : 0 < n) :
149     Module.finrank K (LinearMap.ker (specialDatum q a n).N) = 1 := by
150   change Module.finrank K (LinearMap.ker (shift (K := K) n)) = 1
151   rw [(kernelLine (K := K) n hn).finrank_eq]
152   simp
153 
154 theorem whole_charpoly (q a : Kˣ) (n : ℕ) :
155     (specialDatum q a n).F.toLinearMap.charpoly =
156       ∏ j : Fin n, (X - C ((a * q⁻¹ ^ j.val : Kˣ) : K)) := by
157   have h : (specialDatum q a n).F.toLinearMap =
158       (Matrix.diagonal (fun j : Fin n => ((a * q⁻¹ ^ j.val : Kˣ) : K))).toLin' := by
159     apply LinearMap.ext
160     intro x
161     funext i
162     simp [specialDatum, diagonalF, Matrix.toLin'_apply, Matrix.mulVec, dotProduct, Matrix.diagonal_apply]
163   rw [h, Matrix.charpoly_toLin', Matrix.charpoly_diagonal]
164 
165 end PaperX.SpecialMonodromy

Back to source controls