CategoryPackets.lean

1 import KomorebiVerification.PacketNaturalityCompletion
2 import Mathlib.CategoryTheory.Category.Basic
3 
4 /-!
5 Arbitrary-label packet morphisms, their naturality, and the category of algebraic
6 seeded packet systems.  Packet maps may merge labels and need not be surjective.
7 -/
8 
9 set_option autoImplicit false
10 set_option maxHeartbeats 1600000
11 set_option linter.unnecessarySimpa false
12 set_option linter.unusedVariables false
13 
14 noncomputable section
15 
16 namespace Komorebi.PaperIRelease.CategoryPackets
17 
18 open scoped BigOperators
19 open Foundation CategoryTheory
20 open PacketNaturalityCompletion.StrictNaturality
21 attribute [local instance] Classical.propDecidable
22 
23 universe u
24 
25 variable (K : Type u) [Field K]
26 
27 /-- A finite packet-resolved concrete operator module. -/
28 structure PacketObject where
29   carrier : Type u
30   [addCommGroup : AddCommGroup carrier]
31   [module : Module K carrier]
32   index : Type u
33   [fintype : Fintype index]
34   algebra : Subalgebra K (Module.End K carrier)
35   packets : LinearProjectorFamily K carrier index
36   packet_nonzero : ∀ i, packets.proj i ≠ 0
37 
38 attribute [instance] PacketObject.addCommGroup PacketObject.module PacketObject.fintype
39 
40 variable {K}
41 
42 /-- Empty fibres contribute zero, as required in the manuscript definition. -/
43 def fiberProjector (X : PacketObject K) {J : Type u} (σ : X.index → J) (j : J) :
44     Module.End K X.carrier := by
45   classical
46   exact ∑ i, if σ i = j then X.packets.proj i else 0
47 
48 @[simp] theorem fiberProjector_apply (X : PacketObject K) {J : Type u}
49     (σ : X.index → J) (j : J) (x : X.carrier) :
50     fiberProjector X σ j x = ∑ i, if σ i = j then X.packets.proj i x else 0 := by
51   classical
52   simp only [fiberProjector, LinearMap.sum_apply]
53   apply Finset.sum_congr rfl
54   intro i hi
55   split <;> rfl
56 
57 /-- PSC-I-D-PACKET-MORPHISM, with no injectivity constraint on the labels. -/
58 structure PacketMorphism (X Y : PacketObject K) where
59   linearMap : X.carrier →ₗ[K] Y.carrier
60   algebraMap : X.algebra →ₐ[K] Y.algebra
61   packetMap : X.index → Y.index
62   operator_natural : ∀ T : X.algebra,
63     linearMap.comp T.1 = (algebraMap T).1.comp linearMap
64   packet_natural : ∀ j : Y.index,
65     (Y.packets.proj j).comp linearMap = linearMap.comp (fiberProjector X packetMap j)
66 
67 theorem PacketMorphism.operator_apply {X Y : PacketObject K}
68     (f : PacketMorphism X Y) (T : X.algebra) (x : X.carrier) :
69     f.linearMap (T.1 x) = (f.algebraMap T).1 (f.linearMap x) :=
70   LinearMap.congr_fun (f.operator_natural T) x
71 
72 theorem PacketMorphism.packet_apply {X Y : PacketObject K}
73     (f : PacketMorphism X Y) (j : Y.index) (x : X.carrier) :
74     Y.packets.proj j (f.linearMap x) = f.linearMap (fiberProjector X f.packetMap j x) :=
75   LinearMap.congr_fun (f.packet_natural j) x
76 
77 @[ext] theorem PacketMorphism.ext {X Y : PacketObject K}
78     (f g : PacketMorphism X Y) (hl : f.linearMap = g.linearMap)
79     (ha : f.algebraMap = g.algebraMap) (hp : f.packetMap = g.packetMap) : f = g := by
80   cases f
81   cases g
82   cases hl
83   cases ha
84   cases hp
85   rfl
86 
87 theorem sum_fibers {I J L V : Type u} [Fintype I] [Fintype J]
88     [AddCommMonoid V] (σ : I → J) (τ : J → L) (v : I → V) (k : L) :
89     (∑ j, if τ j = k then ∑ i, if σ i = j then v i else 0 else 0) =
90       ∑ i, if τ (σ i) = k then v i else 0 := by
91   classical
92   calc
93     _ = ∑ j, ∑ i, if σ i = j then (if τ j = k then v i else 0) else 0 := by
94       apply Finset.sum_congr rfl
95       intro j hj
96       by_cases h : τ j = k <;> simp [h]
97     _ = ∑ i, ∑ j, if σ i = j then (if τ j = k then v i else 0) else 0 :=
98       Finset.sum_comm
99     _ = _ := by simp
100 
101 /-- The identity preserves every packet, including in the empty-index zero-space case. -/
102 def PacketMorphism.identity (X : PacketObject K) : PacketMorphism X X where
103   linearMap := LinearMap.id
104   algebraMap := AlgHom.id K X.algebra
105   packetMap := id
106   operator_natural T := by simp
107   packet_natural j := by
108     classical
109     ext x
110     simp [fiberProjector]
111 
112 /-- Composition aggregates the fibres of the composite label map. -/
113 def PacketMorphism.comp {X Y Z : PacketObject K}
114     (f : PacketMorphism X Y) (g : PacketMorphism Y Z) : PacketMorphism X Z where
115   linearMap := g.linearMap.comp f.linearMap
116   algebraMap := g.algebraMap.comp f.algebraMap
117   packetMap := g.packetMap ∘ f.packetMap
118   operator_natural T := by
119     ext x
120     change g.linearMap (f.linearMap (T.1 x)) =
121       (g.algebraMap (f.algebraMap T)).1 (g.linearMap (f.linearMap x))
122     rw [f.operator_apply T x]
123     exact g.operator_apply (f.algebraMap T) (f.linearMap x)
124   packet_natural k := by
125     classical
126     ext x
127     change Z.packets.proj k (g.linearMap (f.linearMap x)) =
128       g.linearMap (f.linearMap (fiberProjector X (g.packetMap ∘ f.packetMap) k x))
129     rw [g.packet_apply k (f.linearMap x)]
130     simp only [fiberProjector_apply, map_sum]
131     have hf (j : Y.index) : Y.packets.proj j (f.linearMap x) =
132         ∑ i, if f.packetMap i = j then f.linearMap (X.packets.proj i x) else 0 := by
133       rw [f.packet_apply j x]
134       simp [fiberProjector_apply, map_sum, apply_ite]
135     simp_rw [hf]
136     simp only [apply_ite, map_zero, map_sum]
137     exact sum_fibers f.packetMap g.packetMap
138       (fun i => g.linearMap (f.linearMap (X.packets.proj i x))) k
139 
140 instance packetCategory : Category (PacketObject K) where
141   Hom := PacketMorphism
142   id := PacketMorphism.identity
143   comp := PacketMorphism.comp
144   id_comp f := by apply PacketMorphism.ext <;> rfl
145   comp_id f := by apply PacketMorphism.ext <;> rfl
146   assoc f g h := by apply PacketMorphism.ext <;> rfl
147 
148 /-- The source hull maps onto exactly the orbit span for the image algebra. -/
149 def ImageHull {X Y : PacketObject K} (f : PacketMorphism X Y) (S : Set X.carrier) :
150     Submodule K Y.carrier :=
151   Submodule.span K {y | ∃ T : X.algebra, ∃ s ∈ S,
152     y = (f.algebraMap T).1 (f.linearMap s)}
153 
154 theorem hull_natural {X Y : PacketObject K} (f : PacketMorphism X Y)
155     (S : Set X.carrier) :
156     Submodule.map f.linearMap (AlgebraGeneratedHull X.algebra S) = ImageHull f S := by
157   rw [AlgebraGeneratedHull, ImageHull, Submodule.map_span]
158   congr 1
159   ext y
160   constructor
161   · rintro ⟨x, ⟨T, s, hs, rfl⟩, rfl⟩
162     exact ⟨T, s, hs, LinearMap.congr_fun (f.operator_natural T) s⟩
163   · rintro ⟨T, s, hs, rfl⟩
164     exact ⟨T.1 s, ⟨T, s, hs, rfl⟩,
165       LinearMap.congr_fun (f.operator_natural T) s⟩
166 
167 theorem imageHull_le {X Y : PacketObject K} (f : PacketMorphism X Y)
168     (S : Set X.carrier) :
169     ImageHull f S ≤ AlgebraGeneratedHull Y.algebra (f.linearMap '' S) := by
170   apply Submodule.span_le.2
171   rintro y ⟨T, s, hs, rfl⟩
172   exact Submodule.subset_span ⟨f.algebraMap T, f.linearMap s, ⟨s, hs, rfl⟩, rfl⟩
173 
174 theorem imageHull_eq_top {X Y : PacketObject K} (f : PacketMorphism X Y)
175     (S : Set X.carrier) (hS : AlgebraGeneratedHull X.algebra S = ⊤)
176     (hf : Function.Surjective f.linearMap) : ImageHull f S = ⊤ := by
177   rw [← hull_natural f S, hS, Submodule.map_top, LinearMap.range_eq_top.mpr hf]
178 
179 theorem sum_conditions_comm {I J V : Type u} [Fintype I] [Fintype J]
180     [AddCommMonoid V] (p : I → Prop) (q : J → Prop) (v : I → J → V) :
181     (∑ i, if p i then ∑ j, if q j then v i j else 0 else 0) =
182       ∑ j, if q j then ∑ i, if p i then v i j else 0 else 0 := by
183   calc
184     _ = ∑ i, ∑ j, if p i then (if q j then v i j else 0) else 0 := by
185       apply Finset.sum_congr rfl
186       intro i hi
187       by_cases hp : p i <;> simp [hp]
188     _ = ∑ j, ∑ i, if p i then (if q j then v i j else 0) else 0 :=
189       Finset.sum_comm
190     _ = _ := by
191       apply Finset.sum_congr rfl
192       intro j hj
193       by_cases hq : q j <;> simp [hq]
194 
195 /-- Noninjective labels produce the exact double sum over source packet fibres. -/
196 theorem transferBlock_naturality_apply {X Y : PacketObject K}
197     (f : PacketMorphism X Y) (T : X.algebra) (j i : Y.index) (x : X.carrier) :
198     Y.packets.proj j ((f.algebraMap T).1 (Y.packets.proj i (f.linearMap x))) =
199       ∑ b, if f.packetMap b = j then
200         ∑ a, if f.packetMap a = i then
201           f.linearMap (X.packets.proj b (T.1 (X.packets.proj a x))) else 0
202         else 0 := by
203   rw [f.packet_apply i x, ← f.operator_apply T, f.packet_apply j]
204   simp only [fiberProjector_apply, map_sum, apply_ite, map_zero]
205   exact sum_conditions_comm (fun a => f.packetMap a = i) (fun b => f.packetMap b = j)
206     (fun a b => f.linearMap (X.packets.proj b (T.1 (X.packets.proj a x))))
207 
208 /-- PSC-I-T-NATURALITY: equality of the actual transfer-block linear maps. -/
209 theorem transferBlock_naturality {X Y : PacketObject K}
210     (f : PacketMorphism X Y) (T : X.algebra) (j i : Y.index) :
211     (transferBlock Y.packets Y.packets (f.algebraMap T).1 j i).comp f.linearMap =
212       ∑ b, if f.packetMap b = j then
213         ∑ a, if f.packetMap a = i then
214           f.linearMap.comp (transferBlock X.packets X.packets T.1 b a) else 0
215         else 0 := by
216   apply LinearMap.ext
217   intro x
218   have heval (p : Prop) (s t : X.carrier →ₗ[K] Y.carrier) :
219       (if p then s else t) x = if p then s x else t x := by
220     by_cases hp : p <;> simp [hp]
221   simp only [LinearMap.sum_apply, heval, LinearMap.zero_apply]
222   exact transferBlock_naturality_apply f T j i x
223 
224 /-- The ordinary A-span equals the scalar span of all A-orbits. -/
225 theorem hull_eq_span (X : PacketObject K) (S : Set X.carrier) :
226     (AlgebraGeneratedHull X.algebra S : Set X.carrier) = Submodule.span X.algebra S := by
227   ext x
228   constructor
229   · intro hx
230     induction hx using Submodule.span_induction with
231     | mem x hx =>
232         rcases hx with ⟨T, s, hs, rfl⟩
233         exact Submodule.smul_mem _ T (Submodule.subset_span hs)
234     | zero => exact Submodule.zero_mem _
235     | add x y hx hy ihx ihy => exact Submodule.add_mem _ ihx ihy
236     | smul c x hx ih =>
237         exact Submodule.smul_mem _ (algebraMap K X.algebra c) ih
238   · intro hx
239     have hstable (T : X.algebra) {x : X.carrier}
240         (hx : x ∈ AlgebraGeneratedHull X.algebra S) :
241         T.1 x ∈ AlgebraGeneratedHull X.algebra S := by
242       induction hx using Submodule.span_induction with
243       | mem x hx =>
244           rcases hx with ⟨U, s, hs, rfl⟩
245           exact Submodule.subset_span ⟨T * U, s, hs, rfl⟩
246       | zero => simpa using (Submodule.zero_mem (AlgebraGeneratedHull X.algebra S))
247       | add x y hx hy ihx ihy => simpa using Submodule.add_mem _ ihx ihy
248       | smul c x hx ih => simpa using Submodule.smul_mem _ c ih
249     induction hx using Submodule.span_induction with
250     | mem x hx => exact Submodule.subset_span ⟨1, x, hx, by simp⟩
251     | zero => exact Submodule.zero_mem _
252     | add x y hx hy ihx ihy => exact Submodule.add_mem _ ihx ihy
253     | smul T x hx ih => exact hstable T ih
254 
255 /-- Algebraic seeded packet objects retain the declared seed set. -/
256 structure SeedObject extends PacketObject K where
257   seeds : Set carrier
258 
259 /-- PSC-I-D-SEED-MORPHISM: the image seeds lie in the target generated hull. -/
260 structure SeedMorphism (X Y : SeedObject (K := K)) extends
261     PacketMorphism X.toPacketObject Y.toPacketObject where
262   seed_condition : ∀ s ∈ X.seeds, linearMap s ∈ Submodule.span Y.algebra Y.seeds
263 
264 @[ext] theorem SeedMorphism.ext {X Y : SeedObject (K := K)}
265     (f g : SeedMorphism X Y) (h : f.toPacketMorphism = g.toPacketMorphism) : f = g := by
266   cases f
267   cases g
268   cases h
269   rfl
270 
271 def SeedMorphism.identity (X : SeedObject (K := K)) : SeedMorphism X X where
272   toPacketMorphism := PacketMorphism.identity X.toPacketObject
273   seed_condition s hs := Submodule.subset_span hs
274 
275 def SeedMorphism.comp {X Y Z : SeedObject (K := K)}
276     (f : SeedMorphism X Y) (g : SeedMorphism Y Z) : SeedMorphism X Z where
277   toPacketMorphism := f.toPacketMorphism.comp g.toPacketMorphism
278   seed_condition s hs := by
279     have hm := map_mem_span_image_of_intertwining g.linearMap g.algebraMap
280       g.operator_natural Y.seeds (f.seed_condition s hs)
281     have hi : Submodule.span Z.algebra (g.linearMap '' Y.seeds) ≤
282         Submodule.span Z.algebra Z.seeds := by
283       apply Submodule.span_le.2
284       rintro x ⟨s, hs, rfl⟩
285       exact g.seed_condition s hs
286     exact hi hm
287 
288 instance seedCategory : Category (SeedObject (K := K)) where
289   Hom := SeedMorphism
290   id := SeedMorphism.identity
291   comp := SeedMorphism.comp
292   id_comp f := by apply SeedMorphism.ext; apply PacketMorphism.ext <;> rfl
293   comp_id f := by apply SeedMorphism.ext; apply PacketMorphism.ext <;> rfl
294   assoc f g h := by apply SeedMorphism.ext; apply PacketMorphism.ext <;> rfl
295 
296 /-- A surjective seeded morphism out of a generated system generates the target. -/
297 theorem seeded_surjection_generates {X Y : SeedObject (K := K)}
298     (f : SeedMorphism X Y) (hf : Function.Surjective f.linearMap)
299     (hX : Submodule.span X.algebra X.seeds = ⊤) :
300     Submodule.span Y.algebra Y.seeds = ⊤ := by
301   have hi := image_generates_of_surjective_intertwining f.linearMap f.algebraMap
302     f.operator_natural hf X.seeds hX
303   apply top_unique
304   rw [← hi]
305   apply Submodule.span_le.2
306   rintro y ⟨s, hs, rfl⟩
307   exact f.seed_condition s hs
308 
309 end Komorebi.PaperIRelease.CategoryPackets

Back to source controls