VectorInverseLimit.lean

1 import PaperXII.StableCores
2 
3 /-! Paper XII, 8.11–8.12. The inverse limit is the actual compatible-sequence submodule. -/
4 namespace PaperXII.VectorInverseLimit
5 
6 open StableCores
7 
8 variable {K : Type*} [Field K] {V : ℕ → Type*}
9     [∀ n, AddCommGroup (V n)] [∀ n, Module K (V n)]
10 
11 /-- The vector space of sequences compatible with every transition map. -/
12 def limit (D : LinearSystem K V) : Submodule K (∀ n, V n) where
13   carrier := {v | ∀ n m (h : m ≤ n), D.map n m h (v n) = v m}
14   zero_mem' := by intro n m h; exact (D.map n m h).map_zero
15   add_mem' := by
16     intro u v hu hv n m h
17     simp only [Pi.add_apply, map_add]
18     rw [hu n m h, hv n m h]
19   smul_mem' := by
20     intro c v hv n m h
21     simp only [Pi.smul_apply, map_smul]
22     rw [hv n m h]
23 
24 /-- Adjacent compatibility implies compatibility with every composite transition. -/
25 theorem compatible_of_adjacent (D : LinearSystem K V) (v : ∀ n, V n)
26     (hv : ∀ n, D.map (n + 1) n (Nat.le_succ n) (v (n + 1)) = v n) :
27     v ∈ limit D := by
28   intro n m hmn
29   induction n, hmn using Nat.le_induction with
30   | base => rw [D.map_self]; rfl
31   | succ n hmn ih =>
32     rw [← D.map_comp (n + 1) n m hmn (Nat.le_succ n), LinearMap.comp_apply, hv, ih]
33 
34 /-- Every coordinate of a compatible sequence lies in the actual stable core. -/
35 theorem coordinate_mem_stableCore (D : LinearSystem K V) (v : limit D) (m : ℕ) :
36     v.val m ∈ stableCore D m := by
37   rw [mem_stableCore_iff]
38   intro n h
39   exact ⟨v.val n, v.property n m h⟩
40 
41 variable [∀ n, FiniteDimensional K (V n)]
42 
43 /-- Choose a preimage under the proved surjective stable-core transition. -/
44 noncomputable def liftCore (D : LinearSystem K V) (m : ℕ)
45     (y : stableCore D m) : stableCore D (m + 1) :=
46   (coreMap_surjective D m y).choose
47 
48 /-- The chosen preimage really maps to the prescribed vector. -/
49 theorem liftCore_spec (D : LinearSystem K V) (m : ℕ) (y : stableCore D m) :
50     coreMap D m (liftCore D m y) = y :=
51   (coreMap_surjective D m y).choose_spec
52 
53 /-- Recursively lift a prescribed first stable-core vector. -/
54 noncomputable def coreSequence (D : LinearSystem K V) (y : stableCore D 0) :
55     ∀ n, stableCore D n
56   | 0 => y
57   | n + 1 => liftCore D n (coreSequence D y n)
58 
59 /-- The recursion produces an actual inverse-limit element. -/
60 noncomputable def fromInitialCore (D : LinearSystem K V) (y : stableCore D 0) : limit D :=
61   ⟨fun n ↦ (coreSequence D y n).val, compatible_of_adjacent D _ (by
62     intro n
63     exact congrArg Subtype.val (liftCore_spec D n (coreSequence D y n)))⟩
64 
65 /-- The initial coordinate of the constructed sequence is exactly prescribed. -/
66 theorem fromInitialCore_zero (D : LinearSystem K V) (y : stableCore D 0) :
67     (fromInitialCore D y).val 0 = y.val := rfl
68 
69 /-- Precise clause of 8.11, stronger because only the first vector need be nonzero. -/
70 theorem prescribed_nonzero_branch (D : LinearSystem K V) (y : V 0)
71     (hy : y ∈ stableCore D 0) (hne : y ≠ 0) :
72     ∃ v : limit D, v.val 0 = y ∧ ∀ n, v.val n ≠ 0 := by
73   let v := fromInitialCore D ⟨y, hy⟩
74   refine ⟨v, rfl, ?_⟩
75   intro n hn
76   have hc := v.property n 0 (Nat.zero_le n)
77   rw [hn, map_zero] at hc
78   exact hne hc.symm
79 
80 /-- A nonzero first stable core forces the actual inverse-limit vector space to be nonzero. -/
81 theorem nontrivial_limit_of_first_core (D : LinearSystem K V)
82     (hcore : stableCore D 0 ≠ ⊥) : Nontrivial (limit D) := by
83   obtain ⟨y, hy, hne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hcore
84   obtain ⟨v, _, hv⟩ := prescribed_nonzero_branch D y hy hne
85   exact ⟨v, 0, fun heq ↦ hv 0 (congrArg (fun w : limit D ↦ w.val 0) heq)⟩
86 
87 /-- Theorem 8.11 under the manuscript's all-level nonzero-core hypothesis. -/
88 theorem nontrivial_limit_of_nonzero_cores (D : LinearSystem K V)
89     (hcore : ∀ m, stableCore D m ≠ ⊥) : Nontrivial (limit D) :=
90   nontrivial_limit_of_first_core D (hcore 0)
91 
92 omit [∀ n, FiniteDimensional K (V n)] in
93 /-- Surjective adjacent transitions make every composite transition surjective. -/
94 theorem maps_surjective (D : LinearSystem K V)
95     (hs : ∀ m, Function.Surjective (D.map (m + 1) m (Nat.le_succ m)))
96     (n m : ℕ) (h : m ≤ n) : Function.Surjective (D.map n m h) := by
97   induction n, h using Nat.le_induction with
98   | base => rw [D.map_self]; exact Function.surjective_id
99   | succ n h ih =>
100     rw [← D.map_comp (n + 1) n m h (Nat.le_succ n)]
101     exact ih.comp (hs n)
102 
103 omit [∀ n, FiniteDimensional K (V n)] in
104 /-- Surjective systems have the whole space as their stable core at every level. -/
105 theorem stableCore_eq_top_of_surjective (D : LinearSystem K V)
106     (hs : ∀ m, Function.Surjective (D.map (m + 1) m (Nat.le_succ m))) (m : ℕ) :
107     stableCore D m = ⊤ := by
108   apply top_unique
109   intro y _
110   rw [mem_stableCore_iff]
111   intro n h
112   exact maps_surjective D hs n m h y
113 
114 /-- Corollary 8.12, with nonzero first space sufficient. -/
115 theorem nontrivial_limit_of_surjective (D : LinearSystem K V) [Nontrivial (V 0)]
116     (hs : ∀ m, Function.Surjective (D.map (m + 1) m (Nat.le_succ m))) :
117     Nontrivial (limit D) := by
118   apply nontrivial_limit_of_first_core
119   rw [stableCore_eq_top_of_surjective D hs]
120   exact top_ne_bot
121 
122 end PaperXII.VectorInverseLimit

Back to source controls