Yamaguchi Lean 4 Library
ProCGroups.ProC.Quotients
ProCGroups/ProC/Quotients

ProCGroups.ProC.Quotients

6 sections | 6 files | 49 declarations

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

ClosedNormal

1 files | 12 declarations | 9 Theorem | 3 Definition
If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by a closed normal subgroup is again pro-\(C\). The proof reconstructs \(G/K\) as the inv...

ClosedSubgroupNeighborhoods

1 files | 2 declarations | 2 Theorem
Given an open subgroup of a closed subgroup of a profinite group, one can shrink it to the intersection with an ambient open normal subgroup.

DescendingClosedSubgroupQuotients

1 files | 4 declarations | 2 Theorem | 2 Definition
The infimum of a family of closed subgroups, repackaged as a closed subgroup.

LeftQuotientMaps

1 files | 9 declarations | 8 Theorem | 1 Definition
The natural projection \(G/K \to G/H\) for closed subgroups K \(\leq\) H is viewed as a quotient-space map on left cosets.

LeftQuotientProjectionSections

1 files | 16 declarations | 10 Theorem | 3 Definition | 1 Structure | 2 Instance
If an intermediate closed subgroup is not contained in the base subgroup, one can choose an element in the set-theoretic difference. This is the witness extraction used in the Z...

OpenSubgroupSections

1 files | 6 declarations | 5 Theorem | 1 Definition
A normalized set-theoretic section of the quotient map by an open subgroup. Since the quotient is discrete, this section is automatically continuous.