SharedCorrection.lean

1 module
2 public import Mathlib.LinearAlgebra.Isomorphisms
3 public import Mathlib.Tactic.Abel
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.SharedCorrection
10 
11 variable {R U V W : Type*} [CommRing R]
12 variable [AddCommGroup U] [Module R U]
13 variable [AddCommGroup V] [Module R V]
14 variable [AddCommGroup W] [Module R W]
15 
16 /-- Corrections invisible to either local map generate the common kernel. -/
17 def commonKernel (J : U →ₗ[R] V) (K : U →ₗ[R] W) : Submodule R U :=
18   LinearMap.ker J ⊔ LinearMap.ker K
19 
20 /-- The common quotient retains exactly the information shared by the two maps. -/
21 abbrev Common (J : U →ₗ[R] V) (K : U →ₗ[R] W) := U ⧸ commonKernel J K
22 
23 /-- Equality in the common quotient is precisely simultaneous realizability
24 of the left image of one correction and the right image of the other. -/
25 theorem quotient_mk_eq_iff_common (J : U →ₗ[R] V) (K : U →ₗ[R] W) (u v : U) :
26     (Submodule.Quotient.mk u : Common J K) = Submodule.Quotient.mk v ↔
27       ∃ w : U, J w = J u ∧ K w = K v := by
28   rw [Submodule.Quotient.eq]
29   change u - v ∈ LinearMap.ker J ⊔ LinearMap.ker K ↔ _
30   constructor
31   · intro h
32     obtain ⟨s, hs, t, ht, hst⟩ := Submodule.mem_sup.mp h
33     have hs0 : J s = 0 := hs
34     have ht0 : K t = 0 := ht
35     refine ⟨u - s, ?_, ?_⟩
36     · rw [map_sub, hs0, sub_zero]
37     · have hw : u - s = v + t := by
38         calc
39           u - s = (u - v) + v - s := by abel
40           _ = (s + t) + v - s := by rw [hst]
41           _ = v + t := by abel
42       rw [hw, map_add, ht0, add_zero]
43   · rintro ⟨w, hwJ, hwK⟩
44     apply Submodule.mem_sup.mpr
45     refine ⟨u - w, ?_, w - v, ?_, ?_⟩
46     · change J (u - w) = 0
47       rw [map_sub, hwJ, sub_self]
48     · change K (w - v) = 0
49       rw [map_sub, hwK, sub_self]
50     · abel
51 
52 /-- Linear label for an attainable left packet. -/
53 def labelJ (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
54     LinearMap.range J →ₗ[R] Common J K :=
55   ((LinearMap.ker J).liftQ (commonKernel J K).mkQ (by
56     rw [Submodule.ker_mkQ]
57     exact le_sup_left)).comp J.quotKerEquivRange.symm.toLinearMap
58 
59 /-- Linear label for an attainable right packet. -/
60 def labelK (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
61     LinearMap.range K →ₗ[R] Common J K :=
62   ((LinearMap.ker K).liftQ (commonKernel J K).mkQ (by
63     rw [Submodule.ker_mkQ]
64     exact le_sup_right)).comp K.quotKerEquivRange.symm.toLinearMap
65 
66 @[simp]
67 theorem labelJ_image (J : U →ₗ[R] V) (K : U →ₗ[R] W) (u : U) :
68     labelJ J K (J.rangeRestrict u) = (commonKernel J K).mkQ u := by
69   have h : J.quotKerEquivRange.symm (J.rangeRestrict u) = (LinearMap.ker J).mkQ u :=
70     J.quotKerEquivRange_symm_apply_image u _
71   simp only [labelJ, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap]
72   rw [h]
73   rfl
74 
75 @[simp]
76 theorem labelK_image (J : U →ₗ[R] V) (K : U →ₗ[R] W) (u : U) :
77     labelK J K (K.rangeRestrict u) = (commonKernel J K).mkQ u := by
78   have h : K.quotKerEquivRange.symm (K.rangeRestrict u) = (LinearMap.ker K).mkQ u :=
79     K.quotKerEquivRange_symm_apply_image u _
80   simp only [labelK, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap]
81   rw [h]
82   rfl
83 
84 /-- The left label covers the common quotient, without assuming J is onto V. -/
85 theorem labelJ_surjective (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
86     Function.Surjective (labelJ J K) := by
87   intro c
88   obtain ⟨u, rfl⟩ := (commonKernel J K).mkQ_surjective c
89   exact ⟨J.rangeRestrict u, labelJ_image J K u⟩
90 
91 /-- The right label also covers the common quotient. -/
92 theorem labelK_surjective (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
93     Function.Surjective (labelK J K) := by
94   intro c
95   obtain ⟨u, rfl⟩ := (commonKernel J K).mkQ_surjective c
96   exact ⟨K.rangeRestrict u, labelK_image J K u⟩
97 
98 /-- A finite left target suffices for a finite common quotient, even if U is infinite. -/
99 theorem common_finite_of_left (J : U →ₗ[R] V) (K : U →ₗ[R] W) [Finite V] :
100     Finite (Common J K) :=
101   Finite.of_surjective (labelJ J K) (labelJ_surjective J K)
102 
103 /-- A finite right target likewise suffices. -/
104 theorem common_finite_of_right (J : U →ₗ[R] V) (K : U →ₗ[R] W) [Finite W] :
105     Finite (Common J K) :=
106   Finite.of_surjective (labelK J K) (labelK_surjective J K)
107 
108 /-- Individually attainable packets have equal labels exactly when a single
109 correction realizes both. -/
110 theorem labels_eq_iff_common (J : U →ₗ[R] V) (K : U →ₗ[R] W)
111     (a : LinearMap.range J) (b : LinearMap.range K) :
112     labelJ J K a = labelK J K b ↔
113       ∃ u : U, J.rangeRestrict u = a ∧ K.rangeRestrict u = b := by
114   obtain ⟨u, hu⟩ := a.property
115   obtain ⟨v, hv⟩ := b.property
116   have ha : J.rangeRestrict u = a := Subtype.ext hu
117   have hb : K.rangeRestrict v = b := Subtype.ext hv
118   rw [← ha, ← hb, labelJ_image, labelK_image]
119   change (Submodule.Quotient.mk u : Common J K) = Submodule.Quotient.mk v ↔ _
120   rw [quotient_mk_eq_iff_common]
121   constructor
122   · rintro ⟨w, hwJ, hwK⟩
123     exact ⟨w, Subtype.ext hwJ, Subtype.ext hwK⟩
124   · rintro ⟨w, hwJ, hwK⟩
125     exact ⟨w, congrArg Subtype.val hwJ, congrArg Subtype.val hwK⟩
126 
127 /-- The map sending one correction to its two local images. -/
128 def joint (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
129     U →ₗ[R] LinearMap.range J × LinearMap.range K :=
130   J.rangeRestrict.prod K.rangeRestrict
131 
132 /-- The genuine fiber-product submodule over the common quotient. -/
133 def fiber (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
134     Submodule R (LinearMap.range J × LinearMap.range K) :=
135   LinearMap.ker ((labelJ J K).comp (LinearMap.fst R (LinearMap.range J) (LinearMap.range K)) -
136     (labelK J K).comp (LinearMap.snd R (LinearMap.range J) (LinearMap.range K)))
137 
138 @[simp]
139 theorem mem_fiber (J : U →ₗ[R] V) (K : U →ₗ[R] W)
140     (z : LinearMap.range J × LinearMap.range K) :
141     z ∈ fiber J K ↔ labelJ J K z.1 = labelK J K z.2 := by
142   change labelJ J K z.1 - labelK J K z.2 = 0 ↔ _
143   exact sub_eq_zero
144 
145 /-- The joint image is exactly the fiber product, not merely contained in it. -/
146 theorem joint_range_eq_fiber (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
147     LinearMap.range (joint J K) = fiber J K := by
148   ext z
149   rw [mem_fiber, labels_eq_iff_common]
150   constructor
151   · rintro ⟨u, hu⟩
152     exact ⟨u, congrArg Prod.fst hu, congrArg Prod.snd hu⟩
153   · rintro ⟨u, huJ, huK⟩
154     exact ⟨u, Prod.ext huJ huK⟩
155 
156 /-- Explicit linear equivalence between the joint image and fiber-product submodule. -/
157 def jointImageEquivFiber (J : U →ₗ[R] V) (K : U →ₗ[R] W) :
158     LinearMap.range (joint J K) ≃ₗ[R] fiber J K :=
159   LinearEquiv.ofEq _ _ (joint_range_eq_fiber J K)
160 
161 variable {T : Type*} [AddCommGroup T] [Module R T]
162 
163 /-- Every linear observation insensitive to either local kernel factors
164 uniquely through the common quotient. -/
165 theorem common_universal (J : U →ₗ[R] V) (K : U →ₗ[R] W) (F : U →ₗ[R] T)
166     (hJ : LinearMap.ker J ≤ LinearMap.ker F)
167     (hK : LinearMap.ker K ≤ LinearMap.ker F) :
168     ∃! q : Common J K →ₗ[R] T, q.comp (commonKernel J K).mkQ = F := by
169   have hF : commonKernel J K ≤ LinearMap.ker F := sup_le hJ hK
170   refine ⟨(commonKernel J K).liftQ F hF, Submodule.liftQ_mkQ _ _ _, ?_⟩
171   intro q hq
172   apply LinearMap.ext
173   intro c
174   obtain ⟨u, rfl⟩ := (commonKernel J K).mkQ_surjective c
175   change q ((commonKernel J K).mkQ u) = F u
176   exact LinearMap.congr_fun hq u
177 
178 /-- A pair of linear observations on attainable local packets that agree
179 on every common correction factor uniquely through the common quotient.
180 This is the pushout universal property for the two range restrictions. -/
181 theorem common_paired_universal (J : U →ₗ[R] V) (K : U →ₗ[R] W)
182     (h : LinearMap.range J →ₗ[R] T) (k : LinearMap.range K →ₗ[R] T)
183     (agree : h.comp J.rangeRestrict = k.comp K.rangeRestrict) :
184     ∃! q : Common J K →ₗ[R] T,
185       q.comp (labelJ J K) = h ∧ q.comp (labelK J K) = k := by
186   let F := h.comp J.rangeRestrict
187   have hJ : LinearMap.ker J ≤ LinearMap.ker F := by
188     intro u hu
189     change h (J.rangeRestrict u) = 0
190     have hJu : J.rangeRestrict u = 0 := Subtype.ext hu
191     rw [hJu, map_zero]
192   have hK : LinearMap.ker K ≤ LinearMap.ker F := by
193     intro u hu
194     change (h.comp J.rangeRestrict) u = 0
195     rw [agree]
196     change k (K.rangeRestrict u) = 0
197     have hKu : K.rangeRestrict u = 0 := Subtype.ext hu
198     rw [hKu, map_zero]
199   obtain ⟨q, hq, _⟩ := common_universal J K F hJ hK
200   have hqJ : q.comp (labelJ J K) = h := by
201     ext a
202     obtain ⟨u, hu⟩ := a.property
203     have ha : J.rangeRestrict u = a := Subtype.ext hu
204     rw [← ha]
205     change q (labelJ J K (J.rangeRestrict u)) = h (J.rangeRestrict u)
206     rw [labelJ_image]
207     exact LinearMap.congr_fun hq u
208   have hqK : q.comp (labelK J K) = k := by
209     ext b
210     obtain ⟨u, hu⟩ := b.property
211     have hb : K.rangeRestrict u = b := Subtype.ext hu
212     rw [← hb]
213     change q (labelK J K (K.rangeRestrict u)) = k (K.rangeRestrict u)
214     rw [labelK_image]
215     have hqu := LinearMap.congr_fun hq u
216     change q ((commonKernel J K).mkQ u) = (h.comp J.rangeRestrict) u at hqu
217     rw [agree] at hqu
218     exact hqu
219   refine ⟨q, ⟨hqJ, hqK⟩, ?_⟩
220   intro q' hq'
221   apply LinearMap.ext
222   intro c
223   obtain ⟨a, rfl⟩ := labelJ_surjective J K c
224   exact (LinearMap.congr_fun hq'.1 a).trans (LinearMap.congr_fun hqJ a).symm
225 
226 #print axioms commonKernel
227 #print axioms Common
228 #print axioms quotient_mk_eq_iff_common
229 #print axioms labelJ
230 #print axioms labelK
231 #print axioms labelJ_image
232 #print axioms labelK_image
233 #print axioms labelJ_surjective
234 #print axioms labelK_surjective
235 #print axioms common_finite_of_left
236 #print axioms common_finite_of_right
237 #print axioms labels_eq_iff_common
238 #print axioms joint
239 #print axioms fiber
240 #print axioms mem_fiber
241 #print axioms joint_range_eq_fiber
242 #print axioms jointImageEquivFiber
243 #print axioms common_universal
244 #print axioms common_paired_universal
245 
246 end Komorebi.SharedCorrection

Back to source controls