SharedUniversal.lean

1 module
2 public import SharedCorrection
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.SharedCorrection
9 
10 variable {R U V W T : Type*} [CommRing R]
11 variable [AddCommGroup U] [Module R U]
12 variable [AddCommGroup V] [Module R V]
13 variable [AddCommGroup W] [Module R W]
14 variable [AddCommGroup T] [Module R T]
15 
16 /-- Every linear observation insensitive to either local kernel factors
17 uniquely through the common quotient. -/
18 theorem common_universal (J : U →ₗ[R] V) (K : U →ₗ[R] W) (F : U →ₗ[R] T)
19     (hJ : LinearMap.ker J ≤ LinearMap.ker F)
20     (hK : LinearMap.ker K ≤ LinearMap.ker F) :
21     ∃! q : Common J K →ₗ[R] T, q.comp (commonKernel J K).mkQ = F := by
22   have hF : commonKernel J K ≤ LinearMap.ker F := sup_le hJ hK
23   refine ⟨(commonKernel J K).liftQ F hF, Submodule.liftQ_mkQ _ _ _, ?_⟩
24   intro q hq
25   apply LinearMap.ext
26   intro c
27   obtain ⟨u, rfl⟩ := (commonKernel J K).mkQ_surjective c
28   change q ((commonKernel J K).mkQ u) = F u
29   exact LinearMap.congr_fun hq u
30 
31 /-- A pair of linear observations on attainable local packets that agree
32 on every common correction factor uniquely through the common quotient.
33 This is the pushout universal property for the two range restrictions. -/
34 theorem common_paired_universal (J : U →ₗ[R] V) (K : U →ₗ[R] W)
35     (h : LinearMap.range J →ₗ[R] T) (k : LinearMap.range K →ₗ[R] T)
36     (agree : h.comp J.rangeRestrict = k.comp K.rangeRestrict) :
37     ∃! q : Common J K →ₗ[R] T,
38       q.comp (labelJ J K) = h ∧ q.comp (labelK J K) = k := by
39   let F := h.comp J.rangeRestrict
40   have hJ : LinearMap.ker J ≤ LinearMap.ker F := by
41     intro u hu
42     change h (J.rangeRestrict u) = 0
43     have hJu : J.rangeRestrict u = 0 := Subtype.ext hu
44     rw [hJu, map_zero]
45   have hK : LinearMap.ker K ≤ LinearMap.ker F := by
46     intro u hu
47     change (h.comp J.rangeRestrict) u = 0
48     rw [agree]
49     change k (K.rangeRestrict u) = 0
50     have hKu : K.rangeRestrict u = 0 := Subtype.ext hu
51     rw [hKu, map_zero]
52   obtain ⟨q, hq, _⟩ := common_universal J K F hJ hK
53   have hqJ : q.comp (labelJ J K) = h := by
54     ext a
55     obtain ⟨u, hu⟩ := a.property
56     have ha : J.rangeRestrict u = a := Subtype.ext hu
57     rw [← ha]
58     change q (labelJ J K (J.rangeRestrict u)) = h (J.rangeRestrict u)
59     rw [labelJ_image]
60     exact LinearMap.congr_fun hq u
61   have hqK : q.comp (labelK J K) = k := by
62     ext b
63     obtain ⟨u, hu⟩ := b.property
64     have hb : K.rangeRestrict u = b := Subtype.ext hu
65     rw [← hb]
66     change q (labelK J K (K.rangeRestrict u)) = k (K.rangeRestrict u)
67     rw [labelK_image]
68     have hqu := LinearMap.congr_fun hq u
69     change q ((commonKernel J K).mkQ u) = (h.comp J.rangeRestrict) u at hqu
70     rw [agree] at hqu
71     exact hqu
72   refine ⟨q, ⟨hqJ, hqK⟩, ?_⟩
73   intro q' hq'
74   apply LinearMap.ext
75   intro c
76   obtain ⟨a, rfl⟩ := labelJ_surjective J K c
77   exact (LinearMap.congr_fun hq'.1 a).trans (LinearMap.congr_fun hqJ a).symm
78 
79 #print axioms common_universal
80 #print axioms common_paired_universal
81 
82 end Komorebi.SharedCorrection

Back to source controls