GeneralChain.lean

1 import PaperXI.MonodromyChain
2 
3 /-! Proposition 2.3 for any operator satisfying the stated block support.
4 The transfer model is constructed from the operator; it is not an extra hypothesis. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.MonodromyChain
8 open scoped BigOperators
9 variable {K W : Type*} [Field K] [AddCommGroup W] [Module K W]
10 variable {m : ℕ}
11 
12 def ChainSupported (N : Module.End K (Fin m → W)) : Prop :=
13   ∀ i j : Fin m, i.val + 1 ≠ j.val → projector i * N * projector j = 0
14 
15 theorem arbitrary_block_reconstruction (N : Module.End K (Fin m → W))
16     (hN : ChainSupported N) :
17     N = ∑ i : Fin m, ∑ j : Fin m,
18       if i.val + 1 = j.val then projector i * N * projector j else 0 := by
19   have h : ∀ i j : Fin m,
20       (if i.val + 1 = j.val then projector i * N * projector j else 0) =
21         projector i * N * projector j := by
22     intro i j
23     split
24     · rfl
25     · rename_i hij; exact (hN i j hij).symm
26   simp_rw [h]
27   simp only [← Finset.mul_sum, projector_sum, mul_one, ← Finset.sum_mul, one_mul]
28 
29 theorem projector_eq_single (j : Fin m) (x : Fin m → W) :
30     projector (K := K) j x = Pi.single j (x j) := by
31   funext i
32   by_cases h : i = j
33   · subst i; simp
34   · simp [h]
35 
36 def extractedTransfers (N : Module.End K (Fin m → W)) (i : ℕ) : Module.End K W :=
37   if h : i + 1 < m then
38     (LinearMap.proj ⟨i, by omega⟩).comp
39       (N.comp (LinearMap.single K (fun _ : Fin m => W) ⟨i + 1, h⟩))
40   else 0
41 
42 theorem coordinate_block_zero (N : Module.End K (Fin m → W)) (hN : ChainSupported N)
43     (i j : Fin m) (h : i.val + 1 ≠ j.val) (x : Fin m → W) :
44     N (projector (K := K) j x) i = 0 := by
45   have hx := congrArg (fun f : Module.End K (Fin m → W) => f x i) (hN i j h)
46   simpa [Module.End.mul_apply] using hx
47 
48 /-- Any chain-supported operator is exactly its extracted transfer chain. -/
49 theorem eq_extracted_shift (N : Module.End K (Fin m → W)) (hN : ChainSupported N) :
50     N = shift (extractedTransfers N) := by
51   apply LinearMap.ext
52   intro x
53   funext i
54   have hx : N x i = ∑ j : Fin m, N (projector (K := K) j x) i := by
55     have hp := congrArg (fun f : Module.End K (Fin m → W) => N (f x) i)
56       (projector_sum (K := K) (W := W) (m := m))
57     simpa [LinearMap.sum_apply, map_sum, Finset.sum_apply] using hp.symm
58   rw [hx, shift_apply]
59   by_cases hi : i.val + 1 < m
60   · rw [dite_eq_left hi]
61     rw [Finset.sum_eq_single (⟨i.val + 1, hi⟩ : Fin m)]
62     · simp [extractedTransfers, hi, projector_eq_single]
63     · intro j _ hj
64       apply coordinate_block_zero N hN i j
65       intro he
66       apply hj
67       apply Fin.ext
68       exact he.symm
69     · simp
70   · rw [dite_eq_right hi]
71     apply Finset.sum_eq_zero
72     intro j _
73     exact coordinate_block_zero N hN i j (by omega) x
74 
75 theorem arbitrary_nilpotent_bound (N : Module.End K (Fin m → W))
76     (hN : ChainSupported N) : N ^ m = 0 := by
77   rw [eq_extracted_shift N hN]
78   exact nilpotent_bound _
79 
80 theorem arbitrary_power_paths (N : Module.End K (Fin m → W)) (hN : ChainSupported N)
81     (r : ℕ) (x : Fin m → W) (i : Fin m) :
82     (N ^ r) x i = if h : i.val + r < m then
83       path (extractedTransfers N) i.val r (x ⟨i.val + r, h⟩) else 0 := by
84   calc
85     (N ^ r) x i = (shift (extractedTransfers N) ^ r) x i := by
86       conv_lhs => rw [eq_extracted_shift N hN]
87     _ = _ := pow_apply _ _ _ _
88 
89 end PaperXI.MonodromyChain

Back to source controls