Source: ProCGroups.FreeProC.FiniteBasis

1import ProCGroups.FreeProC.Basic

3/-!

4# Free pro-C finite-basis utilities

6This module develops the finite-basis interface for

7`ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData`.

8Its canonical finite index is `ULift (Fin n)`, which lies in the carrier

9universe required by the generated-target lifting property. Concrete `Fin n`

10displays can be obtained by reindexing with `ULift.up`.

11-/

13namespace CrowellExactSequence

15noncomputable section

17open scoped Topology

19open ProCGroups.ProC

20open ProCGroups.ProC.HasOpenNormalBasisInClass

22universe u

24/-- Choose an equivalence from a finite epimorphically free pro-\(C\) basis to

25\(\operatorname{Fin} n\). -/

26def freeProCChosenBasisEquivOfBasisCard

27 {C : ProCGroups.FiniteGroupClass.{u}}

28 (sourceData :

29 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

30 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :

31 sourceData.basis ≃ Fin n :=

32 Classical.choice ((Cardinal.mk_eq_nat_iff).1 hbasis)

34/-- The canonical chosen finite family. The universe lift keeps its generator

35type in the same universe as the pro-\(C\) carrier. -/

36def freeProCChosenULiftFamilyOfBasisCard

37 {C : ProCGroups.FiniteGroupClass.{u}}

38 (sourceData :

39 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

40 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :

41 ULift.{u} (Fin n) → sourceData.carrier :=

42 fun i =>

43 sourceData.inclusion

44 ((freeProCChosenBasisEquivOfBasisCard (C := C) sourceData hbasis).symm i.down)

46/-- Reindexing preserves the epimorphically free pro-\(C\) converging-basis property. -/

47theorem freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

48 {C : ProCGroups.FiniteGroupClass.{u}}

49 (sourceData :

50 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

51 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :

52 ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet

53 (C := C) (ULift.{u} (Fin n)) sourceData.carrier

54 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) := by

55 classical

56 let e : ULift.{u} (Fin n) ≃ sourceData.basis :=

57 { toFun := fun i =>

58 (freeProCChosenBasisEquivOfBasisCard (C := C) sourceData hbasis).symm i.down

59 invFun := fun b =>

60 ULift.up ((freeProCChosenBasisEquivOfBasisCard (C := C) sourceData hbasis) b)

61 left_inv := by

62 intro i

63 cases i

64 simp only [Equiv.apply_symm_apply]

65 right_inv := by

66 intro b

67 simp only [Equiv.symm_apply_apply]}

68 letI : Fintype sourceData.basis :=

69 Fintype.ofEquiv (ULift.{u} (Fin n)) e

70 apply ProCGroups.FreeProC.finite_generatingFamily_is_basis

71 (C := C) sourceData.isEpimorphicallyFree (Cardinal.mk_congr e).symm

72 have hRange :

73 Set.range (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) =

74 Set.range sourceData.inclusion := by

75 ext g

76 constructor

77 · rintro ⟨i, rfl⟩

78 exact ⟨e i, rfl⟩

79 · rintro ⟨b, rfl⟩

80 refine ⟨e.symm b, ?_⟩

81 dsimp [freeProCChosenULiftFamilyOfBasisCard, e]

82 rw [Equiv.symm_apply_apply]

83 rw [hRange]

84 exact sourceData.isEpimorphicallyFree.generates_range

86/--

87The canonical chosen family topologically generates the epimorphically free pro-\(C\) source.

88-/

89theorem freeProCChosenULiftFamilyOfBasisCard_generates

90 {C : ProCGroups.FiniteGroupClass.{u}}

91 (sourceData :

92 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

93 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :

94 ProCGroups.Generation.TopologicallyGenerates

95 (G := sourceData.carrier)

96 (Set.range (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)) := by

97 exact

98 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

99 (C := C) sourceData hbasis).generates_range

100

101/-- The image of the finite lifted basis under any target homomorphism satisfies the

102open-subgroup convergence condition used by the epimorphically free pro-\(C\) formulation. -/

103theorem freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

104 {C : ProCGroups.FiniteGroupClass.{u}}

105 (sourceData :

106 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

107 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)

108 {H : Type u} [Group H] [TopologicalSpace H]

109 (ψ : sourceData.carrier →* H) :

110 ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups

111 (G := H)

112 (fun i : ULift.{u} (Fin n) =>

113 ψ (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)) := by

114 exact ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain

115 (G := H)

116 (fun i : ULift.{u} (Fin n) =>

117 ψ (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))

118

119/-- A surjective continuous homomorphism carries the lifted chosen finite basis to a

120topological generating family of the target. -/

121theorem freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

122 {C : ProCGroups.FiniteGroupClass.{u}}

123 (sourceData :

124 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

125 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)

126 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

127 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :

128 ProCGroups.Generation.TopologicallyGenerates

129 (G := H)

130 (Set.range

131 (fun i : ULift.{u} (Fin n) =>

132 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))) := by

133 let family : ULift.{u} (Fin n) → sourceData.carrier :=

134 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis

135 have hsourceGen :

136 ProCGroups.Generation.TopologicallyGenerates

137 (G := sourceData.carrier) (Set.range family) := by

138 simpa [family] using

139 freeProCChosenULiftFamilyOfBasisCard_generates (C := C) sourceData hbasis

140 have himage :=

141 ProCGroups.Generation.topologicallyGenerates_image_of_continuousMonoidHom_surjective

142 (G := sourceData.carrier) (H := H) psi hpsi hsourceGen

143 have hrange :

144 psi '' Set.range family = Set.range (fun i => psi (family i)) := by

145 ext h

146 constructor

147 · rintro ⟨g, ⟨i, rfl⟩, rfl⟩

148 exact ⟨i, rfl⟩

149 · rintro ⟨i, rfl⟩

150 exact ⟨family i, ⟨i, rfl⟩, rfl⟩

151 simpa [family, hrange] using himage

152

153/-- For the lifted finite basis, the generated-target lift of a surjective target map is the

154target map itself. This is the concrete bridge needed when Fox constructions produce a right

155component from the epimorphic lifting property. -/

156theorem freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective

157 {C : ProCGroups.FiniteGroupClass.{u}}

158 (sourceData :

159 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

160 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)

161 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

162 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

163 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))

164 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :

165 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

166 (C := C) sourceData hbasis).liftHom hH

167 (fun i : ULift.{u} (Fin n) =>

168 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))

169 (freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

170 (C := C) sourceData hbasis psi.toMonoidHom)

171 (freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

172 (C := C) sourceData hbasis psi hpsi) =

173 psi := by

174 let hfree :=

175 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis

176 let liftedFamily : ULift.{u} (Fin n) → sourceData.carrier :=

177 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis

178 let φ : ULift.{u} (Fin n) → H := fun i => psi (liftedFamily i)

179 let hconv :

180 ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ :=

181 by

182 simpa [φ, liftedFamily] using

183 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

184 (C := C) sourceData hbasis psi.toMonoidHom

185 let hgen :

186 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by

187 simpa [φ, liftedFamily] using

188 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

189 (C := C) sourceData hbasis psi hpsi

190 ext g

191 have hmon :

192 psi.toMonoidHom = hfree.lift hH φ hconv hgen :=

193 hfree.lift_unique hH φ hconv hgen psi.continuous_toFun (by

194 intro i

195 rfl)

196 exact (congrArg (fun f : sourceData.carrier →* H => f g) hmon).symm

197

198/--

199The chosen lifted finite free basis surjects onto every finite open-normal quotient of the free

200pro-\(C\) source.

201-/

202theorem freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective

203 {C : ProCGroups.FiniteGroupClass.{u}}

204 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

205 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

206 (V : OpenNormalSubgroupInClass C sourceData.carrier) :

207 Function.Surjective

208 ((QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)).comp

209 (FreeGroup.lift

210 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis))) := by

211 classical

212 let X : Type u := ULift.{u} (Fin r)

213 let ι : X → sourceData.carrier :=

214 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis

215 let Q : Type u := sourceData.carrier ⧸ (V.1 : Subgroup sourceData.carrier)

216 letI : DiscreteTopology Q :=

217 QuotientGroup.discreteTopology V.1.toOpenSubgroup.isOpen'

218 let g : X → Q :=

219 fun i => QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier) (ι i)

220 have hsource :

221 ProCGroups.Generation.TopologicallyGenerates

222 (G := sourceData.carrier) (Set.range ι) := by

223 simpa [X, ι] using

224 freeProCChosenULiftFamilyOfBasisCard_generates (C := C) sourceData hbasis

225 have hquot_image :

226 ProCGroups.Generation.TopologicallyGenerates

227 (G := Q)

228 ((QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)) '' Set.range ι) :=

229 ProCGroups.Generation.topologicallyGenerates_quotient_image

230 (G := sourceData.carrier) (N := (V.1 : Subgroup sourceData.carrier)) hsource

231 have hrange :

232 (QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)) '' Set.range ι =

233 Set.range g := by

234 ext y

235 constructor

236 · rintro ⟨x, ⟨i, rfl⟩, rfl⟩

237 exact ⟨i, rfl⟩

238 · rintro ⟨i, rfl⟩

239 exact ⟨ι i, ⟨i, rfl⟩, rfl⟩

240 have hg :

241 ProCGroups.Generation.TopologicallyGenerates (G := Q) (Set.range g) := by

242 rw [← hrange]

243 exact hquot_image

244 have hsurj :

245 Function.Surjective (FreeGroup.lift g) :=

246 ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete

247 (G := Q) g hg

248 have hlift :

249 FreeGroup.lift g =

250 (QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)).comp

251 (FreeGroup.lift ι) := by

252 apply FreeGroup.ext_hom

253 intro i

254 rw [FreeGroup.lift_apply_of, MonoidHom.comp_apply, FreeGroup.lift_apply_of]

255 simpa [hlift, X, ι] using hsurj

256

257/--

258The finite-index lift comparison is an equivalence, with inverse given by the reverse

259comparison map.

260-/

261def finULiftEquiv (r : Nat) : Fin r ≃ ULift.{u} (Fin r) where

262 toFun i := ULift.up i

263 invFun i := i.down

264 left_inv := by

265 intro i

266 rfl

267 right_inv := by

268 intro i

269 cases i

270 rfl

271

272end

273

274end CrowellExactSequence