TopologyCategories.lean

1 import PaperIRelease.CategoryPackets
2 import PaperIRelease.TopologyTransport
3 
4 /-!
5 # Continuous packet and seeded-system categories
6 
7 The operator algebras are concrete algebras of individually continuous
8 linear operators; no additional topology on the operator algebra itself is
9 declared. Carrier morphisms and packet projectors are continuous. The seeded
10 condition uses the closure of the actual algebraic generated hull.
11 -/
12 
13 noncomputable section
14 open Set Function CategoryTheory
15 
16 namespace Komorebi.PaperIRelease.TopologyCategories
17 
18 open Foundation
19 open PacketNaturalityCompletion.StrictNaturality
20 
21 universe u
22 variable (K : Type u) [Field K] [TopologicalSpace K]
23 
24 structure PacketObject extends CategoryPackets.PacketObject K where
25   [topology : TopologicalSpace carrier]
26   [topologicalAdd : IsTopologicalAddGroup carrier]
27   [scalarContinuous : ContinuousSMul K carrier]
28   [hausdorff : T2Space carrier]
29   operator_continuous : ∀ T : algebra, Continuous T.val
30   packet_continuous : ∀ i, Continuous (packets.proj i)
31 
32 attribute [instance] PacketObject.topology PacketObject.topologicalAdd
33   PacketObject.scalarContinuous PacketObject.hausdorff
34 
35 variable {K}
36 
37 structure PacketMorphism (X Y : PacketObject K) extends
38     CategoryPackets.PacketMorphism X.toPacketObject Y.toPacketObject where
39   continuous : Continuous linearMap
40 
41 @[ext]
42 theorem PacketMorphism.ext {X Y : PacketObject K} (f g : PacketMorphism X Y)
43     (h : f.toPacketMorphism = g.toPacketMorphism) : f = g := by
44   cases f
45   cases g
46   cases h
47   rfl
48 
49 def PacketMorphism.identity (X : PacketObject K) : PacketMorphism X X where
50   toPacketMorphism := CategoryPackets.PacketMorphism.identity X.toPacketObject
51   continuous := continuous_id
52 
53 def PacketMorphism.comp {X Y Z : PacketObject K}
54     (f : PacketMorphism X Y) (g : PacketMorphism Y Z) : PacketMorphism X Z where
55   toPacketMorphism := f.toPacketMorphism.comp g.toPacketMorphism
56   continuous := g.continuous.comp f.continuous
57 
58 instance packetCategory : Category (PacketObject K) where
59   Hom := PacketMorphism
60   id := PacketMorphism.identity
61   comp := PacketMorphism.comp
62   id_comp f := by apply PacketMorphism.ext; apply CategoryPackets.PacketMorphism.ext <;> rfl
63   comp_id f := by apply PacketMorphism.ext; apply CategoryPackets.PacketMorphism.ext <;> rfl
64   assoc f g h := by apply PacketMorphism.ext; apply CategoryPackets.PacketMorphism.ext <;> rfl
65 
66 /-- Closure of the actual algebraic operator-generated hull. -/
67 def closedHull (X : PacketObject K) (S : Set X.carrier) : Submodule K X.carrier :=
68   (AlgebraGeneratedHull X.algebra S).topologicalClosure
69 
70 /-- The closed hull is invariant under every individually continuous
71 operator of the acting algebra. -/
72 theorem operator_mem_closedHull (X : PacketObject K) (S : Set X.carrier)
73     (T : X.algebra) {x : X.carrier} (hx : x ∈ closedHull X S) :
74     T.val x ∈ closedHull X S := by
75   have hsmall : T.val '' (AlgebraGeneratedHull X.algebra S : Set X.carrier) ⊆
76       (AlgebraGeneratedHull X.algebra S : Set X.carrier) := by
77     rintro y ⟨x, hx, rfl⟩
78     rw [CategoryPackets.hull_eq_span X.toPacketObject S] at hx ⊢
79     exact Submodule.smul_mem _ T hx
80   change T.val x ∈ closure (AlgebraGeneratedHull X.algebra S : Set X.carrier)
81   exact closure_mono hsmall
82     (image_closure_subset_closure_image (X.operator_continuous T) ⟨x, hx, rfl⟩)
83 
84 structure SeedObject extends toContinuousPacketObject : PacketObject K where
85   seeds : Set carrier
86 
87 structure SeedMorphism (X Y : SeedObject (K := K)) extends
88     toContinuousPacketMorphism : PacketMorphism X.toContinuousPacketObject Y.toContinuousPacketObject where
89   seed_condition : ∀ s ∈ X.seeds, linearMap s ∈ closedHull Y.toContinuousPacketObject Y.seeds
90 
91 @[ext]
92 theorem SeedMorphism.ext {X Y : SeedObject (K := K)} (f g : SeedMorphism X Y)
93     (h : f.toContinuousPacketMorphism = g.toContinuousPacketMorphism) : f = g := by
94   cases f
95   cases g
96   cases h
97   rfl
98 
99 /-- A continuous seeded morphism carries the algebraic hull into the
100 target closed hull. The action-invariance step uses operator continuity. -/
101 theorem SeedMorphism.map_hull {X Y : SeedObject (K := K)}
102     (f : SeedMorphism X Y) {x : X.carrier}
103     (hx : x ∈ AlgebraGeneratedHull X.algebra X.seeds) :
104     f.linearMap x ∈ closedHull Y.toContinuousPacketObject Y.seeds := by
105   induction hx using Submodule.span_induction with
106   | mem x hx =>
107     rcases hx with ⟨T, s, hs, rfl⟩
108     rw [f.toContinuousPacketMorphism.toPacketMorphism.operator_apply T s]
109     exact operator_mem_closedHull Y.toContinuousPacketObject Y.seeds (f.algebraMap T) (f.seed_condition s hs)
110   | zero => simp
111   | add x y hx hy ihx ihy => simpa using Submodule.add_mem _ ihx ihy
112   | smul a x hx ih => simpa using Submodule.smul_mem _ a ih
113 
114 /-- Closure transport is derived from actual continuity and the proved
115 algebraic hull inclusion. -/
116 theorem SeedMorphism.map_closedHull {X Y : SeedObject (K := K)}
117     (f : SeedMorphism X Y) {x : X.carrier}
118     (hx : x ∈ closedHull X.toContinuousPacketObject X.seeds) :
119     f.linearMap x ∈ closedHull Y.toContinuousPacketObject Y.seeds := by
120   have hsmall : f.linearMap '' (AlgebraGeneratedHull X.algebra X.seeds : Set X.carrier) ⊆
121       (closedHull Y.toContinuousPacketObject Y.seeds : Set Y.carrier) := by
122     rintro y ⟨x, hx, rfl⟩
123     exact f.map_hull hx
124   have him := image_closure_subset_closure_image f.continuous ⟨x, hx, rfl⟩
125   exact closure_minimal hsmall (Submodule.isClosed_topologicalClosure _) him
126 
127 def SeedMorphism.identity (X : SeedObject (K := K)) : SeedMorphism X X where
128   toContinuousPacketMorphism := PacketMorphism.identity X.toContinuousPacketObject
129   seed_condition s hs := by
130     change s ∈ closedHull X.toContinuousPacketObject X.seeds
131     apply Submodule.le_topologicalClosure
132     exact Submodule.subset_span ⟨1, s, hs, by simp⟩
133 
134 def SeedMorphism.comp {X Y Z : SeedObject (K := K)}
135     (f : SeedMorphism X Y) (g : SeedMorphism Y Z) : SeedMorphism X Z where
136   toContinuousPacketMorphism := f.toContinuousPacketMorphism.comp g.toContinuousPacketMorphism
137   seed_condition s hs := g.map_closedHull (f.seed_condition s hs)
138 
139 instance seedCategory : Category (SeedObject (K := K)) where
140   Hom := SeedMorphism
141   id := SeedMorphism.identity
142   comp := SeedMorphism.comp
143   id_comp f := by apply SeedMorphism.ext; apply PacketMorphism.ext; apply CategoryPackets.PacketMorphism.ext <;> rfl
144   comp_id f := by apply SeedMorphism.ext; apply PacketMorphism.ext; apply CategoryPackets.PacketMorphism.ext <;> rfl
145   assoc f g h := by apply SeedMorphism.ext; apply PacketMorphism.ext; apply CategoryPackets.PacketMorphism.ext <;> rfl
146 
147 /-- A continuous surjective seeded morphism from a densely generated
148 system has densely generating target seeds. -/
149 theorem seeded_surjection_generates {X Y : SeedObject (K := K)}
150     (f : SeedMorphism X Y) (hf : Surjective f.linearMap)
151     (hX : closedHull X.toContinuousPacketObject X.seeds = ⊤) :
152     closedHull Y.toContinuousPacketObject Y.seeds = ⊤ := by
153   apply top_unique
154   intro y _
155   obtain ⟨x, rfl⟩ := hf y
156   apply f.map_closedHull
157   rw [hX]
158   trivial
159 
160 end Komorebi.PaperIRelease.TopologyCategories

Back to source controls