Module

FiniteCharacterCriterion.lean

Nyll.ProCGroups.Abelian.FiniteCharacterCriterion

3 declarations indexed from sourceView source ↗

Module documentation

Finite coefficient detection of profinite abelian isomorphisms

Every actual circle character has finite image. Thus bijectivity on characters with finite subgroup coefficients gives bijectivity on all circle characters, and consequently a topological group isomorphism of the original groups.

Imports5

Nyll.ProCGroups.Abelian.ProfiniteCharacterCriterion
Nyll.ProCGroups.Abelian.ProfiniteBidual
Nyll.ProCGroups.ProC.OpenNormalSubgroups.Basic
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.Topology.Algebra.PontryaginDual

Imported by2

theorem

exists_finite_character_range

L36 ↗

ProCGroups.Duality.exists_finite_character_range

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Duality
open ProCGroups.ProC
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 exists_finite_character_range (χ : PontryaginDual G) :
    ∃ (A : Subgroup Circle) (_ : Finite A) (χA : G →ₜ* A),
      ∀ g : G, (χA g : Circle) = χ g

theorem

bijective_character_pullback_of_finite

L52 ↗

ProCGroups.Duality.bijective_character_pullback_of_finite

Documentation

Finite coefficient pullbacks determine the pullback on all circle characters.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Duality
open ProCGroups.ProC
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_character_pullback_of_finite (f : G →ₜ* H)
    (hf : ∀ (A : Subgroup Circle) [Finite A], Function.Bijective (f.compLeft A)) :
    Function.Bijective (PontryaginDual.map f)

def

equivOfBijectiveFiniteCharacterPullback

L85 ↗

ProCGroups.Duality.equivOfBijectiveFiniteCharacterPullback

Documentation

An actual map inducing bijections on all finite subgroup-valued characters is a topological isomorphism.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Duality
open ProCGroups.ProC
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

def equivOfBijectiveFiniteCharacterPullback (f : G →ₜ* H)
    (hf : ∀ (A : Subgroup Circle) [Finite A], Function.Bijective (f.compLeft A)) :
    G ≃ₜ* H

Module documentation

Finite coefficient detection of profinite abelian isomorphisms

Declarations

exists_finite_character_range

bijective_character_pullback_of_finite

equivOfBijectiveFiniteCharacterPullback