ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups

9 sections | 9 files | 121 declarations

This aggregate exports the concrete right-quotient and Schreier-cocycle constructions, exact right-Schreier generation, finite permutation targets, rank bounds, and finite-rank basis theorems for open subgroups of free pro-\(C\) groups.

Basis conclusions use EpimorphicallyFreeProCGroupOnConvergingSetData directly. There is no parallel RS-specific carrier/model wrapper layer.

imports

Imported by

ProCGroups.ReidemeisterSchreier.Profinite

BasisFiniteRank

1 file | 4 declarations | 4 Theorems

Starting from a finite converging-set basis, this module constructs a basis of the open subgroup and proves the classical finite Schreier rank formula. The padding lemma works o...

BasisTheorems

1 file | 8 declarations | 7 Theorems | 1 Definition

This module turns the exact right-Schreier generation theorem into completion and basis statements. It isolates finite-quotient lifting, compares dense abstract free groups with...

DenseFreeModel

1 file | 15 declarations | 12 Theorems | 3 Definitions

This module transports right-coset sections across a dense free-group lift, proves that the preimage of an open subgroup remains dense, and applies the discrete Nielsen--Schreie...

ExactRightSchreierGeneration

1 file | 12 declarations | 11 Theorems | 1 Instance

Using a transported right-coset section and the wreath-product embedding, this module identifies the concrete right-Schreier cocycles that topologically generate an open subgrou...

FinitePermutationTargets

This module packages the finite permutation image of the coset action of an open subgroup, proves continuity of the action homomorphism, and transfers finite-group-class members...

MinimalPower

1 file | 3 declarations | 3 Theorems

If the first positive power of a distinguished generator entering an open subgroup is nontrivial, this module constructs a finite converging-set basis containing that power and ...

RankBound

1 file | 6 declarations | 5 Theorems | 1 Definition

This module defines the cardinal Schreier transform, proves its finite and infinite simplifications, and bounds the topological rank of an open subgroup of a compact Hausdorff t...

RightQuotient

For an open subgroup this module specializes the right-coset space used by Schreier rewriting. It supplies the coset action, finiteness under compactness, the discrete quotient ...

SchreierTransversals

The source of truth is `SchreierCocycleData`: it stores a left/right orientation, a section map, the next-coset operation, and the proof that the resulting cocycle lands in the ...