Profinite presentations

Combining the free profinite group (GQ2/FreeProfinite.lean) with the profinite quotient by a closed normal subgroup (GQ2/ProfiniteQuotient.lean), we can form the profinite group presented by a set of generators and relators: the free profinite group modulo the closed normal closure of the relators. This is the shape of the paper's group Γ_A (generators σ, τ, x₀, x₁, i.e. X = Fin 4, and the four relators). Writing the literal relators still needs a genuine profinite ω₂-exponent (ZHat, absent from Mathlib — see docs/foundations-audit.md), but the presentation construction itself is now available.

noncomputable def GQ2.relatorSubgroup {X : Type u} (rels : Set ↑(FreeProfiniteGroup X).toProfinite.toTop) : Subgroup ↑(FreeProfiniteGroup X).toProfinite.toTop

The closed normal closure of a set rels in the free profinite group on X: the smallest closed normal subgroup containing the relators. (Closedness is what makes the quotient profinite; in a profinite group the algebraic normal closure need not be closed.)

Equations

• GQ2.relatorSubgroup rels = (Subgroup.normalClosure rels).topologicalClosure

instance GQ2.instNormalCarrierToTopTotallyDisconnectedSpaceToProfiniteFreeProfiniteGroupRelatorSubgroup {X : Type u} (rels : Set ↑(FreeProfiniteGroup X).toProfinite.toTop) : (relatorSubgroup rels).Normal

noncomputable def GQ2.profinitePresentation {X : Type u} (rels : Set ↑(FreeProfiniteGroup X).toProfinite.toTop) : ProfiniteGrp.{u}

The profinite group presented by generators X and relators rels: the free profinite group on X modulo the closed normal closure of the relators.

Equations

• GQ2.profinitePresentation rels = GQ2.profiniteQuotient (GQ2.relatorSubgroup rels)

theorem GQ2.relator_quotientMk_eq_one {X : Type u} (rels : Set ↑(FreeProfiniteGroup X).toProfinite.toTop) {r : ↑(FreeProfiniteGroup X).toProfinite.toTop} (hr : r ∈ rels) : (quotientMk (relatorSubgroup rels)) r = 1

The presentation does impose the relations: each relator maps to 1 under the quotient projection FreeProfiniteGroup X → FreeProfiniteGroup X ⧸ relatorSubgroup rels.