The candidate profinite group Γ_A as an inverse limit (Stage B, work order B3)

This file realises the manuscript's candidate group Γ_A = F / N_A (manuscript §"The candidate as a profinite group", eq. candidateinverse) as the cofiltered inverse limit, in ProfiniteGrp, of all admissible finite marked quotients. The index category is AdmissibleIndex (work order B1/B2), which is cofiltered (admissibleIndex_isCofiltered), and the diagram sends each admissible index A to its finite carrier Fin A.n viewed as a discrete profinite group.

Main contents:

• admissibleDiagram : AdmissibleIndex ⥤ ProfiniteGrp — the inverse system.
• GammaA : ProfiniteGrp — its categorical limit Γ_A.
• gammaGen : Gen → GammaA — the four universal generators σ, τ, x₀, x₁, realised as the compatible family with coordinate A.q a at every A.
• gammaGen_eval_projection — projecting gammaGen a to the coordinate A returns the marked generator A.q a.
• GammaA_tameRel, GammaA_wildRel — Γ_A satisfies the two relators, in the inverse-limit (coordinatewise) sense: projecting gammaGen to any admissible quotient and evaluating the relator there gives 1 (true because that quotient is admissible). See the doc-comment on GammaA_tameRel for why the relator is stated coordinatewise rather than as a bare GExpr.eval … gammaGen = 1 (the Stage-A GExpr.eval requires a finite group; Γ_A is profinite/infinite).
• gammaGen_topologically_generate — the four generators topologically generate Γ_A (dense generation by finite-coordinate approximation, plan §4).

Construction idiom (ProfiniteGrp)

admissibleDiagram.obj A is ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Fin A.n)) (the discrete-topology profinite group on the finite carrier Fin A.n; bare finite groups carry no topology, so ProfiniteGrp.of (Fin A.n) would not elaborate — cf. Boundary/Z2Limit.lean). Morphisms are ProfiniteGrp.ofFiniteGrpHom (FiniteGrp.ofHom f.toMonoidHom), whose underlying function is definitionally f.toMonoidHom (admissibleDiagram_map_apply).

The categorical limit Limits.limit admissibleDiagram is opaque, so we bridge it to mathlib's explicit model ProfiniteGrp.limit admissibleDiagram (an honest subtype of compatible families, with .val and ProfiniteGrp.limit_ext) via the canonical gammaIso : GammaA ≅ ProfiniteGrp.limit admissibleDiagram (Limits.limit.isoLimitCone against ProfiniteGrp.limitConeIsLimit).

Instance gotcha (inherited from B1/B2)

Fin n carries the global Fin.instMul, not the transported group structure A.groupFin. We never synthesize a standalone Group (Fin n); A.groupFin is the registered instance and all maps go through the bundled AdmissibleHom.

The admissible inverse system and its limit

noncomputable def Q2Presentation.admissibleDiagram : CategoryTheory.Functor AdmissibleIndex ProfiniteGrp.{0}

The inverse system of admissible finite marked quotients, as a functor into ProfiniteGrp. An admissible index A maps to its finite carrier Fin A.n (discrete profinite group); a generator-preserving hom f maps to the induced continuous group homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.admissibleDiagram_map_apply {A B : AdmissibleIndex} (f : A ⟶ B) (x : Fin A.n) : (ProfiniteGrp.Hom.hom (admissibleDiagram.map f)) x = f.toMonoidHom x

The action of admissibleDiagram.map f on a point is definitionally the underlying generator-preserving monoid homomorphism f.toMonoidHom.

instance Q2Presentation.instFiniteAdmissibleObj (A : AdmissibleIndex) : Finite ↑(admissibleDiagram.obj A).toProfinite.toTop

The coordinate carrier admissibleDiagram.obj A is the finite type Fin A.n, so it is Finite (needed so the Stage-A finite evaluator GExpr.eval runs in it).

noncomputable def Q2Presentation.GammaA : ProfiniteGrp.{0}

The candidate profinite group Γ_A, the cofiltered inverse limit (in ProfiniteGrp) of all admissible finite marked quotients (manuscript eq. candidateinverse).

Equations

• Q2Presentation.GammaA = CategoryTheory.Limits.limit Q2Presentation.admissibleDiagram

noncomputable def Q2Presentation.gammaIso : GammaA ≅ ProfiniteGrp.limit admissibleDiagram

Bridge from the opaque categorical limit Γ_A = Limits.limit admissibleDiagram to mathlib's explicit subtype model ProfiniteGrp.limit admissibleDiagram (whose points are compatible families, accessible by .val and with limit_ext).

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.limit_pi_apply (A : AdmissibleIndex) (x : ↑GammaA.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) x = ↑((ProfiniteGrp.Hom.hom gammaIso.hom) x) A

The categorical projection Γ_A ⟶ Fin A.n, computed through gammaIso as the A-coordinate of the explicit compatible family.

theorem Q2Presentation.GammaA_ext {x y : ↑GammaA.toProfinite.toTop} (h : ∀ (A : AdmissibleIndex), (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) y) : x = y

Two points of Γ_A agree once all their coordinate projections agree. The inverse-limit extensionality principle for Γ_A.

The universal generators

def Q2Presentation.gammaGenFamily (a : Gen) : ↑(ProfiniteGrp.limit admissibleDiagram).toProfinite.toTop

The compatible family underlying the universal generator a: at every admissible index A its coordinate is the marked generator A.q a. Compatibility across a transition π : A ⟶ B is exactly marking-preservation π.map_q a.

Equations

• Q2Presentation.gammaGenFamily a = ⟨fun (A : Q2Presentation.AdmissibleIndex) => A.q a, ⋯⟩

noncomputable def Q2Presentation.gammaGen (a : Gen) : ↑GammaA.toProfinite.toTop

The four universal generators σ, τ, x₀, x₁ of Γ_A, as the compatible families of marked generators.

Equations

• Q2Presentation.gammaGen a = (ProfiniteGrp.Hom.hom Q2Presentation.gammaIso.inv) (Q2Presentation.gammaGenFamily a)

theorem Q2Presentation.gammaGen_eval_projection (A : AdmissibleIndex) (a : Gen) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) (gammaGen a) = A.q a

Projecting a universal generator to a coordinate returns the marked generator there. π_A (gammaGen a) = A.q a.

The two relators hold in Γ_A

theorem Q2Presentation.GammaA_tameRel (A : AdmissibleIndex) : (Q2Word.tameRelator.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) (gammaGen a)) = 1

The tame relator holds in Γ_A (manuscript eq. tame), in the inverse-limit sense: projecting the universal generators to any admissible finite quotient A and evaluating the tame relator there gives 1.

We state it coordinatewise rather than as a bare GExpr.eval Q2Word.tameRelator gammaGen = 1, because the Stage-A evaluator GExpr.eval is defined only for finite groups (its powOmega2 case is the finite ω₂-power), whereas Γ_A is profinite, hence infinite. Since two points of Γ_A are equal iff all their coordinates agree (GammaA_ext), this coordinatewise statement is precisely "the universal generators of Γ_A satisfy the tame relation". The proof rewrites each projected generator to A.q a (gammaGen_eval_projection) and invokes admissibility of A (A.admissible.2.1 : tameRel A.q).

theorem Q2Presentation.GammaA_wildRel (A : AdmissibleIndex) : (Q2Word.wildRelator.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) (gammaGen a)) = 1

The wild relator holds in Γ_A (manuscript eq. wild), coordinatewise; see GammaA_tameRel for the rationale for the coordinatewise phrasing. The proof rewrites each projected generator to A.q a and invokes A.admissible.2.2.1 : wildRel A.q.

Topological generation

noncomputable def Q2Presentation.gammaHomeo : ↑GammaA.toProfinite.toTop ≃ₜ ↑(ProfiniteGrp.limit admissibleDiagram).toProfinite.toTop

GammaA and the explicit model ProfiniteGrp.limit admissibleDiagram are homeomorphic via the bridge iso gammaIso (an iso of profinite groups, hence a homeomorphism).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.evalAt (B : AdmissibleIndex) : ↑(ProfiniteGrp.limit admissibleDiagram).toProfinite.toTop →* ↑(admissibleDiagram.obj B).toProfinite.toTop

Evaluation at the coordinate B, as a monoid homomorphism out of the explicit limit model: m ↦ m.val B.

Equations

• Q2Presentation.evalAt B = { toFun := fun (m : ↑(ProfiniteGrp.limit Q2Presentation.admissibleDiagram).toProfinite.toTop) => ↑m B, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.evalAt_apply (B : AdmissibleIndex) (m : ↑(ProfiniteGrp.limit admissibleDiagram).toProfinite.toTop) : (evalAt B) m = ↑m B

theorem Q2Presentation.map_evalAt_closure_eq_top (B : AdmissibleIndex) : Subgroup.map (evalAt B) (Subgroup.closure (Set.range gammaGenFamily)) = ⊤

The coordinate-B evaluation maps the subgroup generated by the universal generators onto Fin B.n: its image is closure (range B.q) = ⊤ because B is admissible (its marking B.q generates).

theorem Q2Presentation.exists_dominating (J : Finset AdmissibleIndex) : ∃ (B : AdmissibleIndex), ∀ A ∈ J, Nonempty (B ⟶ A)

Finite cofiltered domination. Any finite set of admissible indices is dominated by a single index admitting a morphism to each of them (folding the binary cones IsCofiltered.min of the cofiltered index category).

theorem Q2Presentation.dense_gammaGenFamily : Dense ↑(Subgroup.closure (Set.range gammaGenFamily))

The subgroup generated by the universal generators is dense in the explicit limit model. Mirrors ProfiniteGrp.denseRange_toLimit: a nonempty open set fixes finitely many coordinates; cofiltered domination collapses them to one coordinate B; and the generators surject onto Fin B.n there.

theorem Q2Presentation.gammaGen_topologically_generate : (Subgroup.closure (Set.range gammaGen)).topologicalClosure = ⊤

The four universal generators topologically generate Γ_A (plan §4): the closure of the subgroup they generate is everything. Equivalently, that subgroup is dense. Density is transported from the explicit limit model (dense_gammaGenFamily) along the homeomorphism gammaHomeo, using that gammaIso.hom carries the generators to their explicit families.