Profinite and pro-C groups

For a topological group G, first quotient by the closed commutator subgroup, then by the subgroup of q-th powers. Continuous homomorphisms descend to this quotient, and maps to commutative groups of exponent dividing q f…

This aggregate module exposes topological abelianization, its functoriality, and its compatibility with inverse limits.

Distinct classes in the topological abelianization of a profinite group are separated by a continuous homomorphism to an actual finite discrete abelian quotient. Applied to a normal subgroup, this identifies trivial conj…

Evaluation is continuous for compact groups. For finite discrete abelian groups it is an isomorphism: finite character separation gives injectivity, and the finite dual cardinality theorem gives surjectivity.

Every actual circle character has finite image. Thus bijectivity on characters with finite subgroup coefficients gives bijectivity on all circle characters, and consequently a topological group isomorphism of the origina…

A finite group of continuous automorphisms admits arbitrarily small invariant open normal subgroups. The construction is the kernel of the product of the translated finite quotient maps; in particular, invariance is prov…

The kernel of evaluation at n is exactly n times the full Tate module. Division inside that kernel is given by shifting the compatible family to the levels multiplied by n. Thus every character killed by n factors throug…

The full Tate module consists of actual torsion points indexed by positive integers, compatible under multiplication. It is torsion-free: if a positive integer annihilates a compatible family, compatibility with the leve…

Multiplicative automorphisms preserve the subgroup of powers and induce automorphisms of the corresponding quotient, with explicit evaluation.

Continuous characters with values in ZMod q separate profinite commutative groups of exponent q. In particular, simultaneous extension of characters forces the product map on abelianizations modulo q to be injective.

Every circle-valued character factors through a finite quotient, because the circle has no subgroup contained in a sufficiently small arc. Finite duality therefore solves any finite set of evaluation equations. Compactne…

Bijectivity of pullback on continuous circle-valued characters detects bijectivity of the original homomorphism. Surjectivity uses the actual profinite biduality theorem and the continuity of the inverse between the disc…

Restricting positive indices to a submonoid preserves products and therefore the actual multiplication transitions. Each coordinate is an actual torsion point, and the topology is the subspace topology of discrete torsio…

A finite subgroup of the circle is cyclic. Its order identifies it with the actual roots of unity of a separably closed characteristic-zero field. Transporting characters along this finite coefficient isomorphism reduces…

For a closed subgroup, the image of its closed commutator under the subgroup inclusion is the topological closure of its commutator in the ambient group.

This module develops the canonical quotient by the closed commutator subgroup, its universal property for continuous maps to Hausdorff commutative groups, and the induced quotient topology.

Topological abelianization defines a functor from topological groups to commutative topological groups. Its universal property is expressed directly as an equivalence of morphism types for \(T1\) targets.

For a continuous surjection from a compact group to a Hausdorff group, the kernel of the induced map on topological abelianizations is the image of the original kernel. Compactness makes the image of the closed commutato…

This module applies topological abelianization stagewise to inverse systems and compares the resulting limit with the abelianization of the original limit.

Trivial conjugation descends along a continuous homomorphism. Consequently, faithfulness on the image pulls back for normal subgroups containing its kernel.

Profinite and pro-C groups, finite quotients, inverse limits, free products and presentations. Includes completed group algebras, Fox differentials and relation-theoretic constructions.

Group-theoretic consequences of cyclotomic inversion for abelian quotients and topologically cyclic inertia.

If an element is conjugate to its inverse, then its image in an abelian quotient has order dividing two. Consequently an odd-order image is trivial. This is the group-theoretic step used in the residue- characteristic-tw…

In a profinite group, a conjugacy class is compact and hence closed. Thus two elements are conjugate exactly when their images are conjugate in every open-normal quotient.

This file upgrades the elementwise abelian consequence of cyclotomic inversion to a statement about an entire topologically cyclic inertia group. The generator is killed by inversion and oddness, and continuity then kill…

This module develops concrete fiber products of groups, identifies them with the categorical pullback in GrpCat, and proves comparison and kernel criteria for the associated lift maps.

This umbrella module exports the concrete algebraic and continuous pullback, comparison, quotient-pullback, and pushout APIs.

This module develops continuous fiber products and the universal property obtained by testing a continuous square against profinite source groups. The four objects in a tested square are not required to be profinite.

This module compares a profinite-tested continuous pullback square with its concrete fiber product and transports bijectivity and kernel criteria across the canonical comparison map.

This module constructs algebraic group pushouts from free products and normal closures, and develops algebraic and profinite-tested pushout universal properties.

This module identifies the quotient by an intersection with the concrete fiber product of the two quotient maps to the quotient by their supremum, in both the algebraic and continuous settings.

Canonical aggregate generated by the reviewed rehome.

Every continuous map from a pro-C group to a finite discrete space factors through one of the canonical open-normal quotients in C. This is the finite-stage input for reducing continuous finite-coefficient cochains to fi…

This file constructs nontrivial ZMod p-valued multiplicative characters on nontrivial normal subgroups of finite p-groups. Averaging is replaced by the fixed-point theorem for finite p-group actions, so the resulting cha…

A finite-basis free pro-p group lifts continuously through every continuous surjection from a pro-p group. The section form is the projective input for the standard proof that its continuous degree-two cohomology vanishe…

A finite family of ambient-conjugation-invariant continuous mod-p characters on a closed normal subgroup descends to one common finite p-group quotient. The construction preserves all pointwise ZMod p-linear relations, w…

Every ambient-conjugation-invariant continuous mod-p character on a closed normal subgroup of a pro-p group descends to the subgroup's image in one finite p-group quotient. This isolates the finite-stage input needed to…

A strict inclusion of closed ambient-normal subgroups of a pro-p group can be detected by a nonzero continuous ZMod p-valued character. The construction separates one element in a finite p-group quotient and applies the…

Completed group algebras are constructed as inverse limits of finite-quotient group algebras. The library develops their additive, ring, and topological structures together with projections, augmentation maps and ideals,…

This aggregate exports terminal-index and finite-stage augmentations, the canonical all-finite augmentation, its comparison with the \(C\)-indexed augmentation, and the completed augmentation ideal.

This file defines the kernel of the canonical augmentation on the all-finite completed group algebra, packages its short exact sequence, and proves comparison and functoriality formulas for the ideal.

This module defines the all-finite canonical augmentation as the composition of a terminal finite-stage augmentation with the canonical bundled projection, and proves that it can be computed at every finite stage.

The canonical comparison maps between the all-finite and in-class completions commute with their augmentations. This file records both directions of that compatibility.

This file defines augmentation on each finite coefficient-and-group stage of the all-finite system and proves its formulas on basis elements and compatibility with transition, coefficient, and functorial stage maps.

This file constructs a canonical inhabitant of the open-quotient index used by the all-finite completed group algebra, ensuring that its inverse system is nonempty.

This aggregate exports functoriality of the all-finite completed group algebra for continuous group homomorphisms: inverse-image quotient indices, finite-stage and completed algebra maps, group-like compatibility, surjec…

This module constructs the inverse-image finite quotient attached to a continuous group homomorphism and the induced quotient homomorphism. It is the index-level input for all-finite functoriality and has no dependency o…

This module records the action of the all-finite functorial map on canonical group-like elements.

This module proves that the comparison between the all-finite and \(C\)-indexed completions is natural for continuous group homomorphisms, in ring-, algebra-, and equivalence-valued forms.

This module lifts the functorial finite-stage maps to the named all-finite completed carrier and proves their algebraic, topological, and dense-subalgebra characterizations.

This module lifts the quotient homomorphism from Comap to finite group algebras and proves its continuity, transition compatibility, and compatibility with the canonical dense stage maps.

A surjective continuous group homomorphism induces a surjective map of all-finite completed group algebras. The proof combines finite-stage surjectivity with the inverse-limit lifting argument.

This aggregate exports the \(C\)-indexed stage and canonical augmentations, the augmentation ideal, and functoriality of these constructions.

This file defines the kernel of the canonical augmentation on the in-class completed group algebra, establishes the associated short exact sequence, and identifies the ideal through the canonical map from the algebraic g…

Compatible finite-stage augmentations assemble into the canonical augmentation of the in-class completed group algebra. This file proves its projection, coefficient-map, continuity, and surjectivity properties.

Maps of in-class completed group algebras commute with canonical augmentation. This file derives the corresponding comap and image formulas for augmentation ideals, including the surjective case.

This file defines augmentation on each in-class finite stage and proves its values on basis elements and compatibility with transition, coefficient-change, and functorial stage maps.

This aggregate exports both opaque completed-group-algebra carriers, their finite-stage systems, bundled projections and topological structures, and the canonical comparison equivalence between the all-finite and \(C\)-i…

This is the public aggregate for the all-finite completion \(\widehat{R[G]}\). It exports: finite-quotient indices, stages, and transition maps; the opaque named carrier and its explicit compatible-family equivalence; th…

This module defines the all-finite completed group algebra as a named inverse-limit carrier. Its compatible-family realization is available only through the explicit equivalence, coordinate projection, compatibility, and…

This module defines the reverse-ordered finite-quotient indices for the all-finite completion, their quotient groups and quotient projections, and the mutually inverse conversions with \(C\)-indexed quotients when a form…

This module bundles the canonical all-finite stage projections and proves continuity of the coefficient map through the inverse-limit lifting property.

The carrier and its algebraic structures come from the single generic inverse-limit construction. This module adds the stagewise coefficient-change map and the coefficient algebra map. Generic ring-homomorphism lemmas ap…

This module defines the finite group-algebra stages \(R[G/U]\), coefficient-change maps, quotient-transition ring homomorphisms, their compatibility laws, and the topological inverse system used by the all-finite complet…

This module transports the finite-stage topological ring and scalar-action structures through the single all-finite inverse limit, and records its compactness and separation properties.

This module compares the all-finite and \(C\)-indexed named completed carriers through their canonical projections, and bundles the resulting inverse maps as ring, algebra, and topological equivalences for pro-\(C\) grou…

This is the public aggregate for the completion indexed by a finite-group class \(C\). It exports the in-class quotient indices and stages, their inverse system, the opaque named carrier, its coefficient algebra, canonic…

This module defines the reverse-ordered open normal subgroups whose quotients lie in a finite-group class \(C\), together with their finite quotient groups and canonical quotient projections.

This module gives the \(C\)-indexed completion the same opaque-carrier API as the all-finite completion. Its inverse-limit representation is exchanged explicitly, while projections, compatibility, and extensionality are…

This module bundles the canonical \(C\)-indexed finite-stage projection as ring, algebra, linear, and continuous linear maps. The underlying projection and compatibility theorem are defined with the opaque carrier in Lim…

This module defines the \(C\)-indexed finite group-algebra stages, their transition and coefficient-change ring homomorphisms, and the compatibility identities used by the inverse system.

This module assembles the \(C\)-indexed stages into a topological inverse system and supplies the single IsRingSystem witness from which the completed carrier inherits its ring structure.

This module transports finite-stage topological structures through the named \(C\)-indexed inverse-limit carrier and records its compactness and separation properties.

This module records compatibility of completed group algebra functoriality with composition.

This aggregate exports \(C\)-indexed functoriality from quotient-index comaps through completed ring and algebra maps, group-like elements, comparison results, and the resulting continuous unit representation.

An open-normal quotient index on the target pulls back along a continuous group homomorphism to an index on the source. This file defines that comap, the induced finite quotient map, and its monotonicity, compatibility,…

This file computes the canonical maps between all-finite and in-class completed group algebras on group-like elements and their differences from one. It also records the corresponding formulas for functorial maps and res…

This module constructs the \(C\)-indexed completed group-like map through the canonical dense map, and characterizes it by finite-stage projections, multiplication, and continuity.

This module lifts hereditary \(C\)-indexed finite-stage maps to the named completed carrier and proves their algebraic, topological, and dense-subalgebra characterizations.

This file constructs the finite-stage group-algebra map induced by a continuous group homomorphism. It proves formulas on basis elements and scalars and compatibility with coefficient change, transitions, and the complet…

This file studies the continuous group-like unit representation in an in-class completed group algebra. Its image spans densely, and scalar restriction along it equips profinite modules with a continuous group action.

This aggregate exports coefficient-and-group finite quotients, the associated kernel topology, the opaque two-parameter inverse limit, its dense canonical map, and the comparison with the all-finite completed group algeb…

This module constructs the canonical dense maps from the abstract group algebra to the \(C\)-indexed and all-finite named completions, together with their bundled ring, algebra, and linear forms and finite-stage characte…

This file constructs the finite group-algebra stages obtained by quotienting both coefficients and the group. It develops their quotient maps, kernels, transition maps, basis formulas, continuity, and surjectivity.

This module compares the named fixed-coefficient completion with the named two-parameter open-finite quotient completion and studies the induced topology, injectivity, density, and coefficient-quotient kernels.

This aggregate exports the two-parameter inverse limit \(\varprojlim{I,U}(R/I)[G/U]\), its opaque named carrier, canonical bundled quotient projections, inherited topological-ring structure, and the dense canonical map f…

This module lifts the compatible open-finite quotient maps from the abstract group algebra to the named two-parameter completion, and proves its projection, continuity, and density properties.

This module defines the two-parameter open-finite quotient system and its named inverse-limit carrier. The compatible-family representation is exposed only by an explicit equivalence and the canonical projection/compatib…

This module transports the discrete topological-ring structures of the open-finite quotient stages through the single two-parameter inverse limit, and records compactness and separation results.

Open coefficient ideals and open normal group subgroups index a cofiltered system of finite group algebras. This file defines its stages, transitions, projections, and the kernel-neighborhood topology they induce on the…

This aggregate exports bundled profinite rings and modules, their finite quotient and generating set theory, and the topology, augmentation, functoriality, and unit actions of finite group algebras.

This aggregate exports the bundled definitions of profinite rings and modules, their open submodules and ideals, finite quotient separation, and generating sets converging to zero.

This file defines profinite rings, commutative profinite coefficient rings, and profinite modules. It also states their free-extension, discreteness, and finite-index submodule-basis properties.

Open submodules of a profinite module have finite quotients and separate continuous linear maps. This file packages open submodules and supplies quotient-continuity and finite-refinement criteria.

This file defines sets and maps converging to zero through open submodules and relates them to one-point extensions and dense additive generation. Every profinite module is shown to admit an appropriate generating set.

This file develops open-ideal bases at zero in profinite rings, proves their quotients finite, and derives the finite-open-ideal quotient basis and linear-topology properties.

This file constructs open submodules inside identity neighborhoods using scalar multiples of open additive subgroups. It proves the resulting linear topology and the finiteness and discreteness of open-submodule quotient…

This aggregate exports the profinite topology and universal lifting maps for finite group algebras, their augmentation theory, functoriality in the group, and group-like unit representations on modules.

This file defines augmentation of an abstract group algebra, its linear form and kernel ideal, and the resulting short exact sequences. It also proves that the differences \(g-1\) generate the augmentation ideal.

This aggregate exports algebraic augmentation and its ideal for group algebras together with the continuous augmentation obtained after completion.

An algebraic augmentation compatible with the completion map extends uniquely to a continuous augmentation of the completed group algebra. This file constructs that map, its kernel ideal and short exact sequence, and the…

This file studies group-algebra maps induced by homomorphisms of finite groups, including composition, basis formulas, continuity, and surjectivity. It also develops coefficient calculations for cyclic reductions used in…

A finite group algebra over a profinite coefficient ring is identified with a finite product of coefficients and given its profinite ring topology. This file proves continuity of its operations and constructs continuous…

Groups embed as units in their algebraic and completed group algebras. This file relates that representation to augmentation and shows how restriction of scalars gives continuous group actions on modules.

This module contains separation lemmas for completed group algebras using finite quotients.

This aggregate exports canonical inverse-limit models and their lift constructions to finite, discrete, open-submodule quotient, and general profinite modules.

This module packages canonical completed-group-algebra models by their finite-stage cone and inverse-limit universal property, derives comparison equivalences, and develops the continuous group-like map and its spanning…

Maps from the algebraic group algebra that factor through a finite stage extend uniquely from the completion. This file constructs those lifts, specializes them to discrete modules, and proves joint injectivity of the fi…

The finite-quotient universal property yields a unique continuous linear lift to the quotient of a profinite module by an open submodule. This file constructs the lift and records its value on group-like generators and i…

Compatible lifts to all open-submodule quotients are assembled by compactness into a continuous linear map to a profinite module. This file proves existence and uniqueness and applies it to the free profinite-module prop…

This is the aggregate import for pro-\(C\) completion universal properties, finite-quotient lifting, pro-\(C\) integers, and finite-quotient comparison.

The pro-C completion is the quotient of the profinite completion by its pro-C residual core. Its universal property follows from the two actual quotient maps.

This module proves that unique lifting against finite discrete \(C\)-quotients, together with density, implies the full pro-\(C\) completion universal property.

This module constructs the inverse limit of cyclic integer quotients indexed by the moduli admitted by a finite group class, equips it with its topological ring structure, and proves its profinite multiplicative and dens…

This module specializes the pro-C integer construction to prime-power moduli and proves the pro-p density, generation, and procyclicity results.

A profinite group with a topological generator and open normal quotients of every positive order is isomorphic to the actual inverse limit of all finite cyclic groups. Normalizing each coefficient map at the generator pr…

This module compares abstract finite quotients with continuous finite discrete quotients and constructs maps between profinite completions from that comparison.

This module defines the universal property of a pro-\(C\) completion and proves the resulting lift, uniqueness, comparison, and canonical-equivalence results.

The discrete and profinite Crowell--Blanchfield--Lyndon exact sequences, together with the shared four-term linear-sequence interface, the completed continuous Magnus comparison, and applications of the exact sequence. T…

Applications of the profinite Crowell exact sequence, including the finite-rank criterion for free pro-\(C\) presentations.

Crowell exact sequences / Applications / Finite Rank. This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.

Crowell exact sequences / Basic. This module contains the common four-term linear-sequence interface, exactness transport lemmas, and the finite Blanchfield--Lyndon coordinate map used by the discrete and profinite theor…

This aggregate exposes the discrete Magnus comparison and the assembled Crowell--Blanchfield--Lyndon exact sequence.

This aggregate collects the maps and exactness statements for the discrete Blanchfield--Lyndon sequence.

Surjectivity and the kernel/image identities for the relative Fox derivative assemble into the four-term discrete Crowell sequence. The free-group presentation theorem specializes this criterion to the Blanchfield--Lyndo…

This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.

This file constructs the maps in the discrete presentation sequence: the middle coordinate equivalence, the augmentation-generator tail map, and the relative-derivative head map. It also records their formulas on free ge…

This exhaustive aggregate exposes the relation-reflection support, continuous Magnus criterion, and assembled profinite Crowell--Blanchfield--Lyndon sequence.

This module gives the completed Blanchfield--Lyndon boundary maps and exact sequences in canonical lifted coordinates. Concrete Fin n formulations are obtained by reindexing only at their public presentation boundary.

This aggregate combines the reusable completed Magnus theory with the kernel-abelianization injectivity endpoint used in the Crowell exact sequence.

This module proves injectivity of the completed Magnus map on the abelianized presentation kernel, using the closed-commutator kernel calculation and the general kernel-injectivity criterion.

This file reduces exactness at the separated completed differential module to integration of coordinate cycles. It derives the middle image/kernel equality from finite-stage lifts and proves the required boundary vanishi…

For a free pro-\(C\) source, this file combines continuous Magnus injectivity, the completed boundary calculation, and bifiltered finite-stage exactness. The resulting theorems assemble the presented and separated Crowel…

This file constructs the completed and separated boundary maps on the kernel of a profinite presentation. It proves that these maps kill commutators and gives continuity criteria ensuring that they kill the closure of th…

This file factors the completed Crowell boundary through the topological abelianization of the kernel. It proves that the resulting boundary is annihilated by the completed differential map and records the Magnus-kernel…

This module packages the separated completed Crowell and Blanchfield--Lyndon sequences as FourTermLinearSequence values and states their exactness theorems under the required formation hypotheses.

This aggregate exposes the completed Crowell sequence maps and their exactness properties.

This file defines the completed differential boundary and the maps from completed and separated differential modules to the completed \(\mathbb ZC\)-group algebra. It proves their values on universal differentials and co…

This file identifies the completed map with the boundary expressed in closed-generator coordinates and transfers exactness between finite-family, completed, and separated sequences. It gives topological-generation and ba…

This module formalizes elementary duality constructions for profinite groups.

This aggregate module exposes the basic theory of topologically finitely generated groups, characteristic subgroup chains, and the associated finite-index bounds.

This module defines topological finite generation and topologically characteristic subgroups, then relates finite generating sets to free-group maps and generator-converging families.

For a topologically finitely generated profinite group, the intersection of all open subgroups of index at most \(n\) is open and topologically characteristic. These intersections form a descending countable basis at the…

The existing Schreier bound makes the least generating cardinal of an open subgroup finite. A generating set attaining that cardinal then gives an actual finite generating set, without a new finite-generation hypothesis.

This aggregate module exposes the class of all finite groups together with the standard formations, varieties, and closure properties used to define pro-C groups.

This module defines FiniteGroupClass.allFinite and proves its standard closure properties: formation, subgroup, normal-subgroup, quotient, finite-subdirect-product, extension, and hereditary closure. It also supplies the…

FiniteGroupClass bundles an isomorphism-invariant predicate whose members are finite. The module provides universe-independent membership through finite-group representatives and defines the closure conditions used throu…

The induced group is a subgroup of the finite product of copies of its coefficient group. This gives Sigma membership and preserves finite abelian exponent bounds without a choice of coset representatives.

The existing formation, subgroup closure and extension closure proofs supply the full-formation property used by maximal pro-p residual quotients.

These elementary group-theoretic facts are shared by the ab-faithfulness criterion and by Galois-theoretic character arguments.

The finite class equality identifies the actual residual cores and maximal quotients used by the singleton-Sigma and pro-p formulations.

Enlarging the permitted primes preserves the actual prime-divisor condition. No nonemptiness or primality assumption on the containing sets is needed.

This module packages the standard subgroup, finite-product, extension, formation, and hereditary closure properties of FiniteGroupClass.solvable.

This module constructs the cyclic, abelian, solvable, nilpotent, finite \(p\)-group, \(\sigma\)-group, and bounded-exponent abelian classes. It proves the subgroup, quotient, product, extension, formation, and full-forma…

Every open subgroup acts faithfully on the topological abelianization of each open normal subgroup. The relative pro-Σ version uses the same quotient-conjugation action on the maximal pro-Σ quotient.

The topological abelianization of every open subgroup is torsion-free. These are general topological-group definitions and consequences.

This module studies the last closed-derived subgroup of a maximal solvable quotient and formulates torsion-freeness and containment conditions using abelianizations of its open subgroups.

This module formalizes the general constructions for finite-step solvable quotients. It also supplies the general ab-faithfulness, ab-torsion-freeness and slimness criteria used by geometric and arithmetic libraries.

This aggregate module exposes the closed derived series, its finite solvable quotients, closure criteria detected by finite quotients, and uniform commutator-width results.

This module identifies the first closed-derived term with the closure of the abstract commutator subgroup and records closedness and finite-width consequences.

This module relates bounded commutator width to bounded word products and lifts uniform finite-quotient bounds to closedness of the commutator subgroup.

This module defines the closed derived series of a topological group and its maximal finite-step solvable quotients. It also records functoriality, closedness, and normality properties used to compare these quotients und…

This module encodes products of commutators with prescribed factors and proves the functorial and rank-theoretic estimates used to obtain uniform width bounds.

This module defines abelianization-faithfulness for open subgroups and proves that it is preserved under continuous multiplicative equivalences and passage between suitable quotients.

This file proves the profinite group-theoretic criterion used in the boundary argument: a continuous epimorphism inducing injections on the abelianizations of the preimages of all open normal subgroups admits a unique fa…

This module defines torsion-free, slim, slim-modulo, and relatively slim groups, and derives slimness and torsion consequences from faithful conjugation actions on abelianizations.

Fox differentials and Fox coordinates for free groups, group rings, finite algebraic stages, and profinite completions. The library includes bundled crossed homomorphisms, universal differential modules, Fox boundaries,…

This aggregate collects the algebraic interface shared by the discrete and completed theories: bundled crossed homomorphisms, their universal differential modules, Fox boundary identities, free-source differentials, fini…

This module defines crossed homomorphisms for an additive group action and their scalar-character specialization. It supplies the Fox product, inverse, conjugation, commutator, and power rules; restriction to coefficient…

The principal declarations in this module are: - CrossedDifferentialPreModule The free \(R\)-module on the underlying set of a group \(G\). - crossedDifferentialRelationElement The universal crossed-differential relation…

The principal declarations in this module are: - finiteFamilyLinearMap The linear map represented by a finite family of target vectors. - piReindexLinearEquiv Reindex finite coordinate functions by an equivalence of inde…

The principal declarations in this module are: - coefficientFoxBoundary The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto \operatorname{coeff}(g)-1\). - coefficientFoxBoundaryCross…

The principal declarations in this module are: - freeCrossedHomActionLift The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary additive action. - freeCrossedHomForAction The free cr…

The principal declarations in this module are: - foxJacobianMatrix A Fox-Jacobian family packaged as a finite matrix. - foxJacobianId The identity Fox-Jacobian family with Kronecker-delta entries. - foxJacobianMatrixappl…

This module formalizes completed Fox coordinates for profinite groups.

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.AugmentationIdealPrimePower - Completed.CoefficientRings.CompletedGroupAlgebra - Completed.CoefficientRings.Complete…

The principal declarations in this module are: - instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage Each finite-stage prime-power augmentation ideal inherits an additive commutative group structure fro…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.AugmentationIdealPrimePower.Additive - Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation - Complet…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraAugmentationAddHom The canonical prime-power augmentation as an additive homomorphism. - primePowerCompletedGroupAlgebraAugmentationRingHom…

The principal declarations in this module are: - toPrimePowerCompletedGroupAlgebraAugmentationIdeal A prime-power augmentation-kernel point determines a compatible family in the finite-stage augmentation ideals. - ofPrim…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraStageAugmentationIdealTransitionsmul The transition map between finite-stage augmentation ideals is compatible with scalar multiplication. -…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraStageAugmentationIdeal The augmentation ideal on one prime-power finite stage. - primePowerCompletedGroupAlgebraAugmentationKernel The kerne…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup The inverse-limit augmentation ideal is additively equivalent to the additive kernel of the canonical p…

The principal declarations in this module are: - CompletedGroupAlgebraIndexInClass The index set for a completed group algebra over finite quotients belonging to a class C. - CompletedGroupAlgebraQuotientInClass The fini…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal - Co…

The principal declarations in this module are: - modNCompletedGroupAlgebraStageAugmentation The augmentation on one residue-coefficient finite stage. - modNCompletedGroupAlgebraAugmentationAt The augmentation value of a…

augmentation ideal The principal declarations in this module are: - modNCompletedGroupAlgebraStageAugmentationIdeal The augmentation ideal on one residue-coefficient finite stage. - modNCompletedGroupAlgebraAugmentationK…

The principal declarations in this module are: - modNCompletedCoeffMap The coefficient reduction map \(\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) attached to a divisibility relation \(n \mid m\). - modNCompleted…

comm group The principal declarations in this module are: - coezeromodNCompletedGroupAlgebraInClass The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmen…

The principal declarations in this module are: - modNCompletedGroupAlgebraStageAugmentationInClass The augmentation on one class-restricted residue-coefficient finite stage. - modNCompletedGroupAlgebraStageAugmentationIn…

The principal declarations in this module are: - ModNCompletedCoeff The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage. - ModNCompletedGroupRing The group ring \((\mathbb{Z}/n\mathbb{Z}…

coeff map The principal declarations in this module are: - modNCompletedGroupAlgebraStageCoeffMapInClass The coefficient reduction map on one class-restricted finite quotient stage \(G/U\). - modNCompletedGroupAlgebraSta…

The principal declarations in this module are: - instAddCommGroupModNCompletedGroupAlgebraStage Each finite mod-\(n\) group-algebra stage carries its standard additive commutative group. - instAddCommGroupModNCompletedGr…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

The principal declarations in this module are: - ModNCompletedGroupAlgebraStage The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coefficient quotient modulo \(N\). - modNCompletedGr…

The principal declarations in this module are: - toModNCompletedGroupAlgebra The canonical map \((\mathbb{Z}/n\mathbb{Z})[G] \to \varprojlimU (\mathbb{Z}/n\mathbb{Z})[G/U]\). - modNCompletedGroupAlgebraStageMapcompatible…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic - Co…

augmentation The principal declarations in this module are: - primePowerCompletedGroupAlgebraAugmentation The prime-power completed group algebra carries a canonical augmentation to the corresponding coefficient inverse…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basi…

The principal declarations in this module are: - modNCompletedGroupAlgebraCoeffMap The modulus-direction map on residue-coefficient completed group algebras. - modNCompletedGroupAlgebraAugmentationKernelCoeffMap Coeffici…

coeff map This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap - Completed.CoefficientRings.CompletedGroupAlgebraPrimePow…

The principal declarations in this module are: - modNCompletedGroupAlgebraStageCoeffMap The coefficient reduction map on one finite quotient stage \(G/U\). - modNCompletedGroupAlgebraStageCoeffMapof The all-finite stage…

The principal declarations in this module are: - primePowerpos The prime-power moduli used throughout the compatibility layer are positive.

The principal declarations in this module are: - instAddCommGroupPrimePowerCompletedCoeffStage Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group. - instAddCommGroupPrimePowerCompl…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coef…

The principal declarations in this module are: - primePowerCompletedCoeffProjectionone The finite-stage projection sends \(1\) to \(1\). - primePowerCompletedCoeffProjectionmul The finite-stage projection preserves multi…

The principal declarations in this module are: - instCommRingPrimePowerCompletedCoeffStage Each finite prime-power coefficient stage is a commutative ring. - instCommRingPrimePowerCompletedCoeffFamily The family-level pr…

The principal declarations in this module are: - primePowerCompletedCoeffSystem The coefficient inverse system over prime-power group-algebra indices; at index \((a, U)\), its coefficient ring is \(\mathbb{Z}/\ell^a\math…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.In…

augmentation The principal declarations in this module are: - primePowerCompletedCoeffSystemInClass The class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coefficient stage is \(\mathrm{ZMod}\,(\…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMapStageInClass The finite-stage component of a class-restricted prime-power completed group-algebra map. - primePowerCompletedGroupAlgebraM…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.In…

The principal declarations in this module are: - PrimePowerCompletedGroupAlgebraStageInClass The class-restricted prime-power stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\). - primePowerCompletedGroupA…

The principal declarations in this module are: - instAddCommGroupPrimePowerCompletedGroupAlgebraInClass The class-indexed prime-power completion inherits an additive commutative group structure from its injective inclusi…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraP…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraOfInClass The class-restricted completed group-algebra element represented by a group element. - primePowerCompletedGroupAlgebraProjectionIn…

The principal declarations in this module are: - coeoneprimePowerCompletedGroupAlgebraInClass The multiplicative identity in the class-indexed prime-power completed group algebra is computed coordinatewise. - coemulprime…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraProjectionInClassone The finite-stage projection sends \(1\) to \(1\). - primePowerCompletedGroupAlgebraProjectionInClassmul The finite-stag…

The principal declarations in this module are: - primePowerCompletedCoeffToGroupAlgebra The coefficient inverse limit maps canonically into the completed group algebra by taking the stagewise scalar units. - primePowerCo…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Rin…

The principal declarations in this module are: - PrimePowerCompletedGroupAlgebraStage The stage at index \((a,U)\), namely \((\mathrm{ZMod}\,\ell^a)[G/U]\). - primePowerCompletedGroupAlgebraTransition The combined transi…

The principal declarations in this module are: - instAddCommGroupPrimePowerCompletedGroupAlgebraStage Each finite prime-power group-algebra stage carries its standard additive group. - instAddCommGroupPrimePowerCompleted…

This aggregate re-exports the following parts of the Fox differential API: - Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup - Completed.CoefficientRings.CompletedGroupAlgebraPrimePowe…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraOf The canonical map sends a group element to its compatible family of prime-power finite-stage group-like elements. - primePowerCompletedGr…

The principal declarations in this module are: - instRingPrimePowerCompletedGroupAlgebraStage Each finite prime-power group-algebra stage carries its standard ring structure. - instRingPrimePowerCompletedGroupAlgebraFami…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraProjectionnatCast The finite-stage projection preserves natural number casts. - primePowerCompletedGroupAlgebraProjectionintCast The finite-…

This aggregate re-exports the following parts of the Fox differential API: - Completed.Comparison.DiscreteCompletion - Completed.Comparison.FiniteStage - Completed.Comparison.QuotientFamily - Completed.Comparison.SourceP…

The principal declarations in this module are: - foxAlgebraicStageGroupRingReduction Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage target group algebra \((\mathbb{Z}/n\mathbb{…

The principal declarations in this module are: - zcFiniteStageTarget The finite-stage completed Fox target is the indicated group-ring quotient module. - zcCompletedGroupAlgebraScalarStage The coefficient homomorphism ob…

This module transfers discrete Magnus-kernel criteria through finite algebraic stages and completed Fox differential coordinates.

The principal declarations in this module are: - ZCFiniteStageQuotientBundle A bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to carry the topology and topological-group structu…

The principal declarations in this module are: - freeProCZCCompletedFoxBoundaryfiniteStageProjection Finite-stage projection of the source-shaped completed Fox boundary map. - freeProCZCCompletedFoxBoundaryfiniteStagePro…

This aggregate imports the topology and continuity of completed Fox coordinates, their naturality and chain rules, free-source and universal constructions, topological-generation formulas, semidirect-kernel bases, automo…

The principal declarations in this module are: - allFinitefreeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism. - allFinitefr…

This aggregate re-exports the following parts of the Fox differential API: - Completed.Continuous.ChainRule.Basic - Completed.Continuous.ChainRule.Iterated

The principal declarations in this module are: - allFinitefreeProCZCCompletedFoxPullbackGenerator The target generator map pulled back along a continuous homomorphism of free pro-\(C\) sources. - allFinitefreeProCZCCompl…

The principal declarations in this module are: - allFinitefreeProCZCCompletedFoxMiddlePullbackGenerator The pulled-back target generator on the middle free source in a two-step source chain. - allFinitefreeProCZCComplete…

This aggregate collects the construction, equivalences, topology, and comparison formulas for closed-generated coordinates in completed Fox differential modules.

The principal declarations in this module are: - closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom The closed-generated Fox vector, read as a crossed differential with the intended scalar \(\psi\), gives…

The principal declarations in this module are: - continuousfamilyCoordinatesZCzcUnivDiffofclosedGenleftGraph The paper coordinate universal differential is continuous once it is identified with the closed-generated compl…

The principal declarations in this module are: - separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger Coordinate equivalence for the separated completed differential module, obtained from the closed-generat…

The principal declarations in this module are: - closedGeneratedDerivativeCoordinateTopologyProCIntegeroffundamentalformula The coordinate topology on \(A{\psi}(C)\) transported from the closed-generated coordinate equiv…

This aggregate re-exports the following parts of the Fox differential API: - Completed.Continuous.Free.DiscreteGenerators - Completed.Continuous.Free.Rules

The principal declarations in this module are: - freeProCZCCompletedFoxDerivativeVectorboundary Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\) semidirect lift. - freeProCZCC…

The principal declarations in this module are: - continuousfreeProCZCCompletedFoxSemidirectGenerator The completed Fox semidirect generator map is continuous when both component maps are continuous. - continuousfreeProCZ…

The principal declarations in this module are: - existsUniquefreeProCZCCompletedFoxSemidirectLiftHomofdiscreteGenerators Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for discr…

The principal declarations in this module are: - freeProCZCCompletedFoxRightHomContinuousMonoidHom The right component of the completed free pro-\(C\) Fox lift is bundled as a continuous homomorphism. - freeProCZCComplet…

The principal declarations in this module are: - freeProCZCCompletedFoxBoundaryofcontinuousCrossedDifferential Source-shaped completed Fox boundary formula for continuous crossed differentials out of a free pro-\(C\) sou…

This module collects the closed-generation, finite-stage kernel, and closed-commutator results for the completed Magnus map.

This module bundles the completed Fox derivative vector as a scalar crossed homomorphism, first over pro-\(C\) integers and then over the presented coefficient ring. It also records the closed-generation and Magnus-reduc…

This module compares the completed Magnus map with its finite quotient stages and characterizes the kernel through the corresponding discrete Fox calculation.

This module identifies the kernel of the completed Magnus map with the closed commutator subgroup of the presentation kernel, using the finite-stage kernel comparison and the pro-\(C\) closed-commutator criterion.

The principal declarations in this module are: - zcCompletedFoxSemidirectMapTarget Target functoriality for completed Fox semidirect products. - zcCompletedFoxSemidirectMapTargetHom Target functoriality for completed Fox…

The principal declarations in this module are: - presentedCompletedDifferentialFamilyMapProCInteger The \(\mathbb{Z}C\llbracket H\rrbracket\)-linear family map sending the standard coordinate vector \(ei\) to d(family i)…

The principal declarations in this module are: - finiteCoordinateZeroRectangularNeighbourhoodspi Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This is the generic topological…

The principal declarations in this module are: - exactfoxBoundaryMapzcGroupLikesuboneoftopologicallyGenerates If a finite family topologically generates \(H\), the corresponding completed finite Fox boundary is exact at…

Continuous crossed homomorphisms into Hausdorff targets are determined by their values on a topologically generating set. This module applies that principle to bundled completed Fox differentials: it constructs their ker…

The principal declarations in this module are: - freeProCZCCompletedFoxBoundary Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector of completed Fox coefficients against the genera…

This aggregate re-exports the following parts of the Fox differential API: - Completed.Continuous.Universal.AugmentationQuotient - Completed.Continuous.Universal.Basic - Completed.Continuous.Universal.FiniteStage - Compl…

The principal declarations in this module are: - zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard The algebraic product \(I(\ker \psi)I(G)\) inside the algebraic standard source augmentation ideal. - zcCompleted…

The principal declarations in this module are: - zcUniversalDifferentialFinalTopology The final topology on the completed universal differential module generated by the universal crossed differential \(G \to d{\mathbb{Z}…

The principal declarations in this module are: - ZCCompletedDifferentialModuleIndex A finite stage for the completed universal differential module. It consists of a finite source quotient \(G/V\), a coefficient-and-targe…

The principal declarations in this module are: - zcCompletedDifferentialModuleStageProjectionAdd The additive finite-stage projection from the algebraic completed differential module. - zcCompletedDifferentialModuleStage…

The principal declarations in this module are: - zcCompletedDifferentialModuleStageSystem The inverse system of finite source, target, and coefficient stages of \(A{\psi}(C)\). - zcCompletedDifferentialPreModuleStageSyst…

This aggregate re-exports the following parts of the Fox differential API: - Completed.DifferentialModule.Identity - Completed.DifferentialModule.Map - Completed.DifferentialModule.TargetQuotient

The principal declarations in this module are: - identityCompletedGroupAlgebraOpenSubgroup The identity completed-group-algebra open subgroup used for the identity quotient stage. - identityCompletedGroupAlgebraOpenNorma…

This aggregate re-exports the following parts of the Fox differential API: - Completed.DifferentialModule.Map.Comap - Completed.DifferentialModule.Map.GroupLike - Completed.DifferentialModule.Map.Limit - Completed.Differ…

The principal declarations in this module are: - completedGroupAlgebraComapIndex The index map that sends a target finite quotient to its pullback finite quotient on the source. - completedGroupAlgebraComapQuotientMap Th…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMapof The completed prime-power group-algebra map sends the group-like element of g to the group-like element of ψ g.

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMap The ring homomorphism on prime-power completed group algebras induced stagewise by a continuous group homomorphism. - primePowerComplete…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMapStage The finite-stage prime-power group-algebra map induced by the quotient map associated to ψ and i. - primePowerCompletedGroupAlgebra…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMapLiftOfSurjective A choice of a lift along the surjective completed group-algebra map \(\LambdaG \to \LambdaH\), independent of the displa…

This aggregate re-exports the following parts of the Fox differential API: - Completed.DifferentialModule.TargetQuotient.Basic - Completed.DifferentialModule.TargetQuotient.Fundamental - Completed.DifferentialModule.Targ…

The principal declarations in this module are: - foxAlgebraicStageTargetQuotientContinuousMonoidHom The completed Fox-differential map is continuous with respect to the inverse-limit topology on the completed coefficient…

The principal declarations in this module are: - ppCompletedGAFoxDerivToTargetoffundFormulamap The completed Fox derivative satisfies the fundamental formula after passage to the target quotient. - ppCompletedGAFoxDerivT…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetmulprojection The finite-stage projection of the prime-power completed target derivative satisfies the Fox…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMapStagetargetQuotienttransitionsource At a completed finite stage of \(F/N\), the completed map induced by \(F \to F/N\) agrees with first…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraMaptargetQuotientlift A noncomputable lift of a completed target group-algebra coefficient to the source completed group algebra. The defini…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.Basic - Completed.FiniteStage.Bifiltered - Completed.FiniteStage.BoundaryCycleHom - Completed.FiniteStage.BoundaryCycles…

The principal declarations in this module are: - foxCommutatorPowerRelatorSet Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N\). - foxCommutatorPowerSubgroup Normal subgr…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.Bifiltered.Transition - Completed.FiniteStage.Bifiltered.System - Completed.FiniteStage.Bifiltered.InverseSystem

The principal declarations in this module are: - foxAlgebraicStageBifilteredSemidirectFamilyTransition Transition in a bifiltered family of finite Fox semidirect stages. For i \(\le\) j, the j-stage is finer: its normal…

The principal declarations in this module are: - foxAlgebraicStageTargetQuotientMaprfl The target quotient map induced by the identity subgroup refinement is the identity. - foxAlgebraicStageTargetGroupAlgebraMaprfl The…

The principal declarations in this module are: - foxAlgebraicStageBifilteredTargetGroupAlgebraMap Combined coefficient/target transition on finite target group algebras. - foxAlgebraicStageBifilteredCoordinateVectorMap C…

The principal declarations in this module are: - foxAlgebraicStageSourceKernel The kernel of the finite source-to-target quotient \(F/[N,N]N^n \to F/N\). - foxAlgebraicStageSourceKernelDerivativeAddHom The descended fini…

The principal declarations in this module are: - foxAlgebraicStageBoundaryCycleSubmodule The finite-stage Fox boundary-cycle submodule \(\ker \partial\). - foxAlgebraicStageSourceKernelDerivativeSet Quotient-level source…

The principal declarations in this module are: - foxAlgebraicStageCoordinateModuloRelations Finite coordinate vectors modulo the submodule generated by finite relation boundaries. - foxAlgebraicStageBoundaryModuloRelatio…

The principal declarations in this module are: - foxAlgebraicStageSemidirectBoundaryCycleSubgroup Finite semidirect boundary cycles form a subgroup. - foxAlgebraicStageSemidirectSourceKernelDerivativeSubgroup Finite sour…

The principal declarations in this module are: - freeProCZCBifilteredAllFiniteQuotientStageCoeffMapadditivebasis The bifiltered coefficient maps form an additive identity-quotient kernel neighbourhood basis. - freeProCZC…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.CoeffMap.Augmentation - Completed.FiniteStage.CoeffMap.Boundary - Completed.FiniteStage.CoeffMap.BoundaryCycles - Complet…

The principal declarations in this module are: - foxCommutatorPowerSourceGAAugmentationpowerSourceGAMap Source augmentation commutes with finite-stage coefficient/source reduction.

The principal declarations in this module are: - foxAlgebraicStageFoxBoundarycoeffMap Coefficient reduction commutes with the finite-stage Fox boundary map. - foxAlgebraicStageBoundaryCycleSubmodulecoeffMapmem A vector i…

The principal declarations in this module are: - foxAlgebraicStageSemidirectCoeffMapleft The left component of finite-stage semidirect coefficient reduction is obtained by reducing each coordinate coefficient. - foxAlgeb…

The principal declarations in this module are: - foxAlgebraicStageSemidirectCoeffMap Coefficient-reduction map on finite-stage semidirect Fox targets. - foxAlgebraicStageSemidirectCoeffMaplift The finite-stage semidirect…

The principal declarations in this module are: - foxAlgebraicStageSameSourceGroupAlgebraCoeffMap Coefficient-reduction map on a fixed finite Fox source quotient. - foxAlgebraicStagePowerSourceQuotientMap Source quotient…

The principal declarations in this module are: - foxAlgebraicStageTargetGroupAlgebraCoeffMap Coefficient-reduction map on finite-stage target group algebras for a divisor \(n \mid m\). - foxAlgebraicStageTargetGroupAlgeb…

The principal declarations in this module are: - foxAlgebraicStageSemidirectReindexHom Reindex the finite-stage Fox semidirect target along an equivalence of free bases. - foxAlgebraicStageSemidirectReindexHomlift The re…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.Completion - Completed.FiniteStage.PrimePower.Derivative - Completed.FiniteStage.PrimePower.System

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.Completion.Source - Completed.FiniteStage.PrimePower.Completion.Target

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.Completion.Source.Index - Completed.FiniteStage.PrimePower.Completion.Source.LimitMap - Completed.FiniteStage.…

The principal declarations in this module are: - foxCommutatorPowerOpenNormalSubgroup The open normal subgroup associated to the finite Fox commutator-power quotient. - foxAlgebraicStagePrimePowerSourceCompletedIndex The…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraToFoxAlgebraicStagePrimePowerSourceLimit The additive map from the completed source group algebra to the prime-power finite-stage source inv…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerSourceOf The compatible source-limit family represented by a free-group word. - foxAlgebraicStagePrimePowerTargetOf The compatible target-limit…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerTargetLimitToCompletedGroupAlgebra The canonical additive map from the prime-power target inverse limit to the completed group algebra of the fi…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.Derivative.CompletedSource - Completed.FiniteStage.PrimePower.Derivative.CompletedTarget - Completed.FiniteSta…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivative The completed source Fox derivative with values in the prime-power finite-stage target limit. - primePowerCompletedGroupAl…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget The completed source Fox derivative, mapped from the finite-stage target limit into the completed group a…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerDerivativeLimit The inverse-limit Fox derivative obtained by applying the finite-stage derivative at every prime-power stage. - foxAlgebraicStag…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.Derivative.OnGroup.Vector - Completed.FiniteStage.PrimePower.Derivative.OnGroup.Projection

The principal declarations in this module are: - foxAlgebraicStageTargetPrimePowerCompletedCoefficientHom The completed target coefficient homomorphism is associated to the quotient \(\mathrm{FreeGroup}(X) \to F/N\). It…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativegeneratorprojection The generator-value projection formula for the completed source Fox derivative.

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetOnGroup The dense group-level form of the completed-target Fox derivative. This is the completed-target de…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTargetOnGroup The dense group-level completed-target Fox derivative vector. It evaluates the completed-tar…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.Derivative.Source.Fundamental - Completed.FiniteStage.PrimePower.Derivative.Source.GroupLike - Completed.Finit…

The principal declarations in this module are: - ppCompletedGAFoxDerivToTargetoffundFormulaproj The completed-target Fox fundamental formula for a group-like source element after projection to one completed target stage.…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeof The completed source Fox derivative on a group-like element agrees with the prime-power finite-stage derivative limit of…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeofmul Product rule for the completed source Fox derivative on group-like source elements. - primePowerCompletedGroupAlgebra…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTargetone The completed-target Fox derivative sends the unit of the completed source group algebra to zero. - pr…

The principal declarations in this module are: - primePowerCompletedGroupAlgebraFreeFoxDerivativeVectorToCompletedTarget The vector of all completed-target Fox derivatives, indexed by free generators. - primePowerComplet…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.System.Basic - Completed.FiniteStage.PrimePower.System.Limit - Completed.FiniteStage.PrimePower.System.Semidir…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerSourceGroupAlgebra Source group algebra at the \(\ell^a\) finite Fox stage. - foxAlgebraicStagePrimePowerTargetGroupAlgebra Target group algebra…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerSourceLimitToFamilyzero The source-limit family of zero is the zero family. - foxAlgebraicStagePrimePowerSourceLimitToFamilyadd The source-limit…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.PrimePower.System.Limit.AddCommGroup - Completed.FiniteStage.PrimePower.System.Limit.CoeffMap - Completed.FiniteStage.Pri…

The principal declarations in this module are: - FoxAlgebraicStagePrimePowerSourceLimit Inverse limit of the prime-power finite Fox source group-algebra system. - FoxAlgebraicStagePrimePowerTargetLimit Inverse limit of t…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerTargetStageMapcoeffMap Compatibility of target stage maps with coefficient reduction in the completed target group algebra.

The principal declarations in this module are: - foxAlgebraicStagePrimePowerSourceLimitToFamilyone The source-limit family of one is the one family. - foxAlgebraicStagePrimePowerSourceLimitToFamilymul The source-limit fa…

The principal declarations in this module are: - FoxAlgebraicStagePrimePowerSemidirectLimit Inverse limit of the prime-power finite Fox semidirect stage system. - foxAlgebraicStagePrimePowerSemidirectLimitToFamily Forget…

The principal declarations in this module are: - foxAlgebraicStagePrimePowerSemidirectTransition Coefficient reduction between prime-power finite Fox semidirect stages. - foxAlgebraicStagePrimePowerSemidirectSystem The i…

The principal declarations in this module are: - foxAlgebraicStageRelationConjBySource Conjugating a finite-stage relation by an arbitrary source-quotient element gives another finite-stage relation. - foxAlgebraicStageT…

The principal declarations in this module are: - foxAlgebraicStageRelationAugmentationGenerator The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\). - foxAlgebraicSta…

The principal declarations in this module are: - foxAlgebraicStageGroupAlgebraDerivativeVector The vector of target-valued finite Fox derivatives of a source group-algebra element. - foxAlgebraicStageGroupAlgebraDerivati…

The principal declarations in this module are: - foxAlgebraicStageSourceBoundaryPrimitive An element of the source finite group algebra has a relation-compatible source Fox primitive if it is the source boundary of a vec…

The principal declarations in this module are: - foxAlgebraicStageRelationGroup The finite-stage relation group \(\ker(F/[N,N]N^n \to F/N)\). Its elements are exactly finite-stage kernel relations. - foxAlgebraicStageRel…

The principal declarations in this module are: - foxAlgebraicStageSourceKernelDerivativeSetzsmulmem The additive source-kernel derivative set is closed under integer multiples. - foxAlgebraicStageSourceKernelDerivativeSe…

This module records the elementary equivalence between membership in a finite-stage relation submodule and vanishing in its quotient.

The principal declarations in this module are: - foxAlgebraicStageRelationBoundarySubmodule The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors. - foxAlgebraicStageRelation…

The principal declarations in this module are: - foxAlgebraicStageSemidirectSourceKernelPoint The finite semidirect point \((Dq,1)\) attached to a source-quotient element. - foxAlgebraicStageSemidirectKernelWordPoint The…

The principal declarations in this module are: - foxAlgebraicStageSourceCoordinateVector Source-valued coordinate vectors over \((\mathbb{Z}/n\mathbb{Z})[F/([N,N]N^n)]\). - foxAlgebraicStageSourceFoxBoundary The source F…

The principal declarations in this module are: - foxAlgebraicStageSourceBoundaryCycleSubmodule Source boundary cycles in the source coordinate module. - foxAlgebraicStageSourceCycleProjectionExact Source-cycle projection…

The principal declarations in this module are: - foxAlgebraicStageSourceDerivativeVector Source-valued derivative vector of a source quotient element. - foxAlgebraicStageSourceGroupAlgebraDerivativeVector Source-valued d…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.Stage.Derivative - Completed.FiniteStage.Stage.Fundamental - Completed.FiniteStage.Stage.KernelIdeal - Completed.FiniteSt…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.Stage.Derivative.Boundary - Completed.FiniteStage.Stage.Derivative.Quotient - Completed.FiniteStage.Stage.Derivative.Rela…

The principal declarations in this module are: - foxAlgebraicStageFoxBoundary The finite-stage Fox boundary/Euler map \(v \mapsto \sumi vi ([xi] - 1)\) on coordinate vectors. - foxAlgebraicStageFoxBoundaryapply The finit…

The principal declarations in this module are: - foxAlgebraicStageLift Semidirect-product lift defining the finite-stage Fox derivative. - foxAlgebraicStageDerivativeVector Finite-stage Fox derivative vector of a free-gr…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental - Completed.FiniteStage.Stage.Derivative.Quotient.Universal

The principal declarations in this module are: - foxAlgebraicStageQuotientLift The finite-stage lift descended to the source quotient \(F/[N,N]N^n\). - foxAlgebraicStageQuotientCoefficient Coefficient homomorphism for th…

The principal declarations in this module are: - foxAlgebraicStageQuotientDerivativefundamentalformula Finite-stage Fox fundamental formula on the finite source quotient. - foxAlgebraicStageFoxBoundaryquotientDerivativeV…

The principal declarations in this module are: - foxAlgebraicStageQuotientDerivativeVectorLinearMap The linear map from the quotient universal crossed-differential module representing the descended finite-stage Fox deriv…

The principal declarations in this module are: - foxAlgebraicStageLiftrighteqoneofmem If a word lies in N, the finite-stage lift has trivial right component. - memkerfoxAlgebraicStageLiftiff Membership in the kernel of t…

The principal declarations in this module are: - foxAlgebraicStageDerivativeVectorCrossedHom The finite-stage Fox derivative vector, bundled with its scalar Fox--Leibniz law. - foxAlgebraicStageDerivativeone The finite-s…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FiniteStage.Stage.Fundamental.Formula

The principal declarations in this module are: - foxAlgebraicStageGroupAlgebraDerivative Linear extension of a descended finite-stage Fox derivative coordinate to the source group algebra. - foxAlgebraicStageGroupAlgebra…

The principal declarations in this module are: - foxAlgebraicStageGroupAlgebraDerivativeofquotientfundamentalformula Finite-stage Fox fundamental formula on a source quotient basis element after mapping to the target gro…

The principal declarations in this module are: - foxAlgebraicStageSourceGeneratorSubOnememsourceAugmentationIdeal The finite-stage source generator \([xi]-1\) belongs to the source augmentation ideal. - foxAlgebraicStage…

The principal declarations in this module are: - foxAlgebraicStageTargetQuotientMap Natural quotient map \(F/N \to F/M\) induced by an inclusion \(N \le M\). - foxAlgebraicStageTargetGroupAlgebraMap Group-algebra map on…

The principal declarations in this module are: - foxAlgebraicStageTargetQuotient The finite-stage target quotient \(F/N\). - foxAlgebraicStageTargetGroupAlgebra The finite-stage target group algebra \((\mathbb{Z}/n\mathb…

The principal declarations in this module are: - foxAlgebraicStageSourceRepresentative A chosen free-group representative of a finite Fox source quotient element, supplying source-valued coefficients without a canonicali…

The principal declarations in this module are: - foxAlgebraicStageSemidirectMapleft The left coordinate of the finite-stage semidirect point is the specified derivative component. - foxAlgebraicStageSemidirectMapright Th…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FreeProC.BifilteredCoefficientStageProjection - Completed.FreeProC.BifilteredStageProjection - Completed.FreeProC.BifilteredSystemSta…

The principal declarations in this module are: - zcFreeFoxCoordinatesBifilteredStageMap Coordinate maps attached to a compatible family of coefficient maps. - freeProCZCCompletedFoxSemidirectBifilteredStageMapOfCoeff Com…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectStageMapbifilteredTransition Compatibility of two completed-to-finite stage maps with the bifiltered finite transition. Equivalently, if th…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectBifilteredLimitMap Assemble compatible completed-to-finite semidirect stage maps into a map to the bifiltered inverse limit. - freeProCZCCo…

The principal declarations in this module are: - HasIdentityQuotientKernelNeighbourhoodBasis.reindexofkerle Reindex an identity-neighborhood quotient-kernel basis along a cofinal refinement of kernels. The hypothesis say…

The principal declarations in this module are: - zcFreeFoxCoordinatesStageMap Coordinatewise finite-stage projection on completed Fox vectors, induced by a coefficient ring map \(\mathbb{Z}C\llbracket H\rrbracket \to (\m…

The principal declarations in this module are: - freeProCChosenULiftclosedGeneratedCoordinateMap The coordinate map determined by the chosen \(U\)-lifts has the specified closed generated image. - freeProCChosenULiftsepF…

The principal declarations in this module are: - HasLeftOpenSubgroupNeighbourhoodBasis Left open subgroup neighborhood basis, expressed as a proposition rather than a structure. For every neighborhood \(U\) of \(y\), one…

The principal declarations in this module are: - freeProCFiniteQuotientStageHom The free-group map to a finite quotient of H induced by a family X \(\to\) H. - freeProCFiniteQuotientStageKernel The finite-stage relation…

The principal declarations in this module are: - freeProCChosenULiftclosedGeneratedfundamentalformulastageProj At each finite stage, the chosen \(U\)-lift closed-generation map satisfies the fundamental formula after pro…

The principal declarations in this module are: - freeProCClosedGeneratedTargetproCofsurjective For a surjective map from a free pro-\(C\) group, the closed-generated target is again pro-\(C\). - freeProCzcDiffModuleStage…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectPrimePowerStageMap A completed Fox semidirect projection to the \(\ell^a\) finite stage. - freeProCZCCompletedFoxSemidirectPrimePowerLimitM…

The principal declarations in this module are: - zcCompletedGroupAlgebraBifilteredStageCoeffMap The completed-to-finite coefficient map at a bifiltered stage, built from an actual \(\mathbb{Z}C\llbracket H\rrbracket\) st…

The principal declarations in this module are: - zcCompletedGroupAlgebraBifilteredStageRightMap The right quotient map attached to a bifiltered \(\mathbb{Z}C\llbracket H\rrbracket\) stage. It is not independent data: it…

The principal declarations in this module are: - zcCompletedGroupAlgebraStageToFoxAlgebraicStage A finite stage of \(\mathbb{Z}C\llbracket H\rrbracket\) maps to a finite Fox target group algebra once its coefficient modu…

The principal declarations in this module are: - HasIdentityQuotientKernelNeighbourhoodBasis Quotient kernels form a neighborhood basis at the identity. For every open neighborhood of 1, some finite-stage kernel is conta…

This module supplies the finite free-basis family used to reflect completed Fox relations through finite quotient stages, and relates stagewise vanishing to equality in the completed differential module.

The principal declarations in this module are: - boundaryCyclessubsetkernelClosureofrelSubmoduleExact Completed Fox density from finite-stage relation-submodule exactness. - freeProCZCFoxBoundaryCyclessubsetclosedGenTarg…

The principal declarations in this module are: - HasAdditiveIdentityQuotientKernelNeighbourhoodBasis Additive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive analogue of HasIdentityQuo…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectGenerator The generator map into the completed Fox semidirect target attached to a basis-value map \(\varphi: X \to H\). - freeProCZCComple…

The principal declarations in this module are: - subsetclosureofquotientKernelstageexact Quotient-kernel density from exact finite-stage images. For each quotient stage \(j\), let \(T{\mathrm{stage}}(j)\) be the image co…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectStageMap A semidirect projection from the completed Fox semidirect product to a finite Fox stage, constructed from a left coordinate map an…

This aggregate re-exports the following parts of the Fox differential API: - Completed.FreeProC.Uniqueness.Derivative - Completed.FreeProC.Uniqueness.Existence - Completed.FreeProC.Uniqueness.Lift - Completed.FreeProC.Un…

The principal declarations in this module are: - freeProCZCCompletedFoxDerivativeVectoruniqueofsemidirect Any continuous semidirect lift with the prescribed generator components has the canonical free pro-\(C\) completed…

The principal declarations in this module are: - existsUniquefreeProCZCCompletedFoxSemidirectLift Existence and uniqueness of the continuous completed Fox semidirect lift from a free pro-\(C\) source. - existsUniquefreeP…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectLiftunique Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique once their generator values are prescribed. -…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectLiftMorphismunique Categorical completed Fox semidirect morphisms from a free pro-\(C\) source are unique once their generator values are p…

The principal declarations in this module are: - freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential A completed crossed differential and its coefficient homomorphism combine into a semidirect homomorphism. - freePr…

This aggregate re-exports the following parts of the Fox differential API: - Completed.ProCIntegerCoefficients.Augmentation - Completed.ProCIntegerCoefficients.AugmentationIdeal - Completed.ProCIntegerCoefficients.Core -…

The principal declarations in this module are: - zcCompletedGroupAlgebraTopIndex The canonical trivial group quotient used to read the completed augmentation. - zcCompletedGroupAlgebraAugmentationFamily The finite coeffi…

This aggregate re-exports the following parts of the Fox differential API: - Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic - Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure - Completed.ProCInteger…

The principal declarations in this module are: - zcCompletedGroupAlgebraStandardAugmentationIdeal The algebraic ideal generated by the standard completed augmentation generators \([h]-1\). The completed augmentation idea…

The principal declarations in this module are: - zcCompletedGroupAlgebraStageAugmentationIdealmemprojectionstandard Every finite-stage augmentation-ideal element is the projection of an element of the algebraic standard…

The principal declarations in this module are: - zcCompletedGroupAlgebraStageAugmentationIdeal The augmentation ideal in one finite stage of \(\mathbb{Z}C\llbracket H\rrbracket\). - zcCompletedGroupAlgebraStageAugmentati…

The principal declarations in this module are: - groupAlgebraMapDomainKernelAugmentationIdeal The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\). - groupAlgebraMapDomainTargetSection A chosen linear sectio…

The principal declarations in this module are: - ZCCoeff The pro-\(C\) integer coefficient ring. - ZCCompletedGroupAlgebraIndex The two-parameter finite-stage index for \(\mathbb{Z}C\llbracket H\rrbracket\): a coefficien…

This aggregate re-exports the following parts of the Fox differential API: - Completed.ProCIntegerCoefficients.FreeGroup.Fundamental

The principal declarations in this module are: - zcFreeGroupFoxBoundary The completed Fox boundary/Euler map \(v \mapsto \sumi vi ([\psi(xi)]-1)\). - zcDifferentialToFreeFoxCoordinates The linear map from the completed u…

The principal declarations in this module are: - ZCFreeFoxCoordinates Completed Fox-coordinate vectors with coefficients in \(\mathbb{Z}C\llbracket H\rrbracket\). - zcFreeGroupFoxDerivativeVector Completed free-group Fox…

The principal declarations in this module are: - zcFreeGroupFoxBoundaryderivativeVector The boundary-map form of the completed Fox fundamental formula. - zcFreeGroupFoxBoundaryofcrossedHom Conditional completed Fox bound…

The principal declarations in this module are: - zcCompletedGroupAlgebraMapStage The finite-stage component of the target map on \(\mathbb{Z}C\llbracket H\rrbracket\). - zcCompletedGroupAlgebraMapStageKernelIdeal The ker…

This aggregate re-exports the following parts of the Fox differential API: - Completed.Residue.Core - Completed.Residue.FreeGroup

The principal declarations in this module are: - ResidueGroupRing The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\). - residueGroupRingScalar The coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induce…

This aggregate re-exports the following parts of the Fox differential API: - Completed.Residue.FreeGroup.Basic - Completed.Residue.FreeGroup.Boundary - Completed.Residue.FreeGroup.Coordinates - Completed.Residue.FreeGrou…

The principal declarations in this module are: - ResidueFreeFoxCoordinates Residue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\). - residueFreeGroupFoxDerivativeVector Residue free-group Fox…

The principal declarations in this module are: - residueFreeGroupFoxBoundary The residue Fox boundary/Euler map \(v \mapsto \sumi vi ([\psi(xi)]-1)\). - residueFreeGroupFoxBoundaryapply The residue free-group Fox boundar…

The principal declarations in this module are: - residueDifferentialToFreeFoxCoordinates The linear map from the residue universal module to residue Fox-coordinate vectors. - residueFreeFoxCoordinatesLinearMap The linear…

The principal declarations in this module are: - residueFreeGroupFoxBoundaryderivativeVector Boundary-map form of the residue Fox fundamental formula. - residueFreeGroupFoxBoundaryofcrossedHom Any residue crossed homomor…

The principal declarations in this module are: - residueFreeCrossedHomEquivLinearMap Residue crossed homomorphisms on a free group are represented by the universal residue module. - residueFreeGroupFoxDerivativeVectorLin…

The principal declarations in this module are: - ZCCompletedFoxSemidirect The completed Fox semidirect target ZC[[H]]^X ⋊ H. - rightMonoidHom The right projection from the completed Fox semidirect product to the target g…

The principal declarations in this module are: - freeGroupFoxDerivative The absolute Fox derivative of a free-group word, with coefficients in \(\mathbb{Z}[\mathrm{FreeGroup}(X)]\). - freeGroupFoxDerivativeone The absolu…

This module formalizes the discrete Fox calculus.

This aggregate re-exports the following parts of the Fox differential API: - Discrete.DifferentialModule.Boundary

The principal declarations in this module are: - GroupRing The integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra. - groupRingMap A group homomorphism induces the corresponding group-ring map. - groupRin…

The principal declarations in this module are: - groupRingBoundary The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map. - groupRingBoundaryHom The Fox boundary is itself a cr…

The principal declarations in this module are: - DifferentialHom A \(\psi\)-differential map is a map satisfying the Fox Leibniz rule. - liftLinear The linear map out of the free pre-module determined by \(\delta\). - li…

This aggregate re-exports the following parts of the Fox differential API: - Discrete.FoxCalculus.Boundary - Discrete.FoxCalculus.Coordinates - Discrete.FoxCalculus.Derivative - Discrete.FoxCalculus.Semidirect - Discrete…

The principal declarations in this module are: - relativeFreeGroupFoxBoundary The pushed-forward Fox boundary \(a \mapsto \sumx ax (\psi(x) - 1)\). - relativeFreeGroupFoxBoundaryapply The relative free-group Fox boundary…

The principal declarations in this module are: - relativeFreeFoxCoordinatesLinearEquivDifferential The linear equivalence between pushed-forward Fox coordinates and the universal differential module of a finite-rank free…

The principal declarations in this module are: - relativeFreeGroupFoxLift The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\), and whose right component is \(\psi\) itself. -…

The principal declarations in this module are: - RelativeFreeFoxCoordinates Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The coefficients are already pushed forward to \(\mathbb{Z}…

The principal declarations in this module are: - relativeDifferentialToFreeFoxCoordinates The universal map \(A{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox derivative. - relativeFreeFoxCoordinatesLine…

The principal declarations in this module are: - freeCrossedDifferentialExpansion Prescribed values on the free generators determine the Fox-coordinate expansion. - freeCrossedDifferentialExpansionHom The Fox-coordinate…

The principal declarations in this module are: - augmentationAlgHom The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\). - augmentation The augmentation ring homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}…

This aggregate re-exports the following parts of the Fox differential API: - Discrete.Jacobian.Automorphism

The principal declarations in this module are: - freeGroupAutomorphismFoxJacobianMatrixInverse The named inverse matrix for the Fox Jacobian of a free-group automorphism. For \(J{\psi}(e)\), the inverse is the Jacobian o…

The principal declarations in this module are: - freeGroupHomFoxJacobian The relative Fox Jacobian of \(\varphi : \mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(Y)\), with coefficients pushed forward by \(\psi : \mathrm{Fr…

The principal declarations in this module are: - relativeFreeGroupFoxHomcomp The composed derivative \(w \mapsto D(\varphi(w))\) is a crossed differential. - relativeFreeGroupFoxDerivativecompapply The relative Fox deriv…

This aggregate re-exports the following parts of the Fox differential API: - Discrete.KernelBoundary.IdentityAugmentation - Discrete.KernelBoundary.Basic - Discrete.KernelBoundary.Homology - Discrete.KernelBoundary.Quoti…

The principal declarations in this module are: - KernelAbelianizationAdd Additive form of the kernel abelianization map. - kernelBoundary The kernel of \(\psi\) maps multiplicatively into the additive differential module…

The principal declarations in this module are: - kernelGroupRingRep The left-multiplication representation of \(\ker \psi\) on \(\mathbb{Z}[G]\). - kernelSplitEquiv A section-based decomposition G \(\simeq\) \(\ker \psi\…

The principal declarations in this module are: - coinvariantsLEquivOfSubsingleton For a representation of a subsingleton monoid, taking coinvariants does not change the underlying module. - rightRegularRepresentation The…

This module compares the relative free Fox derivative with the universal differential and deduces the discrete Magnus-kernel criterion in relative Fox coordinates.

The principal declarations in this module are: - kernelAbelianizationBoundaryLinearOfSurjectiveinjective The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison. - memcommutatorkerofde…

The principal declarations in this module are: - HeadQuotientOfSurjective The quotient of \(A{\psi}\) by the image of the head map. - toIdentityDifferentialModule The canonical map from \(A{\psi}\) to the derived module…

The principal declarations in this module are: - relativeFreeFoxCoordinatesMap A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward. - relativeFreeFoxCoordinatesMapapply Pushing a relative…

This compatibility-free root collects the geometric-series and semidirect-product constructions used by right Fox calculus. Right differentials themselves use the general CrossedHom API.

The principal declarations in this module are: - geomSeries The geometric series element is the finite sum of successive powers. - geomSerieseqsumpow The geometric series equals the finite sum of powers. - geomSerieszero…

The principal declarations in this module are: - RightFoxSemidirect The right Fox semidirect product records a group element together with its right-derivative coordinate. - rightHom The right Fox semidirect construction…

This module formalizes Frattini-type constructions for profinite groups.

The aggregate exports the concrete generating-data predicates and theorems that concatenate finite generating families to bound the rank of the ambient group.

Independent generating tuples for finitely many subgroups can be concatenated. The two theorems below turn that elementary construction into explicit ambient-group rank bounds.

This file records concrete finite generating maps and finite families of subgroups. The companion bounds concatenate those maps to obtain explicit generating families for the ambient group.

This module identifies the topological abelianization of a free pro-\(C\) group through its universal property and finite abelian targets.

This aggregate module exposes the construction and universal property of free pro-C groups, finite-basis and finite-generation results, canonical source data, characterizations, and applications to abelian and solvable q…

This module defines the free and pointed free pro-\(C\) universal properties, their converging-set form, and the bundled canonical source data used by later constructions.

This module supplies canonical basis maps and proves the rank-one free pro-\(p\) description of the pro-\(p\) integers.

The finite quotient and covering group are arbitrary finite discrete groups. Only the kernel of the covering epimorphism belongs to the specified class. For the Sigma group class this is exactly the split abelian Sigma-k…

A finite quotient of the open subgroup is placed inside an actual finite ambient quotient. Inducing its kernel action gives a split problem for the ambient group. Its proper solution restricts surjectively to the require…

This is the aggregate import for embedding-problem and quasifree characterizations.

This module defines topological embedding problems, their weak and proper solutions, and the finite split lifting properties used in freeness criteria.

The kernel of a discrete quotient of an open subgroup is open in the ambient compact group. Its normal core gives an actual finite ambient quotient whose subgroup image still maps onto the prescribed quotient.

This module formulates quasifree proper-solution growth and its cardinal monotonicity consequences.

Complete the abstract free group, then take its pro-C residual quotient. The constructed source carries the universal property, rather than assuming one.

This is the aggregate import for inverse-limit and finite-subset criteria for free pro-\(C\) groups.

Shared imports for free pro-\(C\) criterion developments.

This module develops the finite-basis interface for ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData. Its canonical finite index is ULift (Fin n), which lies in the carrier universe required by the gene…

This module packages a finite-rank epimorphically free pro-\(C\) group as the canonical source-data structure and records the cardinality of its lifted finite basis.

This module turns a finite discrete converging-set basis into the usual free pro-C universal property.

This module transports free pro-\(C\) data to finite-step solvable quotients and their derived-series constructions.

The original IsFreeProCGroup API keeps the source, free group, finite-group class, and target in one universe. This module factors the universal property for one fixed target into HasFreeLiftTo, then supplies an explicit…

This aggregate exports the universal property and basic API for free pro-\(C\) products.

This module defines the binary free pro-C universal property and its canonical comparison maps and equivalences.

This aggregate imports the closure-based definition of topological generation, families converging to the identity, generator/convergence pairs, finite quotient criteria, and word-product closure results.

This module defines topological generation, convergence to one, the corresponding cardinal ranks, and the finite word-product filtration of a set. It develops extensionality, closed-generated-subgroup, image, quotient, a…

The open-subgroup convergence predicate is shown to be stable under pointed continuous maps, subsets, and finite modifications. For a generating set containing one, the module identifies its closure with a compact one-po…

GeneratorConvergingPair packages representatives that converge modulo a closed normal subgroup and generate together with that subgroup. The refinement preorder is developed far enough to construct upper bounds for chain…

For each open normal quotient, the lifts of its generators form a closed subset of the original compact group. A generator of a common finite quotient solves any finite family of these conditions. Compactness supplies on…

This module characterizes topological generation in inverse limits by generation of every finite-stage image. It specializes the criterion to quotients by open normal subgroups, both for a set alone and for a set togethe…

QuotientGeneratorConvergingPair records a convergent generating family in a closed-normal quotient together with coherent refinement maps. Chain upper bounds and strict extensions feed a maximality argument producing gen…

The word-product filtration is related to multiplication, inversion, and the abstract subgroup generated by a set. Under compactness hypotheses its finite levels are compact or closed, which supports separation of a fini…

Reader-facing facade for the truncated Fox inequality and strict finite generator/relation-rank bound. Canonical aggregate generated by the reviewed rehome.

The quotient of the free source factors continuously through the original presentation. Killing the images of the added relators therefore still surjects onto the infinite source quotient.

If the final quotient were finite, its open, finitely generated relation subgroup would already be generated by one finite prefix. The weighted finite-presentation inequality then contradicts the prefix budget.

The truncated Fox inequality and its numerical criterion imply the classical strict bound d² < 4r for a finite nontrivial pro-p group. The result is first stated for a concrete minimal presentation and then for the canon…

For a finite target group, the dimensions of the augmentation truncations form a bounded monotone sequence and hence eventually stabilize. The degree-zero truncation is the one-dimensional augmentation quotient.

This is the arithmetic step that turns a 3-class rank of at least six and the Shafarevich upper bound r <= d + 2 into the non-strict inequality needed to contradict the finite Golod--Shafarevich bound.

This file packages the finite-dimensional quotients of a mod-p completed group algebra used by the truncated Golod--Shafarevich inequality. The shifted definition uses truncated subtraction, so shifts beyond the cutoff g…

This file isolates the numerical argument used after the truncated Golod--Shafarevich coefficient inequality. A zero-extended backwards shift makes every coefficient statement safe in ℕ. Abel summation turns the coeffici…

This file descends the completed relation matrix, Fox boundary, and canonical augmentation to the shifted closed-augmentation quotients used in the truncated Golod--Shafarevich sequence.

Strict lifting for the filtered Fox complex and the augmentation-ideal description of the boundary range give a concrete right-exact sequence on shifted finite truncations.

The numerical core is rank--nullity for a right-exact sequence of finite dimensional vector spaces. It is stated separately from the filtered Fox maps so the Nat arithmetic and the linear-algebra argument remain reusable…

Arbitrary displayed relator depth bounds are already supported by the truncated Fox inequality. No minimality or finite-presentation assertion about a later countable quotient is required here.

This aggregate module exposes results about centralizers, normalizers, commensurators, conjugation actions on quotients, and quotient-kernel embeddings.

Centralizer lemmas and closed-cyclic-subgroup results used by the profinite applications.

This module constructs the automorphism induced on a characteristic quotient and uses it to descend conjugation by a normal subgroup to an action of the ambient quotient.

A surjection from a finite group onto a p-group admits lifts of p-power order for every element of the quotient.

Restriction to a finite subgroup followed by multiplication along the fibers of a quotient is equivariant and surjective. This produces regular wreath quotients after restricting the right factor to the subgroup.

Vanishing relative fixed points and detection of centralizers by open supergroups force an element centralizing an open subgroup modulo a quotient kernel to be trivial.

The actual right-projection kernel is its left factor. The preimage of a subgroup of the right factor is the semidirect product with the restricted action. Both identifications preserve the displayed coordinates.

The section acts on the actual kernel by conjugation. Multiplication of a kernel element by the image of the section reconstructs the original group. No commutativity or finiteness assumption is required.

This module realizes the quotient by the kernel of a homomorphism as an injective homomorphism into the target and records its value on quotient representatives.

For a subgroup H of G acting on a commutative group B, the induced group consists of functions satisfying f (h x) = h • f x. Right translation gives its G-action. Evaluation at the identity is an H-equivariant epimorphis…

The subgroup action on the induced group is the restriction of its ambient translation action. Evaluation at the identity therefore induces an actual surjective homomorphism of semidirect products.

This aggregate module exposes inverse systems of topological groups, categorical and profinite limits, exactness and factorization results, quotient systems, and stagewise comparison isomorphisms.

This module defines preorder-indexed inverse systems of topological spaces and realizes their inverse limit as the subtype of compatible families. It proves the topological universal property and equips limits of group,…

This file connects the concrete compatible-family inverse limit used by ProCGroups with mathlib's categorical limit API. Since the index and the stages may live in unrelated universes, each stage is moved to their common…

The native homeomorphism already constructs the inverse and proves its continuity. Its forward map is the original coordinate restriction. The existing restricted-system owner supplies both group structures.

For inverse systems over directed preorders, this module controls neighborhoods by finitely many coordinates and studies the map induced by a morphism on limits. It proves density and surjectivity criteria, invariance of…

Compactness gives nonemptiness of directed inverse limits of nonempty Hausdorff stages. This module then defines continuous stagewise morphisms, constructs their induced maps on inverse limits, and gives stagewise hypoth…

A second-countable profinite space is represented as an inverse limit of a sequence of finite discrete spaces. Conversely, the module characterizes second countability by the existence of a finite-discrete inverse-system…

This module bundles morphisms whose stage maps are group homomorphisms and constructs the induced homomorphisms on inverse limits. For compact Hausdorff directed systems with surjective transitions, it lifts stagewise ke…

Products are presented as inverse limits of their finite subproducts. The main factorization results show that continuous maps from a compact inverse limit to a finite discrete target depend on one stage; specialized ver…

The existing restriction keeps the stage groups and transition homomorphisms. This canonical instance permits both homomorphisms to the restricted limit and its coordinatewise group laws to use the original inverse-syste…

For inverse systems of finite discrete groups, the canonical projections are bundled as group homomorphisms. Their kernels are open normal subgroups, and under the usual directedness and surjectivity assumptions these ke…

Clopen equivalence relations on a compact Hausdorff totally disconnected space form an inverse system of finite discrete quotients. This module constructs the canonical homeomorphism from the space to that inverse limit…

A subset of an inverse limit determines an inverse system of its stagewise projection images. This module constructs the comparison lift, proves reconstruction for closed subsets of compact Hausdorff systems, and derives…

A compatible family of closed normal stage subgroups induces an inverse system of quotient groups and a canonical map from the original limit. This module identifies its kernel and, under compact Hausdorff directed-surje…

A compatible family of continuous group isomorphisms defines morphisms in both directions between two inverse systems. The induced maps on their inverse limits are assembled into a canonical continuous multiplicative equ…

The finite-upper-bound lemma in this module turns directedness of a preorder into a single stage dominating any nonempty finite set of indices. It is the common combinatorial step in compactness, cofinality, and finite-c…

This aggregate module exposes generating families converging to the identity and the resulting cardinal invariants, subgroup chains, metrizability criteria, and quotient estimates.

This file defines the cardinality of a family, topological weight, the clopen invariant rho, and local weight. It compares these invariants using topological and neighborhood bases and proves that continuous homomorphism…

This file constructs ordinal-indexed descending chains of closed normal subgroups from local-weight bounds. Successive quotients lie in a prescribed finite-group class, and the resulting series recovers the corresponding…

Countable descending open-normal bases are characterized by generating sets that converge to the identity along open subgroups. For nonempty profinite groups this yields a characterization of metrizability by a countable…

This file identifies local weight with the clopen invariant rho in the presence of a closed generating set, and computes the cardinality of an infinite generating set that converges to the identity along open subgroups.

This file develops local weight for quotients and open subgroups, relates countable local weight to descending open-normal chains, and characterizes metrizability of profinite groups. It also records consequences of topo…

This file packages linearly ordered families of subgroups, defines their carrier union and intersection, and gives membership and trivial-intersection criteria used in transfinite closed-normal series arguments.

This aggregate module exposes the closed-normal-subgroup framework, maximal-normal-subgroup criteria, and finite-intersection and compactness results for simple quotients.

This module defines noncommutative groups, the universal property of a closed normal closure, and perfect subgroups.

This module proves that a proper normal subgroup maximal among normal subgroups yields a simple quotient.

This module translates simplicity of G ⧸ K into a dichotomy for normal subgroups above K and derives the intersection property needed for noncommutative simple quotients.

This aggregate module exposes the algebraic dichotomy for subgroups above a simple-quotient kernel, its finite-intersection form, and the compactness argument for arbitrary intersections.

This module upgrades a finite-intersection property for closed normal subgroups of a compact group to the corresponding arbitrary-intersection property.

This module proves normality of indexed intersections and shows that finite intersections retain the full-product property with the kernel of a noncommutative simple quotient.

This aggregate module exposes the lattice operations and finite-index estimates for closed subgroups used throughout the profinite-group development.

This module equips closed subgroups with basic lattice operations, develops continuous images and preimages, and relates order-theoretic constructions to finite quotients of profinite groups.

This aggregate exposes the canonical profinite presentation API: closed normal closures and free pro-\(C\) relator presentations.

This module defines closed normal closures of relators and free pro-C presentations, together with their basic kernel and universal-property consequences.

This module formalizes the category and quotient theory of pro-\(C\) groups.

This umbrella module exports the bundled category of pro-C groups together with its pullback and pushout comparison APIs.

ProCGrp C is the full subcategory of Mathlib's ProfiniteGrp cut out by HasOpenNormalBasisInClass C. Thus the ambient object supplies the group, topological-group, compact, Hausdorff, and totally disconnected structures;…

This module relates mathlib's CategoryTheory.IsPullback predicate in ProCGrp C to the concrete universal property tested against profinite source groups.

Pushout universal properties in ProCGrp C use mathlib's CategoryTheory.IsPushout predicate and its standard desc, factorization, extensionality, and comparison-isomorphism API. This module remains as the stable import bo…

This file proves that a profinite group with an abelian open-normal quotient basis is itself abelian. The proof tests commutators in all open normal quotients and then uses profinite separation.

Criteria that transfer properties of the finite quotients in an open-normal basis to the underlying profinite group.

This aggregate exports finite pro-\(C\) quotient objects, inverse-limit models and quotient constructions, and standard predicates defined by the finite quotients in an open-normal basis.

This file bundles finite discrete groups and quotients by open normal subgroups as profinite objects. It records the induced pro-\(C\) structures and the corresponding product construction.

This file equips inverse limits of finite topological group systems with their canonical topology and proves the pro-\(C\) basis property for the resulting limits and for quotients by closed normal subgroups.

This file defines cyclic, abelian, and \(p\)-group open-normal quotient bases. It derives the cyclic basis associated with a single topological generator and the basic implications between these predicates.

This file equips kernels of continuous maps between profinite groups with their closed profinite topology and constructs the corresponding topological abelianization. It also transfers open-normal quotient bases in a fin…

This aggregate exports the universal-property definition of a maximal pro-\(C\) quotient, its construction from the intersection of all admissible kernels, and the resulting factorization theorems.

Ambient conjugation descends intrinsically to the residual quotient of a closed normal subgroup. The comparison with a subgroup of a maximal pro-C quotient intertwines this action, including after topological abelianizat…

IsMaximalProCQuotient C π states that π is a continuous quotient map onto a profinite group with a pro-\(C\) basis and that every continuous map to a pro-\(C\) target factors through it uniquely.

The actual quotient map induced by an inclusion of finite-group classes remains surjective after topological abelianization. It intertwines the same ambient conjugation on both residual quotients. Consequently an action…

The abelianized maximal pro-Sigma quotient identifies two classes exactly when they agree modulo every allowed prime power. The proof constructs the factorizations through the actual power quotients and uses finite quoti…

ProCQuotientKernel C G bundles a closed normal subgroup together with an open-normal quotient-in-\(C\) basis on its quotient. The residual core is their intersection; closedness and normality therefore follow directly fr…

A continuous group equivalence carries the pro-C residual core onto the corresponding core. Applying functoriality in both directions requires only hereditariness of C, so total disconnectedness is unnecessary.

For a full formation, taking the residual core inside the residual core gives the whole subgroup. The proof uses closure under extensions and continuous conjugation; no finite generation or abstract characteristic-subgro…

Enlarging the finite-group class decreases its residual core. The identity on the original group therefore induces a continuous surjection from the larger-class residual quotient onto the smaller-class residual quotient.…

The canonical projection from a group to its residual quotient induces a map on topological abelianizations. Equality under ordinary conjugation therefore implies equality under the actual residual conjugation action.

Finite groups annihilated by a Sigma-number lie in the finite Sigma class. Conversely, an element admitting an n-th root for every positive Sigma-number vanishes in every finite Sigma quotient of every pro-Sigma quotient…

When p is outside sigma, every continuous map from a group with an open-normal p-group basis to a Hausdorff group with a Sigma-group basis is trivial. Thus every pro-p subgroup lies in the actual Sigma residual core. The…

The identity map of a pro-C group kills its residual core, so that core is trivial. The resulting actual quotient retraction carries residual conjugation back to ordinary conjugation on topological abelianizations.

For a formation C, the quotient by the intersection of all kernels with pro-C quotient is itself pro-C. The proof realizes the residual quotient as a subdirect product of all the pro-C quotients occurring in the definiti…

Ambient conjugation acts on the actual residual quotient of a closed normal subgroup. Its topological abelianization kills internal conjugation, giving an action of the original quotient group, with a representative-wise…

An ambient continuous group equivalence transports a closed subgroup's intrinsic residual quotient. The induced equivalence on topological abelianizations intertwines actual conjugation, so the corresponding quotient act…

Finite Sigma quotients have order coprime to every excluded prime. Their power maps are injective, and separation transfers this to a pro-Sigma group.

The actual residual quotient has the required pro-C basis. Every continuous map to a pro-C group factors through its residual core, and surjectivity of the quotient projection gives uniqueness of this factorization.

The kernel of a maximal pro-C quotient is the concrete residual core. For a closed subgroup of the quotient, its preimage has the same residual kernel. Consequently its residual quotient is continuously isomorphic to the…

For a hereditary finite-group class, continuous maps from compact groups into pro-\(C\) targets kill the residual core and therefore factor uniquely through the residual quotient. The file also proves functoriality of th…

This aggregate collects the finite quotient, separation, basis, countable-chain, filtered-family, closed-commutator, and inverse-limit APIs built from open normal subgroups.

This file develops bundled open normal subgroups, their finite discrete quotients and projections, maps and comaps, transition morphisms, normal cores, and finite intersections.

Every identity neighborhood in a profinite group contains an open normal subgroup. This file packages that refinement result for later basis, separation, and inverse-limit arguments.

This file expresses closed subgroups as intersections of open subgroups and develops separation by open subgroups. It also proves the disjointness and clopen properties of the relevant cosets.

Membership in the topological closure of the commutator subgroup is characterized by the images in open-normal pro-\(C\) quotients. Equivalent formulations use quotient commutators and cofinal families of open normal sub…

This file defines countable open-normal bases at the identity and characterizes them by descending chains with trivial intersection. It also supplies the refinement property needed to use such chains as neighborhood base…

This file proves compactness and intersection lemmas for directed families of closed and open subgroups. These results produce finite-intersection neighborhood bases and control images of intersections under continuous s…

The canonical map to the inverse limit of all finite open-normal quotients is identified stage by stage and shown to be a multiplicative equivalence. An exact quotient-basis condition then yields the Hausdorff, totally d…

HasOpenNormalBasisInClass C G says exactly that the identity neighborhoods of G have a basis of open normal subgroups whose quotients lie in C. It does not assert compactness, Hausdorffness, total disconnectedness, or ev…

This file detects equality and closed-subgroup membership in all open normal quotients. It also develops refinements avoiding a chosen coset, cyclic-containment consequences, and extensionality of continuous homomorphism…

Finite quotients of a group that is both pro-p and pro-q have trivial order at distinct primes. Applying this to the actual residual quotient shows that the maximal pro-q quotient of a pro-p group is trivial.

This is the existing product/closed-subgroup permanence argument applied to an actual continuous injective homomorphism. It requires no surjectivity of individual coordinates and no inverse-limit identification.

This aggregate exports quotient topology results, left-quotient projections, continuous sections for open and closed subgroups, neighborhood approximation, and inverse systems formed from descending closed subgroups.

This file supplies the profinite topology and normalized continuous sections for closed-normal quotients, identifies iterated quotients, proves closedness of quotient images, and transfers topological generation between…

Given an open neighborhood of a closed subgroup, this file finds an open normal subgroup whose intersection with the closed subgroup lies in that neighborhood, including a version whose finite quotient belongs to a presc…

This file constructs the inverse system of left quotients associated with a directed descending family of closed subgroups and proves the existence of compatible continuous lifts into its limit.

This file defines the canonical projection \(G/L \to G/H\) for nested subgroups and proves its formula, continuity, surjectivity, functoriality, and compatibility with the quotient action.

Using normalized section data ordered by intermediate closed subgroups, this file applies a chain upper-bound argument to construct continuous sections of \(G/K \to G/H\). It concludes with a continuous section of the qu…

Finite quotients by open subgroups admit normalized choice sections, which are continuous because the quotient is discrete. This file records their right-inverse property and derives sections of left-quotient projections…

This aggregate exports inheritance of pro-\(C\) structure by closed subgroups and extensions, together with product and subdirect-product constructions.

The pro-\(C\) basis passes to closed subgroups when \(C\) is subgroup-closed, to Hausdorff continuous quotients when \(C\) is a formation, and across a closed normal extension when \(C\) is extension-closed.

This file transfers an open-normal quotient basis in \(C\) from a product to a closed subgroup when \(C\) is subgroup closed, and specializes the result to subdirect products.

Imports every maintained pro-p integration module in ClassFieldTower.ProP.

For a profinite group with an open-normal finite p-group basis, a set topologically generates the group exactly when its image generates the power--commutator quotient. This is the topological Burnside basis criterion, w…

The finite power-commutator quotient detects generation. Consequently a monotone sequence of closed subgroups with dense union already reaches the whole group. This is the finite-witness step for a hypothetically finite…

For the trivial action, continuous degree-one cohomology is represented by continuous additive characters into the discrete group ZMod p. This file also proves that every such character kills the closed power--commutator…

A fixed element of an equivariant quotient has an invariant fiber. This fiber has the cardinality of the kernel. Orbit counting for an r-group therefore produces a fixed lift whenever r does not divide that cardinality.…

If a finitely generated pro-p group modulo a closed normal relator closure is finite, its open kernel is finitely generated. The finite Frattini quotient of that kernel then supplies a finite prefix with the same closed…

This file compares bounded topological generation of a finite discrete commutative group with the dimension of a supplied ZMod p-module structure on its additive copy. It creates no group or module instance: the canonica…

For a finite Hausdorff p-group, the Frattini subgroup is exactly the closed subgroup generated by pth powers and commutators. The forward inclusion uses maximal subgroups. For the reverse inclusion, the power--commutator…

The LeanEval benchmark presents generator rank as the least cardinality of a finite topological generating set. For a topologically finitely generated profinite group, this agrees with the library's cardinal-valued topol…

This file proves the finite-group source needed for the Burnside basis theorem: a maximal subgroup of a finite p-group is normal, and its quotient has order exactly p.

Reader-facing facade for completed Fox rows and their filtration. Imports every maintained completed and filtered Fox leaf.

Continuity and crossed-product identities turn the inverse image of the displayed-row span into a closed normal subgroup. Since the displayed relators closed-normally generate the kernel, every kernel row lies in their c…

The pro-p integral completed group algebra has both a coefficient index and a finite group-quotient index. Fixing the coefficient index at p ^ 1 leaves a compatible family over the group quotients. Its inverse-limit lift…

The continuous coefficient-reduction homomorphism preserves group-like elements, commutes with augmentation, and carries the algebraic and closed augmentation filtrations to their mod-p counterparts.

Each coordinate of the completed mod-p Fox operator is a continuous linear map. Its right Fox--Leibniz rule lowers the closed augmentation filtration by one, so the Fox derivative of a group element of Zassenhaus depth a…

A continuous linear map out of a completed group algebra is determined by its values on completed group-like elements. Applying this uniqueness principle in each variable extends a crossed-product identity on the underly…

The continuous mod-p Fox derivative on a free pro-p group extends uniquely to its completed group algebra. The resulting continuous linear map is then transported from the all-finite completion to the p-group-indexed mod…

The universal all-finite lift of the mod-p presentation derivative inherits its crossed-product law from group-like elements. The comparison equivalence between all-finite and pro-p-indexed completed group algebras then…

This leaf specializes the existing continuous completed Fox differential to the concrete quotient map carried by a finite pro-p presentation. The formation and closed-target hypotheses are derived from the presentation;…

An additive Fox operator satisfying the right-Fox Leibniz rule lowers powers of the augmentation ideal. Continuity extends this algebraic result to closed powers, and hence makes the drop independent of representatives m…

The chosen presentation generators define the completed mod-p Fox boundary. The mod-p presentation derivative satisfies its fundamental formula, so the displayed relator rows give a finite linear map whose composite with…

Finite reflected Fox exactness supplies a matching presentation word at every finite p-group quotient. The corresponding matching subsets of the compact free pro-p source are nonempty, closed, and directed under refineme…

Coordinatewise coefficient reduction sends the integral completed Fox rows to their mod-p counterparts. The integral closed-span theorem and the closed range of the finite mod-p relation matrix then show that every kerne…

The coordinate module is filtered coordinatewise by closed augmentation powers. A displayed relator of Zassenhaus depth at least ν j gives a row of depth at least ν j - 1; this makes the relation matrix filtered when its…

The completed Fox boundary is strict for the closed augmentation filtration: every element of filtration depth n + 1 has a coordinate preimage of depth n. The proof first shows that the boundary image of the coordinate l…

A finite p-group quotient of the presented group determines a reflected finite Fox stage. Relation-ideal differentiation supplies module-level and function-level exactness of the relation boundary followed by the Fox bou…

Reducing every coordinate of the integral completed Fox derivative modulo p gives a continuous crossed homomorphism into the mod-p completed group algebra coordinates. Its coefficient is the completed group-like element…

A finite p-group quotient of the presented group gives a canonical projection from the mod-p completed group algebra to the reflected finite Fox target. This module constructs the coefficient and coordinate projections,…

The completed mod-p Fox boundary has closed range. Density of the algebraic group algebra, together with the presentation fundamental formula, identifies that range with the canonical augmentation ideal.

The displayed finite relation family and the whole presentation kernel are mapped into the same completed Fox-coordinate module. The closed coefficient span below is the finite relation module used by the filtered constr…

This file constructs the closed subgroup generated by all pth powers and all commutators. It is the concrete side of the pro-p Frattini formula; the identification with frattini G will require the pro-p maximal-subgroup…

This file exposes the quotient by the closed subgroup generated by pth powers and commutators. The quotient is commutative and has exponent dividing p. These facts are the algebraic input for the pro-p Frattini quotient;…

This file packages the natural-valued topological generator rank and proves that, for a topologically finitely generated pro-p group, it equals the ZMod p dimension of the power--commutator quotient. The quotient structu…

This file identifies continuous trivial-coefficient degree-one classes with the linear dual of the power--commutator quotient. For a finitely generated pro-p group the quotient is finite, so continuity is automatic and P…

Every continuous ZMod p character factors uniquely through the closed power--commutator quotient. The resulting equivalence is linear and is kept separate from the later finite-dimensional duality argument.

Equal generator ranks make the induced epimorphism of finite Frattini quotients injective. The original kernel therefore lies in the source Frattini subgroup.

The quotient by the closed subgroup generated by pth powers and commutators is universal for continuous homomorphisms into commutative exponent-p topological groups with closed identity.

Reader-facing facade for finite minimal pro-p presentations. Imports every maintained finite pro-p presentation leaf.

This leaf packages an actual finite free pro-p source, a displayed finite relator family, and the existing IsFreePresentationOf certificate. The free source data is a type index, rather than a structure field, so its can…

The actual finite free basis supplies a finite topological generating set. No minimality assumption on the presentation is required.

The displayed free basis gives the upper rank bound. Minimality supplies a surjection from the target to the source Frattini quotient, and the Burnside basis theorem lifts a small generating set back to the free source,…

The degree-n initial form is constructed in the concrete quotient Iⁿ/Iⁿ⁺¹. A supplied depth witness produces the numerator element, and the quotient criterion identifies vanishing with membership one layer deeper.

Minimality means that the presentation kernel lies in the source power--commutator core. The quotient therefore descends the source Frattini quotient to a continuous surjection from the target.

The relation rank is defined only after an actual finite minimal presentation witness has been constructed. It is the least displayed relation count among such presentations; no existence or comparison theorem is hidden…

A relator in the closed normal closure of the remaining relators can be omitted without changing the presented group or minimality. A presentation realizing the minimal relation rank therefore has an irredundant displaye…

The relation-depth interface reuses the group-level predicate-valued depth. Minimality supplies degree two directly from the identified power--commutator core, without choosing a finite maximum for an element of infinite…

This file defines the profinite Frattini subgroup by detection in every open normal finite quotient. For a group with an open-normal finite p-group basis, it proves the pro-p formula profiniteFrattini G = closedPowerComm…

Reader-facing facade for the mod-p augmentation and Zassenhaus filtration. Imports every maintained augmentation-filtration and Zassenhaus leaf.

This file specializes the completed group algebra already provided by ProCGroups to finite p-group quotients and packages the closures of the powers of its canonical augmentation ideal. The elementary multiplicative lemm…

The n-th subgroup consists of group elements whose completed group-like difference lies in the closure of the n-th augmentation power. This leaf establishes the subgroup, topology, degree-one, and the easy inclusion of t…

For a topologically finitely generated pro-p group, the closed power--commutator subgroup is open. Projection to this finite elementary quotient detects a degree-two completed augmentation relation. The finite degree-one…

Depth is exposed through at least, exactly, and infinite predicates. This avoids assigning an arbitrary finite value to elements lying in every filtration layer, and gives the later relation-counting API a decidable fini…

This file packages the ordinary group elements for which [q]-1 belongs to the square of the mod-p augmentation ideal. Direct group-algebra identities show that this subgroup contains all p-th powers and commutators.

Linear functionals on the elementary power--commutator quotient separate a nonzero class. Combined with dual-number linearization, this proves that [q]-1 ∈ I² forces q into the closed power--commutator subgroup. In a fin…

An additive ZMod p character defines a group-algebra map into the dual numbers. Its square-zero coordinate detects degree one, so the square of the augmentation ideal is annihilated. This is the separation mechanism used…

A continuous group homomorphism induces the existing functorial map on class-indexed completed group algebras. Naturality of augmentation and continuity of that map show that every closed augmentation power, hence every…

The element [g] - 1 translates multiplication, inversion, commutators, and p-th powers in a group into augmentation-filtration identities. Keeping these calculations in one leaf prevents later filtration proofs from re-e…

The completed group-like commutator identity sends elements of filtration degrees i and j to degree i + j. In characteristic p, the completed group-like difference of a p-th power is a p-th power, giving degree p i. The…

Iterating the open power--commutator core produces open normal subgroups inside arbitrary closed augmentation degrees. Applying an actual compact surjective homomorphism to such a source subgroup gives a target open norm…

This aggregate module exposes separation and permanence results for profinite groups and their open subgroups.

This module proves that an element of a profinite group lying in every open normal subgroup is the identity.

Compatible finite-quotient central lifts that survive a fixed open quotient yield a nonidentity element of the profinite center.

This module records openness and closedness properties of open (normal) subgroups, constructs their pullbacks, and proves that they have finite index in compact topological groups.

Discrete and profinite forms of the Reidemeister--Schreier theorem, together with free-group word rewriting, presentation equivalence certificates, verified Tietze scripts, Schreier cocycles, and open-subgroup rank formu…

This module formalizes the classical discrete Reidemeister--Schreier theorem.

This aggregate exposes the discrete open-subgroup development: reduced-word utilities, right Schreier transversals and generators, prefix trees, and the resulting free bases.

This module identifies the classical Schreier generators with the free basis obtained from complement edges, including the inverse-basis convention needed for the standard generator formula.

Using the action groupoid and Schreier prefix tree, this module constructs a free basis indexed by complement edges and transports it to the canonical type of nontrivial Schreier pairs.

From a right Schreier transversal, this module constructs canonical representatives and Schreier generators, identifies the nontrivial representative-generator pairs, and proves their basic action identities.

This module constructs the Schreier prefix tree from a right transversal, proves its positive and negative edge criteria, and relates its complement edges to the nontrivial Schreier generators.

This module defines full and partial right Schreier transversals in free groups, proves their complement and prefix-closure properties, and supplies the existence and extension results used later.

This aggregate exposes prefix operations on reduced free-group words and the compatibility layer connecting them to the Nielsen--Schreier action-groupoid construction.

This module defines the initial reduced-word segments of a free-group element and proves the membership and prefix-parent facts used by discrete Schreier transversals.

This module connects the local word conventions with Mathlib's Nielsen--Schreier action-groupoid basis and establishes the edge and back-edge identities needed to transport that basis.

This aggregate exports equality modulo normal closures, quotient-kernel presentations, presentation automation, semantic Tietze equivalences, and verified elementary Tietze scripts.

This module defines the small proof automation used in relator calculations: it closes elementary RelatorEquivalent goals and reduces normal-closure membership goals to the standard closure lemmas.

This module identifies a presented free-group kernel with its relator quotient. It packages the canonical surjection, computes its kernel, and derives quotient equivalences for the conjugate and transversal relators.

This aggregate module exposes the relator predicates, congruence constructions, free-group lifting lemmas, word operations, and presentation-level results used by the discrete Reidemeister--Schreier development.

This module defines equality modulo a relator normal closure and proves its elementary equivalence, congruence, inversion, multiplication, and quotient characterizations.

This module transports normal-closure membership and relator equivalence through inclusions, homomorphisms, and indexed unions of relator families.

This module relates reduced words and FreeGroup.mk, then proves that lifts whose generator images agree modulo a relator normal closure agree on every free-group word.

This module proves invariance and closure lemmas for changing relator sets, conjugating and cyclically rotating words, products of lists, and ordered finite products.

This module expands conjugated list products and promotes generatorwise normal-closure relations to all words under a free-group endomorphism.

This aggregate separates semantic presentation equivalence from syntactic transformations. The core and generator/relator operation modules construct certificates; Tietze.Script records well-typed elementary move sequenc…

This module packages the algebraic content of a Tietze equivalence: mutually inverse maps between groups presented by relators. Presentation remembers the generator type, while PresentationEquivCertificate composes and r…

This module formalizes adjoining generators with defining words. It builds the inclusion and elimination homomorphisms, transforms the relators, and packages the resulting presented-group equivalence.

This module formalizes deletion of generators forced to be trivial. It defines the elimination homomorphism and relator transformations and packages the induced equivalence of presented quotients.

This module builds relator-quotient equivalences from maps on generators, including indexed relator families, and proves the normal-closure properties of the associated free-group pullback relators.

This module packages mutually inverse maps between relator quotients. It provides reflexive, symmetric, and transitive composition together with a one-sided constructor when the inverse data can be derived.

This module supplies semantic presented-group equivalences for replacing relators: equal normal closures, mutual relator maps, generator maps, and compositions of these transformations.

ElementaryTietzeMove records genuine presentation transformations with indexed source and target presentations. VerifiedTietzeScript is the typed sequence of those moves; it evaluates to a semantic PresentationEquivCerti…

This aggregate exposes the abstract rewriting construction together with its finite-quotient presentation pipeline.

This aggregate exposes finite-quotient Schreier data, tau rewriting, degenerate-symbol elimination, kernel presentations, word certificates, and the cleaned target-presentation equivalence.

This module removes relators attached to degenerate Schreier symbols, builds the finite cleaned relator set, and records the remaining quotient-section and augmented relator families.

This module separates degenerate Schreier symbols from genuine generators and sets up the relator families needed to delete the trivial generators from the finite-quotient presentation.

This module rewrites tau words on the nondegenerate Schreier-symbol alphabet and proves that the cleaned rewriting respects reduction, multiplication, and the original tau evaluation.

This module packages a finite quotient map with chosen section words. It defines the kernel, representatives, finite Schreier symbols, their evaluation, and the basic identities used by tau rewriting.

This module constructs the quotient homomorphisms induced by tau and proves that the Schreier, quotient-section, and augmented relator families give the required kernel-level maps.

This module proves the normal-closure identities behind the finite-quotient Reidemeister--Schreier presentation, including tau images of section words, symbols, and conjugated original relators.

This aggregate exposes the certificate data and normal-word construction which identify the cleaned finite-quotient presentation with the target kernel presentation.

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation / Core. This module defines the structured certificates for prefix-closed quotient-section words and the core data specifyi…

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation / Normal Words. This module packages normal-word witnesses for the cleaned symbols and uses them to construct the cleaned t…

This module defines the finite-state tau rewriting of signed words into Schreier symbols and proves compatibility with concatenation, cancellation, reduction, and free-group multiplication.

This module records checkable prefix-closure conditions for quotient-section words and proves the reduced-word and state-transition facts required by the finite tau presentation.

This module defines abstract right Schreier representatives, their associated symbols and generators, and the rewriting maps that turn kernel words into words on Schreier symbols.

This module formalizes free-group tools used in Reidemeister--Schreier rewriting.

This module constructs the free-group automorphism that inverts every generator, transports free bases along it, and proves the resulting automorphism is involutive.

This module develops the signed-letter view of reduced free-group words, including cancellation at the last letter and the prefix-parent operation used to build Schreier prefix trees.

This module rebuilds the spanning-tree loop construction using public conversion functions between mathlib's vertex type synonyms. No private-root declaration or backward elaboration option enters the public API.

This aggregate exports open-subgroup right-coset cocycles, exact generation, and the proved finite-rank basis theorems for free pro-\(C\) groups.

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 p…

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 on so that its index lives in the ambient un…

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 their pro-\(C\) completions, and construct…

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--Schreier basis theorem to compute the abstract pre…

Using a transported right-coset section and the wreath-product embedding, this module identifies the concrete right-Schreier cocycles that topologically generate an open subgroup. It also proves the finite-quotient lifti…

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 membership to the image.

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 refines the finite-rank Schreier basis theo…

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 totally disconnected group by the classical…

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 topology, and a normalized continuous secti…

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 open subgroup. ActualSchreierSection and Actu…

This module formalizes the quiver and arborescence tools used by the groupoid construction.

This module exposes the right-coset quotient of a group by a subgroup and its natural action g • [a] = [a g⁻¹]. The quotient is intentionally only a coset space: for a non-normal subgroup it has no multiplication. Algebr…

This module formalizes Schreier generators and rewriting.

This module formalizes basic topological-group constructions used by the pro-\(C\) library.

This aggregate module exposes continuous homomorphisms and equivalences, conjugation, open and characteristic subgroups, quotient maps, and full subgroup topologies.

This file bundles conjugation by a normalizing element as a continuous multiplicative equivalence. It also descends conjugation to quotients by topologically characteristic subgroups and records the formula on quotient r…

This file provides standard continuous homomorphisms involving subgroups and quotients, proves an open-mapping criterion for compact-to-Hausdorff surjections, and develops range restrictions. Kernels and ranges are shown…

This file constructs continuous multiplicative equivalences from inverse homomorphisms and from compact-to-Hausdorff bijections. It also gives the topological first-isomorphism equivalence from a quotient by the kernel t…

This aggregate exports abstract quotient formations and varieties, the associated notions of open and closed subgroup, pro-\(C\) closure and residuality, and pullback stability.

A quotient formation specifies admissible normal quotient kernels and their closure properties. This file defines the induced open subgroups, pro-\(C\) closure, closed subgroups, and residuality, and proves their basic l…

A quotient variety is a quotient formation stable under pullback along group homomorphisms. This file shows that the corresponding notion of open subgroup is likewise preserved by comap.

This file records the canonical continuous multiplicative equivalence between a topological group and the subtype of its top open subgroup, together with its forward and inverse formulas.

This file develops algebraic and continuous equivalences induced by surjective homomorphisms, lifts and maps between quotient groups, congruences between quotients, and restrictions to preimages of subgroups.

This file studies subgroups invariant under continuous automorphisms. It proves invariance of the closed commutator subgroup, gives equivalent map and comap formulations, and establishes closure of topologically characte…

This module formalizes permutational wreath products.