Source: ProCGroups.Duality

1import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

2import Mathlib.NumberTheory.Cyclotomic.Basic

3import Mathlib.Topology.Algebra.PontryaginDual

4import Mathlib.Topology.Instances.AddCircle.DenseSubgroup

5import ProCGroups.Profinite.Basic

6import ProCGroups.Topologies.ContinuousMulEquiv

8/-!

9# Pro C Groups / Duality

11This module formalizes elementary duality constructions for profinite groups.

12-/

14open scoped Topology

16namespace ProCGroups.Duality

18universe u v

20section Basic

22variable (G : Type u) [CommGroup G] [TopologicalSpace G]

24/-- A closed proper additive subgroup of an additive circle `AddCircle p` is finite. -/

25theorem properClosedAddSubgroup_addCircle_finite

26 {p : ℝ} [Fact (0 < p)] (B : AddSubgroup (AddCircle p))

27 (hBclosed : IsClosed (B : Set (AddCircle p))) (hBproper : B ≠ ⊤) :

28 Finite B := by

29 classical

30 have hBnotDense : ¬ Dense (B : Set (AddCircle p)) := by

31 intro hDense

32 apply hBproper

33 rw [AddSubgroup.eq_top_iff']

34 intro x

35 change x ∈ (B : Set (AddCircle p))

36 have hclosure : closure (B : Set (AddCircle p)) = Set.univ := hDense.closure_eq

37 rw [← hBclosed.closure_eq]

38 rw [hclosure]

39 trivial

40 have hnot_zmultiples :

41 ¬ ∀ a : AddCircle p, addOrderOf a ≠ 0 → B ≠ AddSubgroup.zmultiples a := by

42 simpa [AddCircle.dense_addSubgroup_iff_ne_zmultiples (p := p) (s := B)] using hBnotDense

43 push Not at hnot_zmultiples

44 rcases hnot_zmultiples with ⟨a, haorder, hBgen⟩

45 have haFin : IsOfFinAddOrder a :=

46 (addOrderOf_ne_zero_iff).mp haorder

47 have hBfiniteSet : (B : Set (AddCircle p)).Finite := by

48 simpa [hBgen] using ((finite_zmultiples (a := a)).2 haFin)

49 exact hBfiniteSet.to_subtype

51/-- Transport a multiplicative subgroup of `Circle` to the standard additive circle

52`ℝ / (2π)ℤ`. This is convenient for applying `AddCircle` subgroup-classification lemmas. -/

53def circleSubgroupToAddCircleSubgroup (A : Subgroup Circle) :

54 AddSubgroup (AddCircle (2 * Real.pi)) := by

55 refine

56 { carrier := {θ | AddCircle.homeomorphCircle' θ ∈ A}

57 zero_mem' := by

58 change Real.Angle.toCircle 0 ∈ A

59 rw [Real.Angle.toCircle_zero]

60 exact A.one_mem

61 add_mem' := ?_

62 neg_mem' := ?_ }

63 · intro a b ha hb

64 change AddCircle.homeomorphCircle' (a + b) ∈ A

65 rw [show AddCircle.homeomorphCircle' (a + b) =

66 AddCircle.homeomorphCircle' a * AddCircle.homeomorphCircle' b by

67 change Real.Angle.toCircle (a + b) = Real.Angle.toCircle a * Real.Angle.toCircle b

68 exact Real.Angle.toCircle_add a b]

69 exact A.mul_mem ha hb

70 · intro a ha

71 change AddCircle.homeomorphCircle' (-a) ∈ A

72 rw [show AddCircle.homeomorphCircle' (-a) = (AddCircle.homeomorphCircle' a)⁻¹ by

73 change Real.Angle.toCircle (-a) = (Real.Angle.toCircle a)⁻¹

74 exact Real.Angle.toCircle_neg a]

75 exact A.inv_mem ha

77/-- Membership in the transported additive subgroup is detected by the circle

78homeomorphism. -/

79@[simp] theorem mem_circleSubgroupToAddCircleSubgroup_iff

80 {A : Subgroup Circle} {θ : AddCircle (2 * Real.pi)} :

81 θ ∈ circleSubgroupToAddCircleSubgroup A ↔ AddCircle.homeomorphCircle' θ ∈ A := by

82 rfl

84/-- Transporting a closed circle subgroup to the additive circle preserves closedness. -/

85theorem isClosed_circleSubgroupToAddCircleSubgroup

86 (A : Subgroup Circle) (hAclosed : IsClosed (A : Set Circle)) :

87 IsClosed (circleSubgroupToAddCircleSubgroup A : Set (AddCircle (2 * Real.pi))) := by

88 change IsClosed (AddCircle.homeomorphCircle' ⁻¹' (A : Set Circle))

89 exact (AddCircle.homeomorphCircle'.isClosed_preimage).2 hAclosed

91/-- Transporting a proper circle subgroup to the additive circle preserves properness. -/

92theorem circleSubgroupToAddCircleSubgroup_ne_top

93 (A : Subgroup Circle) (hAproper : A ≠ ⊤) :

94 circleSubgroupToAddCircleSubgroup A ≠ ⊤ := by

95 intro htop

96 apply hAproper

97 rw [Subgroup.eq_top_iff']

98 intro z

99 have hz : AddCircle.homeomorphCircle'.symm z ∈ circleSubgroupToAddCircleSubgroup A := by

100 rw [htop]

101 simp only [AddCircle.homeomorphCircle'_symm_apply, AddSubgroup.mem_top]

102 have hz' : AddCircle.homeomorphCircle' (AddCircle.homeomorphCircle'.symm z) ∈ A :=

103 mem_circleSubgroupToAddCircleSubgroup_iff.mp hz

104 rw [AddCircle.homeomorphCircle'.apply_symm_apply] at hz'

105 exact hz'

106

107/-- Every proper closed subgroup of the circle is finite. -/

108theorem properClosedSubgroup_circleTarget_finite

109 (A : Subgroup Circle) (hAclosed : IsClosed (A : Set Circle))

110 (hAproper : A ≠ ⊤) :

111 Finite A := by

112 let B := circleSubgroupToAddCircleSubgroup A

113 have hBclosed : IsClosed (B : Set (AddCircle (2 * Real.pi))) :=

114 isClosed_circleSubgroupToAddCircleSubgroup A hAclosed

115 have hBproper : B ≠ ⊤ := circleSubgroupToAddCircleSubgroup_ne_top A hAproper

116 haveI : Fact (0 < 2 * Real.pi) := ⟨by positivity⟩

117 have hBfinite : Finite B := properClosedAddSubgroup_addCircle_finite B hBclosed hBproper

118 let e : B ≃ A :=

119 { toFun := fun θ => ⟨AddCircle.homeomorphCircle' θ, θ.2⟩

120 invFun := fun z => ⟨AddCircle.homeomorphCircle'.symm z, by

121 change AddCircle.homeomorphCircle' (AddCircle.homeomorphCircle'.symm z) ∈ A

122 rw [AddCircle.homeomorphCircle'.apply_symm_apply]

123 exact z.2⟩

124 left_inv := by

125 intro θ

126 apply Subtype.ext

127 exact AddCircle.homeomorphCircle'.symm_apply_apply θ.1

128 right_inv := by

129 intro z

130 apply Subtype.ext

131 exact AddCircle.homeomorphCircle'.apply_symm_apply z.1 }

132 exact Finite.of_equiv B e

133

134variable {G}

135

136/-- The circle target contains two distinct points. -/

137theorem circleTarget_one_ne_exp_pi :

138 (1 : Circle) ≠ Circle.exp Real.pi := by

139 simpa [eq_comm] using Circle.exp_pi_ne_one

140

141/-- The circle target is not totally disconnected. -/

142theorem not_totallyDisconnectedSpace_circleTarget :

143 ¬ TotallyDisconnectedSpace Circle := by

144 intro htd

145 letI : TotallyDisconnectedSpace Circle := htd

146 letI : ConnectedSpace Circle :=

147 AddCircle.homeomorphCircle'.surjective.connectedSpace

148 AddCircle.homeomorphCircle'.continuous_toFun

149 letI : PreconnectedSpace Circle := inferInstance

150 have hEq : (1 : Circle) = Circle.exp Real.pi :=

151 TotallyDisconnectedSpace.eq_of_continuous

152 (f := fun z : Circle => z) continuous_id 1 (Circle.exp Real.pi)

153 exact circleTarget_one_ne_exp_pi hEq

154

155/-- A compact subgroup of `T` contained in the open right half-plane is trivial. -/

156theorem subgroup_eq_bot_of_isCompact_subset_rightHalfPlane

157 (A : Subgroup Circle) (hAcompact : IsCompact (A : Set Circle))

158 (hApos : ∀ z ∈ A, 0 < Complex.re (z : ℂ)) :

159 A = ⊥ := by

160 classical

161 by_cases hAbot : A = ⊥

162 · exact hAbot

163 have hAproper : A ≠ ⊤ := by

164 intro hAtop

165 have hneg : Circle.exp Real.pi ∈ A := by

166 simp only [hAtop, Subgroup.mem_top]

167 have hneg' : ¬ 0 < Complex.re ((Circle.exp Real.pi : Circle) : ℂ) := by

168 simp only [Circle.coe_exp, Complex.exp_pi_mul_I, Complex.neg_re, Complex.one_re,

169 Left.neg_pos_iff, not_lt,

170 zero_le_one]

171 exact hneg' (hApos (Circle.exp Real.pi) hneg)

172 have hAfinite : Finite A :=

173 properClosedSubgroup_circleTarget_finite A hAcompact.isClosed hAproper

174 letI : Fintype A := Fintype.ofFinite A

175 have hCircleToUnits_injective :

176 Function.Injective (Circle.toUnits : Circle →* Units ℂ) := by

177 intro x y hxy

178 apply Circle.ext

179 exact congrArg (fun z : Units ℂ => (z : ℂ)) hxy

180 let B : Subgroup (Units ℂ) := A.map Circle.toUnits

181 let e : A ≃* B := A.equivMapOfInjective Circle.toUnits hCircleToUnits_injective

182 have hBfinite : Finite B := Finite.of_equiv A e

183 letI : Fintype B := Fintype.ofFinite B

184 have hBnebot : B ≠ ⊥ := by

185 intro hBbot

186 apply hAbot

187 exact (Subgroup.map_eq_bot_iff_of_injective

188 (H := A) (f := Circle.toUnits) hCircleToUnits_injective).mp (by simpa [B] using hBbot)

189 have hsumB : ∑ x : B, ((x : Units ℂ) : ℂ) = 0 :=

190 FiniteField.sum_subgroup_units_eq_zero hBnebot

191 have hsumA : ∑ x : A, (x : ℂ) = 0 := by

192 calc

193 ∑ x : A, (x : ℂ) = ∑ x : A, (((e x : B) : Units ℂ) : ℂ) := by

194 exact Fintype.sum_congr _ _ fun x => by

195 simp only [Subgroup.coe_equivMapOfInjective_apply, Circle.toUnits_apply,

196 Units.val_mk0, B, e]

197 _ = ∑ y : B, ((y : Units ℂ) : ℂ) := by

198 simpa using (e.toEquiv.sum_comp fun y : B => ((y : Units ℂ) : ℂ))

199 _ = 0 := hsumB

200 have hsumRePos : 0 < Complex.re (∑ x : A, (x : ℂ)) := by

201 rw [Complex.re_sum]

202 simpa using

203 (Finset.sum_pos' (s := (Finset.univ : Finset A))

204 (f := fun x : A => Complex.re (x : ℂ))

205 (fun x hx => le_of_lt (hApos x x.2))

206 ⟨1, by simp only [Finset.mem_univ], hApos (1 : Circle) A.one_mem⟩)

207 exfalso

208 rw [hsumA] at hsumRePos

209 simp only [Complex.zero_re, lt_self_iff_false] at hsumRePos

210

211/-- The Pontryagin dual of a compact abelian group is discrete. -/

212theorem dualGroup_discrete_of_compact [CompactSpace G] :

213 DiscreteTopology (PontryaginDual G) := by

214 let U : Set Circle := {z | 0 < Complex.re (z : ℂ)}

215 let V : Set (PontryaginDual G) := {χ | Set.MapsTo χ Set.univ U}

216 have hUopen : IsOpen U := by

217 change IsOpen {z : Circle | 0 < Complex.re (z : ℂ)}

218 exact isOpen_lt continuous_const (Complex.continuous_re.comp continuous_subtype_val)

219 have hVopen : IsOpen V := by

220 let W : Set C(G, Circle) := {f | Set.MapsTo f Set.univ U}

221 have hWopen : IsOpen W := by

222 simpa [W] using

223 (ContinuousMap.isOpen_setOf_mapsTo

224 (X := G) (Y := Circle) (K := Set.univ) (U := U) isCompact_univ hUopen)

225 exact (ContinuousMonoidHom.isInducing_toContinuousMap G Circle).isOpen_iff.mpr

226 ⟨W, hWopen, by ext χ; rfl⟩

227 have hVeq : V = ({1} : Set (PontryaginDual G)) := by

228 ext χ

229 constructor

230 · intro hχ

231 rw [Set.mem_singleton_iff]

232 let A : Subgroup Circle := χ.toMonoidHom.range

233 have hAcompact : IsCompact (A : Set Circle) := by

234 simpa [A] using isCompact_range χ.continuous_toFun

235 have hApos : ∀ z ∈ A, 0 < Complex.re (z : ℂ) := by

236 intro z hz

237 rcases hz with ⟨g, rfl⟩

238 exact hχ (by simp only [Set.mem_univ])

239 have hAbot : A = ⊥ :=

240 subgroup_eq_bot_of_isCompact_subset_rightHalfPlane A hAcompact hApos

241 apply ContinuousMonoidHom.ext

242 intro g

243 have hg : χ g ∈ A := ⟨g, rfl⟩

244 have hg' : χ g ∈ (⊥ : Subgroup Circle) := by

245 simpa [hAbot] using hg

246 change χ g = (1 : Circle)

247 exact Subgroup.mem_bot.mp hg'

248 · intro hχ

249 rw [Set.mem_singleton_iff] at hχ

250 subst hχ

251 intro _g _hg

252 change 0 < Complex.re ((1 : Circle) : ℂ)

253 norm_num

254 have hOneOpen : IsOpen ({1} : Set (PontryaginDual G)) := by

255 rw [hVeq] at hVopen

256 exact hVopen

257 exact discreteTopology_of_isOpen_singleton_one hOneOpen

258

259/-- A discrete abelian group has compact Pontryagin dual. -/

260instance dualCompactSpaceOfDiscreteTopology [DiscreteTopology G] :

261 CompactSpace (PontryaginDual G) := by

262 infer_instance

263

264/-- The Pontryagin dual of a discrete abelian group is compact. -/

265theorem dualGroup_compact_of_discrete [DiscreteTopology G] :

266 CompactSpace (PontryaginDual G) := by

267 infer_instance

268

269private noncomputable def torsionPowerWitnessOfElement

270 {G : Type u} [CommGroup G] (htors : Monoid.IsTorsion G) (g : G) :

271 {n : ℕ // 0 < n ∧ g ^ n = 1} := by

272 let h := (isOfFinOrder_iff_pow_eq_one).mp (htors g)

273 exact ⟨Classical.choose h, Classical.choose_spec h⟩

274

275/-- The Pontryagin dual of a discrete torsion abelian group is totally disconnected. -/

276theorem dualGroup_totallyDisconnected_of_discrete_torsion

277 (G : Type u) [CommGroup G] [TopologicalSpace G]

278 [DiscreteTopology G] (htors : Monoid.IsTorsion G) :

279 TotallyDisconnectedSpace (PontryaginDual G) := by

280 let n : G → ℕ := fun g => (torsionPowerWitnessOfElement htors g).1

281 let Ω : G → Type := fun g => { z : Circle // (z : ℂ) ^ n g = 1 }

282 have hΩfinite : ∀ g : G, Finite (Ω g) := by

283 intro g

284 classical

285 letI : NeZero (n g) :=

286 ⟨Nat.ne_of_gt (torsionPowerWitnessOfElement htors g).2.1⟩

287 have hcomplexFinite :

288 Finite {z : ℂ // z ∈ Polynomial.nthRoots (n g) (1 : ℂ)} := by

289 simpa using

290 (((Polynomial.nthRoots (n g) (1 : ℂ)).toFinset.finite_toSet).to_subtype)

291 refine Finite.of_injective

292 (f := fun z : Ω g =>

293 (⟨(z : ℂ), (Polynomial.mem_nthRoots (Nat.pos_of_neZero (n g))).2 z.2⟩ :

294 {z : ℂ // z ∈ Polynomial.nthRoots (n g) (1 : ℂ)})) ?_

295 intro x y hxy

296 have hxyComplex : ((x : Ω g) : ℂ) = ((y : Ω g) : ℂ) := by

297 exact congrArg

298 (fun w : {z : ℂ // z ∈ Polynomial.nthRoots (n g) (1 : ℂ)} => (w : ℂ)) hxy

299 have hxyCircle : ((x : Ω g) : Circle) = ((y : Ω g) : Circle) := by

300 apply Subtype.ext

301 exact hxyComplex

302 exact Subtype.ext hxyCircle

303 letI : ∀ g : G, Finite (Ω g) := hΩfinite

304 letI : ∀ g : G, TopologicalSpace (Ω g) := fun _ => inferInstance

305 letI : ∀ g : G, DiscreteTopology (Ω g) := fun _ => inferInstance

306 let F : PontryaginDual G → ∀ g : G, Ω g := fun χ g =>

307 ⟨χ g, by

308 have hgpow : g ^ n g = 1 := (torsionPowerWitnessOfElement htors g).2.2

309 have hpow : χ g ^ n g = 1 := by

310 calc

311 χ g ^ n g = χ (g ^ n g) := by simp only [map_pow]

312 _ = 1 := by rw [hgpow, map_one]

313 exact congrArg (fun z : Circle => (z : ℂ)) hpow⟩

314 have hFcont : Continuous F := by

315 refine continuous_pi ?_

316 intro g

317 exact

318 ((continuous_eval_const (F := C(G, Circle)) g).comp

319 (ContinuousMonoidHom.isInducing_toContinuousMap G Circle).continuous).subtype_mk

320 fun χ => (F χ g).2

321 have hFinj : Function.Injective F := by

322 intro χ ψ hχψ

323 apply ContinuousMonoidHom.ext

324 intro g

325 exact congrArg (fun z : Ω g => (z : Circle)) (congrFun hχψ g)

326 let FRange : PontryaginDual G → Set.range F := fun χ => ⟨F χ, ⟨χ, rfl⟩⟩

327 have hFRange_continuous : Continuous FRange := hFcont.subtype_mk fun _ => ⟨_, rfl⟩

328 have hFRange_bij : Function.Bijective FRange := by

329 refine ⟨?_, ?_⟩

330 · intro χ ψ hχψ

331 exact hFinj <| congrArg Subtype.val hχψ

332 · rintro ⟨y, χ, rfl⟩

333 exact ⟨χ, rfl⟩

334 let eTop : PontryaginDual G ≃ₜ Set.range F :=

335 Continuous.homeoOfEquivCompactToT2

336 (f := Equiv.ofBijective FRange hFRange_bij) hFRange_continuous

337 letI : TotallyDisconnectedSpace (Set.range F) := inferInstance

338 exact Homeomorph.totallyDisconnectedSpace eTop.symm

339

340/-- For a discrete abelian group, multiplicative characters to the circle are the same as

341additive characters on the additive type synonym. -/

342noncomputable def dualGroupEquivAddCharCircle

343 (A : Type u) [CommGroup A] [TopologicalSpace A] [DiscreteTopology A] :

344 PontryaginDual A ≃ AddChar (Additive A) Circle where

345 toFun := fun χ =>

346 { toFun := fun a => χ a.toMul

347 map_zero_eq_one' := by simp only [toMul_zero, map_one]

348 map_add_eq_mul' := by

349 intro a b

350 exact map_mul χ a.toMul b.toMul }

351 invFun := fun χ =>

352 { toFun := fun a => χ (Additive.ofMul a)

353 map_one' := by simp only [ofMul_one, AddChar.map_zero_eq_one]

354 map_mul' := by

355 intro a b

356 exact χ.map_add_eq_mul (Additive.ofMul a) (Additive.ofMul b)

357 continuous_toFun := continuous_of_discreteTopology }

358 left_inv := by

359 intro χ

360 apply ContinuousMonoidHom.ext

361 intro a

362 rfl

363 right_inv := by

364 intro χ

365 ext a

366 rfl

367

368/-- The Pontryagin dual of a finite discrete abelian group is finite. -/

369theorem dualGroup_finite_of_finite_discrete

370 (A : Type u) [CommGroup A] [TopologicalSpace A] [Finite A] [DiscreteTopology A] :

371 Finite (PontryaginDual A) := by

372 classical

373 letI : Fintype A := Fintype.ofFinite A

374 letI : Fintype (Additive A) := Fintype.ofFinite (Additive A)

375 haveI : Finite (AddChar (Additive A) ℂ) := by infer_instance

376 haveI : Finite (AddChar (Additive A) Circle) :=

377 Finite.of_equiv (AddChar (Additive A) ℂ)

378 (AddChar.circleEquivComplex (α := Additive A)).symm

379 exact Finite.of_equiv (AddChar (Additive A) Circle)

380 (dualGroupEquivAddCharCircle A).symm

381

382/-- A finite discrete abelian group and its Pontryagin dual have the same cardinality. -/

383theorem card_dualGroup_eq_card_of_finite_discrete

384 (A : Type u) [CommGroup A] [TopologicalSpace A] [Finite A] [DiscreteTopology A] :

385 Nat.card (PontryaginDual A) = Nat.card A := by

386 classical

387 letI : Fintype A := Fintype.ofFinite A

388 letI : Fintype (Additive A) := Fintype.ofFinite (Additive A)

389 let e₁ := dualGroupEquivAddCharCircle A

390 let e₂ := (AddChar.circleEquivComplex (α := Additive A)).toEquiv

391 haveI : Finite (PontryaginDual A) := dualGroup_finite_of_finite_discrete A

392 letI : Fintype (PontryaginDual A) := Fintype.ofFinite (PontryaginDual A)

393 haveI : Finite (AddChar (Additive A) Circle) :=

394 Finite.of_equiv (AddChar (Additive A) ℂ)

395 (AddChar.circleEquivComplex (α := Additive A)).symm

396 letI : Fintype (AddChar (Additive A) Circle) :=

397 Fintype.ofFinite (AddChar (Additive A) Circle)

398 calc

399 Nat.card (PontryaginDual A) = Fintype.card (PontryaginDual A) := Nat.card_eq_fintype_card

400 _ = Fintype.card (AddChar (Additive A) Circle) := Fintype.card_congr e₁

401 _ = Fintype.card (AddChar (Additive A) ℂ) := Fintype.card_congr e₂

402 _ = Fintype.card (Additive A) := AddChar.card_eq (α := Additive A)

403 _ = Fintype.card A := rfl

404 _ = Nat.card A := Nat.card_eq_fintype_card.symm

405

406/-- A topological group equivalence induces an equivalence on Pontryagin duals. -/

407noncomputable def dualGroupEquiv

408 {H : Type v} [CommGroup H] [TopologicalSpace H]

409 (e : G ≃ₜ* H) :

410 PontryaginDual H ≃* PontryaginDual G :=

411{ toFun := PontryaginDual.map (ContinuousMonoidHom.toContinuousMonoidHom e)

412 invFun := PontryaginDual.map (ContinuousMonoidHom.toContinuousMonoidHom e.symm)

413 left_inv := by

414 intro χ

415 apply ContinuousMonoidHom.ext

416 intro g

417 change χ (e (e.symm g)) = χ g

418 rw [e.apply_symm_apply]

419 right_inv := by

420 intro χ

421 apply ContinuousMonoidHom.ext

422 intro g

423 change χ (e.symm (e g)) = χ g

424 rw [e.symm_apply_apply]

425 map_mul' := by

426 intro χ ψ

427 exact (PontryaginDual.map (ContinuousMonoidHom.toContinuousMonoidHom e)).map_mul χ ψ }

428

429/-- A topological group equivalence induces a continuous equivalence on Pontryagin duals. -/

430noncomputable def dualGroupContinuousMulEquiv

431 {H : Type v} [CommGroup H] [TopologicalSpace H]

432 (e : G ≃ₜ* H) :

433 PontryaginDual H ≃ₜ* PontryaginDual G :=

434 ContinuousMulEquiv.ofHomInv

435 (PontryaginDual.map (ContinuousMonoidHom.toContinuousMonoidHom e))

436 (PontryaginDual.map (ContinuousMonoidHom.toContinuousMonoidHom e.symm))

437 (by

438 intro χ

439 apply ContinuousMonoidHom.ext

440 intro h

441 change χ (e (e.symm h)) = χ h

442 rw [e.apply_symm_apply])

443 (by

444 intro χ

445 apply ContinuousMonoidHom.ext

446 intro g

447 change χ (e.symm (e g)) = χ g

448 rw [e.symm_apply_apply])

449

450/-- Forgetting topology from the dual homeomorphism gives the algebraic dual-group

451equivalence. -/

452@[simp] theorem dualGroupContinuousMulEquiv_toMulEquiv

453 {H : Type v} [CommGroup H] [TopologicalSpace H]

454 (e : G ≃ₜ* H) :

455 (dualGroupContinuousMulEquiv (G := G) e).toMulEquiv = dualGroupEquiv (G := G) e :=

456 rfl

457

458end Basic

459

460end ProCGroups.Duality