Yamaguchi Lean 4 Library
Source: ProCGroups.ProC.Category.Pullbacks
ProCGroups/ProC/Category/Pullbacks/Source

Source: ProCGroups.ProC.Category.Pullbacks

1import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
2import ProCGroups.Categorical.ProfinitePullbacks
3import ProCGroups.ProC.Category.Basic
5/-!
6# Pro C Groups / pro-C / Category / Pullbacks
8This module relates mathlib's `CategoryTheory.IsPullback` predicate in
9`ProCGrp C` to the concrete universal property tested against profinite
10source groups.
11-/
13open CategoryTheory
14open CategoryTheory.Limits
15open ProCGroups.Categorical
17universe u
19namespace ProCGrp
21variable {ProC : ProCGroups.FiniteGroupClass.{u}}
22variable {G H H1 H2 : ProCGrp ProC}
24/-- A continuous profinite-test pullback square is a pullback in `ProCGrp`. -/
25theorem isPullback_of_hasProfiniteTestPullbackProperty
26 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
27 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
28 (hpb : HasProfiniteTestPullbackProperty
29 (continuousHom alpha1) (continuousHom alpha2)
30 (continuousHom beta1) (continuousHom beta2)) :
31 CategoryTheory.IsPullback alpha1 alpha2 beta1 beta2 := by
32 have hw : alpha1 ≫ beta1 = alpha2 ≫ beta2 := by
33 apply hom_ext
34 change (continuousHom beta1).comp (continuousHom alpha1) =
35 (continuousHom beta2).comp (continuousHom alpha2)
36 exact hpb.1
37 let condition :
38 ∀ s : PullbackCone beta1 beta2,
39 (continuousHom beta1).comp (continuousHom s.fst) =
40 (continuousHom beta2).comp (continuousHom s.snd) :=
41 fun s => by
42 have hs := congrArg (fun f : s.pt ⟶ H => continuousHom f) s.condition
43 change (continuousHom beta1).comp (continuousHom s.fst) =
44 (continuousHom beta2).comp (continuousHom s.snd) at hs
45 exact hs
46 let lift : ∀ s : PullbackCone beta1 beta2, s.pt ⟶ G :=
47 fun s => ConcreteCategory.ofHom (C := ProCGrp ProC)
48 (pullbackDescCont hpb (continuousHom s.fst) (continuousHom s.snd)
49 (condition s))
50 refine { w := hw, isLimit' := ⟨?_⟩ }
51 refine PullbackCone.IsLimit.mk hw lift ?_ ?_ ?_
52 · intro s
53 apply hom_ext
54 change (continuousHom alpha1).comp
55 (pullbackDescCont hpb (continuousHom s.fst) (continuousHom s.snd)
56 (condition s)) =
57 continuousHom s.fst
58 exact pullbackDescCont_left hpb (continuousHom s.fst) (continuousHom s.snd)
59 (condition s)
60 · intro s
61 apply hom_ext
62 change (continuousHom alpha2).comp
63 (pullbackDescCont hpb (continuousHom s.fst) (continuousHom s.snd)
64 (condition s)) =
65 continuousHom s.snd
66 exact pullbackDescCont_right hpb (continuousHom s.fst) (continuousHom s.snd)
67 (condition s)
68 · intro s m hm1 hm2
69 apply hom_ext
70 change continuousHom m =
71 pullbackDescCont hpb (continuousHom s.fst) (continuousHom s.snd)
72 (condition s)
73 apply pullbackDescCont_uniq hpb (continuousHom s.fst) (continuousHom s.snd)
74 (condition s)
75 constructor
76 · have h := congrArg (fun f : s.pt ⟶ H1 => continuousHom f) hm1
77 change (continuousHom alpha1).comp (continuousHom m) =
78 continuousHom s.fst at h
79 exact h
80 · have h := congrArg (fun f : s.pt ⟶ H2 => continuousHom f) hm2
81 change (continuousHom alpha2).comp (continuousHom m) =
82 continuousHom s.snd at h
83 exact h
85/-- In the all-finite category, a pullback has the profinite-test universal property. -/
86theorem hasProfiniteTestPullbackProperty_of_isPullback_allFinite
88 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}
89 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}
90 (hpb : CategoryTheory.IsPullback alpha1 alpha2 beta1 beta2) :
91 HasProfiniteTestPullbackProperty
92 (continuousHom alpha1) (continuousHom alpha2)
93 (continuousHom beta1) (continuousHom beta2) := by
94 refine ⟨?_, ?_⟩
95 · change continuousHom (alpha1 ≫ beta1) = continuousHom (alpha2 ≫ beta2)
96 exact congrArg (fun f : G ⟶ H => continuousHom f) hpb.w
97 · intro K _ _ _ _ _ _ phi1 phi2 hphi
100 (ProCGrp.allFinite_property (ProfiniteGrp.of K))
101 let phi1' : Kc ⟶ H1 :=
102 ConcreteCategory.ofHom (C := ProCGrp ProCGroups.FiniteGroupClass.allFinite) phi1
103 let phi2' : Kc ⟶ H2 :=
104 ConcreteCategory.ofHom (C := ProCGrp ProCGroups.FiniteGroupClass.allFinite) phi2
105 have hphi' : phi1' ≫ beta1 = phi2' ≫ beta2 := by
106 apply hom_ext
107 exact hphi
108 let psi : Kc ⟶ G := hpb.lift phi1' phi2' hphi'
109 refine ⟨continuousHom psi, ?_, ?_⟩
110 · constructor
111 · have h := hpb.lift_fst phi1' phi2' hphi'
112 exact congrArg (fun f : Kc ⟶ H1 => continuousHom f) h
113 · have h := hpb.lift_snd phi1' phi2' hphi'
114 exact congrArg (fun f : Kc ⟶ H2 => continuousHom f) h
115 · intro theta htheta
116 let theta' : Kc ⟶ G :=
117 ConcreteCategory.ofHom (C := ProCGrp ProCGroups.FiniteGroupClass.allFinite) theta
118 have htheta1 : theta' ≫ alpha1 = phi1' := by
119 apply hom_ext
120 exact htheta.1
121 have htheta2 : theta' ≫ alpha2 = phi2' := by
122 apply hom_ext
123 exact htheta.2
124 have hthetaEq : theta' = psi := by
125 apply hpb.hom_ext
126 · exact htheta1.trans (hpb.lift_fst phi1' phi2' hphi').symm
127 · exact htheta2.trans (hpb.lift_snd phi1' phi2' hphi').symm
128 have h := congrArg (fun f : Kc ⟶ G => continuousHom f) hthetaEq
129 change theta = continuousHom psi at h
130 exact h
132end ProCGrp