ProCGroups/ProC/Category/Pullbacks.lean

1import ProCGroups.Categorical.ProfinitePullbacks

2import ProCGroups.ProC.Category.Basic

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ProCGroups/ProC/Category/Pullbacks.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Pro-C groups and open normal quotients

15Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

16-/

18open CategoryTheory

20universe u

22namespace ProCGrp

24variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}

25variable {G G' H H1 H2 : ProCGrp ProC}

27/-- A pullback square in the bundled category `ProCGrp ProC`. -/

28def IsPullbackSquare

29 (alpha1 : G ⟶ H1) (alpha2 : G ⟶ H2)

30 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H) : Prop :=

31 alpha1 ≫ beta1 = alpha2 ≫ beta2 ∧

32 ∀ ⦃K : ProCGrp ProC⦄ (phi1 : K ⟶ H1) (phi2 : K ⟶ H2),

33 phi1 ≫ beta1 = phi2 ≫ beta2 →

34 ∃! phi : K ⟶ G, phi ≫ alpha1 = phi1 ∧ phi ≫ alpha2 = phi2

36/-- Chosen morphism induced by a pro-`C` pullback universal property. -/

37noncomputable def pullbackLift

38 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

39 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

40 {K : ProCGrp ProC}

41 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

42 (phi1 : K ⟶ H1) (phi2 : K ⟶ H2)

43 (hphi : phi1 ≫ beta1 = phi2 ≫ beta2) : K ⟶ G :=

44 Classical.choose (ExistsUnique.exists (hpb.2 phi1 phi2 hphi))

46/-- The chosen pullback lift has the prescribed composites. -/

47theorem pullbackLift_spec

48 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

49 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

50 {K : ProCGrp ProC}

51 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

52 (phi1 : K ⟶ H1) (phi2 : K ⟶ H2)

53 (hphi : phi1 ≫ beta1 = phi2 ≫ beta2) :

54 pullbackLift hpb phi1 phi2 hphi ≫ alpha1 = phi1 ∧

55 pullbackLift hpb phi1 phi2 hphi ≫ alpha2 = phi2 :=

56 Classical.choose_spec (ExistsUnique.exists (hpb.2 phi1 phi2 hphi))

58/-- The pullback lift has the prescribed left projection. -/

59@[simp] theorem pullbackLift_left

60 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

61 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

62 {K : ProCGrp ProC}

63 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

64 (phi1 : K ⟶ H1) (phi2 : K ⟶ H2)

65 (hphi : phi1 ≫ beta1 = phi2 ≫ beta2) :

66 pullbackLift hpb phi1 phi2 hphi ≫ alpha1 = phi1 :=

67 (pullbackLift_spec hpb phi1 phi2 hphi).1

69/-- The pullback lift has the prescribed right projection. -/

70@[simp] theorem pullbackLift_right

71 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

72 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

73 {K : ProCGrp ProC}

74 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

75 (phi1 : K ⟶ H1) (phi2 : K ⟶ H2)

76 (hphi : phi1 ≫ beta1 = phi2 ≫ beta2) :

77 pullbackLift hpb phi1 phi2 hphi ≫ alpha2 = phi2 :=

78 (pullbackLift_spec hpb phi1 phi2 hphi).2

80/-- Uniqueness of the chosen pullback lift. -/

81theorem pullbackLift_unique

82 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

83 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

84 {K : ProCGrp ProC}

85 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

86 (phi1 : K ⟶ H1) (phi2 : K ⟶ H2)

87 (hphi : phi1 ≫ beta1 = phi2 ≫ beta2)

88 {psi : K ⟶ G}

89 (hpsi : psi ≫ alpha1 = phi1 ∧ psi ≫ alpha2 = phi2) :

90 psi = pullbackLift hpb phi1 phi2 hphi := by

91 rcases hpb.2 phi1 phi2 hphi with ⟨u, hu, huniq⟩

92 have hpsi' : psi = u := huniq _ hpsi

93 have hchosen : pullbackLift hpb phi1 phi2 hphi = u :=

94 huniq _ (pullbackLift_spec hpb phi1 phi2 hphi)

95 exact hpsi'.trans hchosen.symm

97/-- The self-lift of a pullback object is the identity morphism. -/

98@[simp] theorem pullbackLift_self

99 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

100 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

101 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2) :

102 pullbackLift hpb alpha1 alpha2 hpb.1 = 𝟙 G := by

103 symm

104 exact pullbackLift_unique hpb alpha1 alpha2 hpb.1 (psi := 𝟙 G) (by simp only [Category.id_comp, and_self])

105

106/-- Extensionality of morphisms into a pro-`C` pullback object. -/

107theorem pullback_hom_ext

108 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

109 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

110 {K : ProCGrp ProC}

111 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

112 {psi psi' : K ⟶ G}

113 (h1 : psi ≫ alpha1 = psi' ≫ alpha1)

114 (h2 : psi ≫ alpha2 = psi' ≫ alpha2) :

115 psi = psi' := by

116 have hphi : (psi ≫ alpha1) ≫ beta1 = (psi ≫ alpha2) ≫ beta2 := by

117 calc

118 (psi ≫ alpha1) ≫ beta1 = psi ≫ (alpha1 ≫ beta1) := by simp only [Category.assoc]

119 _ = psi ≫ (alpha2 ≫ beta2) := by rw [hpb.1]

120 _ = (psi ≫ alpha2) ≫ beta2 := by simp only [Category.assoc]

121 have hpsi :

122 psi = pullbackLift hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi := by

123 exact pullbackLift_unique hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi

124 (psi := psi) ⟨rfl, rfl⟩

125 have hpsi' :

126 psi' = pullbackLift hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi := by

127 exact pullbackLift_unique hpb (psi ≫ alpha1) (psi ≫ alpha2) hphi

128 (psi := psi') ⟨h1.symm, h2.symm⟩

129 exact hpsi.trans hpsi'.symm

130

131/-- Canonical comparison map from one pro-`C` pullback object to another. -/

132noncomputable def pullbackMapOfIsPullback

133 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

134 {alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}

135 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

136 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

137 (hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :

138 G' ⟶ G :=

139 pullbackLift hpb alpha1' alpha2' hpb'.1

140

141/-- The comparison map from a pullback object to itself is the identity. -/

142@[simp] theorem pullbackMapOfIsPullback_self

143 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

144 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

145 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2) :

146 pullbackMapOfIsPullback beta1 beta2 hpb hpb = 𝟙 G := by

147 exact pullbackLift_self (hpb := hpb)

148

149/-- The comparison map between pullback objects respects the left projection. -/

150@[simp] theorem pullbackMapOfIsPullback_left

151 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

152 {alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}

153 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

154 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

155 (hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :

156 pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha1 = alpha1' :=

157 pullbackLift_left hpb alpha1' alpha2' hpb'.1

158

159/-- The comparison map between pullback objects respects the right projection. -/

160@[simp] theorem pullbackMapOfIsPullback_right

161 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

162 {alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}

163 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

164 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

165 (hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :

166 pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha2 = alpha2' :=

167 pullbackLift_right hpb alpha1' alpha2' hpb'.1

168

169/-- Any two pro-`C` pullback objects of the same cospan are canonically isomorphic. -/

170noncomputable def pullbackIsoOfIsPullback

171 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

172 {alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}

173 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

174 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

175 (hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :

176 G ≅ G' where

177 hom := pullbackMapOfIsPullback beta1 beta2 hpb' hpb

178 inv := pullbackMapOfIsPullback beta1 beta2 hpb hpb'

179 hom_inv_id := by

180 apply pullback_hom_ext hpb

181 · calc

182 (pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫

183 pullbackMapOfIsPullback beta1 beta2 hpb hpb') ≫ alpha1 =

184 pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫ alpha1' := by

185 rw [Category.assoc, pullbackMapOfIsPullback_left]

186 _ = alpha1 := pullbackMapOfIsPullback_left beta1 beta2 hpb' hpb

187 · calc

188 (pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫

189 pullbackMapOfIsPullback beta1 beta2 hpb hpb') ≫ alpha2 =

190 pullbackMapOfIsPullback beta1 beta2 hpb' hpb ≫ alpha2' := by

191 rw [Category.assoc, pullbackMapOfIsPullback_right]

192 _ = alpha2 := pullbackMapOfIsPullback_right beta1 beta2 hpb' hpb

193 inv_hom_id := by

194 apply pullback_hom_ext hpb'

195 · calc

196 (pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫

197 pullbackMapOfIsPullback beta1 beta2 hpb' hpb) ≫ alpha1' =

198 pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha1 := by

199 rw [Category.assoc, pullbackMapOfIsPullback_left]

200 _ = alpha1' := pullbackMapOfIsPullback_left beta1 beta2 hpb hpb'

201 · calc

202 (pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫

203 pullbackMapOfIsPullback beta1 beta2 hpb' hpb) ≫ alpha2' =

204 pullbackMapOfIsPullback beta1 beta2 hpb hpb' ≫ alpha2 := by

205 rw [Category.assoc, pullbackMapOfIsPullback_right]

206 _ = alpha2' := pullbackMapOfIsPullback_right beta1 beta2 hpb hpb'

207

208/-- The canonical pullback isomorphism respects the left projection. -/

209@[simp] theorem pullbackIsoOfIsPullback_hom_left

210 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

211 {alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}

212 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

213 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

214 (hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :

215 (pullbackIsoOfIsPullback beta1 beta2 hpb hpb').hom ≫ alpha1' = alpha1 :=

216 pullbackMapOfIsPullback_left beta1 beta2 hpb' hpb

217

218/-- The canonical pullback isomorphism respects the right projection. -/

219@[simp] theorem pullbackIsoOfIsPullback_hom_right

220 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

221 {alpha1' : G' ⟶ H1} {alpha2' : G' ⟶ H2}

222 (beta1 : H1 ⟶ H) (beta2 : H2 ⟶ H)

223 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2)

224 (hpb' : IsPullbackSquare alpha1' alpha2' beta1 beta2) :

225 (pullbackIsoOfIsPullback beta1 beta2 hpb hpb').hom ≫ alpha2' = alpha2 :=

226 pullbackMapOfIsPullback_right beta1 beta2 hpb' hpb

227

228/-- A concrete continuous profinite pullback square is a pullback in `ProCGrp`. -/

229theorem isPullbackSquare_of_hasProfiniteTestPullbackProperty

230 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

231 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

232 (hpb : ProCGroups.Categorical.HasProfiniteTestPullbackProperty

233 alpha1.hom alpha2.hom beta1.hom beta2.hom) :

234 IsPullbackSquare alpha1 alpha2 beta1 beta2 := by

235 refine ⟨?_, ?_⟩

236 · apply hom_ext

237 change beta1.hom.comp alpha1.hom = beta2.hom.comp alpha2.hom

238 exact hpb.1

239 · intro K phi1 phi2 hphi

240 have hK : ProCGroups.IsProfiniteGroup K :=

241 ProCGroups.ProC.ProCGroup.profiniteGroup ProC K

242 have hphi' : beta1.hom.comp phi1.hom = beta2.hom.comp phi2.hom := by

243 simpa using congrArg (fun f : K ⟶ H => f.hom) hphi

244 rcases hpb.2 (K := K) hK phi1.hom phi2.hom hphi' with ⟨psi, hpsi, huniq⟩

245 let psi' : K ⟶ G := ConcreteCategory.ofHom (C := ProCGrp ProC) psi

246 refine ⟨psi', ?_, ?_⟩

247 · constructor

248 · apply hom_ext

249 change alpha1.hom.comp psi = phi1.hom

250 exact hpsi.1

251 · apply hom_ext

252 change alpha2.hom.comp psi = phi2.hom

253 exact hpsi.2

254 · intro theta htheta

255 apply hom_ext

256 change theta.hom = psi

257 apply huniq

258 constructor

259 · simpa using congrArg (fun f : K ⟶ H1 => f.hom) htheta.1

260 · simpa using congrArg (fun f : K ⟶ H2 => f.hom) htheta.2

261

262/-- For the all-finite predicate, the bundled `ProCGrp` pullback property is equivalent to the

263concrete profinite pullback property. -/

264theorem hasProfiniteTestPullbackProperty_of_isPullbackSquare_allFinite

265 {G H H1 H2 : ProCGrp ProCGroups.ProC.allFiniteProC}

266 {alpha1 : G ⟶ H1} {alpha2 : G ⟶ H2}

267 {beta1 : H1 ⟶ H} {beta2 : H2 ⟶ H}

268 (hpb : IsPullbackSquare alpha1 alpha2 beta1 beta2) :

269 ProCGroups.Categorical.HasProfiniteTestPullbackProperty

270 alpha1.hom alpha2.hom beta1.hom beta2.hom := by

271 refine ⟨?_, ?_⟩

272 · change (alpha1 ≫ beta1).hom = (alpha2 ≫ beta2).hom

273 exact congrArg (fun f : G ⟶ H => f.hom) hpb.1

274 · intro K _ _ _ hK phi1 phi2 hphi

275 letI : ProCGroups.ProC.ProCGroup ProCGroups.ProC.allFiniteProC K :=

276 ProCGroups.ProC.ProCGroup.of_isProCGroup ProCGroups.ProC.allFiniteProC K

277 (ProCGroups.ProC.allFiniteProC_isProCGroup_of_profinite hK)

278 let Kc : ProCGrp ProCGroups.ProC.allFiniteProC :=

279 ProCGrp.of ProCGroups.ProC.allFiniteProC K

280 let phi1' : Kc ⟶ H1 := ConcreteCategory.ofHom (C := ProCGrp ProCGroups.ProC.allFiniteProC) phi1

281 let phi2' : Kc ⟶ H2 := ConcreteCategory.ofHom (C := ProCGrp ProCGroups.ProC.allFiniteProC) phi2

282 have hphi' : phi1' ≫ beta1 = phi2' ≫ beta2 := by

283 apply hom_ext

284 exact hphi

285 rcases hpb.2 phi1' phi2' hphi' with ⟨psi, hpsi, huniq⟩

286 refine ⟨psi.hom, ?_, ?_⟩

287 · constructor

288 · simpa using congrArg (fun f : Kc ⟶ H1 => f.hom) hpsi.1

289 · simpa using congrArg (fun f : Kc ⟶ H2 => f.hom) hpsi.2

290 · intro theta htheta

291 let theta' : Kc ⟶ G :=

292 ConcreteCategory.ofHom (C := ProCGrp ProCGroups.ProC.allFiniteProC) theta

293 have htheta' : theta' ≫ alpha1 = phi1' ∧ theta' ≫ alpha2 = phi2' := by

294 constructor

295 · apply hom_ext

296 exact htheta.1

297 · apply hom_ext

298 exact htheta.2

299 have hthetaEq : theta' = psi := huniq theta' htheta'

300 simpa using congrArg (fun f : Kc ⟶ G => f.hom) hthetaEq

301

302end ProCGrp