PacketDescent.lean

1 import KomorebiVerification.ExactCoordinates
2 import KomorebiVerification.PaperITransport
3 
4 /-!
5 # Actual restriction, quotient and exact sequences of finite packets
6 
7 All induced maps are constructed from the given invariant submodule. Zero
8 projectors can be discarded by the explicit finite subtype `NonzeroIndex`.
9 The intersections below use comaps along subtype inclusions, so their ambient
10 module is explicit even where the printed paper suppresses that embedding.
11 -/
12 
13 set_option autoImplicit false
14 set_option linter.unnecessarySimpa false
15 
16 namespace Komorebi.Foundation.LinearProjectorFamily
17 
18 universe u v w
19 
20 variable {R : Type u} {M : Type v} {ι : Type w}
21 variable [Ring R] [AddCommGroup M] [Module R M] [Fintype ι]
22 
23 /-- Every projector preserves the actual submodule. -/
24 def Preserves (P : LinearProjectorFamily R M ι) (K : Submodule R M) : Prop :=
25   ∀ i, ∀ x ∈ K, P.proj i x ∈ K
26 
27 /-- The literal restriction of the given projectors to an invariant submodule. -/
28 def restrictTo (P : LinearProjectorFamily R M ι) (K : Submodule R M)
29     (hK : P.Preserves K) : LinearProjectorFamily R K ι where
30   proj i :=
31     { toFun := fun x ↦ ⟨P.proj i x, hK i x x.property⟩
32       map_add' := fun x y ↦ Subtype.ext ((P.proj i).map_add x y)
33       map_smul' := fun a x ↦ Subtype.ext ((P.proj i).map_smul a x) }
34   idempotent i x := Subtype.ext (P.idempotent i x)
35   orthogonal hij x := Subtype.ext (P.orthogonal hij x)
36   complete x := by
37     apply Subtype.ext
38     simpa using P.complete (x : M)
39 
40 @[simp] theorem restrictTo_proj_apply
41     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
42     (hK : P.Preserves K) (i : ι) (x : K) :
43     ((P.restrictTo K hK).proj i x : M) = P.proj i x := rfl
44 
45 /-- The quotient projectors are induced by the original linear maps. -/
46 def descendTo (P : LinearProjectorFamily R M ι) (K : Submodule R M)
47     (hK : P.Preserves K) : LinearProjectorFamily R (M ⧸ K) ι where
48   proj i := K.mapQ K (P.proj i) (hK i)
49   idempotent i z := by
50     obtain ⟨x, rfl⟩ := K.mkQ_surjective z
51     change K.mkQ (P.proj i (P.proj i x)) = K.mkQ (P.proj i x)
52     rw [P.idempotent]
53   orthogonal hij z := by
54     obtain ⟨x, rfl⟩ := K.mkQ_surjective z
55     change K.mkQ (P.proj _ (P.proj _ x)) = 0
56     rw [P.orthogonal hij, map_zero]
57   complete z := by
58     obtain ⟨x, rfl⟩ := K.mkQ_surjective z
59     change (∑ i, K.mkQ (P.proj i x)) = K.mkQ x
60     rw [← map_sum, P.complete]
61 
62 @[simp] theorem descendTo_proj_mkQ
63     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
64     (hK : P.Preserves K) (i : ι) (x : M) :
65     (P.descendTo K hK).proj i (K.mkQ x) = K.mkQ (P.proj i x) := rfl
66 
67 /-- The literal quotient-map intertwining identity. -/
68 theorem descendTo_intertwines
69     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
70     (hK : P.Preserves K) (i : ι) :
71     K.mkQ.comp (P.proj i) = ((P.descendTo K hK).proj i).comp K.mkQ := by
72   ext x
73   rfl
74 
75 /-- The actual finite subtype of indices whose projectors are nonzero. -/
76 abbrev NonzeroIndex (P : LinearProjectorFamily R M ι) := {i : ι // P.proj i ≠ 0}
77 
78 noncomputable instance nonzeroIndexFintype (P : LinearProjectorFamily R M ι) :
79     Fintype P.NonzeroIndex := by
80   classical
81   exact inferInstanceAs (Fintype {i // P.proj i ≠ 0})
82 
83 /-- Discard zero projectors; the identity sum is retained, including for the
84 zero module where the remaining index type may be empty. -/
85 noncomputable def discardZeros (P : LinearProjectorFamily R M ι) :
86     LinearProjectorFamily R M P.NonzeroIndex := by
87   classical
88   exact
89     { proj := fun i ↦ P.proj i.val
90       idempotent := fun i x ↦ P.idempotent i.val x
91       orthogonal := fun hij x ↦ P.orthogonal (fun h ↦ hij (Subtype.ext h)) x
92       complete := fun x ↦ by
93         have h := Fintype.sum_subtype_add_sum_subtype
94           (fun i : ι ↦ P.proj i ≠ 0) (fun i ↦ P.proj i x)
95         have hz : (∑ i : {i : ι // ¬ P.proj i ≠ 0}, P.proj i.val x) = 0 := by
96           apply Finset.sum_eq_zero
97           intro i _
98           have hi : P.proj i.val = 0 := not_not.mp i.property
99           simp [hi]
100         rw [hz, add_zero] at h
101         exact h.trans (P.complete x) }
102 
103 theorem discardZeros_proj_ne_zero (P : LinearProjectorFamily R M ι)
104     (i : P.NonzeroIndex) : P.discardZeros.proj i ≠ 0 := i.property
105 
106 /-- The packet system on the invariant submodule after all zero restricted
107 packets have been removed. -/
108 noncomputable def nonzeroRestriction
109     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
110     (hK : P.Preserves K) :
111     LinearProjectorFamily R K (P.restrictTo K hK).NonzeroIndex :=
112   (P.restrictTo K hK).discardZeros
113 
114 /-- The canonical quotient packet system after all zero descended packets
115 have been removed. Its index type need not equal the original index type. -/
116 noncomputable def nonzeroQuotient
117     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
118     (hK : P.Preserves K) :
119     LinearProjectorFamily R (M ⧸ K) (P.descendTo K hK).NonzeroIndex :=
120   (P.descendTo K hK).discardZeros
121 
122 /-- The quotient projectors are uniquely determined by intertwining with the
123 surjective quotient map. -/
124 theorem descendTo_unique
125     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
126     (hK : P.Preserves K) (i : ι) (Q : Module.End R (M ⧸ K))
127     (hQ : Q.comp K.mkQ = K.mkQ.comp (P.proj i)) :
128     Q = (P.descendTo K hK).proj i := by
129   apply LinearMap.ext
130   intro z
131   obtain ⟨x, rfl⟩ := K.mkQ_surjective z
132   exact congrArg (fun f : M →ₗ[R] M ⧸ K ↦ f x) hQ
133 
134 /-- A projector fixes every point in its range. -/
135 theorem proj_eq_self_of_mem_range (P : LinearProjectorFamily R M ι)
136     (i : ι) {x : M} (hx : x ∈ LinearMap.range (P.proj i)) :
137     P.proj i x = x := by
138   obtain ⟨y, rfl⟩ := hx
139   exact P.idempotent i y
140 
141 /-- The restricted packet is exactly the intersection, as a submodule of `K`. -/
142 theorem restrictTo_range
143     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
144     (hK : P.Preserves K) (i : ι) :
145     LinearMap.range ((P.restrictTo K hK).proj i) =
146       (LinearMap.range (P.proj i)).comap K.subtype := by
147   ext x
148   constructor
149   · rintro ⟨y, rfl⟩
150     exact ⟨(y : M), rfl⟩
151   · intro hx
152     exact ⟨x, Subtype.ext (P.proj_eq_self_of_mem_range i hx)⟩
153 
154 /-- The same intersection after embedding the restricted packet in `M`. -/
155 theorem restrictTo_range_in_ambient
156     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
157     (hK : P.Preserves K) (i : ι) :
158     (LinearMap.range ((P.restrictTo K hK).proj i)).map K.subtype =
159       K ⊓ LinearMap.range (P.proj i) := by
160   rw [P.restrictTo_range]
161   ext x
162   constructor
163   · rintro ⟨y, hy, rfl⟩
164     exact ⟨y.property, hy⟩
165   · rintro ⟨hxK, hxP⟩
166     exact ⟨⟨x, hxK⟩, hxP, rfl⟩
167 
168 /-- Quotient map restricted to the actual `i`th packet and corestricted to
169 the actual range of the descended projector. -/
170 def packetQuotientMap
171     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
172     (hK : P.Preserves K) (i : ι) :
173     LinearMap.range (P.proj i) →ₗ[R]
174       LinearMap.range ((P.descendTo K hK).proj i) where
175   toFun x := ⟨K.mkQ x, ⟨K.mkQ x, by
176     rw [P.descendTo_proj_mkQ, P.proj_eq_self_of_mem_range i x.property]⟩⟩
177   map_add' x y := Subtype.ext (K.mkQ.map_add x y)
178   map_smul' a x := Subtype.ext (K.mkQ.map_smul a x)
179 
180 @[simp] theorem packetQuotientMap_coe
181     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
182     (hK : P.Preserves K) (i : ι) (x : LinearMap.range (P.proj i)) :
183     (P.packetQuotientMap K hK i x : M ⧸ K) = K.mkQ x := rfl
184 
185 theorem packetQuotientMap_surjective
186     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
187     (hK : P.Preserves K) (i : ι) :
188     Function.Surjective (P.packetQuotientMap K hK i) := by
189   rintro ⟨z, y, hy⟩
190   obtain ⟨x, rfl⟩ := K.mkQ_surjective y
191   refine ⟨⟨P.proj i x, ⟨x, rfl⟩⟩, Subtype.ext ?_⟩
192   exact hy
193 
194 /-- The descended packet is exactly the image of the original packet under
195 the quotient map. -/
196 theorem descendTo_range
197     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
198     (hK : P.Preserves K) (i : ι) :
199     LinearMap.range ((P.descendTo K hK).proj i) =
200       (LinearMap.range (P.proj i)).map K.mkQ := by
201   ext z
202   constructor
203   · rintro ⟨y, rfl⟩
204     obtain ⟨x, rfl⟩ := K.mkQ_surjective y
205     exact ⟨P.proj i x, ⟨x, rfl⟩, rfl⟩
206   · rintro ⟨x, ⟨y, rfl⟩, rfl⟩
207     exact ⟨K.mkQ y, rfl⟩
208 
209 /-- The inverse image of the quotient packet is the literal sum `X_i + K`. -/
210 theorem descendTo_range_preimage
211     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
212     (hK : P.Preserves K) (i : ι) :
213     (LinearMap.range ((P.descendTo K hK).proj i)).comap K.mkQ =
214       LinearMap.range (P.proj i) ⊔ K := by
215   rw [P.descendTo_range]
216   ext x
217   constructor
218   · rintro ⟨y, hy, hxy⟩
219     have hdiff : x - y ∈ K := by
220       apply (Submodule.Quotient.eq K).mp
221       exact hxy.symm
222     exact Submodule.mem_sup.mpr ⟨y, hy, x - y, hdiff, by abel⟩
223   · intro hx
224     obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx
225     refine ⟨y, hy, ?_⟩
226     rw [map_add, show K.mkQ z = 0 from (Submodule.Quotient.mk_eq_zero K).mpr hz,
227       add_zero]
228 
229 /-- Its kernel is literally the intersection inside the source packet. -/
230 theorem packetQuotientMap_ker
231     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
232     (hK : P.Preserves K) (i : ι) :
233     LinearMap.ker (P.packetQuotientMap K hK i) =
234       K.comap (LinearMap.range (P.proj i)).subtype := by
235   ext x
236   change (P.packetQuotientMap K hK i x = 0) ↔ (x : M) ∈ K
237   rw [← Subtype.val_inj]
238   change (Submodule.Quotient.mk (x : M) : M ⧸ K) = Submodule.Quotient.mk 0 ↔ _
239   simpa using (Submodule.Quotient.eq K (x := (x : M)) (y := 0))
240 
241 /-- First-isomorphism equivalence from the actual packet quotient map. -/
242 noncomputable def packetQuotientEquiv
243     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
244     (hK : P.Preserves K) (i : ι) :
245     (LinearMap.range (P.proj i) ⧸ K.comap (LinearMap.range (P.proj i)).subtype)
246       ≃ₗ[R] LinearMap.range ((P.descendTo K hK).proj i) :=
247   (Submodule.quotEquivOfEq _ _ (P.packetQuotientMap_ker K hK i).symm).trans
248     ((P.packetQuotientMap K hK i).quotKerEquivOfSurjective
249       (P.packetQuotientMap_surjective K hK i))
250 
251 /-- Second-isomorphism equivalence with `(X_i + K)/K`, with the denominator
252 explicitly pulled back to the sum submodule. -/
253 noncomputable def descendedPacketEquivSumQuotient
254     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
255     (hK : P.Preserves K) (i : ι) :
256     LinearMap.range ((P.descendTo K hK).proj i) ≃ₗ[R]
257       (↥(LinearMap.range (P.proj i) ⊔ K) ⧸
258         K.comap (LinearMap.range (P.proj i) ⊔ K).subtype) :=
259   (P.packetQuotientEquiv K hK i).symm.trans
260     ((Submodule.quotEquivOfEq _ _ (by simp)).trans
261       (LinearMap.quotientInfEquivSupQuotient (LinearMap.range (P.proj i)) K))
262 
263 /-- Transfer blocks preserve the invariant submodule and land in the target
264 packet, hence map every restricted source packet into the restricted target. -/
265 theorem transferBlock_preserves_packet
266     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
267     (hK : P.Preserves K) (T : Module.End R M)
268     (hT : ∀ x ∈ K, T x ∈ K) (j i : ι) {x : M}
269     (hx : x ∈ K ⊓ LinearMap.range (P.proj i)) :
270     transferBlock P P T j i x ∈ K ⊓ LinearMap.range (P.proj j) :=
271   ⟨hK j _ (hT _ (hK i x hx.1)), ⟨T (P.proj i x), rfl⟩⟩
272 
273 /-- Transfer blocks intertwine with the constructed quotient operator. -/
274 theorem transferBlock_descends
275     (P : LinearProjectorFamily R M ι) (K : Submodule R M)
276     (hK : P.Preserves K) (T : Module.End R M)
277     (hT : ∀ x ∈ K, T x ∈ K) (j i : ι) :
278     K.mkQ.comp (transferBlock P P T j i) =
279       (transferBlock (P.descendTo K hK) (P.descendTo K hK)
280         (K.mapQ K T hT) j i).comp K.mkQ := by
281   ext x
282   rfl
283 
284 end Komorebi.Foundation.LinearProjectorFamily
285 
286 #print axioms Komorebi.Foundation.LinearProjectorFamily.restrictTo
287 #print axioms Komorebi.Foundation.LinearProjectorFamily.descendTo
288 #print axioms Komorebi.Foundation.LinearProjectorFamily.discardZeros
289 #print axioms Komorebi.Foundation.LinearProjectorFamily.packetQuotientEquiv
290 #print axioms Komorebi.Foundation.LinearProjectorFamily.descendedPacketEquivSumQuotient
291 #print axioms Komorebi.Foundation.LinearProjectorFamily.transferBlock_descends

Back to source controls