Strong completeness of profinite groups

DefinitionStrongly complete group#✓fully proved

A group \(G\) equipped with a topology is strongly complete when every subgroup of finite index in \(G\) is open.

def IsStronglyComplete (G : Type*) [Group G] [TopologicalSpace G] : Prop :=
  ∀ H : Subgroup G, H.FiniteIndex → IsOpen (H : Set G)

Used by 2

Used byStrongly complete profinite groups via the profinite completion · Nikolov–Segal strong completeness theorem

TheoremFinite-index normal subgroups are closed when the completion map is onto#✓fully proved

Let \(P\) be a profinite group and let \(\hat P\) be the profinite completion of \(P\) as an abstract group, that is, the inverse limit of the finite quotients \(P/N\) over all normal subgroups \(N\) of finite index in \(P\). If the canonical map \(P \to \hat P\) is surjective, then every normal subgroup of finite index in \(P\) is closed in \(P\).

theorem isClosed_toSubgroup_of_surjective_etaFn
    (N : FiniteIndexNormalSubgroup (GrpCat.of ↥P))
    (hsurj : Function.Surjective (etaFn (GrpCat.of ↥P))) :
    IsClosed (N.toSubgroup : Set ↥P)

Used by 1

Used byFinite-index normal subgroups are open when the completion map is onto

TheoremFinite-index normal subgroups are open when the completion map is onto#✓fully proved

Let \(P\) be a profinite group and let \(\hat P\) be the profinite completion of \(P\) as an abstract group, that is, the inverse limit of the finite quotients \(P/N\) over all normal subgroups \(N\) of finite index in \(P\). If the canonical map \(P \to \hat P\) is surjective, then every normal subgroup of finite index in \(P\) is open in \(P\).

theorem isOpen_toSubgroup_of_surjective_etaFn
    (N : FiniteIndexNormalSubgroup (GrpCat.of ↥P))
    (hsurj : Function.Surjective (etaFn (GrpCat.of ↥P))) :
    IsOpen (N.toSubgroup : Set ↥P)

Uses 1 · Used by 1

Proof usesFinite-index normal subgroups are closed when the completion map is onto

Used byStrongly complete profinite groups via the profinite completion

TheoremStrongly complete profinite groups via the profinite completion#✓fully proved

Let \(P\) be a profinite group and let \(\hat P\) be the profinite completion of \(P\) as an abstract group, that is, the inverse limit of the finite quotients \(P/N\) over all normal subgroups \(N\) of finite index in \(P\). Then \(P\) is strongly complete if and only if the canonical map \(P \to \hat P\) is bijective.

theorem isStronglyComplete_iff_bijective_etaFn :
    IsStronglyComplete ↥P ↔ Function.Bijective (etaFn (GrpCat.of ↥P))

Uses 2

Statement usesStrongly complete group

Proof usesFinite-index normal subgroups are open when the completion map is onto

DefinitionTopologically finitely generated group#✓fully proved

A topological group is topologically finitely generated if some finite set generates a dense abstract subgroup.

def IsTopologicallyFinitelyGenerated
    (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
  ∃ S : Finset G, (Subgroup.closure (S : Set G)).topologicalClosure = ⊤

Used by 1

Used byNikolov–Segal strong completeness theorem

TheoremNikolov–Segal strong completeness theorem#●ready to prove

Every finite-index subgroup of a topologically finitely generated profinite group is open.

public theorem_wanted nikolov_segal
    (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hG : IsTopologicallyFinitelyGenerated G) :
    IsStronglyComplete G

Sources

• Nikolay Nikolov and Dan Segal, On finitely generated profinite groups, I: strong completeness and uniform bounds, Annals of Mathematics 165 (2007), no. 1, 171–238, Theorem 1.1, https://doi.org/10.4007/annals.2007.165.171; On finitely generated profinite groups, II: products in quasisimple groups, Annals of Mathematics 165 (2007), no. 1, 239–273, https://doi.org/10.4007/annals.2007.165.239. Problem nikolov_segal of the lean-eval benchmark.

Uses 2

Statement usesStrongly complete group · Topologically finitely generated group

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.