instance Q2Presentation.instFiniteCarrierToTopTotallyDisconnectedSpaceToProfiniteOfFiniteGrpOf_q2Presentation {H : Type} [Group H] [Finite H] : Finite ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)).toProfinite.toTop

The bundled finite-group carrier is finite (definitional).

theorem Q2Presentation.relator_eval_one_of_hom {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) (w : GExpr) (hw : ∀ (A : AdmissibleIndex), (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) (gammaGen a)) = 1) : (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom φ) (gammaGen a)) = 1

Relator transport: a word killed at every admissible coordinate is killed along any continuous hom into a finite group.

theorem Q2Presentation.tameRelator_eval_one_of_hom {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) : (Q2Word.tameRelator.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom φ) (gammaGen a)) = 1

The tame relator dies along any hom out of Γ_A.

theorem Q2Presentation.wildRelator_eval_one_of_hom {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) : (Q2Word.wildRelator.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom φ) (gammaGen a)) = 1

The wild relator dies along any hom out of Γ_A.