Module

ProfiniteCharacterCriterion.lean

Nyll.ProCGroups.Abelian.ProfiniteCharacterCriterion

2 declarations indexed from sourceView source ↗

Module documentation

Detecting isomorphisms of profinite abelian groups by actual characters

Bijectivity of pullback on continuous circle-valued characters detects bijectivity of the original homomorphism. Surjectivity uses the actual profinite biduality theorem and the continuity of the inverse between the discrete character groups.

Imports3

Nyll.ProCGroups.Abelian.ProfiniteBidual
Mathlib.Topology.Algebra.PontryaginDual
Mathlib.Topology.Homeomorph.Lemmas

Imported by2

theorem

bijective_of_bijective_character_pullback

L34 ↗

ProCGroups.Duality.bijective_of_bijective_character_pullback

Documentation

Actual character pullback detects bijectivity of a continuous homomorphism.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups.Duality
universe u v
variable {G : Type u} {H : Type v} [CommGroup G] [CommGroup H]
  [TopologicalSpace G] [TopologicalSpace H]
  [IsTopologicalGroup G] [IsTopologicalGroup H]
  [CompactSpace G] [CompactSpace H]
  [TotallyDisconnectedSpace G] [TotallyDisconnectedSpace H]

Lean source · statement

theorem bijective_of_bijective_character_pullback (f : G →ₜ* H)
    (hf : Function.Bijective (PontryaginDual.map f)) : Function.Bijective f

def

equivOfBijectiveCharacterPullback

L64 ↗

ProCGroups.Duality.equivOfBijectiveCharacterPullback