ProCGroups.ProC.OpenNormalSubgroups

9 sections | 9 files | 136 declarations

This module develops finite quotient, subgroup, free pro-\(C\), generation, and cardinal-invariant constructions for profinite and pro-\(C\) groups.

Basic

1 files | 28 declarations | 19 Theorem | 6 Definition | 3 Instance

Open normal subgroups have a top element: the whole group.

BasisAtOne

1 files | 1 declarations | 1 Theorem

In a compact totally disconnected topological group, any open neighborhood of \(1\) contains an open normal subgroup.

ClosedAndCosets

1 files | 4 declarations | 4 Theorem

A closed subgroup of a profinite group is the intersection of all open subgroups containing it.

ClosedCommutator

1 files | 11 declarations | 11 Theorem

A quotient-level commutator descent along a surjective homomorphism. If \(f: N \to K\) is onto, f n is in the ordinary commutator subgroup of K, and the kernel of f dies in the ...

CountableChains

1 files | 4 declarations | 3 Theorem | 1 Definition

Preparatory countable-chain layer for later use: \(1\) has a countable fundamental system of open normal subgroups. This isolates the part of the corollary that does not yet dep...

FilteredFamilies

1 files | 7 declarations | 7 Theorem

A nonempty finite subfamily of a directed family of sets has a common lower bound for the reverse-inclusion order.

LimitPresentation

1 files | 7 declarations | 5 Theorem | 2 Definition

A pro-\(C\) group is canonically the inverse limit of its quotients by open normal subgroups whose quotients lie in \(C\).

ProCGroup

A neighborhood-basis formulation using open normal subgroups whose quotients lie in \(C\). We isolate it as a separate predicate because it is the main usable local output for l...

Separation

1 files | 10 declarations | 8 Theorem | 2 Definition

Membership in a closed subset of a profinite group can be tested on all open-normal quotients.