InvariantCompletion.lean

1 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
2 import Mathlib.Tactic.Push
3 
4 /-! P8, finite-dimensional closure. Iteration adds actual images under
5 operators. Finite stabilization and leastness are proved, not supplied
6 as hypotheses. The action index may even be infinite. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM
9 open Module
10 universe u v w
11 variable {K : Type u} [DivisionRing K]
12 variable {V : Type v} [AddCommGroup V] [Module K V]
13 variable {I : Type w}
14 
15 /-- Invariance under the whole declared family. -/
16 def CommonInvariant (L : I → V →ₗ[K] V) (W : Submodule K V) : Prop :=
17   ∀ i, W.map (L i) ≤ W
18 
19 /-- One enrichment step. -/
20 def invariantStep (L : I → V →ₗ[K] V) (W : Submodule K V) : Submodule K V :=
21   W ⊔ ⨆ i, W.map (L i)
22 
23 /-- The actual finite sequence of enriched observable spaces. -/
24 def invariantSequence (L : I → V →ₗ[K] V) (W₀ : Submodule K V) : ℕ → Submodule K V
25   | 0 => W₀
26   | n+1 => invariantStep L (invariantSequence L W₀ n)
27 
28 theorem invariantStep_le (L : I → V →ₗ[K] V) (W : Submodule K V) :
29     W ≤ invariantStep L W := le_sup_left
30 
31 theorem invariantStep_monotone (L : I → V →ₗ[K] V) : Monotone (invariantStep L) := by
32   intro W U h
33   exact sup_le_sup h (iSup_mono fun _ => Submodule.map_mono h)
34 
35 theorem invariantStep_eq_iff (L : I → V →ₗ[K] V) (W : Submodule K V) :
36     invariantStep L W = W ↔ CommonInvariant L W := by
37   constructor
38   · intro h i
39     calc
40       W.map (L i) ≤ ⨆ j, W.map (L j) := le_iSup (fun j => W.map (L j)) i
41       _ ≤ invariantStep L W := le_sup_right
42       _ = W := h
43   · intro h
44     exact le_antisymm (sup_le le_rfl (iSup_le h)) (invariantStep_le L W)
45 
46 theorem invariantSequence_le_succ (L : I → V →ₗ[K] V) (W₀ : Submodule K V) (n : ℕ) :
47     invariantSequence L W₀ n ≤ invariantSequence L W₀ (n+1) := invariantStep_le L _
48 
49 theorem invariantSequence_monotone (L : I → V →ₗ[K] V) (W₀ : Submodule K V) :
50     Monotone (invariantSequence L W₀) :=
51   monotone_nat_of_le_succ (invariantSequence_le_succ L W₀)
52 
53 theorem initial_le_invariantSequence (L : I → V →ₗ[K] V)
54     (W₀ : Submodule K V) (n : ℕ) : W₀ ≤ invariantSequence L W₀ n :=
55   invariantSequence_monotone L W₀ (Nat.zero_le n)
56 
57 theorem invariantSequence_minimal (L : I → V →ₗ[K] V)
58     (W₀ U : Submodule K V) (h₀ : W₀ ≤ U) (hU : CommonInvariant L U) (n : ℕ) :
59     invariantSequence L W₀ n ≤ U := by
60   induction n with
61   | zero => exact h₀
62   | succ n ih =>
63       calc
64         invariantSequence L W₀ (n+1) ≤ invariantStep L U := invariantStep_monotone L ih
65         _ = U := (invariantStep_eq_iff L U).mpr hU
66 
67 /-- Equality at one stage persists at all later stages. -/
68 theorem invariantSequence_stays (L : I → V →ₗ[K] V) (W₀ : Submodule K V)
69     (n : ℕ) (h : invariantSequence L W₀ (n+1) = invariantSequence L W₀ n) (k : ℕ) :
70     invariantSequence L W₀ (n+k) = invariantSequence L W₀ n := by
71   induction k with
72   | zero => simp
73   | succ k ih =>
74       rw [Nat.add_succ, invariantSequence, ih]
75       exact h
76 
77 variable [FiniteDimensional K V]
78 
79 /-- Every strict enrichment increases dimension by at least one. -/
80 theorem invariantSequence_dimension_growth (L : I → V →ₗ[K] V) (W₀ : Submodule K V)
81     (n : ℕ) (strict : ∀ k < n,
82       invariantSequence L W₀ k ≠ invariantSequence L W₀ (k+1)) :
83     finrank K W₀ + n ≤ finrank K (invariantSequence L W₀ n) := by
84   induction n with
85   | zero => exact Nat.le_refl _
86   | succ n ih =>
87       have hn := ih (fun k hk => strict k (Nat.lt_succ_of_lt hk))
88       have hs : invariantSequence L W₀ n < invariantSequence L W₀ (n+1) :=
89         lt_of_le_of_ne (invariantSequence_le_succ L W₀ n) (strict n (Nat.lt_succ_self n))
90       have hd := Submodule.finrank_lt_finrank_of_lt hs
91       omega
92 
93 /-- Stabilization occurs no later than the ambient dimension deficit. -/
94 theorem invariantSequence_exists_stable (L : I → V →ₗ[K] V) (W₀ : Submodule K V) :
95     ∃ n ≤ finrank K V - finrank K W₀,
96       invariantSequence L W₀ (n+1) = invariantSequence L W₀ n := by
97   classical
98   by_contra h
99   push Not at h
100   let N := finrank K V - finrank K W₀
101   have hg := invariantSequence_dimension_growth L W₀ (N+1) (by
102     intro k hk
103     exact Ne.symm (h k (by omega)))
104   have hu := Submodule.finrank_le (invariantSequence L W₀ (N+1))
105   have h₀ := Submodule.finrank_le W₀
106   dsimp [N] at hg hu
107   omega
108 
109 /-- A bounded, explicitly indexed completion, not a supplied fixed point. -/
110 noncomputable def invariantCompletion (L : I → V →ₗ[K] V) (W₀ : Submodule K V) : Submodule K V :=
111   invariantSequence L W₀ (finrank K V - finrank K W₀)
112 
113 theorem invariantCompletion_fixed (L : I → V →ₗ[K] V) (W₀ : Submodule K V) :
114     invariantStep L (invariantCompletion L W₀) = invariantCompletion L W₀ := by
115   obtain ⟨n, hn, hs⟩ := invariantSequence_exists_stable L W₀
116   have he := invariantSequence_stays L W₀ n hs (finrank K V - finrank K W₀ - n)
117   rw [Nat.add_sub_of_le hn] at he
118   change invariantStep L (invariantSequence L W₀ _) = invariantSequence L W₀ _
119   rw [he]
120   exact hs
121 
122 theorem invariantCompletion_invariant (L : I → V →ₗ[K] V) (W₀ : Submodule K V) :
123     CommonInvariant L (invariantCompletion L W₀) :=
124   (invariantStep_eq_iff L _).mp (invariantCompletion_fixed L W₀)
125 
126 omit [FiniteDimensional K V] in
127 theorem initial_le_invariantCompletion (L : I → V →ₗ[K] V) (W₀ : Submodule K V) :
128     W₀ ≤ invariantCompletion L W₀ := initial_le_invariantSequence L W₀ _
129 
130 omit [FiniteDimensional K V] in
131 theorem invariantCompletion_minimal (L : I → V →ₗ[K] V)
132     (W₀ U : Submodule K V) (h₀ : W₀ ≤ U) (hU : CommonInvariant L U) :
133     invariantCompletion L W₀ ≤ U := invariantSequence_minimal L W₀ U h₀ hU _
134 
135 /-- The bounded construction is the unique least common invariant extension. -/
136 theorem invariantCompletion_isLeast (L : I → V →ₗ[K] V) (W₀ : Submodule K V) :
137     IsLeast {W : Submodule K V | W₀ ≤ W ∧ CommonInvariant L W} (invariantCompletion L W₀) := by
138   refine ⟨⟨initial_le_invariantCompletion L W₀, invariantCompletion_invariant L W₀⟩, ?_⟩
139   intro U hU
140   exact invariantCompletion_minimal L W₀ U hU.1 hU.2
141 
142 end Komorebi.LSM

Back to source controls