ProCGroups/Duality.lean
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/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/ProCGroups/Duality.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Duality for profinite and discrete structures
19Develops dual groups and functorial formulas needed for profinite abelian and finite quotient arguments.
20-/
22open scoped Topology
24namespace ProCGroups.Duality
26universe u v
28section Basic
30variable (G : Type u) [CommGroup G] [TopologicalSpace G]
32/-- A closed proper additive subgroup of an additive circle `AddCircle p` is finite. -/
34 {p : ℝ} [Fact (0 < p)] (B : AddSubgroup (AddCircle p))
35 (hBclosed : IsClosed (B : Set (AddCircle p))) (hBproper : B ≠ ⊤) :
36 Finite B := by
37 classical
38 have hBnotDense : ¬ Dense (B : Set (AddCircle p)) := by
39 intro hDense
40 apply hBproper
41 rw [AddSubgroup.eq_top_iff']
42 intro x
43 change x ∈ (B : Set (AddCircle p))
44 have hclosure : closure (B : Set (AddCircle p)) = Set.univ := hDense.closure_eq
45 rw [← hBclosed.closure_eq]
46 rw [hclosure]
47 trivial
48 have hnot_zmultiples :
49 ¬ ∀ a : AddCircle p, addOrderOf a ≠ 0 → B ≠ AddSubgroup.zmultiples a := by
50 simpa [AddCircle.dense_addSubgroup_iff_ne_zmultiples (p := p) (s := B)] using hBnotDense
51 push_neg at hnot_zmultiples
52 rcases hnot_zmultiples with ⟨a, haorder, hBgen⟩
53 have haFin : IsOfFinAddOrder a :=
54 (addOrderOf_ne_zero_iff).mp haorder
55 have hBfiniteSet : (B : Set (AddCircle p)).Finite := by
56 simpa [hBgen] using ((finite_zmultiples (a := a)).2 haFin)
57 exact hBfiniteSet.to_subtype
59/-- Transport a multiplicative subgroup of `Circle` to the standard additive circle
61def circleSubgroupToAddCircleSubgroup (A : Subgroup Circle) :
62 AddSubgroup (AddCircle (2 * Real.pi)) := by
63 refine
64 { carrier := {θ | AddCircle.homeomorphCircle' θ ∈ A}
65 zero_mem' := by
66 simp only [AddCircle.homeomorphCircle'_apply, Set.mem_setOf_eq, Real.Angle.toCircle_zero, one_mem]
67 add_mem' := ?_
68 neg_mem' := ?_ }
69 · intro a b ha hb
70 change AddCircle.homeomorphCircle' (a + b) ∈ A
71 rw [show AddCircle.homeomorphCircle' (a + b) =
72 AddCircle.homeomorphCircle' a * AddCircle.homeomorphCircle' b by
73 change Real.Angle.toCircle (a + b) = Real.Angle.toCircle a * Real.Angle.toCircle b
74 exact Real.Angle.toCircle_add a b]
75 exact A.mul_mem ha hb
76 · intro a ha
77 change AddCircle.homeomorphCircle' (-a) ∈ A
78 rw [show AddCircle.homeomorphCircle' (-a) = (AddCircle.homeomorphCircle' a)⁻¹ by
79 change Real.Angle.toCircle (-a) = (Real.Angle.toCircle a)⁻¹
80 exact Real.Angle.toCircle_neg a]
81 exact A.inv_mem ha
83@[simp] theorem mem_circleSubgroupToAddCircleSubgroup_iff
84 {A : Subgroup Circle} {θ : AddCircle (2 * Real.pi)} :
85 θ ∈ circleSubgroupToAddCircleSubgroup A ↔ AddCircle.homeomorphCircle' θ ∈ A := by
86 rfl
89 (A : Subgroup Circle) (hAclosed : IsClosed (A : Set Circle)) :
90 IsClosed (circleSubgroupToAddCircleSubgroup A : Set (AddCircle (2 * Real.pi))) := by
91 change IsClosed (AddCircle.homeomorphCircle' ⁻¹' (A : Set Circle))
92 exact (AddCircle.homeomorphCircle'.isClosed_preimage).2 hAclosed
95 (A : Subgroup Circle) (hAproper : A ≠ ⊤) :
96 circleSubgroupToAddCircleSubgroup A ≠ ⊤ := by
97 intro htop
98 apply hAproper
99 rw [Subgroup.eq_top_iff']
100 intro z
101 have hz : AddCircle.homeomorphCircle'.symm z ∈ circleSubgroupToAddCircleSubgroup A := by
102 rw [htop]
103 simp only [AddCircle.homeomorphCircle'_symm_apply, AddSubgroup.mem_top]
104 have hz' : AddCircle.homeomorphCircle' (AddCircle.homeomorphCircle'.symm z) ∈ A :=
105 mem_circleSubgroupToAddCircleSubgroup_iff.mp hz
106 rw [AddCircle.homeomorphCircle'.apply_symm_apply] at hz'
107 exact hz'
109/-- Every proper closed subgroup of the circle is finite. -/
111 (A : Subgroup Circle) (hAclosed : IsClosed (A : Set Circle))
112 (hAproper : A ≠ ⊤) :
113 Finite A := by
114 let B := circleSubgroupToAddCircleSubgroup A
115 have hBclosed : IsClosed (B : Set (AddCircle (2 * Real.pi))) :=
116 isClosed_circleSubgroupToAddCircleSubgroup A hAclosed
117 have hBproper : B ≠ ⊤ := circleSubgroupToAddCircleSubgroup_ne_top A hAproper
118 haveI : Fact (0 < 2 * Real.pi) := ⟨by positivity⟩
119 have hBfinite : Finite B := properClosedAddSubgroup_addCircle_finite B hBclosed hBproper
120 let e : B ≃ A :=
121 { toFun := fun θ => ⟨AddCircle.homeomorphCircle' θ, θ.2⟩
122 invFun := fun z => ⟨AddCircle.homeomorphCircle'.symm z, by
123 change AddCircle.homeomorphCircle' (AddCircle.homeomorphCircle'.symm z) ∈ A
124 rw [AddCircle.homeomorphCircle'.apply_symm_apply]
125 exact z.2⟩
126 left_inv := by
127 intro θ
128 apply Subtype.ext
129 exact AddCircle.homeomorphCircle'.symm_apply_apply θ.1
130 right_inv := by
131 intro z
132 apply Subtype.ext
133 exact AddCircle.homeomorphCircle'.apply_symm_apply z.1 }
134 exact Finite.of_equiv B e
136variable {G}
138/-- The circle target contains two distinct points. -/
139theorem circleTarget_one_ne_exp_pi :
140 (1 : Circle) ≠ Circle.exp Real.pi := by
141 simpa [eq_comm] using Circle.exp_pi_ne_one
143/-- The circle target is not totally disconnected. -/
145 ¬ TotallyDisconnectedSpace Circle := by
146 intro htd
147 letI : TotallyDisconnectedSpace Circle := htd
148 letI : ConnectedSpace Circle :=
149 AddCircle.homeomorphCircle'.surjective.connectedSpace
150 AddCircle.homeomorphCircle'.continuous_toFun
151 letI : PreconnectedSpace Circle := inferInstance
152 have hEq : (1 : Circle) = Circle.exp Real.pi :=
153 TotallyDisconnectedSpace.eq_of_continuous
154 (f := fun z : Circle => z) continuous_id 1 (Circle.exp Real.pi)
155 exact circleTarget_one_ne_exp_pi hEq
157/-- A compact subgroup of `T` contained in the open right half-plane is trivial. -/
160 (hApos : ∀ z ∈ A, 0 < Complex.re (z : ℂ)) :
161 A = ⊥ := by
162 classical
163 by_cases hAbot : A = ⊥
164 · exact hAbot
165 have hAproper : A ≠ ⊤ := by
166 intro hAtop
167 have hneg : Circle.exp Real.pi ∈ A := by
168 simp only [hAtop, Subgroup.mem_top]
169 have hneg' : ¬ 0 < Complex.re ((Circle.exp Real.pi : Circle) : ℂ) := by
170 simp only [Circle.coe_exp, Complex.exp_pi_mul_I, Complex.neg_re, Complex.one_re, Left.neg_pos_iff, not_lt,
171 zero_le_one]
172 exact hneg' (hApos (Circle.exp Real.pi) hneg)
173 have hAfinite : Finite A :=
174 properClosedSubgroup_circleTarget_finite A hAcompact.isClosed hAproper
175 letI : Fintype A := Fintype.ofFinite A
176 have hCircleToUnits_injective :
177 Function.Injective (Circle.toUnits : Circle →* Units ℂ) := by
178 simpa [Circle.toUnits] using unitSphereToUnits_injective (𝕜 := ℂ)
179 let B : Subgroup (Units ℂ) := A.map Circle.toUnits
180 let e : A ≃* B := A.equivMapOfInjective Circle.toUnits hCircleToUnits_injective
181 have hBfinite : Finite B := Finite.of_equiv A e
182 letI : Fintype B := Fintype.ofFinite B
183 have hBnebot : B ≠ ⊥ := by
184 intro hBbot
185 apply hAbot
186 exact (Subgroup.map_eq_bot_iff_of_injective
187 (H := A) (f := Circle.toUnits) hCircleToUnits_injective).mp (by simpa [B] using hBbot)
188 have hsumB : ∑ x : B, ((x : Units ℂ) : ℂ) = 0 :=
189 FiniteField.sum_subgroup_units_eq_zero hBnebot
190 have hsumA : ∑ x : A, (x : ℂ) = 0 := by
191 calc
192 ∑ x : A, (x : ℂ) = ∑ x : A, (((e x : B) : Units ℂ) : ℂ) := by
193 exact Fintype.sum_congr _ _ fun x => by
194 simp only [Subgroup.coe_equivMapOfInjective_apply, Circle.toUnits_apply, Units.val_mk0, B, e]
195 _ = ∑ y : B, ((y : Units ℂ) : ℂ) := by
196 simpa using (e.toEquiv.sum_comp fun y : B => ((y : Units ℂ) : ℂ))
197 _ = 0 := hsumB
198 have hsumRePos : 0 < Complex.re (∑ x : A, (x : ℂ)) := by
199 rw [Complex.re_sum]
200 simpa using
201 (Finset.sum_pos' (s := (Finset.univ : Finset A))
202 (f := fun x : A => Complex.re (x : ℂ))
203 (fun x hx => le_of_lt (hApos x x.2))
204 ⟨1, by simp only [Finset.mem_univ], hApos (1 : Circle) A.one_mem⟩)
205 exfalso
206 rw [hsumA] at hsumRePos
207 simp only [Complex.zero_re, lt_self_iff_false] at hsumRePos
209/-- The Pontryagin dual of a compact abelian group is discrete. -/
210theorem dualGroup_discrete_of_compact [CompactSpace G] :
211 DiscreteTopology (PontryaginDual G) := by
212 let U : Set Circle := {z | 0 < Complex.re (z : ℂ)}
213 let V : Set (PontryaginDual G) := {χ | Set.MapsTo χ Set.univ U}
214 have hUopen : IsOpen U := by
215 change IsOpen {z : Circle | 0 < Complex.re (z : ℂ)}
216 exact isOpen_lt continuous_const (Complex.continuous_re.comp continuous_subtype_val)
217 have hVopen : IsOpen V := by
218 let W : Set C(G, Circle) := {f | Set.MapsTo f Set.univ U}
219 have hWopen : IsOpen W := by
220 simpa [W] using
221 (ContinuousMap.isOpen_setOf_mapsTo
222 (X := G) (Y := Circle) (K := Set.univ) (U := U) isCompact_univ hUopen)
223 exact (ContinuousMonoidHom.isInducing_toContinuousMap G Circle).isOpen_iff.mpr
224 ⟨W, hWopen, by ext χ; rfl⟩
225 have hVeq : V = ({1} : Set (PontryaginDual G)) := by
226 ext χ
227 constructor
228 · intro hχ
229 rw [Set.mem_singleton_iff]
230 let A : Subgroup Circle := χ.toMonoidHom.range
232 simpa [A] using isCompact_range χ.continuous_toFun
233 have hApos : ∀ z ∈ A, 0 < Complex.re (z : ℂ) := by
234 intro z hz
235 rcases hz with ⟨g, rfl⟩
236 exact hχ (by simp only [Set.mem_univ])
237 have hAbot : A = ⊥ :=
238 subgroup_eq_bot_of_isCompact_subset_rightHalfPlane A hAcompact hApos
239 apply ContinuousMonoidHom.ext
240 intro g
241 have hg : χ g ∈ A := ⟨g, rfl⟩
242 have hg' : χ g ∈ (⊥ : Subgroup Circle) := by
243 simpa [hAbot] using hg
244 simpa using hg'
245 · intro hχ
246 rw [Set.mem_singleton_iff] at hχ
247 subst hχ
248 intro _g _hg
249 change 0 < Complex.re ((1 : Circle) : ℂ)
250 norm_num
251 have hOneOpen : IsOpen ({1} : Set (PontryaginDual G)) := by
252 simpa [hVeq] using hVopen
253 exact discreteTopology_of_isOpen_singleton_one hOneOpen
255/-- A discrete abelian group has compact Pontryagin dual. -/
256instance dualCompactSpaceOfDiscreteTopology [DiscreteTopology G] :
257 CompactSpace (PontryaginDual G) := by
258 infer_instance
260/-- The Pontryagin dual of a discrete abelian group is compact. -/
261theorem dualGroup_compact_of_discrete [DiscreteTopology G] :
262 CompactSpace (PontryaginDual G) := by
263 infer_instance
265private noncomputable def torsionPowerWitnessOfElement
266 {G : Type u} [CommGroup G] (htors : Monoid.IsTorsion G) (g : G) : ℕ :=
267 Classical.choose <| (isOfFinOrder_iff_pow_eq_one).mp (htors g)
269private theorem torsionPowerWitnessOfElement_pos
270 {G : Type u} [CommGroup G] (htors : Monoid.IsTorsion G) (g : G) :
271 0 < torsionPowerWitnessOfElement htors g :=
272 (Classical.choose_spec <| (isOfFinOrder_iff_pow_eq_one).mp (htors g)).1
274private theorem pow_torsionPowerWitnessOfElement_eq_one
275 {G : Type u} [CommGroup G] (htors : Monoid.IsTorsion G) (g : G) :
276 g ^ torsionPowerWitnessOfElement htors g = 1 :=
277 (Classical.choose_spec <| (isOfFinOrder_iff_pow_eq_one).mp (htors g)).2
279/-- The Pontryagin dual of a discrete torsion abelian group is totally disconnected. -/
281 (G : Type u) [CommGroup G] [TopologicalSpace G]
282 [DiscreteTopology G] (htors : Monoid.IsTorsion G) :
283 TotallyDisconnectedSpace (PontryaginDual G) := by
284 let n : G → ℕ := torsionPowerWitnessOfElement htors
285 let Ω : G → Type := fun g => { z : Circle // (z : ℂ) ^ n g = 1 }
286 have hΩfinite : ∀ g : G, Finite (Ω g) := by
287 intro g
288 classical
289 letI : NeZero (n g) := ⟨Nat.ne_of_gt <| torsionPowerWitnessOfElement_pos htors g⟩
290 have hcomplexFinite :
291 Finite {z : ℂ // z ∈ Polynomial.nthRoots (n g) (1 : ℂ)} := by
292 simpa using
293 (((Polynomial.nthRoots (n g) (1 : ℂ)).toFinset.finite_toSet).to_subtype)
294 refine Finite.of_injective
295 (f := fun z : Ω g =>
296 (⟨(z : ℂ), (Polynomial.mem_nthRoots (Nat.pos_of_neZero (n g))).2 z.2⟩ :
297 {z : ℂ // z ∈ Polynomial.nthRoots (n g) (1 : ℂ)})) ?_
298 intro x y hxy
299 have hxyComplex : ((x : Ω g) : ℂ) = ((y : Ω g) : ℂ) := by
300 exact congrArg
301 (fun w : {z : ℂ // z ∈ Polynomial.nthRoots (n g) (1 : ℂ)} => (w : ℂ)) hxy
302 have hxyCircle : ((x : Ω g) : Circle) = ((y : Ω g) : Circle) := by
303 apply Subtype.ext
304 exact hxyComplex
305 exact Subtype.ext hxyCircle
306 letI : ∀ g : G, Finite (Ω g) := hΩfinite
307 letI : ∀ g : G, TopologicalSpace (Ω g) := fun _ => inferInstance
308 letI : ∀ g : G, DiscreteTopology (Ω g) := fun _ => inferInstance
309 let F : PontryaginDual G → ∀ g : G, Ω g := fun χ g =>
310 ⟨χ g, by
311 have hpow : χ g ^ n g = 1 := by
312 calc
313 χ g ^ n g = χ (g ^ n g) := by simp only [map_pow]
314 _ = 1 := by simp only [pow_torsionPowerWitnessOfElement_eq_one (htors := htors) g, map_one, n]
315 exact congrArg (fun z : Circle => (z : ℂ)) hpow⟩
316 have hFcont : Continuous F := by
317 refine continuous_pi ?_
318 intro g
319 exact
320 ((continuous_eval_const (F := C(G, Circle)) g).comp
321 (ContinuousMonoidHom.isInducing_toContinuousMap G Circle).continuous).subtype_mk
322 fun χ => (F χ g).2
323 have hFinj : Function.Injective F := by
324 intro χ ψ hχψ
325 apply ContinuousMonoidHom.ext
326 intro g
327 exact congrArg (fun z : Ω g => (z : Circle)) (congrFun hχψ g)
328 let FRange : PontryaginDual G → Set.range F := fun χ => ⟨F χ, ⟨χ, rfl⟩⟩
329 have hFRange_continuous : Continuous FRange := hFcont.subtype_mk fun _ => ⟨_, rfl⟩
330 have hFRange_bij : Function.Bijective FRange := by
331 refine ⟨?_, ?_⟩
332 · intro χ ψ hχψ
333 exact hFinj <| congrArg Subtype.val hχψ
334 · rintro ⟨y, χ, rfl⟩
335 exact ⟨χ, rfl⟩
336 let eTop : PontryaginDual G ≃ₜ Set.range F :=
337 Continuous.homeoOfBijectiveCompactToT2 hFRange_continuous hFRange_bij
338 letI : TotallyDisconnectedSpace (Set.range F) := inferInstance
339 exact Homeomorph.totallyDisconnectedSpace eTop.symm
341/-- The Pontryagin dual of a discrete torsion abelian group is profinite. -/
343 (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
344 [DiscreteTopology G] (htors : Monoid.IsTorsion G) :
345 IsProfiniteGroup (PontryaginDual G) := by
346 exact ⟨inferInstance, dualGroup_compact_of_discrete (G := G), inferInstance,
347 dualGroup_totallyDisconnected_of_discrete_torsion (G := G) htors⟩
349/-- Evaluation formula for the induced dual map. -/
350@[simp] theorem dualGroup_map_apply
351 {H : Type v} [CommGroup H] [TopologicalSpace H]
352 (f : G →ₜ* H) (χ : PontryaginDual H) (g : G) :
353 PontryaginDual.map f χ g = χ (f g) := by
354 exact PontryaginDual.map_apply f χ g
356/-- Identity compatibility for the induced dual map. -/
357@[simp] theorem dualGroup_map_one :
358 PontryaginDual.map (1 : G →ₜ* G) = 1 := by
359 exact PontryaginDual.map_one
361/-- Composition compatibility for the induced dual map. -/
362@[simp] theorem dualGroup_map_comp
363 {H K : Type*} [CommGroup H] [TopologicalSpace H]
364 [CommGroup K] [TopologicalSpace K]
365 (g : H →ₜ* K) (f : G →ₜ* H) :
366 PontryaginDual.map (g.comp f) = (PontryaginDual.map f).comp (PontryaginDual.map g) := by
367 exact PontryaginDual.map_comp g f
369/-- Multiplicative compatibility for the induced dual map. -/
370@[simp] theorem dualGroup_map_mul
371 {H : Type*} [CommGroup H] [TopologicalSpace H] [IsTopologicalGroup H]
372 (f₁ f₂ : G →ₜ* H) :
373 PontryaginDual.map (f₁ * f₂) = PontryaginDual.map f₁ * PontryaginDual.map f₂ := by
374 exact PontryaginDual.map_mul f₁ f₂
376/-- For a discrete abelian group, multiplicative characters to the circle are the same as
377additive characters on the additive type synonym. -/
378noncomputable def dualGroupEquivAddCharCircle
379 (A : Type u) [CommGroup A] [TopologicalSpace A] [DiscreteTopology A] :
380 PontryaginDual A ≃ AddChar (Additive A) Circle where
381 toFun := fun χ =>
382 { toFun := fun a => χ a.toMul
384 map_add_eq_mul' := by
385 intro a b
387 invFun := fun χ =>
388 { toFun := fun a => χ (Additive.ofMul a)
389 map_one' := by simp only [ofMul_one, AddChar.map_zero_eq_one]
390 map_mul' := by
391 intro a b
392 exact χ.map_add_eq_mul (Additive.ofMul a) (Additive.ofMul b)
393 continuous_toFun := continuous_of_discreteTopology }
394 left_inv := by
395 intro χ
396 apply ContinuousMonoidHom.ext
397 intro a
398 rfl
399 right_inv := by
400 intro χ
401 ext a
402 rfl
404/-- The Pontryagin dual of a finite discrete abelian group is finite. -/
406 (A : Type u) [CommGroup A] [TopologicalSpace A] [Finite A] [DiscreteTopology A] :
407 Finite (PontryaginDual A) := by
408 classical
409 letI : Fintype A := Fintype.ofFinite A
410 letI : Fintype (Additive A) := Fintype.ofFinite (Additive A)
411 haveI : Finite (AddChar (Additive A) ℂ) := by infer_instance
412 haveI : Finite (AddChar (Additive A) Circle) :=
413 Finite.of_equiv (AddChar (Additive A) ℂ)
414 (AddChar.circleEquivComplex (α := Additive A)).symm
415 exact Finite.of_equiv (AddChar (Additive A) Circle)
416 (dualGroupEquivAddCharCircle A).symm
418/-- A finite discrete abelian group and its Pontryagin dual have the same cardinality. -/
420 (A : Type u) [CommGroup A] [TopologicalSpace A] [Finite A] [DiscreteTopology A] :
421 Nat.card (PontryaginDual A) = Nat.card A := by
422 classical
423 letI : Fintype A := Fintype.ofFinite A
424 letI : Fintype (Additive A) := Fintype.ofFinite (Additive A)
425 let e₁ := dualGroupEquivAddCharCircle A
426 let e₂ := (AddChar.circleEquivComplex (α := Additive A)).toEquiv
427 haveI : Finite (PontryaginDual A) := dualGroup_finite_of_finite_discrete A
428 letI : Fintype (PontryaginDual A) := Fintype.ofFinite (PontryaginDual A)
429 haveI : Finite (AddChar (Additive A) Circle) :=
430 Finite.of_equiv (AddChar (Additive A) ℂ)
431 (AddChar.circleEquivComplex (α := Additive A)).symm
432 letI : Fintype (AddChar (Additive A) Circle) :=
433 Fintype.ofFinite (AddChar (Additive A) Circle)
434 calc
435 Nat.card (PontryaginDual A) = Fintype.card (PontryaginDual A) := Nat.card_eq_fintype_card
436 _ = Fintype.card (AddChar (Additive A) Circle) := Fintype.card_congr e₁
437 _ = Fintype.card (AddChar (Additive A) ℂ) := Fintype.card_congr e₂
438 _ = Fintype.card (Additive A) := AddChar.card_eq (α := Additive A)
439 _ = Fintype.card A := rfl
440 _ = Nat.card A := Nat.card_eq_fintype_card.symm
442/-- A topological group equivalence induces an equivalence on Pontryagin duals. -/
443noncomputable def dualGroupEquiv
444 {H : Type v} [CommGroup H] [TopologicalSpace H]
445 (e : G ≃ₜ* H) :
446 PontryaginDual H ≃* PontryaginDual G :=
447{ toFun := PontryaginDual.map e.toContinuousMonoidHom
448 invFun := PontryaginDual.map e.symm.toContinuousMonoidHom
449 left_inv := by
450 intro χ
451 apply ContinuousMonoidHom.ext
452 intro g
454 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.apply_symm_apply]
455 right_inv := by
456 intro χ
457 apply ContinuousMonoidHom.ext
458 intro g
460 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply]
461 map_mul' := by
462 intro χ ψ
465/-- A topological group equivalence induces a continuous equivalence on Pontryagin duals. -/
466noncomputable def dualGroupContinuousMulEquiv
467 {H : Type v} [CommGroup H] [TopologicalSpace H]
468 (e : G ≃ₜ* H) :
469 PontryaginDual H ≃ₜ* PontryaginDual G :=
471 (PontryaginDual.map e.toContinuousMonoidHom)
472 (PontryaginDual.map e.symm.toContinuousMonoidHom)
473 (by
474 intro χ
475 apply ContinuousMonoidHom.ext
476 intro h
478 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.apply_symm_apply])
479 (by
480 intro χ
481 apply ContinuousMonoidHom.ext
482 intro g
484 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply])
486@[simp] theorem dualGroupContinuousMulEquiv_toMulEquiv
487 {H : Type v} [CommGroup H] [TopologicalSpace H]
488 (e : G ≃ₜ* H) :
489 (dualGroupContinuousMulEquiv (G := G) e).toMulEquiv = dualGroupEquiv (G := G) e :=
490 rfl
492end Basic
494end ProCGroups.Duality