Module

SameFiniteQuotients.lean

Nyll.ProCGroups.Completion.SameFiniteQuotients

3 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Completion / Same Finite Quotients

This module compares abstract finite quotients with continuous finite discrete quotients and constructs maps between profinite completions from that comparison.

Imports3

Mathlib.GroupTheory.Finiteness
Nyll.ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
Nyll.ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation

Imported by1

Nyll.ProCGroups.Completion.All

def

HasSameContinuousFiniteDiscreteQuotients

L25 ↗

ProCGroups.Completion.HasSameContinuousFiniteDiscreteQuotients

Documentation

Topological finite quotient predicate using continuous maps to finite discrete groups.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups.Completion
universe u

Lean source · statement

def HasSameContinuousFiniteDiscreteQuotients
    (G₁ : Type u) [Group G₁] [TopologicalSpace G₁]
    (G₂ : Type u) [Group G₂] [TopologicalSpace G₂] : Prop

theorem

exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients

L37 ↗

ProCGroups.Completion.exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients

Documentation

The continuous finite quotient hypothesis yields a surjective continuous homomorphism between topologically finitely generated profinite groups.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups.Completion
universe u

Lean source · statement

theorem
  exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients
    {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
    {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]
    [CompactSpace G₁]
    [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]
    (hG₁fg : FiniteGeneration.TopologicallyFinitelyGenerated G₁)
    (hquot : HasSameContinuousFiniteDiscreteQuotients G₁ G₂) :
    ∃ φ : ContinuousMonoidHom G₁ G₂, Function.Surjective φ

theorem

topologicallyFinitelyGenerated_profiniteGroups_iso_of_sameContinuousFiniteQuotients

L246 ↗

ProCGroups.Completion.topologicallyFinitelyGenerated_profiniteGroups_iso_of_sameContinuousFiniteQuotients

Documentation

Topologically finitely generated profinite groups are determined by their continuous finite discrete quotients.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups.Completion
universe u

Lean source · statement

theorem topologicallyFinitelyGenerated_profiniteGroups_iso_of_sameContinuousFiniteQuotients
    {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
    {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]
    [CompactSpace G₁] [T2Space G₁] [TotallyDisconnectedSpace G₁]
    [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]
    (hfg₁ : FiniteGeneration.TopologicallyFinitelyGenerated G₁)
    (hfg₂ : FiniteGeneration.TopologicallyFinitelyGenerated G₂)
    (hquot : HasSameContinuousFiniteDiscreteQuotients G₁ G₂) :
    Nonempty (G₁ ≃ₜ* G₂)

Module documentation

Pro C Groups / Completion / Same Finite Quotients

Declarations

HasSameContinuousFiniteDiscreteQuotients

exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients

topologicallyFinitelyGenerated_profiniteGroups_iso_of_sameContinuousFiniteQuotients