MonodromyChain.lean

1 import Mathlib.LinearAlgebra.Pi
2 import Mathlib.Algebra.Module.End
3 import Mathlib.Tactic
4 
5 /-! Paper XI, Proposition 2.3. Actual operators on a finite chain of copies of W.
6 The transfers A i are arbitrary linear maps. Nilpotence is a conclusion.
7 `path` lists all composable transfers in their matrix multiplication order. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.MonodromyChain
11 open scoped BigOperators
12 
13 variable {K W : Type*} [Field K] [AddCommGroup W] [Module K W]
14 variable {m : ℕ}
15 
16 def shift (A : ℕ → Module.End K W) : Module.End K (Fin m → W) where
17   toFun x i := if h : i.val + 1 < m then A i.val (x ⟨i.val + 1, h⟩) else 0
18   map_add' x y := by funext i; by_cases h : i.val + 1 < m <;> simp [h]
19   map_smul' c x := by funext i; by_cases h : i.val + 1 < m <;> simp [h]
20 
21 @[simp] theorem shift_apply (A : ℕ → Module.End K W) (x : Fin m → W) (i : Fin m) :
22     shift A x i = if h : i.val + 1 < m then A i.val (x ⟨i.val + 1, h⟩) else 0 := rfl
23 
24 def path (A : ℕ → Module.End K W) (i : ℕ) : ℕ → Module.End K W
25   | 0 => 1
26   | r + 1 => path A i r * A (i + r)
27 
28 @[simp] theorem path_zero (A : ℕ → Module.End K W) (i : ℕ) : path A i 0 = 1 := rfl
29 @[simp] theorem path_succ (A : ℕ → Module.End K W) (i r : ℕ) :
30     path A i (r + 1) = path A i r * A (i + r) := rfl
31 
32 /-- The complete path formula, including the zero case beyond the chain endpoint. -/
33 theorem pow_apply (A : ℕ → Module.End K W) (r : ℕ) (x : Fin m → W) (i : Fin m) :
34     (shift A ^ r) x i =
35       if h : i.val + r < m then path A i.val r (x ⟨i.val + r, h⟩) else 0 := by
36   induction r generalizing x with
37   | zero => simp [i.isLt]
38   | succ r ih =>
39       rw [pow_succ, Module.End.mul_apply, ih]
40       by_cases hr : i.val + r < m
41       · rw [dite_eq_left hr, shift_apply]
42         by_cases hs : i.val + (r + 1) < m
43         · simp only [Nat.add_assoc] at *
44           rw [dite_eq_left hs, dite_eq_left hs, path_succ, Module.End.mul_apply]
45         · simp only [Nat.add_assoc] at *
46           rw [dite_eq_right hs, dite_eq_right hs, map_zero]
47       · have hs : ¬ i.val + (r + 1) < m := by omega
48         rw [dite_eq_right hr, dite_eq_right hs]
49 
50 /-- Proposition 2.3: arbitrary nearest-neighbor transfers have nilpotence bound m. -/
51 theorem nilpotent_bound (A : ℕ → Module.End K W) :
52     (shift A : Module.End K (Fin m → W)) ^ m = 0 := by
53   apply LinearMap.ext
54   intro x
55   funext i
56   rw [pow_apply, dite_eq_right (by omega)]
57   rfl
58 
59 def projector (j : Fin m) : Module.End K (Fin m → W) where
60   toFun x i := if i = j then x i else 0
61   map_add' x y := by funext i; split <;> simp_all
62   map_smul' c x := by funext i; split <;> simp_all
63 
64 @[simp] theorem projector_apply (j : Fin m) (x : Fin m → W) (i : Fin m) :
65     projector (K := K) j x i = if i = j then x i else 0 := rfl
66 
67 theorem projector_idempotent (j : Fin m) :
68     (projector (K := K) (W := W) j) ^ 2 = projector j := by
69   apply LinearMap.ext
70   intro x
71   funext i
72   by_cases h : i = j <;> simp [pow_two, Module.End.mul_apply, h]
73 
74 theorem projector_orthogonal {i j : Fin m} (h : i ≠ j) :
75     (projector (K := K) (W := W) i) * projector j = 0 := by
76   apply LinearMap.ext
77   intro x
78   funext k
79   by_cases hk : k = i
80   · subst k; simp [Module.End.mul_apply, h]
81   · simp [Module.End.mul_apply, hk]
82 
83 theorem projector_sum : (∑ j : Fin m, projector (K := K) (W := W) j) = 1 := by
84   apply LinearMap.ext
85   intro x
86   funext i
87   simp [LinearMap.sum_apply, Finset.sum_apply]
88 
89 /-- All matrix blocks outside the nearest-neighbor diagonal vanish. -/
90 theorem block_vanishes (A : ℕ → Module.End K W) (i j : Fin m)
91     (h : i.val + 1 ≠ j.val) :
92     projector i * shift A * projector j = 0 := by
93   apply LinearMap.ext
94   intro x
95   funext k
96   by_cases hk : k = i
97   · subst k
98     simp only [Module.End.mul_apply, projector_apply, ite_true, shift_apply]
99     split
100     · rename_i hi
101       have hij : (⟨i.val + 1, hi⟩ : Fin m) ≠ j := by
102         intro he; exact h (congrArg Fin.val he)
103       simp [hij]
104     · rfl
105   · simp [Module.End.mul_apply, hk]
106 
107 /-- Proposition 2.3: the full operator equals the sum of its admissible blocks.
108 The double sum is the boundary-safe form of Σ_{j=1}^{m-1} P_{j-1} N P_j. -/
109 theorem block_reconstruction (A : ℕ → Module.End K W) :
110     shift A = ∑ i : Fin m, ∑ j : Fin m,
111       if i.val + 1 = j.val then projector i * shift A * projector j else 0 := by
112   have h : ∀ i j : Fin m,
113       (if i.val + 1 = j.val then projector i * shift A * projector j else 0) =
114         projector i * shift A * projector j := by
115     intro i j
116     split
117     · rfl
118     · rename_i hij; exact (block_vanishes A i j hij).symm
119   simp_rw [h]
120   simp only [← Finset.mul_sum, projector_sum, mul_one, ← Finset.sum_mul, one_mul]
121 
122 end PaperXI.MonodromyChain

Back to source controls