StableCores.lean

1 import PaperXII.FiniteCarrier
2 
3 /-! Paper XII, Definition 8.9 and Lemma 8.10. All ranges are ranges of actual linear maps. -/
4 namespace PaperXII.StableCores
5 
6 /-- A countable inverse system, with the ordinary identity and composition laws. -/
7 structure LinearSystem (K : Type*) [Field K] (V : ℕ → Type*)
8     [∀ n, AddCommGroup (V n)] [∀ n, Module K (V n)] where
9   map : ∀ n m, m ≤ n → V n →ₗ[K] V m
10   map_self : ∀ n, map n n le_rfl = LinearMap.id
11   map_comp : ∀ (a b c) (hcb : c ≤ b) (hba : b ≤ a),
12     (map b c hcb).comp (map a b hba) = map a c (hcb.trans hba)
13 
14 variable {K : Type*} [Field K] {V : ℕ → Type*}
15     [∀ n, AddCommGroup (V n)] [∀ n, Module K (V n)]
16 
17 /-- Padded image family: indices before the target level contribute the whole space. -/
18 def imageAt (D : LinearSystem K V) (m n : ℕ) : Submodule K (V m) :=
19   ⨅ h : m ≤ n, LinearMap.range (D.map n m h)
20 
21 /-- The actual intersection of the images from every later level. -/
22 def stableCore (D : LinearSystem K V) (m : ℕ) : Submodule K (V m) :=
23   ⨅ n, imageAt D m n
24 
25 /-- Membership is precisely membership in every later transition image. -/
26 theorem mem_stableCore_iff (D : LinearSystem K V) (m : ℕ) (v : V m) :
27     v ∈ stableCore D m ↔ ∀ n (h : m ≤ n), ∃ w, D.map n m h w = v := by
28   simp only [stableCore, imageAt, Submodule.mem_iInf, LinearMap.mem_range]
29 
30 /-- A valid later index has its literal transition range as padded image. -/
31 theorem imageAt_eq_range (D : LinearSystem K V) {m n : ℕ} (h : m ≤ n) :
32     imageAt D m n = LinearMap.range (D.map n m h) := by
33   simp [imageAt, h]
34 
35 /-- Composition makes the transition images descend. -/
36 theorem imageAt_antitone (D : LinearSystem K V) (m : ℕ) : Antitone (imageAt D m) := by
37   intro a b hab
38   apply le_iInf
39   intro hma
40   rw [imageAt_eq_range D (hma.trans hab)]
41   rintro y ⟨v, rfl⟩
42   refine ⟨D.map b a hab v, ?_⟩
43   exact LinearMap.congr_fun (D.map_comp b a m hma hab) v
44 
45 /-- Finite dimensionality makes each stable core equal an eventual transition image. -/
46 theorem stableCore_eq_eventual_image (D : LinearSystem K V) [∀ n, FiniteDimensional K (V n)]
47     (m : ℕ) : ∃ (N : ℕ) (hN : m ≤ N), ∀ (n : ℕ) (hn : N ≤ n),
48       stableCore D m = LinearMap.range (D.map n m (hN.trans hn)) := by
49   obtain ⟨N, hN, hstable⟩ := FiniteCarrier.exists_iInf_eq (imageAt D m) (imageAt_antitone D m)
50   refine ⟨max m N, le_max_left _ _, ?_⟩
51   intro n hn
52   have hmn : m ≤ n := (le_max_left m N).trans hn
53   change (⨅ j, imageAt D m j) = _
54   rw [hN, ← hstable n ((le_max_right m N).trans hn), imageAt_eq_range D hmn]
55 
56 /-- Every transition carries a stable-core element into the earlier stable core. -/
57 theorem map_mem_stableCore (D : LinearSystem K V) {a b : ℕ} (hab : b ≤ a)
58     {v : V a} (hv : v ∈ stableCore D a) : D.map a b hab v ∈ stableCore D b := by
59   rw [mem_stableCore_iff] at hv ⊢
60   intro n hbn
61   let k := max n a
62   obtain ⟨w, hw⟩ := hv k (le_max_right n a)
63   refine ⟨D.map k n (le_max_left n a) w, ?_⟩
64   calc
65     D.map n b hbn (D.map k n (le_max_left n a) w) =
66         D.map k b (hbn.trans (le_max_left n a)) w :=
67       LinearMap.congr_fun (D.map_comp k n b hbn (le_max_left n a)) w
68     _ = D.map a b hab (D.map k a (le_max_right n a) w) :=
69       (LinearMap.congr_fun (D.map_comp k a b hab (le_max_right n a)) w).symm
70     _ = D.map a b hab v := by rw [hw]
71 
72 /-- The restriction of the actual transition map to actual stable cores. -/
73 def coreMap (D : LinearSystem K V) (m : ℕ) :
74     stableCore D (m + 1) →ₗ[K] stableCore D m :=
75   (D.map (m + 1) m (Nat.le_succ m)).restrict
76     (fun _ h ↦ map_mem_stableCore D (Nat.le_succ m) h)
77 
78 /-- Lemma 8.10: transition maps on stable cores are surjective. -/
79 theorem coreMap_surjective (D : LinearSystem K V) [∀ n, FiniteDimensional K (V n)]
80     (m : ℕ) : Function.Surjective (coreMap D m) := by
81   intro y
82   obtain ⟨N, hN, hstable⟩ := stableCore_eq_eventual_image D (m + 1)
83   obtain ⟨w, hw⟩ := (mem_stableCore_iff D m y).mp y.property N ((Nat.le_succ m).trans hN)
84   have hz : D.map N (m + 1) hN w ∈ stableCore D (m + 1) := by
85     rw [hstable N le_rfl]
86     exact ⟨w, rfl⟩
87   refine ⟨⟨_, hz⟩, Subtype.ext ?_⟩
88   change D.map (m + 1) m (Nat.le_succ m) (D.map N (m + 1) hN w) = y
89   rw [← LinearMap.comp_apply, D.map_comp]
90   exact hw
91 
92 end PaperXII.StableCores

Back to source controls