PacketUniversal.lean

1 import KomorebiVerification.ExactCoordinates
2 import KomorebiVerification.PaperIBlockCompletion
3 
4 set_option autoImplicit false
5 noncomputable section
6 namespace Komorebi.PaperIRelease.PacketUniversal
7 open Komorebi.Foundation Komorebi.Foundation.LinearProjectorFamily
8 universe u v w x y
9 variable {R : Type u} [CommSemiring R]
10 variable {M : Type v} [AddCommMonoid M] [Module R M]
11 variable {N : Type w} [AddCommMonoid N] [Module R N]
12 variable {ι : Type x} [Fintype ι]
13 variable (P : LinearProjectorFamily R M ι)
14 
15 /-- Projection with its actual range as codomain. -/
16 def packetProjection (i : ι) : M →ₗ[R] (P.proj i).range := (P.proj i).rangeRestrict
17 
18 /-- Extend linear maps out of every packet by the finite sum. -/
19 def assembleOut (f : (i : ι) → (P.proj i).range →ₗ[R] N) : M →ₗ[R] N :=
20   ∑ i, (f i).comp (packetProjection P i)
21 
22 @[simp] theorem assembleOut_packet (f : (i : ι) → (P.proj i).range →ₗ[R] N)
23     (i : ι) (m : (P.proj i).range) : assembleOut P f m = f i m := by
24   classical
25   rw [assembleOut, LinearMap.sum_apply, Finset.sum_eq_single i]
26   · change f i (packetProjection P i m) = f i m
27     congr 1
28     apply Subtype.ext
29     obtain ⟨x, hx⟩ := m.property
30     change P.proj i m = m
31     rw [← hx]
32     exact P.idempotent i x
33   · intro j _ hji
34     change f j (packetProjection P j m) = 0
35     have hz : packetProjection P j m = 0 := by
36       apply Subtype.ext
37       obtain ⟨x, hx⟩ := m.property
38       change P.proj j m = 0
39       rw [← hx]
40       exact P.orthogonal hji x
41     rw [hz, map_zero]
42   · simp
43 
44 /-- Existence and uniqueness of extension from the actual packet inclusions. -/
45 theorem unique_packet_extension (f : (i : ι) → (P.proj i).range →ₗ[R] N) :
46     ∃! g : M →ₗ[R] N, ∀ (i : ι) (m : (P.proj i).range), g (m : M) = f i m := by
47   refine ⟨assembleOut P f, assembleOut_packet P f, ?_⟩
48   intro g hg
49   ext m
50   rw [← P.complete m, map_sum, map_sum]
51   apply Finset.sum_congr rfl
52   intro i _
53   exact (hg i ⟨P.proj i m, ⟨m, rfl⟩⟩).trans
54     (assembleOut_packet P f i ⟨P.proj i m, ⟨m, rfl⟩⟩).symm
55 
56 /-- Assemble linear maps into the packets using actual synthesis. -/
57 def assembleIn (f : (i : ι) → N →ₗ[R] (P.proj i).range) : N →ₗ[R] M :=
58   P.rangeSynthesis.comp (LinearMap.pi f)
59 
60 @[simp] theorem packet_assembleIn (f : (i : ι) → N →ₗ[R] (P.proj i).range)
61     (i : ι) (n : N) : packetProjection P i (assembleIn P f n) = f i n := by
62   exact congrFun (P.rangeAnalysis_rangeSynthesis (fun j => f j n)) i
63 
64 /-- Existence and uniqueness of assembly into actual packet ranges. -/
65 theorem unique_packet_lift (f : (i : ι) → N →ₗ[R] (P.proj i).range) :
66     ∃! g : N →ₗ[R] M, ∀ i n, packetProjection P i (g n) = f i n := by
67   refine ⟨assembleIn P f, packet_assembleIn P f, ?_⟩
68   intro g hg
69   ext n
70   apply P.exactPacketCoordinates.injective
71   funext i
72   exact (hg i n).trans (packet_assembleIn P f i n).symm
73 
74 /-- A linear map is determined by all its transfer blocks. -/
75 theorem transferBlock_ext {κ : Type y} [Fintype κ]
76     (Q : LinearProjectorFamily R N κ) (U V : M →ₗ[R] N)
77     (h : ∀ j i, transferBlock P Q U j i = transferBlock P Q V j i) : U = V := by
78   rw [← transferBlock_reconstruction_linearMap P Q U,
79     ← transferBlock_reconstruction_linearMap P Q V]
80   apply Finset.sum_congr rfl
81   intro j _
82   apply Finset.sum_congr rfl
83   intro i _
84   exact h j i
85 
86 /-- The full blockwise intertwining equivalence, with distinct source and target packets. -/
87 theorem block_intertwining_iff {κ : Type y} [Fintype κ]
88     (Q : LinearProjectorFamily R N κ) (T : Module.End R M)
89     (S : Module.End R N) (U : M →ₗ[R] N) :
90     U.comp T = S.comp U ↔ ∀ j i,
91       (∑ b, (transferBlock P Q U j b).comp (transferBlock P P T b i)) =
92       ∑ d, (transferBlock Q Q S j d).comp (transferBlock P Q U d i) := by
93   constructor
94   · intro h j i
95     rw [← transferBlock_comp_linearMap P P Q T U,
96       ← transferBlock_comp_linearMap P Q Q U S, h]
97   · intro h
98     apply transferBlock_ext P Q
99     intro j i
100     rw [transferBlock_comp_linearMap P P Q T U,
101       transferBlock_comp_linearMap P Q Q U S]
102     exact h j i
103 
104 end Komorebi.PaperIRelease.PacketUniversal

Back to source controls