Profinite completion of topological groups

AbbreviationOpen finite-index normal subgroups#✓fully proved

For a group \(G\) with a topology, this is the set of normal subgroups \(H\) of \(G\) that have finite index and are open in \(G\), ordered by inclusion and viewed as a category: there is a morphism \(H \to K\) exactly when \(H \subseteq K\).

abbrev Index (G : Type u) [Group G] [TopologicalSpace G] :=
  { H : FiniteIndexNormalSubgroup G // IsOpen (H : Set G) }

Used by 7

Used byOpen profinite completion of a group · The canonical map has dense image · Diagram of finite quotients as profinite groups · Canonical map into the open profinite completion · Coordinates of the canonical map · Continuity of the canonical map · Diagram of finite quotients

DefinitionDiagram of finite quotients#✓fully proved

For a group \(G\) with a topology, this is the functor from the category of open finite-index normal subgroups of \(G\) to finite groups that sends \(H\) to the quotient group \(G/H\) and sends an inclusion \(H \subseteq K\) to the projection \(G/H \to G/K\), \(gH \mapsto gK\).

def finiteGrpDiagram (G : Type u) [Group G]
    [TopologicalSpace G] : Index G ⥤ FiniteGrp.{u} where
  obj H := FiniteGrp.of <| G ⧸ H.1.toSubgroup
  map f :=
    FiniteGrp.ofHom <| QuotientGroup.map _ _ (MonoidHom.id _) f.le
  map_id H := by ext ⟨x⟩; rfl
  map_comp f g := by ext ⟨x⟩; rfl

Uses 1 · Used by 2

Statement usesOpen finite-index normal subgroups

Used byThe canonical map has dense image · Diagram of finite quotients as profinite groups

DefinitionDiagram of finite quotients as profinite groups#✓fully proved

For a group \(G\) with a topology, this is the functor that sends each open finite-index normal subgroup \(H\) of \(G\) to the finite quotient group \(G/H\) with the discrete topology, regarded as a profinite group, and each inclusion \(H \subseteq K\) to the projection \(G/H \to G/K\), \(gH \mapsto gK\). It is the diagram of finite quotients followed by the inclusion of finite groups into profinite groups.

def diagram (G : Type u) [Group G] [TopologicalSpace G] :
    Index G ⥤ ProfiniteGrp.{u} :=
  finiteGrpDiagram G ⋙ forget₂ (FiniteGrp.{u}) (ProfiniteGrp.{u})

Uses 2 · Used by 5

Statement usesOpen finite-index normal subgroups · Diagram of finite quotients

Used byOpen profinite completion of a group · The canonical map has dense image · Canonical map into the open profinite completion · Coordinates of the canonical map · Continuity of the canonical map

DefinitionOpen profinite completion of a group#✓fully proved

For a group \(G\) with a topology, the open profinite completion of \(G\) is the limit, in profinite groups, of the diagram of finite quotients \(G/H\), where \(H\) runs over the open finite-index normal subgroups of \(G\) and the transition maps are the projections \(G/H \to G/K\) for \(H \subseteq K\). Concretely, it is the group of families \((x_H)_H\) with \(x_H \in G/H\) that are compatible under these projections, with the topology of a subspace of the product of the discrete groups \(G/H\).

def completion (G : Type u) [Group G] [TopologicalSpace G] :
    ProfiniteGrp.{u} :=
  ProfiniteGrp.limit (diagram G)

Uses 2 · Used by 5

Statement usesOpen finite-index normal subgroups · Diagram of finite quotients as profinite groups

Used byDensity of the canonical homomorphism · The canonical map has dense image · Canonical homomorphism into the open profinite completion · Canonical map into the open profinite completion · Continuity of the canonical map

DefinitionCanonical map into the open profinite completion#✓fully proved

For a group \(G\) with a topology, this is the map from \(G\) to its open profinite completion that sends \(x \in G\) to the family of cosets \((xH)_H\), where \(H\) runs over the open finite-index normal subgroups of \(G\).

def etaFn (G : Type u) [Group G] [TopologicalSpace G]
    (x : G) : completion G :=
  ⟨fun _ => QuotientGroup.mk x, fun _ _ _ => rfl⟩

Uses 3 · Used by 4

Statement usesOpen finite-index normal subgroups · Open profinite completion of a group · Diagram of finite quotients as profinite groups

Used byThe canonical map has dense image · Canonical homomorphism into the open profinite completion · Coordinates of the canonical map · Continuity of the canonical map

TheoremCoordinates of the canonical map#✓fully proved

Let \(G\) be a group with a topology. For every \(x \in G\) and every open finite-index normal subgroup \(H\) of \(G\), the \(H\)-coordinate of the image of \(x\) under the canonical map into the open profinite completion of \(G\) is the coset \(xH \in G/H\).

@[simp]
theorem etaFn_apply (G : Type u) [Group G] [TopologicalSpace G] (x : G)
    (H : Index G) : ((etaFn G x).val H : G ⧸ H.1.toSubgroup) =
    QuotientGroup.mk x

Uses 3

Statement usesOpen finite-index normal subgroups · Diagram of finite quotients as profinite groups · Canonical map into the open profinite completion

TheoremContinuity of the canonical map#✓fully proved

Let \(G\) be a group with a topology in which multiplication is separately continuous: \(x \mapsto ax\) and \(x \mapsto xa\) are continuous for every \(a \in G\). Then the canonical map from \(G\) to its open profinite completion is continuous.

Joint continuity of multiplication is not needed.

theorem etaFn_continuous (G : Type u) [Group G] [TopologicalSpace G]
    [SeparatelyContinuousMul G] : Continuous (etaFn G)

Uses 4 · Used by 1

Statement usesOpen profinite completion of a group · Canonical map into the open profinite completion

Proof usesOpen finite-index normal subgroups · Diagram of finite quotients as profinite groups

Used byCanonical homomorphism into the open profinite completion

DefinitionCanonical homomorphism into the open profinite completion#✓fully proved

Let \(G\) be a group with a topology in which multiplication is separately continuous. This is the canonical map from \(G\) to its open profinite completion, \(x \mapsto (xH)_H\) with \(H\) running over the open finite-index normal subgroups of \(G\), regarded as a continuous group homomorphism.

def eta (G : Type u) [Group G] [TopologicalSpace G]
    [SeparatelyContinuousMul G] : G →ₜ* completion G where
  toFun := etaFn G
  map_one' := rfl
  map_mul' _ _ := rfl
  continuous_toFun := etaFn_continuous G

Uses 3 · Used by 1

Statement usesOpen profinite completion of a group · Canonical map into the open profinite completion · Continuity of the canonical map

Used byDensity of the canonical homomorphism

TheoremThe canonical map has dense image#✓fully proved

For every group \(G\) with a topology, the image of the canonical map from \(G\) to its open profinite completion is dense.

No compatibility between the multiplication and the topology of \(G\) is assumed.

theorem denseRange_etaFn (G : Type u) [Group G] [TopologicalSpace G] :
    DenseRange (etaFn G)

Uses 5 · Used by 1

Statement usesOpen profinite completion of a group · Canonical map into the open profinite completion

Proof usesOpen finite-index normal subgroups · Diagram of finite quotients as profinite groups · Diagram of finite quotients

Used byDensity of the canonical homomorphism

TheoremDensity of the canonical homomorphism#✓fully proved

Let \(G\) be a group with a topology in which multiplication is separately continuous. Then the canonical continuous homomorphism from \(G\) to its open profinite completion has dense image.

theorem denseRange_eta (G : Type u) [Group G] [TopologicalSpace G]
    [SeparatelyContinuousMul G] : DenseRange (eta G)

Uses 3

Statement usesOpen profinite completion of a group · Canonical homomorphism into the open profinite completion

Proof usesThe canonical map has dense image

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.