BoundedStar.lean

1 import PaperIRelease.AlgebraSupport
2 import KomorebiVerification.TopologicalCompletion
3 import Mathlib.Algebra.Star.Subalgebra
4 
5 /-!
6 # Bounded Hilbert support patterns
7 
8 The necessary conditions use actual bounded rank-one operators between the
9 nonzero projector ranges. No bounded realization of arbitrary algebraic
10 blocks is assumed.
11 -/
12 
13 noncomputable section
14 set_option autoImplicit false
15 set_option maxHeartbeats 2000000
16 
17 open scoped InnerProduct
18 open InnerProductSpace
19 open KomorebiVerification.TopologicalCompletion
20 
21 namespace Komorebi.PaperIRelease.BoundedSupport
22 
23 universe u v w
24 variable {K : Type u} [RCLike K]
25 variable {X : Type v} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X]
26 variable {I : Type w} [Fintype I]
27 
28 abbrev Block (P : BoundedProjectorFamily K X I) (T : X →L[K] X) (b a : I) :=
29   BoundedProjectorFamily.transferBlock (P.proj b) T (P.proj a)
30 
31 /-- Source-first relation convention, with literal vanishing ambient blocks. -/
32 def Supported (P : BoundedProjectorFamily K X I) (rel : I → I → Prop)
33     (T : X →L[K] X) : Prop := ∀ b a, ¬ rel a b → Block P T b a = 0
34 
35 def underlying (P : BoundedProjectorFamily K X I) :
36     Komorebi.Foundation.LinearProjectorFamily K X I where
37   proj i := (P.proj i).toLinearMap
38   idempotent := P.idempotent
39   orthogonal := P.annihilate
40   complete := P.complete
41 
42 omit [CompleteSpace X] in
43 theorem supported_iff_underlying (P : BoundedProjectorFamily K X I)
44     (rel : I → I → Prop) (T : X →L[K] X) :
45     Supported P rel T ↔ OperatorSupported (underlying P) rel T.toLinearMap := by
46   rw [operatorSupported_iff_ambient]
47   constructor
48   · intro h b a hab
49     exact congrArg ContinuousLinearMap.toLinearMap (h b a hab)
50   · intro h b a hab
51     ext x
52     exact LinearMap.congr_fun (h b a hab) x
53 
54 omit [CompleteSpace X] in
55 theorem proj_mem (P : BoundedProjectorFamily K X I) (a : I) {x : X}
56     (hx : x ∈ P.packet a) : P.proj a x = x := by
57   obtain ⟨y, rfl⟩ := hx
58   exact P.idempotent a y
59 
60 omit [CompleteSpace X] in
61 theorem proj_other (P : BoundedProjectorFamily K X I) {a b : I} (h : b ≠ a)
62     {x : X} (hx : x ∈ P.packet a) : P.proj b x = 0 := by
63   obtain ⟨y, rfl⟩ := hx
64   exact P.annihilate h y
65 
66 theorem block_rankOne (P : BoundedProjectorFamily K X I)
67     (hself : ∀ i, (P.proj i).adjoint = P.proj i) (x y : X) (b a : I) :
68     Block P (rankOne K x y) b a = rankOne K (P.proj b x) (P.proj a y) := by
69   simp only [Block, BoundedProjectorFamily.transferBlock, rankOne_comp,
70     comp_rankOne, hself]
71 
72 /-- A bounded rank-one map with both vectors in their actual packet ranges
73 has precisely the prescribed single possible transfer block. -/
74 theorem supported_rankOne (P : BoundedProjectorFamily K X I)
75     (hself : ∀ i, (P.proj i).adjoint = P.proj i) (rel : I → I → Prop)
76     {a b : I} (hab : rel a b) {x y : X}
77     (hx : x ∈ P.packet b) (hy : y ∈ P.packet a) :
78     Supported P rel (rankOne K x y) := by
79   intro d c hcd
80   rw [block_rankOne P hself]
81   by_cases hd : d = b
82   · subst d
83     have hc : c ≠ a := by intro heq; subst c; exact hcd hab
84     rw [proj_other P hc hy]
85     simp
86   · rw [proj_other P hd hx]
87     simp
88 
89 omit [CompleteSpace X] in
90 theorem exists_nonzero_packet (P : BoundedProjectorFamily K X I)
91     [∀ i, Nontrivial (P.packet i)] (a : I) : ∃ x : X, x ∈ P.packet a ∧ x ≠ 0 := by
92   obtain ⟨x, hx⟩ := exists_ne (0 : P.packet a)
93   exact ⟨x, x.property, fun h => hx (Subtype.ext h)⟩
94 
95 /-- Adjoint closure is exactly symmetry, including its rank-one converse. -/
96 theorem adjoint_closed_iff_symmetric (P : BoundedProjectorFamily K X I)
97     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
98     [∀ i, Nontrivial (P.packet i)] (rel : I → I → Prop) :
99     (∀ T : X →L[K] X, Supported P rel T → Supported P rel T.adjoint) ↔
100       (∀ ⦃a b⦄, rel a b → rel b a) := by
101   constructor
102   · intro h a b hab
103     by_contra hba
104     obtain ⟨x, hx, hx0⟩ := exists_nonzero_packet P b
105     obtain ⟨y, hy, hy0⟩ := exists_nonzero_packet P a
106     have hz := h (rankOne K x y) (supported_rankOne P hself rel hab hx hy) a b hba
107     rw [adjoint_rankOne, block_rankOne P hself, proj_mem P a hy, proj_mem P b hx] at hz
108     exact rankOne_ne_zero hy0 hx0 hz
109   · intro hsym T hT b a hab
110     have hz := hT a b (fun hba => hab (hsym hba))
111     have hadj := congrArg ContinuousLinearMap.adjoint hz
112     rw [BoundedProjectorFamily.adjoint_transferBlock _ _ _ (hself b) (hself a)] at hadj
113     simpa using hadj
114 
115 omit [CompleteSpace X] in
116 theorem identity_supported_iff_reflexive (P : BoundedProjectorFamily K X I)
117     [∀ i, Nontrivial (P.packet i)] (rel : I → I → Prop) :
118     Supported P rel (1 : X →L[K] X) ↔ (∀ a, rel a a) := by
119   constructor
120   · intro h a
121     by_contra haa
122     obtain ⟨x, hx, hx0⟩ := exists_nonzero_packet P a
123     have heq := congrArg (fun T : X →L[K] X => T x) (h a a haa)
124     apply hx0
125     simpa [Block, BoundedProjectorFamily.transferBlock, proj_mem P a hx] using heq
126   · intro hrefl b a hab
127     have hba : b ≠ a := by intro h; subst b; exact hab (hrefl a)
128     ext x
129     exact P.annihilate hba x
130 
131 /-- Composition closure forces transitivity through bounded rank-one maps. -/
132 theorem transitive_of_mul_closed (P : BoundedProjectorFamily K X I)
133     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
134     [∀ i, Nontrivial (P.packet i)] (rel : I → I → Prop)
135     (hclosed : ∀ S T : X →L[K] X, Supported P rel S → Supported P rel T →
136       Supported P rel (S * T)) : ∀ ⦃a b c⦄, rel a b → rel b c → rel a c := by
137   intro a b c hab hbc
138   by_contra hac
139   obtain ⟨x, hx, hx0⟩ := exists_nonzero_packet P a
140   obtain ⟨y, hy, hy0⟩ := exists_nonzero_packet P b
141   obtain ⟨z, hz, hz0⟩ := exists_nonzero_packet P c
142   have heq := hclosed (rankOne K z y) (rankOne K y x)
143     (supported_rankOne P hself rel hbc hz hy)
144     (supported_rankOne P hself rel hab hy hx) c a hac
145   have hblock : Block P (rankOne K z y * rankOne K y x) c a =
146       inner K y y • rankOne K z x := by
147     change Block P ((rankOne K z y).comp (rankOne K y x)) c a = _
148     rw [rankOne_comp_rankOne]
149     have hs : Block P (inner K y y • rankOne K z x) c a =
150         inner K y y • Block P (rankOne K z x) c a := by
151       ext v
152       simp only [Block, BoundedProjectorFamily.transferBlock,
153         ContinuousLinearMap.comp_apply, smul_apply, map_smul]
154     rw [hs, block_rankOne P hself, proj_mem P c hz, proj_mem P a hx]
155   rw [hblock] at heq
156   exact smul_ne_zero (inner_self_ne_zero.mpr hy0) (rankOne_ne_zero hz0 hx0) heq
157 
158 variable [DecidableEq I]
159 
160 /-- Bounded operators with a reflexive transitive support pattern form an
161 actual subalgebra of the bounded operator algebra. -/
162 def supportSubalgebra (P : BoundedProjectorFamily K X I) (rel : I → I → Prop)
163     (hrefl : ∀ a, rel a a) (htrans : ∀ ⦃a b c⦄, rel a b → rel b c → rel a c) : Subalgebra K (X →L[K] X) where
164   carrier := {T | Supported P rel T}
165   zero_mem' := by intro b a _; ext x; simp [Block, BoundedProjectorFamily.transferBlock]
166   add_mem' := by
167     intro S T hS hT
168     apply (supported_iff_underlying P rel (S + T)).mpr
169     exact (Komorebi.PaperIRelease.supportSubalgebra (underlying P) rel hrefl
170       (fun _ _ _ h1 h2 => htrans h1 h2)).add_mem
171         ((supported_iff_underlying P rel S).mp hS)
172         ((supported_iff_underlying P rel T).mp hT)
173   mul_mem' := by
174     intro S T hS hT
175     apply (supported_iff_underlying P rel (S * T)).mpr
176     exact (Komorebi.PaperIRelease.supportSubalgebra (underlying P) rel hrefl
177       (fun _ _ _ h1 h2 => htrans h1 h2)).mul_mem
178         ((supported_iff_underlying P rel S).mp hS)
179         ((supported_iff_underlying P rel T).mp hT)
180   algebraMap_mem' k := by
181     apply (supported_iff_underlying P rel (algebraMap K (X →L[K] X) k)).mpr
182     exact (Komorebi.PaperIRelease.supportSubalgebra (underlying P) rel hrefl
183       (fun _ _ _ h1 h2 => htrans h1 h2)).algebraMap_mem k
184 
185 /-- Actual unital star-subalgebra, obtained from an equivalence relation. -/
186 def supportStarSubalgebra (P : BoundedProjectorFamily K X I)
187     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
188     [∀ i, Nontrivial (P.packet i)] (rel : I → I → Prop) (heq : Equivalence rel) :
189     StarSubalgebra K (X →L[K] X) where
190   toSubalgebra := supportSubalgebra P rel heq.refl (fun {_ _ _} h1 h2 => heq.trans h1 h2)
191   star_mem' := by
192     intro T hT
193     exact (adjoint_closed_iff_symmetric P hself rel).mpr (fun {_ _} h => heq.symm h) T hT
194 
195 /-- Literal Paper I corollary: equality with the bounded support space is
196 equivalent to an equivalence relation, with no supplied closure certificates. -/
197 theorem star_subalgebra_iff_equivalence (P : BoundedProjectorFamily K X I)
198     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
199     [∀ i, Nontrivial (P.packet i)] (rel : I → I → Prop) :
200     (∃ A : StarSubalgebra K (X →L[K] X), ∀ T, T ∈ A ↔ Supported P rel T) ↔
201       Equivalence rel := by
202   constructor
203   · rintro ⟨A, hA⟩
204     refine ⟨(identity_supported_iff_reflexive P rel).mp ((hA 1).mp A.one_mem), ?_, ?_⟩
205     · apply (adjoint_closed_iff_symmetric P hself rel).mp
206       intro T hT
207       exact (hA T.adjoint).mp (star_mem ((hA T).mpr hT))
208     · apply transitive_of_mul_closed P hself rel
209       intro S T hS hT
210       exact (hA (S*T)).mp (A.mul_mem ((hA S).mpr hS) ((hA T).mpr hT))
211   · intro heq
212     exact ⟨supportStarSubalgebra P hself rel heq, fun _ => Iff.rfl⟩
213 
214 /-- Equality support (block diagonal operators) is a genuine star-subalgebra. -/
215 theorem equality_pattern_boundary (P : BoundedProjectorFamily K X I)
216     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
217     [∀ i, Nontrivial (P.packet i)] :
218     ∃ A : StarSubalgebra K (X →L[K] X), ∀ T, T ∈ A ↔ Supported P Eq T := by
219   apply (star_subalgebra_iff_equivalence P hself Eq).mpr
220   exact ⟨fun _ => rfl, fun h => h.symm, fun h1 h2 => h1.trans h2⟩
221 
222 /-- The full support pattern recovers a star-subalgebra containing every
223 bounded operator, including in the empty-index/zero-space case. -/
224 theorem universal_pattern_boundary (P : BoundedProjectorFamily K X I)
225     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
226     [∀ i, Nontrivial (P.packet i)] :
227     ∃ A : StarSubalgebra K (X →L[K] X), ∀ T, T ∈ A := by
228   let rel : I → I → Prop := fun _ _ => True
229   have heq : Equivalence rel := ⟨fun _ => trivial, fun _ => trivial, fun _ _ => trivial⟩
230   refine ⟨supportStarSubalgebra P hself rel heq, ?_⟩
231   intro T b a h
232   exact (h trivial).elim
233 
234 /-- On two nonzero packets a single allowed arrow fails adjoint closure. -/
235 theorem directed_two_packet_boundary (P : BoundedProjectorFamily K X Bool)
236     (hself : ∀ i, (P.proj i).adjoint = P.proj i)
237     [∀ i, Nontrivial (P.packet i)] :
238     ¬ (∀ T : X →L[K] X,
239       Supported P (fun a b => a = false ∧ b = true) T →
240       Supported P (fun a b => a = false ∧ b = true) T.adjoint) := by
241   intro h
242   have hs := (adjoint_closed_iff_symmetric P hself _).mp h
243   have hbad := hs (a := false) (b := true) ⟨rfl, rfl⟩
244   cases hbad.1
245 
246 omit [CompleteSpace X] [DecidableEq I] in
247 /-- An empty relation cannot contain the identity when a nonzero packet exists. -/
248 theorem empty_pattern_boundary [Nonempty I] (P : BoundedProjectorFamily K X I)
249     [∀ i, Nontrivial (P.packet i)] :
250     ¬ Supported P (fun _ _ => False) (1 : X →L[K] X) := by
251   intro h
252   obtain ⟨i⟩ := ‹Nonempty I›
253   exact (identity_supported_iff_reflexive P _).mp h i
254 
255 end Komorebi.PaperIRelease.BoundedSupport

Back to source controls