PacketNaturalityCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.ExactCoordinates
7 import KomorebiVerification.PaperIBlockCompletion
8 import KomorebiVerification.PaperITransport
9 import KomorebiVerification.SeedRankBasics
10 
11 /-!
12 # Paper I: packet, block, reachability, and naturality completion
13 
14 This module closes the remaining finite algebraic content of the packet and
15 naturality portions of Paper I.  It supplies the literal packetwise equality
16 equivalence, a recursive path expansion for every packet power, an exact
17 equivalence between endomorphisms and arbitrary packet-to-packet linear maps,
18 the associated dimension and support laws, an algebraic reachability
19 obstruction, coordinate invariance of transfer edges, a fully typed strict
20 morphism, and the finite two-vertex quiver certificate from the paper.
21 -/
22 
23 set_option autoImplicit false
24 
25 -- Suppress only style/unused lints in the frozen completion proofs; warnings remain fatal.
26 set_option linter.unnecessarySeqFocus false
27 set_option linter.unnecessarySimpa false
28 set_option linter.unusedSectionVars false
29 set_option linter.unusedVariables false
30 set_option maxHeartbeats 4000000
31 set_option maxRecDepth 100000
32 
33 namespace Komorebi.PacketNaturalityCompletion
34 
35 open scoped BigOperators
36 
37 namespace Packets
38 
39 open Foundation
40 open Foundation.LinearProjectorFamily
41 
42 universe u v w
43 
44 variable {R : Type u} {M : Type v} {ι : Type w}
45 variable [Semiring R] [AddCommMonoid M] [Module R M]
46 variable [Fintype ι] [DecidableEq ι]
47 
48 /-- Literal `if and only if` form of packetwise equality. -/
49 theorem eq_iff_projectors_eq
50     (P : LinearProjectorFamily R M ι) (x y : M) :
51     x = y ↔ ∀ i, P.proj i x = P.proj i y := by
52   constructor
53   · rintro rfl i
54     rfl
55   · exact P.eq_of_projectors_eq
56 
57 /--
58 The recursively expanded sum of all length-`m` packet paths from `a` to `b`.
59 At a successor step, the final factor is a one-step transfer block.
60 -/
61 noncomputable def packetPathSum
62     (P : LinearProjectorFamily R M ι) (T : Module.End R M) :
63     ℕ → ι → ι → Module.End R M
64   | 0, b, a => if b = a then P.proj a else 0
65   | m + 1, b, a =>
66       ∑ c, (packetPathSum P T m b c).comp (transferBlock P P T c a)
67 
68 @[simp] theorem packetPathSum_zero_same
69     (P : LinearProjectorFamily R M ι) (T : Module.End R M) (a : ι) :
70     packetPathSum P T 0 a a = P.proj a := by
71   simp [packetPathSum]
72 
73 theorem packetPathSum_zero_ne
74     (P : LinearProjectorFamily R M ι) (T : Module.End R M)
75     {b a : ι} (h : b ≠ a) :
76     packetPathSum P T 0 b a = 0 := by
77   simp [packetPathSum, h]
78 
79 /-- The zero-th power has the expected diagonal packet blocks. -/
80 theorem transferBlock_pow_zero
81     (P : LinearProjectorFamily R M ι) (T : Module.End R M) (b a : ι) :
82     transferBlock P P ((1 : Module.End R M)) b a =
83       packetPathSum P T 0 b a := by
84   classical
85   ext x
86   by_cases h : b = a
87   · subst b
88     simp [transferBlock, packetPathSum, P.idempotent]
89   · simp [transferBlock, packetPathSum, h, P.orthogonal h]
90 
91 /--
92 Full packet-power path expansion, including the diagonal length-zero case.
93 The successor clause of `packetPathSum` is precisely the sum over all choices
94 of the first intermediate packet after the input packet.
95 -/
96 theorem transferBlock_pow_eq_packetPathSum
97     (P : LinearProjectorFamily R M ι) (T : Module.End R M) :
98     ∀ m b a, transferBlock P P (T ^ m) b a = packetPathSum P T m b a := by
99   classical
100   intro m
101   induction m with
102   | zero =>
103       intro b a
104       simpa using transferBlock_pow_zero P T b a
105   | succ m ih =>
106       intro b a
107       rw [pow_succ]
108       change transferBlock P P ((T ^ m).comp T) b a = _
109       rw [Foundation.transferBlock_comp_end]
110       simp only [packetPathSum]
111       apply Finset.sum_congr rfl
112       intro c hc
113       rw [ih]
114 
115 end Packets
116 
117 namespace FullBlocks
118 
119 open Foundation
120 open Foundation.LinearProjectorFamily
121 
122 universe u v w
123 
124 variable {R : Type u} {M : Type v} {ι : Type w}
125 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
126 variable [Fintype ι] [DecidableEq ι]
127 
128 /-- A fully arbitrary heterogeneous matrix of packet-to-packet linear maps. -/
129 abbrev PacketBlocks (P : LinearProjectorFamily R M ι) : Type max v w :=
130   (b : ι) → (a : ι) →
131     LinearMap.range (P.proj a) →ₗ[R] LinearMap.range (P.proj b)
132 
133 /-- Projection from the ambient module onto a certified packet range. -/
134 def packetProjection (P : LinearProjectorFamily R M ι) (a : ι) :
135     M →ₗ[R] LinearMap.range (P.proj a) where
136   toFun x := ⟨P.proj a x, ⟨x, rfl⟩⟩
137   map_add' x y := by
138     apply Subtype.ext
139     exact (P.proj a).map_add x y
140   map_smul' c x := by
141     apply Subtype.ext
142     exact (P.proj a).map_smul c x
143 
144 /-- Inclusion of a packet range into the ambient module. -/
145 def packetInclusion (P : LinearProjectorFamily R M ι) (a : ι) :
146     LinearMap.range (P.proj a) →ₗ[R] M :=
147   Submodule.subtype _
148 
149 @[simp] theorem packetProjection_apply_coe
150     (P : LinearProjectorFamily R M ι) (a : ι)
151     (x : LinearMap.range (P.proj a)) :
152     packetProjection P a (x : M) = x := by
153   apply Subtype.ext
154   rcases x.property with ⟨y, hy⟩
155   change P.proj a (x : M) = (x : M)
156   rw [← hy]
157   exact P.idempotent a y
158 
159 theorem packetProjection_inclusion_ne
160     (P : LinearProjectorFamily R M ι) {a b : ι} (h : a ≠ b)
161     (x : LinearMap.range (P.proj b)) :
162     packetProjection P a (packetInclusion P b x) = 0 := by
163   apply Subtype.ext
164   change P.proj a (x : M) = 0
165   rcases x.property with ⟨y, hy⟩
166   rw [← hy]
167   exact P.orthogonal h y
168 
169 /-- Restrict an ambient endomorphism to each input and output packet. -/
170 def restrictBlocks (P : LinearProjectorFamily R M ι)
171     (T : Module.End R M) : PacketBlocks P :=
172   fun b a => (packetProjection P b).comp (T.comp (packetInclusion P a))
173 
174 /-- Synthesize an ambient endomorphism from an arbitrary family of blocks. -/
175 def synthesizeBlocks (P : LinearProjectorFamily R M ι)
176     (B : PacketBlocks P) : Module.End R M :=
177   ∑ b, ∑ a,
178     (packetInclusion P b).comp ((B b a).comp (packetProjection P a))
179 
180 /-- Packet projection of a synthesized operator selects its output row. -/
181 theorem packetProjection_synthesizeBlocks
182     (P : LinearProjectorFamily R M ι) (B : PacketBlocks P)
183     (b : ι) (x : M) :
184     packetProjection P b (synthesizeBlocks P B x) =
185       ∑ a, B b a (packetProjection P a x) := by
186   classical
187   apply Subtype.ext
188   simp only [synthesizeBlocks, LinearMap.sum_apply, map_sum,
189     Submodule.coe_sum]
190   rw [Finset.sum_eq_single b]
191   · apply Finset.sum_congr rfl
192     intro a ha
193     exact congrArg Subtype.val
194       (packetProjection_apply_coe P b (B b a (packetProjection P a x)))
195   · intro d _ hdb
196     apply Finset.sum_eq_zero
197     intro a ha
198     exact congrArg Subtype.val
199       (packetProjection_inclusion_ne P hdb.symm
200         (B d a (packetProjection P a x)))
201   · simp
202 
203 /-- A synthesized arbitrary block family restricts back to itself. -/
204 theorem restrictBlocks_synthesizeBlocks
205     (P : LinearProjectorFamily R M ι) (B : PacketBlocks P) :
206     restrictBlocks P (synthesizeBlocks P B) = B := by
207   funext b a
208   ext x
209   classical
210   simp only [restrictBlocks, LinearMap.comp_apply]
211   rw [packetProjection_synthesizeBlocks]
212   rw [Finset.sum_eq_single a]
213   · exact congrArg Subtype.val
214       (congrArg (B b a) (packetProjection_apply_coe P a x))
215   · intro c _ hca
216     rw [packetProjection_inclusion_ne P hca]
217     simp
218   · simp
219 
220 /-- Each synthesized restricted block is the corresponding ambient transfer block. -/
221 theorem synthesized_restricted_block
222     (P : LinearProjectorFamily R M ι) (T : Module.End R M)
223     (b a : ι) :
224     (packetInclusion P b).comp
225         (((restrictBlocks P T) b a).comp (packetProjection P a)) =
226       transferBlock P P T b a := by
227   ext x
228   rfl
229 
230 /-- Restricting all blocks and synthesizing reconstructs the operator exactly. -/
231 @[simp] theorem synthesizeBlocks_restrictBlocks
232     (P : LinearProjectorFamily R M ι) (T : Module.End R M) :
233     synthesizeBlocks P (restrictBlocks P T) = T := by
234   classical
235   simp only [synthesizeBlocks, synthesized_restricted_block]
236   exact Foundation.transferBlock_reconstruction_end P T
237 
238 /-- Restriction is injective because all packet blocks reconstruct the operator. -/
239 theorem restrictBlocks_injective
240     (P : LinearProjectorFamily R M ι) :
241     Function.Injective (restrictBlocks P) := by
242   intro S T h
243   calc
244     S = synthesizeBlocks P (restrictBlocks P S) :=
245       (synthesizeBlocks_restrictBlocks P S).symm
246     _ = synthesizeBlocks P (restrictBlocks P T) := congrArg _ h
247     _ = T := synthesizeBlocks_restrictBlocks P T
248 
249 /-- Every arbitrary family of packet maps is realized by a unique operator. -/
250 theorem restrictBlocks_surjective
251     (P : LinearProjectorFamily R M ι) :
252     Function.Surjective (restrictBlocks P) := by
253   intro B
254   exact ⟨synthesizeBlocks P B, restrictBlocks_synthesizeBlocks P B⟩
255 
256 /-- Restriction as a linear map. -/
257 def restrictBlocksLinear (P : LinearProjectorFamily R M ι) :
258     Module.End R M →ₗ[R] PacketBlocks P where
259   toFun := restrictBlocks P
260   map_add' S T := by
261     funext b a
262     ext x
263     simp [restrictBlocks, packetProjection, packetInclusion]
264   map_smul' c T := by
265     funext b a
266     ext x
267     simp [restrictBlocks, packetProjection, packetInclusion]
268 
269 /-- The exact linear equivalence underlying the algebraic full-block representation. -/
270 noncomputable def fullBlockLinearEquiv
271     (P : LinearProjectorFamily R M ι) :
272     Module.End R M ≃ₗ[R] PacketBlocks P :=
273   LinearEquiv.ofBijective (restrictBlocksLinear P)
274     ⟨restrictBlocks_injective P, restrictBlocks_surjective P⟩
275 
276 /--
277 A type synonym carrying the genuine dependent packet-block algebra structure.
278 The structure is transported from ambient endomorphisms across the proved
279 block equivalence, avoiding any homogeneous-matrix surrogate.
280 -/
281 def PacketBlockAlgebra (P : LinearProjectorFamily R M ι) := PacketBlocks P
282 
283 /-- The inverse block equivalence, used to transport the algebra structure. -/
284 noncomputable def packetBlockEquivToEnd
285     (P : LinearProjectorFamily R M ι) :
286     PacketBlockAlgebra P ≃ Module.End R M :=
287   (fullBlockLinearEquiv P).symm.toEquiv
288 
289 noncomputable instance packetBlockAlgebraSemiring
290     (P : LinearProjectorFamily R M ι) : Semiring (PacketBlockAlgebra P) :=
291   Equiv.semiring (packetBlockEquivToEnd P)
292 
293 noncomputable instance packetBlockAlgebraAlgebra
294     (P : LinearProjectorFamily R M ι) : Algebra R (PacketBlockAlgebra P) :=
295   Equiv.algebra R (packetBlockEquivToEnd P)
296 
297 /-- The full dependent block representation as an algebra equivalence. -/
298 noncomputable def fullBlockAlgEquiv
299     (P : LinearProjectorFamily R M ι) :
300     Module.End R M ≃ₐ[R] PacketBlockAlgebra P :=
301   (Equiv.algEquiv R (packetBlockEquivToEnd P)).symm
302 
303 @[simp] theorem fullBlockAlgEquiv_apply
304     (P : LinearProjectorFamily R M ι) (T : Module.End R M) :
305     fullBlockAlgEquiv P T = restrictBlocks P T :=
306   rfl
307 
308 /-- Operator-valued matrix multiplication on arbitrary packet blocks. -/
309 def blockMul (P : LinearProjectorFamily R M ι)
310     (B C : PacketBlocks P) : PacketBlocks P :=
311   fun b a => ∑ c, (B b c).comp (C c a)
312 
313 /-- Restriction carries composition to operator-valued matrix multiplication. -/
314 theorem restrictBlocks_comp
315     (P : LinearProjectorFamily R M ι) (S T : Module.End R M) :
316     restrictBlocks P (S.comp T) =
317       blockMul P (restrictBlocks P S) (restrictBlocks P T) := by
318   funext b a
319   ext x
320   classical
321   rcases x.property with ⟨y, hy⟩
322   have hx : P.proj a (x : M) = (x : M) := by
323     rw [← hy]
324     exact P.idempotent a y
325   simpa [restrictBlocks, blockMul, packetProjection, packetInclusion, hx,
326     LinearMap.sum_apply, Submodule.coe_sum] using
327       Foundation.transferBlock_comp P P P T S b a (x : M)
328 
329 /-- The transported algebra multiplication is exactly packet block multiplication. -/
330 theorem packetBlockAlgebra_mul_eq_blockMul
331     (P : LinearProjectorFamily R M ι)
332     (B C : PacketBlockAlgebra P) :
333     B * C = blockMul P B C := by
334   obtain ⟨S, rfl⟩ := (fullBlockAlgEquiv P).surjective B
335   obtain ⟨T, rfl⟩ := (fullBlockAlgEquiv P).surjective C
336   rw [← map_mul]
337   change restrictBlocks P (S.comp T) =
338     blockMul P (restrictBlocks P S) (restrictBlocks P T)
339   exact restrictBlocks_comp P S T
340 
341 /-- The block-space dimension is exactly the ambient endomorphism dimension. -/
342 theorem finrank_end_eq_finrank_blocks
343     {K : Type u} {V : Type v} [Field K]
344     [AddCommGroup V] [Module K V]
345     [FiniteDimensional K V]
346     (P : LinearProjectorFamily K V ι) :
347     Module.finrank K (Module.End K V) =
348       Module.finrank K (PacketBlocks P) :=
349   (fullBlockLinearEquiv P).finrank_eq
350 
351 /-- The dimension of the ambient module is the sum of its packet dimensions. -/
352 theorem finrank_eq_sum_packet_finrank
353     {K : Type u} {V : Type v} [Field K]
354     [AddCommGroup V] [Module K V]
355     [FiniteDimensional K V]
356     (P : LinearProjectorFamily K V ι) :
357     Module.finrank K V =
358       ∑ a, Module.finrank K (LinearMap.range (P.proj a)) := by
359   rw [← Module.finrank_pi_fintype]
360   exact (P.exactPacketCoordinates.finrank_eq)
361 
362 /-- The full block space has the expected double-sum dimension. -/
363 theorem finrank_blocks_eq_sum_products
364     {K : Type u} {V : Type v} [Field K]
365     [AddCommGroup V] [Module K V]
366     [FiniteDimensional K V]
367     (P : LinearProjectorFamily K V ι) :
368     Module.finrank K (PacketBlocks P) =
369       ∑ b, ∑ a,
370         Module.finrank K (LinearMap.range (P.proj a)) *
371           Module.finrank K (LinearMap.range (P.proj b)) := by
372   rw [Module.finrank_pi_fintype]
373   apply Finset.sum_congr rfl
374   intro b hb
375   rw [Module.finrank_pi_fintype]
376   apply Finset.sum_congr rfl
377   intro a ha
378   exact Module.finrank_linearMap K K _ _
379 
380 /-- Paper I's complete dimension count, including both displayed equalities. -/
381 theorem end_finrank_eq_packet_sum_eq_square
382     {K : Type u} {V : Type v} [Field K]
383     [AddCommGroup V] [Module K V]
384     [FiniteDimensional K V]
385     (P : LinearProjectorFamily K V ι) :
386     Module.finrank K (Module.End K V) =
387         ∑ b, ∑ a,
388           Module.finrank K (LinearMap.range (P.proj a)) *
389             Module.finrank K (LinearMap.range (P.proj b)) ∧
390       (∑ b, ∑ a,
391           Module.finrank K (LinearMap.range (P.proj a)) *
392             Module.finrank K (LinearMap.range (P.proj b))) =
393         (∑ a, Module.finrank K (LinearMap.range (P.proj a))) ^ 2 := by
394   constructor
395   · exact (finrank_end_eq_finrank_blocks P).trans
396       (finrank_blocks_eq_sum_products P)
397   · rw [pow_two, Finset.mul_sum]
398     apply Finset.sum_congr rfl
399     intro b hb
400     rw [Finset.sum_mul]
401 
402 /-! ### Arbitrary packet-Hom support patterns -/
403 
404 /-- A heterogeneous block family is supported on an input-to-output relation. -/
405 def BlocksSupported (P : LinearProjectorFamily R M ι)
406     (rel : ι → ι → Prop) (B : PacketBlocks P) : Prop :=
407   ∀ b a, ¬ rel a b → B b a = 0
408 
409 /-- Universal closure of arbitrary packet-Hom matrices under block multiplication. -/
410 def BlockMulClosed (P : LinearProjectorFamily R M ι)
411     (rel : ι → ι → Prop) : Prop :=
412   ∀ B C : PacketBlocks P,
413     BlocksSupported P rel B → BlocksSupported P rel C →
414       BlocksSupported P rel (blockMul P B C)
415 
416 /-- A single heterogeneous packet block. -/
417 def singleBlock (P : LinearProjectorFamily R M ι)
418     (b a : ι)
419     (f : LinearMap.range (P.proj a) →ₗ[R] LinearMap.range (P.proj b)) :
420     PacketBlocks P :=
421   Pi.single b (Pi.single a f)
422 
423 theorem singleBlock_supported
424     (P : LinearProjectorFamily R M ι) (rel : ι → ι → Prop)
425     {b a : ι} (hab : rel a b)
426     (f : LinearMap.range (P.proj a) →ₗ[R] LinearMap.range (P.proj b)) :
427     BlocksSupported P rel (singleBlock P b a f) := by
428   intro d c hdc
429   classical
430   by_cases hd : d = b
431   · subst d
432     by_cases hc : c = a
433     · subst c
434       exact (hdc hab).elim
435     · simp [singleBlock, hc]
436   · simp [singleBlock, hd]
437 
438 /-- Transitivity is sufficient for closure of every allowed packet-Hom family. -/
439 theorem blockMulClosed_of_transitive
440     (P : LinearProjectorFamily R M ι) (rel : ι → ι → Prop)
441     (htrans : ∀ a c b, rel a c → rel c b → rel a b) :
442     BlockMulClosed P rel := by
443   intro B C hB hC b a hab
444   classical
445   apply LinearMap.ext
446   intro x
447   simp only [blockMul, LinearMap.sum_apply]
448   apply Finset.sum_eq_zero
449   intro c hc
450   by_cases hac : rel a c
451   · have hcb : ¬ rel c b := fun h => hab (htrans a c b hac h)
452     rw [hB b c hcb]
453     simp
454   · rw [hC c a hac]
455     simp
456 
457 /-- Nonzero packet spaces possess two maps with nonzero composite. -/
458 theorem exists_packet_maps_nonzero_comp
459     {K : Type u} {V : Type v} [Field K]
460     [AddCommGroup V] [Module K V]
461     (P : LinearProjectorFamily K V ι)
462     [hpacket : ∀ i, Nontrivial (LinearMap.range (P.proj i))]
463     (a c b : ι) :
464     ∃ f : LinearMap.range (P.proj a) →ₗ[K] LinearMap.range (P.proj c),
465       ∃ g : LinearMap.range (P.proj c) →ₗ[K] LinearMap.range (P.proj b),
466         g.comp f ≠ 0 := by
467   obtain ⟨x, hx⟩ := exists_ne (0 : LinearMap.range (P.proj a))
468   obtain ⟨y, hy⟩ := exists_ne (0 : LinearMap.range (P.proj c))
469   obtain ⟨z, hz⟩ := exists_ne (0 : LinearMap.range (P.proj b))
470   have hxbot : x ∉ (⊥ : Submodule K (LinearMap.range (P.proj a))) := by
471     simpa using hx
472   have hybot : y ∉ (⊥ : Submodule K (LinearMap.range (P.proj c))) := by
473     simpa using hy
474   obtain ⟨lx, hlx0, hlx⟩ :=
475     LinearMap.exists_extend_of_notMem
476       (K := K) (0 : (⊥ : Submodule K (LinearMap.range (P.proj a))) →ₗ[K] K)
477       hxbot 1
478   obtain ⟨ly, hly0, hly⟩ :=
479     LinearMap.exists_extend_of_notMem
480       (K := K) (0 : (⊥ : Submodule K (LinearMap.range (P.proj c))) →ₗ[K] K)
481       hybot 1
482   let f := LinearMap.smulRight lx y
483   let g := LinearMap.smulRight ly z
484   refine ⟨f, g, ?_⟩
485   intro hzero
486   have h := LinearMap.congr_fun hzero x
487   simp [f, g, hlx, hly] at h
488   exact hz h
489 
490 /--
491 For arbitrary maps between nonzero packet spaces, multiplication closure is
492 equivalent to transitivity of the packet support relation.
493 -/
494 theorem blockMulClosed_iff_transitive
495     {K : Type u} {V : Type v} [Field K]
496     [AddCommGroup V] [Module K V]
497     (P : LinearProjectorFamily K V ι)
498     [∀ i, Nontrivial (LinearMap.range (P.proj i))]
499     (rel : ι → ι → Prop) :
500     BlockMulClosed P rel ↔
501       ∀ a c b, rel a c → rel c b → rel a b := by
502   constructor
503   · intro hclosed a c b hac hcb
504     by_contra hab
505     obtain ⟨f, g, hgf⟩ := exists_packet_maps_nonzero_comp P a c b
506     let C := singleBlock P c a f
507     let B := singleBlock P b c g
508     have hC : BlocksSupported P rel C :=
509       singleBlock_supported P rel hac f
510     have hB : BlocksSupported P rel B :=
511       singleBlock_supported P rel hcb g
512     have hzero := hclosed B C hB hC b a hab
513     have hentry : blockMul P B C b a = g.comp f := by
514       classical
515       simp only [blockMul, B, C, singleBlock, Pi.single_eq_same]
516       rw [Fintype.sum_eq_single c]
517       · simp
518       · intro d hdc
519         simp [Pi.single_eq_of_ne hdc]
520     exact hgf (hentry ▸ hzero)
521   · exact blockMulClosed_of_transitive P rel
522 
523 /-- The block identity is supported exactly when the relation is reflexive. -/
524 theorem identity_blocks_supported_iff_reflexive
525     {K : Type u} {V : Type v} [Field K]
526     [AddCommGroup V] [Module K V]
527     (P : LinearProjectorFamily K V ι)
528     [∀ i, Nontrivial (LinearMap.range (P.proj i))]
529     (rel : ι → ι → Prop) :
530     BlocksSupported P rel (restrictBlocks P 1) ↔ ∀ a, rel a a := by
531   constructor
532   · intro h a
533     by_contra haa
534     have hzero := h a a haa
535     obtain ⟨x, hx⟩ := exists_ne (0 : LinearMap.range (P.proj a))
536     have happ := LinearMap.congr_fun hzero x
537     have : x = 0 := by
538       calc
539         x = packetProjection P a (packetInclusion P a x) :=
540           (packetProjection_apply_coe P a x).symm
541         _ = 0 := by simpa [restrictBlocks] using happ
542     exact hx this
543   · intro hrefl b a hab
544     have hba : b ≠ a := by
545       intro h
546       subst b
547       exact hab (hrefl a)
548     ext x
549     exact congrArg Subtype.val (packetProjection_inclusion_ne P hba x)
550 
551 end FullBlocks
552 
553 namespace Reachability
554 
555 open Foundation
556 
557 universe u v w
558 
559 variable {R : Type u} {M : Type v} {ι : Type w}
560 variable [Semiring R] [AddCommMonoid M] [Module R M]
561 variable [Fintype ι]
562 
563 /-- A vector has no packet component outside `S`. -/
564 def VectorSupported (P : LinearProjectorFamily R M ι)
565     (S : Set ι) (x : M) : Prop :=
566   ∀ b, b ∉ S → P.proj b x = 0
567 
568 /-- The vectors supported on `S` form a submodule. -/
569 def supportedSubmodule (P : LinearProjectorFamily R M ι)
570     (S : Set ι) : Submodule R M where
571   carrier := {x | VectorSupported P S x}
572   zero_mem' := by
573     intro b hb
574     simp
575   add_mem' := by
576     intro x y hx hy b hb
577     simp [hx b hb, hy b hb]
578   smul_mem' := by
579     intro c x hx b hb
580     simp [hx b hb]
581 
582 /-- The transfer edge relation generated by a declared operator family. -/
583 def TransferEdge (P : LinearProjectorFamily R M ι)
584     (ops : Set (Module.End R M)) (a b : ι) : Prop :=
585   ∃ T ∈ ops, transferBlock P P T b a ≠ 0
586 
587 /-- Packet `b` is reachable from at least one declared source packet. -/
588 def ReachableFrom (P : LinearProjectorFamily R M ι)
589     (ops : Set (Module.End R M)) (S₀ : Set ι) (b : ι) : Prop :=
590   ∃ a ∈ S₀, Relation.ReflTransGen (TransferEdge P ops) a b
591 
592 theorem reachable_forward
593     (P : LinearProjectorFamily R M ι) (ops : Set (Module.End R M))
594     (S₀ : Set ι) {a b : ι}
595     (ha : ReachableFrom P ops S₀ a) (hab : TransferEdge P ops a b) :
596     ReachableFrom P ops S₀ b := by
597   rcases ha with ⟨s, hs, hsa⟩
598   exact ⟨s, hs, hsa.tail hab⟩
599 
600 /-- Every source packet is reachable by a path of length zero. -/
601 theorem source_reachable
602     (P : LinearProjectorFamily R M ι) (ops : Set (Module.End R M))
603     (S₀ : Set ι) {a : ι} (ha : a ∈ S₀) :
604     ReachableFrom P ops S₀ a :=
605   ⟨a, ha, Relation.ReflTransGen.refl⟩
606 
607 /-- Every declared operator preserves support on the reachable packet set. -/
608 theorem operator_preserves_reachable_support
609     (P : LinearProjectorFamily R M ι) (ops : Set (Module.End R M))
610     (S₀ : Set ι) {T : Module.End R M} (hT : T ∈ ops)
611     {x : M} (hx : VectorSupported P (ReachableFrom P ops S₀) x) :
612     VectorSupported P (ReachableFrom P ops S₀) (T x) := by
613   intro b hb
614   classical
615   calc
616     P.proj b (T x) = P.proj b (T (∑ a, P.proj a x)) := by
617       rw [P.complete]
618     _ = ∑ a, P.proj b (T (P.proj a x)) := by simp
619     _ = 0 := by
620       apply Finset.sum_eq_zero
621       intro a ha
622       by_cases hra : ReachableFrom P ops S₀ a
623       · have hblock : transferBlock P P T b a = 0 := by
624           by_contra hne
625           exact hb (reachable_forward P ops S₀ hra ⟨T, hT, hne⟩)
626         exact LinearMap.congr_fun hblock x
627       · rw [hx a hra]
628         simp
629 
630 /-- A typed word in the declared operator family. -/
631 abbrev OperatorWord (ops : Set (Module.End R M)) :=
632   List {T : Module.End R M // T ∈ ops}
633 
634 /-- Apply an operator word from left to right. -/
635 def wordApply {ops : Set (Module.End R M)} : OperatorWord ops → M → M
636   | [], x => x
637   | T :: word, x => wordApply word (T.1 x)
638 
639 theorem wordApply_preserves_reachable_support
640     (P : LinearProjectorFamily R M ι) (ops : Set (Module.End R M))
641     (S₀ : Set ι) (word : OperatorWord ops) {x : M}
642     (hx : VectorSupported P (ReachableFrom P ops S₀) x) :
643     VectorSupported P (ReachableFrom P ops S₀) (wordApply word x) := by
644   induction word generalizing x with
645   | nil => exact hx
646   | cons T word ih =>
647       exact ih (operator_preserves_reachable_support P ops S₀ T.property hx)
648 
649 /-- The orbit set of seeds under all finite declared operator words. -/
650 def OrbitSet (ops : Set (Module.End R M)) (seeds : Set M) : Set M :=
651   {y | ∃ s ∈ seeds, ∃ word : OperatorWord ops, y = wordApply word s}
652 
653 /-- The algebraic generated hull of a seed family under declared operators. -/
654 def algebraicOrbitHull (ops : Set (Module.End R M))
655     (seeds : Set M) : Submodule R M :=
656   Submodule.span R (OrbitSet ops seeds)
657 
658 /--
659 The complete algebraic reachability theorem: the generated hull is contained
660 in the direct sum of packets reachable from the seed support.
661 -/
662 theorem algebraicOrbitHull_le_reachable_support
663     (P : LinearProjectorFamily R M ι) (ops : Set (Module.End R M))
664     (S₀ : Set ι) (seeds : Set M)
665     (hseeds : ∀ s ∈ seeds, VectorSupported P S₀ s) :
666     algebraicOrbitHull ops seeds ≤
667       supportedSubmodule P (ReachableFrom P ops S₀) := by
668   rw [algebraicOrbitHull, Submodule.span_le]
669   rintro y ⟨s, hs, word, rfl⟩
670   apply wordApply_preserves_reachable_support P ops S₀ word
671   intro b hb
672   exact hseeds s hs b (fun hbS => hb (source_reachable P ops S₀ hbS))
673 
674 /-- A nonzero unreachable packet prevents algebraic generation of the ambient module. -/
675 theorem unreachable_nonzero_packet_obstruction
676     (P : LinearProjectorFamily R M ι) (ops : Set (Module.End R M))
677     (S₀ : Set ι) (seeds : Set M)
678     (hseeds : ∀ s ∈ seeds, VectorSupported P S₀ s)
679     (b : ι) (hb : ¬ ReachableFrom P ops S₀ b)
680     [Nontrivial (LinearMap.range (P.proj b))] :
681     algebraicOrbitHull ops seeds ≠ ⊤ := by
682   intro htop
683   obtain ⟨z, hz⟩ := exists_ne (0 : LinearMap.range (P.proj b))
684   have hzmem : (z : M) ∈ algebraicOrbitHull ops seeds := by
685     rw [htop]
686     trivial
687   have hsupp := algebraicOrbitHull_le_reachable_support P ops S₀ seeds hseeds hzmem
688   have hzero : P.proj b (z : M) = 0 := hsupp b hb
689   rcases z.property with ⟨x, hx⟩
690   have hfixed : P.proj b (z : M) = (z : M) := by
691     rw [← hx]
692     exact P.idempotent b x
693   exact hz (Subtype.ext (hfixed.symm.trans hzero))
694 
695 /-! ### Coordinate invariance of the transfer graph -/
696 
697 variable {N : Type*} [AddCommMonoid N] [Module R N]
698 
699 theorem conjugateEnd_eq_zero_iff (U : M ≃ₗ[R] N) (T : Module.End R M) :
700     Foundation.conjugateEnd U T = 0 ↔ T = 0 := by
701   constructor
702   · intro h
703     ext x
704     have hx := LinearMap.congr_fun h (U x)
705     apply U.injective
706     simpa [Foundation.conjugateEnd] using hx
707   · rintro rfl
708     ext y
709     simp [Foundation.conjugateEnd]
710 
711 theorem conjugate_transferBlock_ne_zero_iff
712     (P : LinearProjectorFamily R M ι) (U : M ≃ₗ[R] N)
713     (T : Module.End R M) (b a : ι) :
714     transferBlock (P.conjugate U) (P.conjugate U)
715         (Foundation.conjugateEnd U T) b a ≠ 0 ↔
716       transferBlock P P T b a ≠ 0 := by
717   rw [Foundation.conjugate_transferBlock]
718   exact not_congr (conjugateEnd_eq_zero_iff U _)
719 
720 /-- The complete transfer-edge relation is unchanged by coordinate conjugation. -/
721 theorem conjugate_transferEdge_iff
722     (P : LinearProjectorFamily R M ι) (U : M ≃ₗ[R] N)
723     (ops : Set (Module.End R M)) (a b : ι) :
724     TransferEdge (P.conjugate U)
725         (Foundation.conjugateEnd U '' ops) a b ↔
726       TransferEdge P ops a b := by
727   constructor
728   · rintro ⟨T', ⟨T, hT, rfl⟩, hblock⟩
729     exact ⟨T, hT, (conjugate_transferBlock_ne_zero_iff P U T b a).mp hblock⟩
730   · rintro ⟨T, hT, hblock⟩
731     exact ⟨Foundation.conjugateEnd U T, ⟨T, hT, rfl⟩,
732       (conjugate_transferBlock_ne_zero_iff P U T b a).mpr hblock⟩
733 
734 /-- Coordinate transport preserves all finite packet reachability statements. -/
735 theorem conjugate_reachableFrom_iff
736     (P : LinearProjectorFamily R M ι) (U : M ≃ₗ[R] N)
737     (ops : Set (Module.End R M)) (S₀ : Set ι) (b : ι) :
738     ReachableFrom (P.conjugate U) (Foundation.conjugateEnd U '' ops) S₀ b ↔
739       ReachableFrom P ops S₀ b := by
740   have hedge : TransferEdge (P.conjugate U)
741       (Foundation.conjugateEnd U '' ops) = TransferEdge P ops := by
742     funext a c
743     exact propext (conjugate_transferEdge_iff P U ops a c)
744   simp only [ReachableFrom, hedge]
745 
746 end Reachability
747 
748 namespace StrictNaturality
749 
750 open Foundation
751 
752 universe u v w x y
753 
754 variable {K : Type u} {M : Type v} {N : Type w}
755 variable {ι : Type x} {κ : Type y}
756 variable [Field K]
757 variable [AddCommGroup M] [Module K M]
758 variable [AddCommGroup N] [Module K N]
759 variable [Fintype ι] [Fintype κ]
760 
761 /--
762 A fully typed strict morphism of finite packet seed systems.  The acting
763 algebras are concrete subalgebras of endomorphisms, so the intertwining law is
764 well-typed without applying an abstract algebra map to an unrelated operator.
765 -/
766 structure StrictSeedMorphism
767     (A : Subalgebra K (Module.End K M))
768     (B : Subalgebra K (Module.End K N))
769     (P : LinearProjectorFamily K M ι)
770     (Q : LinearProjectorFamily K N κ) where
771   linearMap : M →ₗ[K] N
772   algebraMap : A →ₐ[K] B
773   packetMap : ι → κ
774   packetMap_injective : Function.Injective packetMap
775   operator_natural : ∀ T : A,
776     linearMap.comp T.1 = (algebraMap T).1.comp linearMap
777   packet_natural : ∀ a : ι,
778     linearMap.comp (P.proj a) = (Q.proj (packetMap a)).comp linearMap
779 
780 variable {A : Subalgebra K (Module.End K M)}
781 variable {B : Subalgebra K (Module.End K N)}
782 variable {P : LinearProjectorFamily K M ι}
783 variable {Q : LinearProjectorFamily K N κ}
784 
785 /-- The ordinary algebraic orbit of a seed set under a concrete algebra. -/
786 def AlgebraOrbitSet (A : Subalgebra K (Module.End K M))
787     (S : Set M) : Set M :=
788   {x | ∃ T : A, ∃ s ∈ S, x = T.1 s}
789 
790 /-- Algebraic generated hull, expressed as the scalar span of the algebra orbit. -/
791 def AlgebraGeneratedHull (A : Subalgebra K (Module.End K M))
792     (S : Set M) : Submodule K M :=
793   Submodule.span K (AlgebraOrbitSet A S)
794 
795 /-- Orbit in the target under exactly the image of the source algebra. -/
796 def MappedOrbitSet
797     (F : StrictSeedMorphism A B P Q) (S : Set M) : Set N :=
798   {y | ∃ T : A, ∃ s ∈ S,
799     y = (F.algebraMap T).1 (F.linearMap s)}
800 
801 /-- Target hull under exactly the image algebra, rather than all of `B`. -/
802 def MappedGeneratedHull
803     (F : StrictSeedMorphism A B P Q) (S : Set M) : Submodule K N :=
804   Submodule.span K (MappedOrbitSet F S)
805 
806 /-! ### Seed-rank functoriality -/
807 
808 /-- Intertwining converts the source-algebra scalar action into the target action. -/
809 theorem linearMap_smul_of_intertwining
810     (Φ : M →ₗ[K] N) (φ : A →ₐ[K] B)
811     (hnat : ∀ T : A, Φ.comp T.1 = (φ T).1.comp Φ)
812     (T : A) (x : M) :
813     Φ (T • x) = φ T • Φ x := by
814   exact LinearMap.congr_fun (hnat T) x
815 
816 /-- The image of an `A`-span lies in the `B`-span of the image seeds. -/
817 theorem map_mem_span_image_of_intertwining
818     (Φ : M →ₗ[K] N) (φ : A →ₐ[K] B)
819     (hnat : ∀ T : A, Φ.comp T.1 = (φ T).1.comp Φ)
820     (S : Set M) {x : M} (hx : x ∈ Submodule.span A S) :
821     Φ x ∈ Submodule.span B (Φ '' S) := by
822   induction hx using Submodule.span_induction with
823   | mem x hx =>
824       exact Submodule.subset_span ⟨x, hx, rfl⟩
825   | zero => simp
826   | add x y hx hy ihx ihy =>
827       simpa using (Submodule.add_mem _ ihx ihy)
828   | smul T x hx ih =>
829       rw [linearMap_smul_of_intertwining Φ φ hnat]
830       exact Submodule.smul_mem _ (φ T) ih
831 
832 /-- A surjective intertwiner sends generators to generators. -/
833 theorem image_generates_of_surjective_intertwining
834     (Φ : M →ₗ[K] N) (φ : A →ₐ[K] B)
835     (hnat : ∀ T : A, Φ.comp T.1 = (φ T).1.comp Φ)
836     (hΦ : Function.Surjective Φ) (S : Set M)
837     (hS : SeedRankBasics.Generates A M S) :
838     SeedRankBasics.Generates B N (Φ '' S) := by
839   rw [SeedRankBasics.Generates]
840   apply top_unique
841   intro y hy
842   obtain ⟨x, rfl⟩ := hΦ y
843   apply map_mem_span_image_of_intertwining Φ φ hnat S
844   rw [hS]
845   trivial
846 
847 /-- Seed rank cannot increase through a surjective algebra intertwiner. -/
848 theorem seedRank_le_of_surjective_intertwining
849     (Φ : M →ₗ[K] N) (φ : A →ₐ[K] B)
850     (hnat : ∀ T : A, Φ.comp T.1 = (φ T).1.comp Φ)
851     (hΦ : Function.Surjective Φ) :
852     Cardinal.lift.{v} (SeedRankBasics.seedRank B N) ≤
853       Cardinal.lift.{w} (SeedRankBasics.seedRank A M) := by
854   obtain ⟨S, hS, hcard⟩ :=
855     SeedRankBasics.exists_generating_set_card_eq_seedRank A M
856   have himage : SeedRankBasics.Generates B N (Φ '' S) :=
857     image_generates_of_surjective_intertwining Φ φ hnat hΦ S hS
858   have hrank := SeedRankBasics.seedRank_le_mk_of_generates B N himage
859   calc
860     Cardinal.lift.{v} (SeedRankBasics.seedRank B N) ≤
861         Cardinal.lift.{v} (Cardinal.mk (Φ '' S)) := Cardinal.lift_le.2 hrank
862     _ ≤ Cardinal.lift.{w} (Cardinal.mk S) := Cardinal.mk_image_le_lift
863     _ = Cardinal.lift.{w} (SeedRankBasics.seedRank A M) :=
864       congrArg Cardinal.lift hcard
865 
866 /-- Paper I's seed-rank inequality for a surjective strict morphism. -/
867 theorem strict_seedRank_le
868     (F : StrictSeedMorphism A B P Q)
869     (hΦ : Function.Surjective F.linearMap) :
870     Cardinal.lift.{v} (SeedRankBasics.seedRank B N) ≤
871       Cardinal.lift.{w} (SeedRankBasics.seedRank A M) :=
872   seedRank_le_of_surjective_intertwining F.linearMap F.algebraMap
873     F.operator_natural hΦ
874 
875 /--
876 If the realization map is bijective and the acting-algebra map is an
877 isomorphism, seed rank is preserved exactly.
878 -/
879 theorem strict_seedRank_eq_of_bijective
880     (F : StrictSeedMorphism A B P Q)
881     (hΦ : Function.Bijective F.linearMap)
882     (hφ : Function.Bijective F.algebraMap) :
883     Cardinal.lift.{w} (SeedRankBasics.seedRank A M) =
884       Cardinal.lift.{v} (SeedRankBasics.seedRank B N) := by
885   let Φe : M ≃ₗ[K] N := LinearEquiv.ofBijective F.linearMap hΦ
886   let φe : A ≃ₐ[K] B := AlgEquiv.ofBijective F.algebraMap hφ
887   have hreverse : ∀ T : B,
888       Φe.symm.toLinearMap.comp T.1 =
889         (φe.symm T).1.comp Φe.symm.toLinearMap := by
890     intro T
891     ext y
892     change Φe.symm (T.1 y) = (φe.symm T).1 (Φe.symm y)
893     apply Φe.injective
894     rw [Φe.apply_symm_apply]
895     symm
896     have hφinv : F.algebraMap (φe.symm T) = T := by
897       change φe (φe.symm T) = T
898       exact φe.apply_symm_apply T
899     calc
900       Φe ((φe.symm T).1 (Φe.symm y)) =
901           (F.algebraMap (φe.symm T)).1 (Φe (Φe.symm y)) := by
902         exact LinearMap.congr_fun (F.operator_natural (φe.symm T)) (Φe.symm y)
903       _ = T.1 y := by rw [hφinv, Φe.apply_symm_apply]
904   apply le_antisymm
905   · exact seedRank_le_of_surjective_intertwining
906       Φe.symm.toLinearMap φe.symm.toAlgHom hreverse Φe.symm.surjective
907   · exact strict_seedRank_le F hΦ.2
908 
909 theorem map_algebraOrbitSet
910     (F : StrictSeedMorphism A B P Q) (S : Set M) :
911     F.linearMap '' AlgebraOrbitSet A S = MappedOrbitSet F S := by
912   ext y
913   constructor
914   · rintro ⟨x, ⟨T, s, hs, rfl⟩, rfl⟩
915     refine ⟨T, s, hs, ?_⟩
916     have h := LinearMap.congr_fun (F.operator_natural T) s
917     simpa using h
918   · rintro ⟨T, s, hs, rfl⟩
919     refine ⟨T.1 s, ⟨T, s, hs, rfl⟩, ?_⟩
920     have h := LinearMap.congr_fun (F.operator_natural T) s
921     simpa using h
922 
923 /-- Exact naturality of the algebraically generated hull. -/
924 theorem generatedHull_natural
925     (F : StrictSeedMorphism A B P Q) (S : Set M) :
926     Submodule.map F.linearMap (AlgebraGeneratedHull A S) =
927       MappedGeneratedHull F S := by
928   rw [AlgebraGeneratedHull, MappedGeneratedHull, Submodule.map_span]
929   exact congrArg (Submodule.span K) (map_algebraOrbitSet F S)
930 
931 /-- A generating source family maps to a generator for the image algebra when `Φ` is onto. -/
932 theorem mappedGeneratedHull_eq_top
933     (F : StrictSeedMorphism A B P Q) (S : Set M)
934     (hS : AlgebraGeneratedHull A S = ⊤)
935     (hΦ : Function.Surjective F.linearMap) :
936     MappedGeneratedHull F S = ⊤ := by
937   rw [← generatedHull_natural F S, hS, Submodule.map_top,
938     LinearMap.range_eq_top.mpr hΦ]
939 
940 /-- Packet analysis commutes with every strict morphism. -/
941 theorem packet_natural_apply
942     (F : StrictSeedMorphism A B P Q) (a : ι) (x : M) :
943     F.linearMap (P.proj a x) =
944       Q.proj (F.packetMap a) (F.linearMap x) := by
945   exact LinearMap.congr_fun (F.packet_natural a) x
946 
947 /-- Type-correct block naturality for any separately intertwined operators. -/
948 theorem transferBlock_natural_general
949     (F : StrictSeedMorphism A B P Q)
950     (T : Module.End K M) (T' : Module.End K N)
951     (hT : F.linearMap.comp T = T'.comp F.linearMap)
952     (b a : ι) :
953     F.linearMap.comp (transferBlock P P T b a) =
954       (transferBlock Q Q T' (F.packetMap b) (F.packetMap a)).comp
955         F.linearMap := by
956   ext x
957   have hb (z : M) :
958       F.linearMap (P.proj b z) = Q.proj (F.packetMap b) (F.linearMap z) :=
959     packet_natural_apply F b z
960   have ha :
961       F.linearMap (P.proj a x) = Q.proj (F.packetMap a) (F.linearMap x) :=
962     packet_natural_apply F a x
963   have hTx (z : M) : F.linearMap (T z) = T' (F.linearMap z) := by
964     exact LinearMap.congr_fun hT z
965   change F.linearMap (P.proj b (T (P.proj a x))) =
966     Q.proj (F.packetMap b)
967       (T' (Q.proj (F.packetMap a) (F.linearMap x)))
968   rw [hb, hTx, ha]
969 
970 /-- Block naturality for an operator belonging to the source acting algebra. -/
971 theorem transferBlock_natural_algebra
972     (F : StrictSeedMorphism A B P Q) (T : A) (b a : ι) :
973     F.linearMap.comp (transferBlock P P T.1 b a) =
974       (transferBlock Q Q (F.algebraMap T).1
975         (F.packetMap b) (F.packetMap a)).comp F.linearMap :=
976   transferBlock_natural_general F T.1 (F.algebraMap T).1
977     (F.operator_natural T) b a
978 
979 /-- Under a bijective realization map, corresponding blocks vanish simultaneously. -/
980 theorem transferBlock_eq_zero_iff_of_bijective
981     (F : StrictSeedMorphism A B P Q)
982     (hbij : Function.Bijective F.linearMap)
983     (T : A) (b a : ι) :
984     transferBlock P P T.1 b a = 0 ↔
985       transferBlock Q Q (F.algebraMap T).1
986         (F.packetMap b) (F.packetMap a) = 0 := by
987   let S := transferBlock P P T.1 b a
988   let S' := transferBlock Q Q (F.algebraMap T).1
989     (F.packetMap b) (F.packetMap a)
990   have hnat : F.linearMap.comp S = S'.comp F.linearMap :=
991     transferBlock_natural_algebra F T b a
992   constructor
993   · intro hS
994     apply LinearMap.ext
995     intro y
996     obtain ⟨x, rfl⟩ := hbij.2 y
997     have h := LinearMap.congr_fun hnat x
998     simpa [S, S', hS] using h.symm
999   · intro hS'
1000     apply LinearMap.ext
1001     intro x
1002     apply hbij.1
1003     have h := LinearMap.congr_fun hnat x
1004     simpa [S, S', hS'] using h
1005 
1006 /-- An input-output packet pair is an edge for at least one algebra operator. -/
1007 def AlgebraTransferEdge
1008     (A : Subalgebra K (Module.End K M))
1009     (P : LinearProjectorFamily K M ι) (a b : ι) : Prop :=
1010   ∃ T : A, transferBlock P P T.1 b a ≠ 0
1011 
1012 /-- Every algebra operator has a zero block at the given input-output pair. -/
1013 def AlgebraZeroAt
1014     (A : Subalgebra K (Module.End K M))
1015     (P : LinearProjectorFamily K M ι) (a b : ι) : Prop :=
1016   ∀ T : A, transferBlock P P T.1 b a = 0
1017 
1018 /-- The complete edge pattern of the acting algebra. -/
1019 def AlgebraTransferPattern
1020     (A : Subalgebra K (Module.End K M))
1021     (P : LinearProjectorFamily K M ι) : Set (ι × ι) :=
1022   {ab | AlgebraTransferEdge A P ab.1 ab.2}
1023 
1024 /-- The complete universal-zero pattern of the acting algebra. -/
1025 def AlgebraZeroPattern
1026     (A : Subalgebra K (Module.End K M))
1027     (P : LinearProjectorFamily K M ι) : Set (ι × ι) :=
1028   {ab | AlgebraZeroAt A P ab.1 ab.2}
1029 
1030 theorem algebraTransferEdge_iff_of_bijective
1031     (F : StrictSeedMorphism A B P Q)
1032     (hΦ : Function.Bijective F.linearMap)
1033     (hφ : Function.Surjective F.algebraMap)
1034     (a b : ι) :
1035     AlgebraTransferEdge A P a b ↔
1036       AlgebraTransferEdge B Q (F.packetMap a) (F.packetMap b) := by
1037   constructor
1038   · rintro ⟨T, hT⟩
1039     refine ⟨F.algebraMap T, ?_⟩
1040     exact (not_congr (transferBlock_eq_zero_iff_of_bijective F hΦ T b a)).mp hT
1041   · rintro ⟨T', hT'⟩
1042     obtain ⟨T, rfl⟩ := hφ T'
1043     refine ⟨T, ?_⟩
1044     exact (not_congr (transferBlock_eq_zero_iff_of_bijective F hΦ T b a)).mpr hT'
1045 
1046 theorem algebraZeroAt_iff_of_bijective
1047     (F : StrictSeedMorphism A B P Q)
1048     (hΦ : Function.Bijective F.linearMap)
1049     (hφ : Function.Surjective F.algebraMap)
1050     (a b : ι) :
1051     AlgebraZeroAt A P a b ↔
1052       AlgebraZeroAt B Q (F.packetMap a) (F.packetMap b) := by
1053   constructor
1054   · intro hsource T'
1055     obtain ⟨T, rfl⟩ := hφ T'
1056     exact (transferBlock_eq_zero_iff_of_bijective F hΦ T b a).mp (hsource T)
1057   · intro htarget T
1058     exact (transferBlock_eq_zero_iff_of_bijective F hΦ T b a).mpr
1059       (htarget (F.algebraMap T))
1060 
1061 /--
1062 A bijective strict morphism identifies the entire transfer-edge pattern and
1063 the entire universal-zero pattern.  Bijectivity of `packetMap` makes the pair
1064 map a bijection, while surjectivity of the algebra map ensures that no target
1065 operator is omitted.
1066 -/
1067 theorem full_transfer_edge_zero_pattern_correspondence
1068     (F : StrictSeedMorphism A B P Q)
1069     (hΦ : Function.Bijective F.linearMap)
1070     (hφ : Function.Bijective F.algebraMap)
1071     (hpacket : Function.Bijective F.packetMap) :
1072     Function.Bijective (Prod.map F.packetMap F.packetMap) ∧
1073       (Prod.map F.packetMap F.packetMap) ⁻¹'
1074           AlgebraTransferPattern B Q = AlgebraTransferPattern A P ∧
1075       (Prod.map F.packetMap F.packetMap) ⁻¹'
1076           AlgebraZeroPattern B Q = AlgebraZeroPattern A P := by
1077   refine ⟨hpacket.prodMap hpacket, ?_, ?_⟩
1078   · ext ab
1079     change AlgebraTransferEdge B Q (F.packetMap ab.1) (F.packetMap ab.2) ↔
1080       AlgebraTransferEdge A P ab.1 ab.2
1081     exact (algebraTransferEdge_iff_of_bijective F hΦ hφ.2 ab.1 ab.2).symm
1082   · ext ab
1083     change AlgebraZeroAt B Q (F.packetMap ab.1) (F.packetMap ab.2) ↔
1084       AlgebraZeroAt A P ab.1 ab.2
1085     exact (algebraZeroAt_iff_of_bijective F hΦ hφ.2 ab.1 ab.2).symm
1086 
1087 /-- A compact theorem bundling generation, packets, blocks, and label injectivity. -/
1088 theorem strict_naturality_package
1089     (F : StrictSeedMorphism A B P Q) (S : Set M) :
1090     Submodule.map F.linearMap (AlgebraGeneratedHull A S) =
1091         MappedGeneratedHull F S ∧
1092       (∀ a x, F.linearMap (P.proj a x) =
1093         Q.proj (F.packetMap a) (F.linearMap x)) ∧
1094       (∀ (T : A) b a,
1095         F.linearMap.comp (transferBlock P P T.1 b a) =
1096           (transferBlock Q Q (F.algebraMap T).1
1097             (F.packetMap b) (F.packetMap a)).comp F.linearMap) ∧
1098       Function.Injective F.packetMap := by
1099   exact ⟨generatedHull_natural F S, packet_natural_apply F,
1100     transferBlock_natural_algebra F, F.packetMap_injective⟩
1101 
1102 end StrictNaturality
1103 
1104 namespace TypedQuiver
1105 
1106 open Reachability
1107 
1108 universe u
1109 
1110 variable {K : Type u} [Field K]
1111 
1112 /-- The two-dimensional source vertex in the displayed quiver. -/
1113 abbrev U (K : Type u) := Fin 2 → K
1114 
1115 /-- The three-dimensional target vertex in the displayed quiver. -/
1116 abbrev V (K : Type u) := Fin 3 → K
1117 
1118 /-- The total vertex-graded representation space. -/
1119 abbrev X (K : Type u) := U K × V K
1120 
1121 def eU₁ : U K := ![1, 0]
1122 def eU₂ : U K := ![0, 1]
1123 def eV₁ : V K := ![1, 0, 0]
1124 def eV₂ : V K := ![0, 1, 0]
1125 def eV₃ : V K := ![0, 0, 1]
1126 
1127 /-- The rotation `R(u₁,u₂)=(-u₂,u₁)`. -/
1128 def rotation : U K →ₗ[K] U K where
1129   toFun u := ![-u 1, u 0]
1130   map_add' u v := by
1131     funext i
1132     fin_cases i <;> simp <;> ring
1133   map_smul' c u := by
1134     funext i
1135     fin_cases i <;> simp
1136 
1137 /-- The arrow `A(u₁,u₂)=(u₁,u₂,0)`. -/
1138 def arrowA : U K →ₗ[K] V K where
1139   toFun u := ![u 0, u 1, 0]
1140   map_add' u v := by
1141     funext i
1142     fin_cases i <;> simp
1143   map_smul' c u := by
1144     funext i
1145     fin_cases i <;> simp
1146 
1147 /-- The arrow `B(v₁,v₂,v₃)=(v₁,v₂)`. -/
1148 def arrowB : V K →ₗ[K] U K where
1149   toFun v := ![v 0, v 1]
1150   map_add' v w := by
1151     funext i
1152     fin_cases i <;> simp
1153   map_smul' c v := by
1154     funext i
1155     fin_cases i <;> simp
1156 
1157 /-- The bound-quiver relation `BA=e_U` holds exactly. -/
1158 theorem arrowB_comp_arrowA :
1159     (arrowB (K := K)).comp (arrowA (K := K)) = LinearMap.id := by
1160   ext u i
1161   fin_cases i <;> rfl
1162 
1163 @[simp] theorem rotation_eU₁ : rotation (K := K) eU₁ = eU₂ := by
1164   funext i
1165   fin_cases i <;> simp [rotation, eU₁, eU₂]
1166 
1167 @[simp] theorem arrowA_eU₁ : arrowA (K := K) eU₁ = eV₁ := by
1168   funext i
1169   fin_cases i <;> simp [arrowA, eU₁, eV₁]
1170 
1171 @[simp] theorem arrowA_eU₂ : arrowA (K := K) eU₂ = eV₂ := by
1172   funext i
1173   fin_cases i <;> simp [arrowA, eU₂, eV₂]
1174 
1175 @[simp] theorem arrowB_eV₃ : arrowB (K := K) eV₃ = 0 := by
1176   funext i
1177   fin_cases i <;> simp [arrowB, eV₃]
1178 
1179 theorem eV₃_ne_zero : eV₃ (K := K) ≠ 0 := by
1180   intro h
1181   have := congrFun h 2
1182   simpa [eV₃] using this
1183 
1184 /-- The missing third direction is a nonzero vector in `ker B`. -/
1185 theorem eV₃_mem_ker_arrowB :
1186     eV₃ (K := K) ∈ LinearMap.ker (arrowB (K := K)) := by
1187   simp
1188 
1189 /-- Every vector in `im A` has zero third coordinate. -/
1190 theorem range_arrowA_third_zero
1191     {v : V K} (hv : v ∈ LinearMap.range (arrowA (K := K))) :
1192     v 2 = 0 := by
1193   rcases hv with ⟨u, rfl⟩
1194   rfl
1195 
1196 /-- The kernel direction is not reachable through the arrow `A`. -/
1197 theorem eV₃_not_mem_range_arrowA :
1198     eV₃ (K := K) ∉ LinearMap.range (arrowA (K := K)) := by
1199   intro h
1200   have := range_arrowA_third_zero h
1201   simpa [eV₃] using this
1202 
1203 /-- `R` acting on the source vertex and zero on the target vertex. -/
1204 def totalR : Module.End K (X K) where
1205   toFun x := (rotation x.1, 0)
1206   map_add' x y := by
1207     ext <;> simp
1208   map_smul' c x := by
1209     ext <;> simp
1210 
1211 /-- The typed arrow `A`, extended by zero away from its source vertex. -/
1212 def totalA : Module.End K (X K) where
1213   toFun x := (0, arrowA x.1)
1214   map_add' x y := by
1215     ext <;> simp
1216   map_smul' c x := by
1217     ext <;> simp
1218 
1219 /-- The typed arrow `B`, extended by zero away from its source vertex. -/
1220 def totalB : Module.End K (X K) where
1221   toFun x := (arrowB x.2, 0)
1222   map_add' x y := by
1223     ext <;> simp
1224   map_smul' c x := by
1225     ext <;> simp
1226 
1227 /-- The three primitive operators of the finite typed quiver. -/
1228 def quiverOps : Set (Module.End K (X K)) :=
1229   {totalR, totalA, totalB}
1230 
1231 /-- The invariant proper subrepresentation reachable from the `U` vertex. -/
1232 def uReachableSubmodule : Submodule K (X K) where
1233   carrier := {x | x.2 2 = 0}
1234   zero_mem' := by simp
1235   add_mem' := by
1236     intro x y hx hy
1237     change x.2 2 + y.2 2 = 0
1238     change x.2 2 = 0 at hx
1239     change y.2 2 = 0 at hy
1240     rw [hx, hy, add_zero]
1241   smul_mem' := by
1242     intro c x hx
1243     change c * x.2 2 = 0
1244     change x.2 2 = 0 at hx
1245     rw [hx, mul_zero]
1246 
1247 theorem quiverOp_preserves_uReachable
1248     {T : Module.End K (X K)} (hT : T ∈ quiverOps)
1249     {x : X K} (hx : x ∈ uReachableSubmodule) :
1250     T x ∈ uReachableSubmodule := by
1251   simp only [quiverOps, Set.mem_insert_iff, Set.mem_singleton_iff] at hT
1252   rcases hT with rfl | rfl | rfl
1253   · simp [uReachableSubmodule, totalR]
1254   · simp [uReachableSubmodule, totalA, arrowA]
1255   · simp [uReachableSubmodule, totalB]
1256 
1257 theorem quiverWord_preserves_uReachable
1258     (word : OperatorWord (quiverOps (K := K)))
1259     {x : X K} (hx : x ∈ uReachableSubmodule) :
1260     wordApply word x ∈ uReachableSubmodule := by
1261   induction word generalizing x with
1262   | nil => exact hx
1263   | cons T word ih =>
1264       exact ih (quiverOp_preserves_uReachable T.property hx)
1265 
1266 /-- Every seed family supported at `U` generates only the proper `U ⊕ im A` plane. -/
1267 theorem u_supported_hull_le_uReachable
1268     (seeds : Set (X K)) (hseeds : ∀ s ∈ seeds, s.2 = 0) :
1269     algebraicOrbitHull (quiverOps (K := K)) seeds ≤ uReachableSubmodule := by
1270   rw [algebraicOrbitHull, Submodule.span_le]
1271   rintro y ⟨s, hs, word, rfl⟩
1272   apply quiverWord_preserves_uReachable word
1273   simpa [uReachableSubmodule, hseeds s hs]
1274 
1275 /-- No family supported solely at `U` generates the full quiver representation. -/
1276 theorem no_u_supported_seeds_generate
1277     (seeds : Set (X K)) (hseeds : ∀ s ∈ seeds, s.2 = 0) :
1278     algebraicOrbitHull (quiverOps (K := K)) seeds ≠ ⊤ := by
1279   intro htop
1280   let missing : X K := (0, eV₃)
1281   have hmem : missing ∈ algebraicOrbitHull (quiverOps (K := K)) seeds := by
1282     rw [htop]
1283     trivial
1284   have hplane := u_supported_hull_le_uReachable seeds hseeds hmem
1285   have : (1 : K) = 0 := by
1286     simpa [missing, uReachableSubmodule, eV₃] using hplane
1287   exact one_ne_zero this
1288 
1289 /-- The two displayed seeds `e₁ ∈ U` and `e₃ ∈ V`. -/
1290 def sourceSeed : X K := (eU₁, 0)
1291 def missingSeed : X K := (0, eV₃)
1292 def certificateSeeds : Set (X K) := {sourceSeed, missingSeed}
1293 
1294 theorem orbit_mem_hull
1295     {seeds : Set (X K)} {s : X K} (hs : s ∈ seeds)
1296     (word : OperatorWord (quiverOps (K := K))) :
1297     wordApply word s ∈ algebraicOrbitHull (quiverOps (K := K)) seeds := by
1298   exact Submodule.subset_span ⟨s, hs, word, rfl⟩
1299 
1300 /-- The two certified seeds generate all five coordinate directions. -/
1301 theorem certificateSeeds_generate :
1302     algebraicOrbitHull (quiverOps (K := K))
1303       (certificateSeeds (K := K)) = ⊤ := by
1304   apply top_unique
1305   rintro ⟨u, v⟩ htop
1306   let rOp : {T : Module.End K (X K) // T ∈ quiverOps} :=
1307     ⟨totalR, by simp [quiverOps]⟩
1308   let aOp : {T : Module.End K (X K) // T ∈ quiverOps} :=
1309     ⟨totalA, by simp [quiverOps]⟩
1310   have hsU : sourceSeed (K := K) ∈ certificateSeeds := by
1311     simp [certificateSeeds]
1312   have hsV : missingSeed (K := K) ∈ certificateSeeds := by
1313     simp [certificateSeeds]
1314   have hu₁ : sourceSeed (K := K) ∈
1315       algebraicOrbitHull (quiverOps (K := K)) certificateSeeds :=
1316     orbit_mem_hull hsU []
1317   have hu₂ : totalR (sourceSeed (K := K)) ∈
1318       algebraicOrbitHull (quiverOps (K := K)) certificateSeeds :=
1319     orbit_mem_hull hsU [rOp]
1320   have hv₁ : totalA (sourceSeed (K := K)) ∈
1321       algebraicOrbitHull (quiverOps (K := K)) certificateSeeds :=
1322     orbit_mem_hull hsU [aOp]
1323   have hv₂ : totalA (totalR (sourceSeed (K := K))) ∈
1324       algebraicOrbitHull (quiverOps (K := K)) certificateSeeds :=
1325     orbit_mem_hull hsU [rOp, aOp]
1326   have hv₃ : missingSeed (K := K) ∈
1327       algebraicOrbitHull (quiverOps (K := K)) certificateSeeds :=
1328     orbit_mem_hull hsV []
1329   have hdecomp :
1330       (u, v) =
1331         u 0 • sourceSeed +
1332         u 1 • totalR sourceSeed +
1333         v 0 • totalA sourceSeed +
1334         v 1 • totalA (totalR sourceSeed) +
1335         v 2 • missingSeed := by
1336     apply Prod.ext
1337     · funext i
1338       fin_cases i <;>
1339         simp [sourceSeed, missingSeed, totalR, totalA, rotation, arrowA,
1340           eU₁, eV₃]
1341     · funext i
1342       fin_cases i <;>
1343         simp [sourceSeed, missingSeed, totalR, totalA, rotation, arrowA,
1344           eU₁, eV₃]
1345   rw [hdecomp]
1346   apply Submodule.add_mem
1347   · apply Submodule.add_mem
1348     · apply Submodule.add_mem
1349       · apply Submodule.add_mem
1350         · exact Submodule.smul_mem _ (u 0) hu₁
1351         · exact Submodule.smul_mem _ (u 1) hu₂
1352       · exact Submodule.smul_mem _ (v 0) hv₁
1353     · exact Submodule.smul_mem _ (v 1) hv₂
1354   · exact Submodule.smul_mem _ (v 2) hv₃
1355 
1356 /-- The complete finite typed-quiver certificate from Paper I. -/
1357 theorem typed_reachability_certificate :
1358     (arrowB (K := K)).comp arrowA = LinearMap.id ∧
1359       eV₃ (K := K) ∈ LinearMap.ker arrowB ∧
1360       eV₃ (K := K) ∉ LinearMap.range arrowA ∧
1361       (∀ seeds : Set (X K), (∀ s ∈ seeds, s.2 = 0) →
1362         algebraicOrbitHull (quiverOps (K := K)) seeds ≠ ⊤) ∧
1363       algebraicOrbitHull (quiverOps (K := K)) certificateSeeds = ⊤ := by
1364   exact ⟨arrowB_comp_arrowA, eV₃_mem_ker_arrowB,
1365     eV₃_not_mem_range_arrowA, no_u_supported_seeds_generate,
1366     certificateSeeds_generate⟩
1367 
1368 end TypedQuiver
1369 
1370 end Komorebi.PacketNaturalityCompletion

Back to source controls