TensorPackets.lean

1 import KomorebiVerification.PacketNaturalityCompletion
2 import Mathlib.LinearAlgebra.TensorProduct.Map
3 import Mathlib.LinearAlgebra.Dual.Defs
4 
5 set_option autoImplicit false
6 set_option maxHeartbeats 2000000
7 
8 namespace Komorebi.PaperIRelease
9 open Komorebi.Foundation
10 open TensorProduct
11 
12 universe u v w v' w'
13 variable {K : Type u} [Field K]
14 variable {X : Type v} [AddCommGroup X] [Module K X]
15 variable {Y : Type w} [AddCommGroup Y] [Module K Y]
16 variable {I : Type v'} [Fintype I] {J : Type w'} [Fintype J]
17 
18 /-- The actual tensor maps of the two given families, with all packet laws proved. -/
19 noncomputable def tensorPackets
20     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J) :
21     LinearProjectorFamily K (X ⊗[K] Y) (I × J) where
22   proj ij := TensorProduct.map (P.proj ij.1) (Q.proj ij.2)
23   idempotent ij z := by
24     induction z using TensorProduct.induction_on with
25     | zero => simp
26     | tmul x y => simp only [TensorProduct.map_tmul, P.idempotent, Q.idempotent]
27     | add a b ha hb => simp only [map_add, ha, hb]
28   orthogonal := by
29     intro ij kl h z
30     induction z using TensorProduct.induction_on with
31     | zero => simp
32     | tmul x y =>
33       by_cases h1 : ij.1 = kl.1
34       · have h2 : ij.2 ≠ kl.2 := fun h2 => h (Prod.ext h1 h2)
35         simp only [TensorProduct.map_tmul, Q.orthogonal h2, tmul_zero]
36       · simp only [TensorProduct.map_tmul, P.orthogonal h1, zero_tmul]
37     | add a b ha hb => simp only [map_add, ha, hb, add_zero]
38   complete z := by
39     induction z using TensorProduct.induction_on with
40     | zero => simp
41     | tmul x y =>
42       simp only [TensorProduct.map_tmul, Fintype.sum_prod_type]
43       simp only [← TensorProduct.tmul_sum, Q.complete]
44       rw [← TensorProduct.sum_tmul, P.complete]
45     | add a b ha hb => simp only [map_add, Finset.sum_add_distrib, ha, hb]
46 
47 /-- Tensor packet range equals the span of tensors of the original packet ranges. -/
48 theorem tensor_packet_range
49     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J)
50     (i : I) (j : J) :
51     LinearMap.range ((tensorPackets P Q).proj (i,j)) =
52       Submodule.map₂ (TensorProduct.mk K X Y)
53         (LinearMap.range (P.proj i)) (LinearMap.range (Q.proj j)) := by
54   exact TensorProduct.range_map _ _
55 
56 /-- The resulting finite direct-product coordinates use the actual tensor-projector ranges. -/
57 noncomputable def tensorPacketCoordinates
58     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J) :=
59   (tensorPackets P Q).exactPacketCoordinates
60 
61 /-- Transfer blocks of a tensor map factor in the same source/target order. -/
62 theorem tensor_transfer_blocks
63     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J)
64     (S : Module.End K X) (T : Module.End K Y) (b a : I) (d c : J) :
65     transferBlock (tensorPackets P Q) (tensorPackets P Q)
66       (TensorProduct.map S T) (b,d) (a,c) =
67     TensorProduct.map (transferBlock P P S b a) (transferBlock Q Q T d c) := by
68   simp only [transferBlock, tensorPackets, ← TensorProduct.map_comp]
69 
70 /-- Algebraic dual projectors; finite dimensionality is not needed for this construction. -/
71 def dualPackets (P : LinearProjectorFamily K X I) :
72     LinearProjectorFamily K (Module.Dual K X) I where
73   proj i := (P.proj i).dualMap
74   idempotent i φ := by
75     ext x
76     exact congrArg φ (P.idempotent i x)
77   orthogonal := by
78     intro i j hij φ
79     ext x
80     change φ (P.proj j (P.proj i x)) = 0
81     rw [P.orthogonal hij.symm, map_zero]
82   complete φ := by
83     ext x
84     simp only [LinearMap.sum_apply, LinearMap.dualMap_apply]
85     change (∑ i, φ (P.proj i x)) = φ x
86     rw [← map_sum, P.complete]
87 
88 open Komorebi.PacketNaturalityCompletion.FullBlocks
89 
90 /-- Inclusion of tensor factors identifies their tensor product with the actual tensor packet. -/
91 noncomputable def tensorPacketRangeEquiv
92     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J) (i : I) (j : J) :
93     (LinearMap.range (P.proj i) ⊗[K] LinearMap.range (Q.proj j)) ≃ₗ[K]
94       LinearMap.range ((tensorPackets P Q).proj (i,j)) := by
95   classical
96   let inc := TensorProduct.map (packetInclusion P i) (packetInclusion Q j)
97   let pr := TensorProduct.map (packetProjection P i) (packetProjection Q j)
98   have hleft : Function.LeftInverse pr inc := by
99     intro z
100     induction z using TensorProduct.induction_on with
101     | zero => simp [inc, pr]
102     | tmul x y =>
103       simp only [inc, pr, TensorProduct.map_tmul, packetInclusion,
104         Submodule.subtype_apply, packetProjection_apply_coe]
105     | add a b ha hb => simp only [map_add, ha, hb]
106   have hrange : LinearMap.range inc = LinearMap.range ((tensorPackets P Q).proj (i,j)) := by
107     simp only [inc, packetInclusion, tensorPackets, TensorProduct.range_map,
108       Submodule.range_subtype]
109   exact (LinearEquiv.ofInjective inc hleft.injective).trans (LinearEquiv.ofEq _ _ hrange)
110 
111 /-- Tensor coordinates with the tensor products of original packet spaces as factors. -/
112 noncomputable def tensorFactorCoordinates
113     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J) :
114     (X ⊗[K] Y) ≃ₗ[K] ((ij : I × J) →
115       LinearMap.range (P.proj ij.1) ⊗[K] LinearMap.range (Q.proj ij.2)) :=
116   (tensorPackets P Q).exactPacketCoordinates.trans
117     (LinearEquiv.piCongrRight fun ij => (tensorPacketRangeEquiv P Q ij.1 ij.2).symm)
118 
119 /-- Restriction identifies the range of the dual projector with the dual of its range. -/
120 noncomputable def dualPacketRangeEquiv (P : LinearProjectorFamily K X I) (i : I) :
121     LinearMap.range ((dualPackets P).proj i) ≃ₗ[K]
122       Module.Dual K (LinearMap.range (P.proj i)) where
123   toFun φ := (φ : Module.Dual K X).comp (packetInclusion P i)
124   invFun ψ := ⟨ψ.comp (packetProjection P i), by
125     refine ⟨ψ.comp (packetProjection P i), ?_⟩
126     ext x
127     change ψ ⟨P.proj i (P.proj i x), _⟩ = ψ ⟨P.proj i x, _⟩
128     congr 1
129     exact Subtype.ext (P.idempotent i x)⟩
130   left_inv φ := by
131     apply Subtype.ext
132     ext x
133     rcases φ.property with ⟨ψ, hψ⟩
134     have hfix : (dualPackets P).proj i (φ : Module.Dual K X) = φ := by
135       rw [← hψ]
136       exact (dualPackets P).idempotent i ψ
137     exact congrArg (fun f : Module.Dual K X => f x) hfix
138   right_inv ψ := by
139     classical
140     ext x
141     change ψ (packetProjection P i (x : X)) = ψ x
142     rw [packetProjection_apply_coe]
143   map_add' φ ψ := by ext x; rfl
144   map_smul' c φ := by ext x; rfl
145 
146 /-- Dual coordinates are the product of the duals of the original packet ranges. -/
147 noncomputable def dualPacketCoordinates (P : LinearProjectorFamily K X I) :
148     Module.Dual K X ≃ₗ[K] ((i : I) → Module.Dual K (LinearMap.range (P.proj i))) :=
149   (dualPackets P).exactPacketCoordinates.trans
150     (LinearEquiv.piCongrRight fun i => dualPacketRangeEquiv P i)
151 
152 /-- Literal finite-direct-sum form of the tensor packet theorem. -/
153 noncomputable def tensorPacketDirectSumCoordinates
154     (P : LinearProjectorFamily K X I) (Q : LinearProjectorFamily K Y J) :
155     (X ⊗[K] Y) ≃ₗ[K] DirectSum (I × J) (fun ij =>
156       LinearMap.range (P.proj ij.1) ⊗[K] LinearMap.range (Q.proj ij.2)) := by
157   classical
158   exact (tensorFactorCoordinates P Q).trans (DirectSum.linearEquivFunOnFintype K _ _).symm
159 
160 /-- Literal finite-direct-sum form of algebraic dual packet coordinates. -/
161 noncomputable def dualPacketDirectSumCoordinates (P : LinearProjectorFamily K X I) :
162     Module.Dual K X ≃ₗ[K] DirectSum I (fun i => Module.Dual K (LinearMap.range (P.proj i))) := by
163   classical
164   exact (dualPacketCoordinates P).trans (DirectSum.linearEquivFunOnFintype K _ _).symm
165 
166 end Komorebi.PaperIRelease

Back to source controls