Skip to content

Profinite groups

Reusable Lean APIs for finite-stage limits, finite-target map colimits, maps into limits of finite-space diagrams, profinite-group morphisms, finite-quotient Hom systems, compatible quotient-subgroup and Sylow families, closed subgroups with Sylow finite images, finite-quotient conjugacy, continuous sections, free profinite and pro-p constructions, primewise p-adic models, and procyclic invariants, power images, and closed-subgroup inheritance.

Quoted from the project description in formalization.yaml of FormalFrontier/profinite-groups at commit bf258c54, Apache-2.0.

No articles: its formalization.yaml lists no highlights, and none of its 8 headline results links a declaration that the scan finds in the linked file at this commit, so they are quoted below.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/profinite-groups, read at commit bf258c54 (2026-11-04).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “other”.
  • Review notes: “Read README.md for headline results and import examples, and docs/Mathematics.md for hypotheses, constructions and limitations.”
  • Automation: agent; framework “Codex CLI and Hive Tasks”; tool setup “AI agents developed code and documentation with a pinned Lean/mathlib Lake environment; independent agent executions reviewed mathematics.”; prompting notes “Mathematical assumptions, source boundaries and concrete declarations are explained in README.md, docs/Mathematics.md and docs/API.md.”
  • Automation notes: “Beacon contributed the initial implementation and API and regression-client repairs. Formal Frontier Agents contributed further mathematics, tests, reference documentation and independent reviews. The native reference adapter and catalogue follow the finite-group Tate cohomology, polynomial-root-stability and Anchor ideal-completion adaptation lineage; Folio contributed headline input.”

Literature

The sources its formalization.yaml names, with their relationship to it.

  • Cohomology of Number Fields (corrected second edition, electronic version 2.3, May 2020), Jürgen Neukirch, Alexander Schmidt, Kay Wingberg, Chapter I, section 1 (including exercises 1 and 3–5); section 6 (finite-quotient pro-p and Sylow arguments); section 7 (before proposition 1.7.7) (book; background).

Builds on

Used by

Headline results

Quoted from the headline results in README.md of FormalFrontier/profinite-groups at commit bf258c54, Apache-2.0.

Explore finite diagrams, maps and constructions, product models and classification, and homomorphisms, powers and coefficients.

Finite diagrams and inverse-limit characterizations

Skeletal finite quotients and equivalence. Every profinite space in the same universe is the limit of its included skeletal finite-quotient diagram. The associated dual ind-object realizes to that space, giving an equivalence between dual ind-objects of finite sets and profinite spaces whose forward functor is the profinite realization. The generic inverse's chosen object is compared with the skeletal presentation by an isomorphism. Empty spaces and finite stages are allowed; no arbitrary diagram projection is assumed surjective. See IndDualEquivalence and its clients.

Finite-stage inverse-limit characterizations. A Hausdorff space is an inverse limit of finite discrete spaces over a small, nonempty cofiltered category if and only if it is compact with a clopen basis, equivalently compact and totally disconnected. A topological group is an inverse limit of finite groups over such a category if and only if it is compact and totally disconnected (FiniteGroupPresentation.nonempty_iff). For a Hausdorff topological group, this is also equivalent to compactness with an identity-neighborhood basis of open normal subgroups. The presentations use the actual inverse-limit topology and include empty spaces and trivial groups; arbitrary finite-stage projections need not be surjective. See FiniteDiscreteCharacterization and FiniteGroupCharacterization.

Maps, closed subgroups and universal constructions

Finite maps and morphisms. In profinite groups, categorical monomorphisms are injective and epimorphisms are surjective. For groups in the same universe, continuous Hom is the limit over finite target quotients of the colimits over finite source quotients. Separately, injective and surjective maps of profinite spaces have finite-map limit presentations, not a finite-presentation theorem for groups. See EpiMono, FiniteQuotientHom, FinitePresentation.

Closed-subgroup conjugacy. Two closed subgroups of a profinite group are conjugate precisely when their images are conjugate in every finite open-normal quotient. The quotient conjugators need not form a compatible family; no countability or openness assumption is used. See FiniteQuotientConjugacy and its guide.

Continuous sections. For closed K ≤ H in a profinite group, the projection G/K → G/H has a continuous right inverse; a supporting result supplies sections of surjective local homeomorphisms over compact Hausdorff totally disconnected spaces. For any closed H, a chosen bundled continuous map G/H → G selects a representative of each coset. The choice is neither asserted to be homomorphic nor normalized at the identity; normality is not needed. See ContinuousSection and ContinuousCosetRepresentative.

Primewise models, product ideals and procyclic classification

Procyclic classification and realization. Given proofs of procyclicity, groups in independent universes are continuously equivalent exactly when their generator-independent primewise exponents agree. Every exponent family is realized by residue factors ZMod (p^n) and p-adic factors: zero exponent is trivial, infinity retains the full p-adic factor. With a supplied generator, torsion-freeness means all exponents are zero or infinity. For a torsion-free procyclic profinite group, its all-primes quotient model, and hence the group itself, is continuously equivalent to the product of p-adic integer factors over the infinite-exponent primes, with zero-exponent coordinates omitted. The support can be empty or infinite and is generator-independent; the group equivalence uses a chosen topological generator. The invariant is noncomputable and not assigned to arbitrary nonprocyclic groups; generator independence equates kernel ideals and exponents, not the associated maps. See ProcyclicInvariant, ProcyclicRealization, ProcyclicTorsionFree and ProcyclicTorsionFreeProduct.

Homomorphisms, powers and coefficients

Power images and open subgroups. For a procyclic group, positive nth powers form an open subgroup with cyclic finite quotient and index dividing n, not necessarily equal to n. Every open subgroup equals the power image at its actual index. The zero-power image is trivial and need not be open; no arbitrary-procyclic closed-subgroup classification is asserted. See ProcyclicPower.

Closed subgroups of procyclic groups. Every closed subgroup of an arbitrary procyclic profinite group is procyclic in its inherited group and topology, without an openness or finite-index assumption. It has a generator inside the subgroup whose integral powers are dense there. The result also accepts an ordinary subgroup with a closedness proof. It does not classify arbitrary closed subgroups by exponents. See ProcyclicClosedSubgroup.

All results and their hypotheses · Mathematical details, hypotheses and API limitations.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.