Free profinite groups

The paper's presentation lives in the free profinite group on the four generators σ, τ, x₀, x₁. Mathlib has no FreeProfiniteGroup (see docs/foundations-audit.md), but it now has ProfiniteGrp.profiniteCompletion (the profinite completion functor, left adjoint to the forgetful functor ProfiniteGrp ⥤ GrpCat, by A. Topaz). Composing it with the ordinary free group gives free profinite groups, with the expected universal property.

• GQ2.FreeProfiniteGroup X — the free profinite group on X.
• GQ2.FreeProfiniteGroup.of — the inclusion of generators.
• GQ2.FreeProfiniteGroup.homEquiv — the universal property: continuous homs FreeProfiniteGroup X ⟶ P into a profinite group P biject with set maps X → P.

noncomputable def GQ2.FreeProfiniteGroup (X : Type u) : ProfiniteGrp.{u}

The free profinite group on a type X: the profinite completion of the discrete free group FreeGroup X.

Equations

• GQ2.FreeProfiniteGroup X = ProfiniteGrp.profiniteCompletion.obj (GrpCat.of (FreeGroup X))

noncomputable def GQ2.FreeProfiniteGroup.of {X : Type u} (x : X) : ↑(FreeProfiniteGroup X).toProfinite.toTop

The canonical inclusion of the generators X → FreeProfiniteGroup X.

Equations

• GQ2.FreeProfiniteGroup.of x = ProfiniteGrp.ProfiniteCompletion.etaFn (GrpCat.of (FreeGroup X)) (FreeGroup.of x)

def GQ2.grpCatHomEquiv (A : Type u) [Group A] (P : ProfiniteGrp.{u}) : (GrpCat.of A ⟶ GrpCat.of ↑P.toProfinite.toTop) ≃ (A →* ↑P.toProfinite.toTop)

GrpCat morphisms between of-objects are exactly monoid homs.

Equations

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

noncomputable def GQ2.FreeProfiniteGroup.homEquiv (X : Type u) (P : ProfiniteGrp.{u}) : (FreeProfiniteGroup X ⟶ P) ≃ (X → ↑P.toProfinite.toTop)

Universal property of the free profinite group. Morphisms of profinite groups FreeProfiniteGroup X ⟶ P correspond naturally to set maps X → P. Obtained by composing the profinite-completion adjunction with the universal property of the free group.

Equations

• GQ2.FreeProfiniteGroup.homEquiv X P = (ProfiniteGrp.ProfiniteCompletion.homEquiv (GrpCat.of (FreeGroup X)) P).trans ((GQ2.grpCatHomEquiv (FreeGroup X) P).trans FreeGroup.lift.symm)

@[simp]

theorem GQ2.FreeProfiniteGroup.homEquiv_apply {X : Type u} (P : ProfiniteGrp.{u}) (f : FreeProfiniteGroup X ⟶ P) (x : X) : (homEquiv X P) f x = (ProfiniteGrp.Hom.hom f) (of x)

Naturality / usability of the universal property. The bijection homEquiv sends a continuous hom f : FreeProfiniteGroup X ⟶ P to the set map x ↦ f (of x) — i.e. homEquiv really is "restrict to the generators". This makes the universal property usable for defining maps out of FreeProfiniteGroup X (and, in turn, profinite presentations such as Γ_A).

@[simp]

theorem GQ2.FreeProfiniteGroup.homEquiv_symm_of {X : Type u} (P : ProfiniteGrp.{u}) (m : X → ↑P.toProfinite.toTop) (x : X) : (ProfiniteGrp.Hom.hom ((homEquiv X P).symm m)) (of x) = m x

Evaluation of the inverse of the universal property: the continuous hom classified by a set map m : X → P sends the generator of x to m x.