Module

ProPOfFiniteEmbedding.lean

Nyll.ProCGroups.ProC.ProPOfFiniteEmbedding

1 declaration indexed from sourceView source ↗

Module documentation

A compact group separated by continuous finite p-group coordinates

This is the existing product/closed-subgroup permanence argument applied to an actual continuous injective homomorphism. It requires no surjectivity of individual coordinates and no inverse-limit identification.

Imports6

Nyll.ProCGroups.ProC.Subgroups.Products
Nyll.ProCGroups.ProC.InverseLimits.Predicates
Nyll.ProCGroups.FiniteGroups.PGroupFormation
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Mathlib.Topology.Algebra.Group.Quotient
Mathlib.Topology.LocallyConstant.Basic

Imported by2

theorem

hasPGroupOpenNormalBasis_of_finiteCoordinates

L28 ↗

ProCGroups.ProC.hasPGroupOpenNormalBasis_of_finiteCoordinates

Documentation

A compact group embedded in a product of actual finite p-groups has an open-normal basis with finite p-group quotients.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u

Lean source · statement

theorem hasPGroupOpenNormalBasis_of_finiteCoordinates
    (p : ℕ) [Fact p.Prime]
    (G : GrpCat.{u}) [TopologicalSpace G.carrier] [IsTopologicalGroup G.carrier]
    [CompactSpace G.carrier]
    (ι : Type u) (H : ι → FiniteGrp.{u})
    (f : ∀ i : ι, G.carrier →* (H i).toGrp.carrier)
    (hf : ∀ i : ι, IsLocallyConstant (f i).toFun)
    (hsep : ∀ x y : G.carrier, (∀ i : ι, (f i).toFun x = (f i).toFun y) → x = y)
    (hp : ∀ i : ι, IsPGroup p (H i).toGrp.carrier) :
    HasPGroupOpenNormalBasis p G.carrier

Module documentation

A compact group separated by continuous finite p-group coordinates

Declarations

hasPGroupOpenNormalBasis_of_finiteCoordinates