ReidemeisterSchreier.Profinite.OpenSubgroups

Hypotheses used by the cardinal-rank Schreier basis theorem. The bridge is only needed in the infinite-rank branch, but bundling it here gives a single public theorem whose conc...

Hypotheses used by the finite-rank Schreier basis theorem. The bundle keeps the mathematical statement from hiding the variety/isomorphism/extension/cyclic assumptions behind sh...

Hypotheses used by the infinite-rank Schreier basis theorem. This mirrors SchreierBasisFiniteRankHypotheses, with the additional bridge needed in the infinite-rank argument.

Finite-discrete quotient lift property for a dense abstract Schreier model of an open subgroup.

The right relator map is compatible with comap of the open subgroup.

The profinite minimal-power argument reduces its distinguished Schreier generator to the discrete minimal-power Schreier-transversal theorem for the finite quotient/comap subgroup.

The finite permutation representation attached to an open subgroup of a concrete pro-\(C\) group has image in \(C\), packaged through \(\mathrm{ULift}\) to match universes.

A free pro-\(C\) basis on a fixed carrier.

This is the pointed profinite Reidemeister--Schreier theorem over a converging-set basis, with a prescribed minimal generator power landing in the open subgroup.

Cardinal form of the Schreier rank transform for an open subgroup of finite index \(n\). For finite rank this is the usual Schreier transform \(1+n(d-1)\). For infinite cardinal...

The right-coset space \(F/H\), encoded via right quotients.

The normalized continuous section of the left quotient by an open subgroup.