Profinite groups defined by generators and relators

This file constructs profinite and pro-p groups from generators and relators. In each case the relators are quotiented by their closed normal closure, so the result remains profinite. The quotient maps and factorisation theorems let maps out of a presented group be specified on its generators together with the condition that they kill its relators.

The profinite construction allows finite quotients of any order. The pro-p construction starts with the free pro-p group and therefore retains only finite p-group quotients. Both universal properties are used to describe groups by finite sets of generators and relators.

The generators generate a presented group topologically, so a group presented on a finite type is topologically finitely generated. With no relators the presented group is the free group of the same kind (presentedProfiniteGroup.equivFreeProfiniteGroup, presentedProP.equivFreeProP). Every Hausdorff group that is a continuous image of freeProfiniteGroup X or of freeProP p X is presented on X, with the kernel as its set of relators (presentedProfiniteGroup.equivOfSurjective, presentedProP.equivOfSurjective). Combined with IsProP.exists_surjective_freeProP, a topologically finitely generated pro-p group G has a presentation on any finite type with at least topologicalGeneratorRankNat G elements; a presentation on exactly that many generators is what is called a minimal presentation of G.

A presented group is functorial in its presentation: a continuous homomorphism of the underlying free groups that sends the relators of the source into the closed normal closure of the relators of the target induces a continuous homomorphism of the presented groups, and a topological isomorphism of the free groups matching the two closed normal closures induces a topological isomorphism of the presented groups. In particular a presented group depends on its relators only through their closed normal closure. Finally, the pro-p group presented by the images of a set of profinite relators is a quotient of the profinite group they present.

Main results

• TauCeti.presentedProfiniteGroup.existsUnique_lift, TauCeti.presentedProP.existsUnique_lift: the universal properties.
• TauCeti.presentedProfiniteGroup.dense_closure_range_of, TauCeti.presentedProP.dense_closure_range_of: the generators generate topologically.
• TauCeti.presentedProfiniteGroup.isTopologicallyFinitelyGenerated, TauCeti.presentedProP.isTopologicallyFinitelyGenerated: a group presented on a finite type is topologically finitely generated.
• TauCeti.presentedProfiniteGroup.equivFreeProfiniteGroup, TauCeti.presentedProP.equivFreeProP: with no relators, the presented group is free.
• TauCeti.presentedProfiniteGroup.equivOfSurjective, TauCeti.presentedProP.equivOfSurjective: a continuous image of the free group is presented on X by the kernel.
• TauCeti.IsProP.exists_continuousMulEquiv_presentedProP: a topologically finitely generated pro-p group has a presentation on any finite type with at least topologicalGeneratorRankNat elements.
• TauCeti.presentedProfiniteGroup.map, TauCeti.presentedProP.map: functoriality in the generators and the relators.
• TauCeti.presentedProfiniteGroup.congr, TauCeti.presentedProP.congr: an isomorphism of the free groups matching the relators induces an isomorphism of the presented groups; TauCeti.presentedProP.congrSingleton is the one-relator case, for an isomorphism carrying the relator to the relator.
• TauCeti.presentedProfiniteGroup.congrOfClosureEq, TauCeti.presentedProP.congrOfClosureEq: relators with the same closed normal closure present the same group.
• TauCeti.presentedProfiniteGroup.toPresentedProP_surjective: a presented profinite group maps onto the pro-p group presented by the images of its relators.
• TauCeti.presentedProPGen: the generators of a pro-p group presented on Fin n, indexed by ℕ with value 1 out of range, as the images of TauCeti.freeProPGen.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Chapter 3 and Section 7.8.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Section III.9.
• Mathlib.GroupTheory.PresentedGroup, whose discrete analogues PresentedGroup.map and PresentedGroup.equivPresentedGroup are the model for the shape of the functoriality API here.

@[reducible, inline]

noncomputable abbrev TauCeti.presentedProfiniteGroup (X : Type u) (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) : Type u

The profinite group presented by generators X and relators rels, obtained by quotienting the free profinite group by the closed normal closure of the relators.

Equations

• TauCeti.presentedProfiniteGroup X rels = (↑(TauCeti.freeProfiniteGroup X).toProfinite.toTop ⧸ (Subgroup.normalClosure rels).topologicalClosure)

noncomputable def TauCeti.presentedProfiniteGroup.mk {X : Type u} (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* presentedProfiniteGroup X rels

The canonical quotient map from the free profinite group to the presented profinite group.

Equations

• TauCeti.presentedProfiniteGroup.mk rels = { toMonoidHom := QuotientGroup.mk' (Subgroup.normalClosure rels).topologicalClosure, continuous_toFun := ⋯ }

theorem TauCeti.presentedProfiniteGroup.mk_surjective {X : Type u} (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) : Function.Surjective ⇑(mk rels)

The canonical quotient map onto a presented profinite group is surjective.

noncomputable def TauCeti.presentedProfiniteGroup.of {X : Type u} (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) (x : X) : presentedProfiniteGroup X rels

The canonical generator in a presented profinite group.

Equations

• TauCeti.presentedProfiniteGroup.of rels x = (TauCeti.presentedProfiniteGroup.mk rels) (TauCeti.freeProfiniteGroup.of x)

@[simp]

theorem TauCeti.presentedProfiniteGroup.mk_of {X : Type u} (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) (x : X) : (mk rels) (freeProfiniteGroup.of x) = of rels x

The canonical generators of a presented profinite group are the images of the free generators under the quotient map.

@[simp]

theorem TauCeti.presentedProfiniteGroup.mk_relator {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} (r : ↑(freeProfiniteGroup X).toProfinite.toTop) (hr : r ∈ rels) : (mk rels) r = 1

The quotient map kills every relator.

@[simp]

theorem TauCeti.presentedProfiniteGroup.mk_eq_one_iff {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} (r : ↑(freeProfiniteGroup X).toProfinite.toTop) : (mk rels) r = 1 ↔ r ∈ (Subgroup.normalClosure rels).topologicalClosure

The kernel of the presentation map consists exactly of the closed normal closure of the relators.

theorem TauCeti.presentedProfiniteGroup.dense_closure_range_of {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} : Dense ↑(Subgroup.closure (Set.range (of rels)))

The generators generate the presented profinite group topologically.

noncomputable def TauCeti.presentedProfiniteGroup.lift {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] (ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hψ : ∀ r ∈ rels, ψ r = 1) : presentedProfiniteGroup X rels →ₜ* G

A continuous homomorphism from the free profinite group that kills the relators factors through the presented profinite group.

Equations

• TauCeti.presentedProfiniteGroup.lift ψ hψ = TauCeti.ContinuousMonoidHom.quotientLift (Subgroup.normalClosure rels).topologicalClosure ψ ⋯

@[simp]

theorem TauCeti.presentedProfiniteGroup.lift_comp_mk {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] (ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hψ : ∀ r ∈ rels, ψ r = 1) : (lift ψ hψ).comp (mk rels) = ψ

The factorisation through a presented profinite group recovers the original map after the canonical quotient projection.

@[simp]

theorem TauCeti.presentedProfiniteGroup.lift_mk {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] (ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hψ : ∀ r ∈ rels, ψ r = 1) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (lift ψ hψ) ((mk rels) x) = ψ x

The factorisation through a presented profinite group computes on classes as the original map.

@[simp]

theorem TauCeti.presentedProfiniteGroup.lift_of {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] (ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hψ : ∀ r ∈ rels, ψ r = 1) (x : X) : (lift ψ hψ) (of rels x) = ψ (freeProfiniteGroup.of x)

The factorisation from a presented profinite group evaluates on its generators as the original map does on the free generators.

theorem TauCeti.presentedProfiniteGroup.hom_ext {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] {φ ψ : presentedProfiniteGroup X rels →ₜ* G} (h : φ.comp (mk rels) = ψ.comp (mk rels)) : φ = ψ

Two continuous homomorphisms out of a presented profinite group are equal if they agree after precomposition with its quotient map.

theorem TauCeti.presentedProfiniteGroup.hom_ext_of {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] {φ ψ : presentedProfiniteGroup X rels →ₜ* G} (h : ∀ (x : X), φ (of rels x) = ψ (of rels x)) : φ = ψ

Two continuous homomorphisms out of a presented profinite group are equal if they agree on the canonical generators.

theorem TauCeti.presentedProfiniteGroup.hom_ext_of_iff {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] {φ ψ : presentedProfiniteGroup X rels →ₜ* G} : φ = ψ ↔ ∀ (x : X), φ (of rels x) = ψ (of rels x)

theorem TauCeti.presentedProfiniteGroup.existsUnique_lift {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] (ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hψ : ∀ r ∈ rels, ψ r = 1) : ∃! φ : presentedProfiniteGroup X rels →ₜ* G, φ.comp (mk rels) = ψ

A continuous homomorphism out of the free profinite group that kills the relators factors uniquely through the presented profinite group.

@[simp]

theorem TauCeti.presentedProfiniteGroup.comp_lift {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] {H : Type w} [Group H] [TopologicalSpace H] [T1Space H] (g : G →ₜ* H) (ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hψ : ∀ r ∈ rels, ψ r = 1) : g.comp (lift ψ hψ) = lift (g.comp ψ) ⋯

The factorisation through a presented profinite group is natural in the target.

theorem TauCeti.presentedProfiniteGroup.lift_surjective {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {G : Type v} [Group G] [TopologicalSpace G] [T1Space G] {ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G} (hψ : ∀ r ∈ rels, ψ r = 1) (hs : Function.Surjective ⇑ψ) : Function.Surjective ⇑(lift ψ hψ)

The factorisation through a presented profinite group of a surjection is surjective.

theorem TauCeti.presentedProfiniteGroup.isTopologicallyFinitelyGenerated {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} [Finite X] : IsTopologicallyFinitelyGenerated (presentedProfiniteGroup X rels)

A profinite group presented on a finite type is topologically finitely generated.

Functoriality in the generators and the relators

The shape of this API follows Mathlib's discrete analogues PresentedGroup.map and PresentedGroup.equivPresentedGroup in Mathlib.GroupTheory.PresentedGroup.

noncomputable def TauCeti.presentedProfiniteGroup.map {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (hφ : ∀ r ∈ rels, (mk rels') (φ r) = 1) : presentedProfiniteGroup X rels →ₜ* presentedProfiniteGroup Y rels'

The continuous homomorphism of presented profinite groups induced by a continuous homomorphism of the underlying free profinite groups that sends every relator into the closed normal closure of the target relators.

Equations

• TauCeti.presentedProfiniteGroup.map φ hφ = TauCeti.presentedProfiniteGroup.lift ((TauCeti.presentedProfiniteGroup.mk rels').comp φ) hφ

@[simp]

theorem TauCeti.presentedProfiniteGroup.map_mk {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (hφ : ∀ r ∈ rels, (mk rels') (φ r) = 1) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (map φ hφ) ((mk rels) x) = (mk rels') (φ x)

The induced homomorphism computes on classes as the homomorphism of free profinite groups.

@[simp]

theorem TauCeti.presentedProfiniteGroup.map_of {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (hφ : ∀ r ∈ rels, (mk rels') (φ r) = 1) (x : X) : (map φ hφ) (of rels x) = (mk rels') (φ (freeProfiniteGroup.of x))

The induced homomorphism sends a generator to the class of its image.

theorem TauCeti.presentedProfiniteGroup.mk_eq_one_of_mk_eq_one {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (hφ : ∀ r ∈ rels, (mk rels') (φ r) = 1) {x : ↑(freeProfiniteGroup X).toProfinite.toTop} (hx : (mk rels) x = 1) : (mk rels') (φ x) = 1

A continuous homomorphism of free profinite groups that sends the relators into the closed normal closure of the target relators sends the whole closed normal closure into it.

@[simp]

theorem TauCeti.presentedProfiniteGroup.map_id {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} : map (ContinuousMonoidHom.id ↑(freeProfiniteGroup X).toProfinite.toTop) ⋯ = ContinuousMonoidHom.id (presentedProfiniteGroup X rels)

The identity of the free profinite group induces the identity of a presented group.

theorem TauCeti.presentedProfiniteGroup.map_comp {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} {Z : Type w} {rels'' : Set ↑(freeProfiniteGroup Z).toProfinite.toTop} (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (hφ : ∀ r ∈ rels, (mk rels') (φ r) = 1) (ψ : ↑(freeProfiniteGroup Y).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Z).toProfinite.toTop) (hψ : ∀ r ∈ rels', (mk rels'') (ψ r) = 1) : (map ψ hψ).comp (map φ hφ) = map (ψ.comp φ) ⋯

The homomorphisms induced by a composite are the composite of the induced homomorphisms.

theorem TauCeti.presentedProfiniteGroup.map_surjective {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} {φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop} (hφ : ∀ r ∈ rels, (mk rels') (φ r) = 1) (hs : Function.Surjective ⇑φ) : Function.Surjective ⇑(map φ hφ)

A surjection of free profinite groups induces a surjection of presented profinite groups.

noncomputable def TauCeti.presentedProfiniteGroup.congr {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (e : ↑(freeProfiniteGroup X).toProfinite.toTop ≃ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (h : ∀ r ∈ rels, (mk rels') (e r) = 1) (h' : ∀ r ∈ rels', (mk rels) (e.symm r) = 1) : presentedProfiniteGroup X rels ≃ₜ* presentedProfiniteGroup Y rels'

A topological isomorphism of the free profinite groups sending each set of relators into the closed normal closure of the other induces a topological isomorphism of the presented profinite groups.

Equations

• TauCeti.presentedProfiniteGroup.congr e h h' = e.quotientCongr (Subgroup.normalClosure rels).topologicalClosure (Subgroup.normalClosure rels').topologicalClosure ⋯

@[simp]

theorem TauCeti.presentedProfiniteGroup.congr_mk {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (e : ↑(freeProfiniteGroup X).toProfinite.toTop ≃ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (h : ∀ r ∈ rels, (mk rels') (e r) = 1) (h' : ∀ r ∈ rels', (mk rels) (e.symm r) = 1) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (congr e h h') ((mk rels) x) = (mk rels') (e x)

The induced isomorphism computes on classes as the isomorphism of free profinite groups.

@[simp]

theorem TauCeti.presentedProfiniteGroup.congr_symm_mk {X : Type u} {rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop} {Y : Type v} {rels' : Set ↑(freeProfiniteGroup Y).toProfinite.toTop} (e : ↑(freeProfiniteGroup X).toProfinite.toTop ≃ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop) (h : ∀ r ∈ rels, (mk rels') (e r) = 1) (h' : ∀ r ∈ rels', (mk rels) (e.symm r) = 1) (y : ↑(freeProfiniteGroup Y).toProfinite.toTop) : (congr e h h').symm ((mk rels') y) = (mk rels) (e.symm y)

The inverse of the induced isomorphism computes on classes as the inverse isomorphism of free profinite groups.

noncomputable def TauCeti.presentedProfiniteGroup.congrOfClosureEq {X : Type u} {rels rels₂ : Set ↑(freeProfiniteGroup X).toProfinite.toTop} (h : (Subgroup.normalClosure rels).topologicalClosure = (Subgroup.normalClosure rels₂).topologicalClosure) : presentedProfiniteGroup X rels ≃ₜ* presentedProfiniteGroup X rels₂

Two sets of relators with the same closed normal closure present the same profinite group, by an isomorphism matching the classes of every element of the free profinite group.

Equations

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

@[simp]

theorem TauCeti.presentedProfiniteGroup.congrOfClosureEq_mk {X : Type u} {rels rels₂ : Set ↑(freeProfiniteGroup X).toProfinite.toTop} (h : (Subgroup.normalClosure rels).topologicalClosure = (Subgroup.normalClosure rels₂).topologicalClosure) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (congrOfClosureEq h) ((mk rels) x) = (mk rels₂) x

The isomorphism between presentations with the same closed normal closure fixes the class of every element of the free profinite group.

@[simp]

theorem TauCeti.presentedProfiniteGroup.congrOfClosureEq_symm_mk {X : Type u} {rels rels₂ : Set ↑(freeProfiniteGroup X).toProfinite.toTop} (h : (Subgroup.normalClosure rels).topologicalClosure = (Subgroup.normalClosure rels₂).topologicalClosure) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (congrOfClosureEq h).symm ((mk rels₂) x) = (mk rels) x

The inverse of the isomorphism between presentations with the same closed normal closure also fixes the class of every element of the free profinite group.

The empty set of relators

noncomputable def TauCeti.presentedProfiniteGroup.equivFreeProfiniteGroup {X : Type u} : presentedProfiniteGroup X ∅ ≃ₜ* ↑(freeProfiniteGroup X).toProfinite.toTop

With no relators, the presented profinite group is the free profinite group: the canonical quotient map is a topological isomorphism.

Equations

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

@[simp]

theorem TauCeti.presentedProfiniteGroup.equivFreeProfiniteGroup_symm_apply {X : Type u} (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : equivFreeProfiniteGroup.symm x = (mk ∅) x

The inverse of the isomorphism with the free profinite group is the canonical quotient map.

@[simp]

theorem TauCeti.presentedProfiniteGroup.equivFreeProfiniteGroup_mk {X : Type u} (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : equivFreeProfiniteGroup ((mk ∅) x) = x

The isomorphism with the free profinite group sends the class of an element to that element.

@[simp]

theorem TauCeti.presentedProfiniteGroup.equivFreeProfiniteGroup_of {X : Type u} (x : X) : equivFreeProfiniteGroup (of ∅ x) = freeProfiniteGroup.of x

The isomorphism with the free profinite group matches the generators.

Continuous images of free profinite groups are presented

noncomputable def TauCeti.presentedProfiniteGroup.equivOfSurjective {X : Type u} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hφ : Function.Surjective ⇑φ) : presentedProfiniteGroup X ↑(↑φ).ker ≃ₜ* G

A Hausdorff group that is a continuous image of the free profinite group on X is presented on X, with the kernel as its set of relators. Algebraically this is the first isomorphism theorem, QuotientGroup.liftEquiv.

Equations

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

@[simp]

theorem TauCeti.presentedProfiniteGroup.equivOfSurjective_mk {X : Type u} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hφ : Function.Surjective ⇑φ) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (equivOfSurjective φ hφ) ((mk ↑(↑φ).ker) x) = φ x

The presentation isomorphism of a continuous image sends the class of an element to its image.

@[simp]

theorem TauCeti.presentedProfiniteGroup.equivOfSurjective_of {X : Type u} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* G) (hφ : Function.Surjective ⇑φ) (x : X) : (equivOfSurjective φ hφ) (of (↑(↑φ).ker) x) = φ (freeProfiniteGroup.of x)

The presentation isomorphism of a continuous image matches the generators.

@[reducible, inline]

noncomputable abbrev TauCeti.presentedProP (p : ℕ) (X : Type u) (rels : Set (freeProP p X)) : Type u

The pro-p group presented by generators X and relators rels, obtained by quotienting the free pro-p group by the closed normal closure of the relators.

Equations

• TauCeti.presentedProP p X rels = (TauCeti.freeProP p X ⧸ (Subgroup.normalClosure rels).topologicalClosure)

noncomputable def TauCeti.presentedProP.mk (p : ℕ) {X : Type u} (rels : Set (freeProP p X)) : freeProP p X →ₜ* presentedProP p X rels

The canonical quotient map from the free pro-p group to the presented pro-p group.

Equations

• TauCeti.presentedProP.mk p rels = { toMonoidHom := QuotientGroup.mk' (Subgroup.normalClosure rels).topologicalClosure, continuous_toFun := ⋯ }

theorem TauCeti.presentedProP.mk_surjective (p : ℕ) {X : Type u} (rels : Set (freeProP p X)) : Function.Surjective ⇑(mk p rels)

The canonical quotient map onto a presented pro-p group is surjective.

noncomputable def TauCeti.presentedProP.of (p : ℕ) {X : Type u} (rels : Set (freeProP p X)) (x : X) : presentedProP p X rels

The canonical generator in a presented pro-p group.

Equations

• TauCeti.presentedProP.of p rels x = (TauCeti.presentedProP.mk p rels) (TauCeti.freeProP.of x)

@[simp]

theorem TauCeti.presentedProP.mk_of (p : ℕ) {X : Type u} (rels : Set (freeProP p X)) (x : X) : (mk p rels) (freeProP.of x) = of p rels x

The canonical generators of a presented pro-p group are the images of the free generators under the quotient map.

theorem TauCeti.presentedProP.isProP (p : ℕ) (X : Type u) (rels : Set (freeProP p X)) : IsProP p (presentedProP p X rels)

A presented pro-p group is pro-p, since it is a quotient of a free pro-p group.

@[simp]

theorem TauCeti.presentedProP.mk_relator {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} (r : freeProP p X) (hr : r ∈ rels) : (mk p rels) r = 1

The quotient map kills every relator.

@[simp]

theorem TauCeti.presentedProP.mk_eq_one_iff {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} (r : freeProP p X) : (mk p rels) r = 1 ↔ r ∈ (Subgroup.normalClosure rels).topologicalClosure

The kernel of the presentation map consists exactly of the closed normal closure of the relators.

@[simp]

theorem TauCeti.presentedProP.ker_mk {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} : (↑(mk p rels)).ker = (Subgroup.normalClosure rels).topologicalClosure

The kernel of the quotient map onto a presented pro-p group is the closed normal closure of the relators.

theorem TauCeti.presentedProP.dense_closure_range_of {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} : Dense ↑(Subgroup.closure (Set.range (of p rels)))

The generators generate the presented pro-p group topologically.

theorem TauCeti.presentedProP.topologicalClosure_closure_range_of_eq_top {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} : (Subgroup.closure (Set.range (of p rels))).topologicalClosure = ⊤

The generators generate the presented pro-p group topologically, as an equation of subgroups.

theorem TauCeti.presentedProP.isTopologicallyFinitelyGenerated {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} [Finite X] : IsTopologicallyFinitelyGenerated (presentedProP p X rels)

A pro-p group presented on a finite type is topologically finitely generated.

noncomputable def TauCeti.presentedProP.lift {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] (ψ : freeProP p X →ₜ* P) (hψ : ∀ r ∈ rels, ψ r = 1) : presentedProP p X rels →ₜ* P

A continuous homomorphism from the free pro-p group that kills the relators factors through the presented pro-p group.

Equations

• TauCeti.presentedProP.lift ψ hψ = TauCeti.ContinuousMonoidHom.quotientLift (Subgroup.normalClosure rels).topologicalClosure ψ ⋯

@[simp]

theorem TauCeti.presentedProP.lift_comp_mk {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] (ψ : freeProP p X →ₜ* P) (hψ : ∀ r ∈ rels, ψ r = 1) : (lift ψ hψ).comp (mk p rels) = ψ

The factorisation through a presented pro-p group recovers the original map after the canonical quotient projection.

@[simp]

theorem TauCeti.presentedProP.lift_mk {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] (ψ : freeProP p X →ₜ* P) (hψ : ∀ r ∈ rels, ψ r = 1) (x : freeProP p X) : (lift ψ hψ) ((mk p rels) x) = ψ x

The factorisation through a presented pro-p group computes on classes as the original map.

@[simp]

theorem TauCeti.presentedProP.lift_of {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] (ψ : freeProP p X →ₜ* P) (hψ : ∀ r ∈ rels, ψ r = 1) (x : X) : (lift ψ hψ) (of p rels x) = ψ (freeProP.of x)

The factorisation from a presented pro-p group evaluates on its generators as the original map does on the free generators.

theorem TauCeti.presentedProP.hom_ext {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] {φ ψ : presentedProP p X rels →ₜ* P} (h : φ.comp (mk p rels) = ψ.comp (mk p rels)) : φ = ψ

Two continuous homomorphisms out of a presented pro-p group are equal if they agree after precomposition with its quotient map.

theorem TauCeti.presentedProP.hom_ext_of {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T2Space P] {φ ψ : presentedProP p X rels →ₜ* P} (h : ∀ (x : X), φ (of p rels x) = ψ (of p rels x)) : φ = ψ

Two continuous homomorphisms out of a presented pro-p group are equal if they agree on the canonical generators.

theorem TauCeti.presentedProP.hom_ext_of_iff {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T2Space P] {φ ψ : presentedProP p X rels →ₜ* P} : φ = ψ ↔ ∀ (x : X), φ (of p rels x) = ψ (of p rels x)

theorem TauCeti.presentedProP.existsUnique_lift {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] (ψ : freeProP p X →ₜ* P) (hψ : ∀ r ∈ rels, ψ r = 1) : ∃! φ : presentedProP p X rels →ₜ* P, φ.comp (mk p rels) = ψ

A continuous homomorphism out of the free pro-p group that kills the relators factors uniquely through the presented pro-p group.

@[simp]

theorem TauCeti.presentedProP.comp_lift {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] {Q : Type w} [Group Q] [TopologicalSpace Q] [T1Space Q] (g : P →ₜ* Q) (ψ : freeProP p X →ₜ* P) (hψ : ∀ r ∈ rels, ψ r = 1) : g.comp (lift ψ hψ) = lift (g.comp ψ) ⋯

The factorisation through a presented pro-p group is natural in the target.

theorem TauCeti.presentedProP.lift_surjective {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {P : Type v} [Group P] [TopologicalSpace P] [T1Space P] {ψ : freeProP p X →ₜ* P} (hψ : ∀ r ∈ rels, ψ r = 1) (hs : Function.Surjective ⇑ψ) : Function.Surjective ⇑(lift ψ hψ)

The factorisation through a presented pro-p group of a surjection is surjective.

Functoriality in the generators and the relators

The shape of this API follows Mathlib's discrete analogues PresentedGroup.map and PresentedGroup.equivPresentedGroup in Mathlib.GroupTheory.PresentedGroup.

noncomputable def TauCeti.presentedProP.map {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (φ : freeProP p X →ₜ* freeProP p Y) (hφ : ∀ r ∈ rels, (mk p rels') (φ r) = 1) : presentedProP p X rels →ₜ* presentedProP p Y rels'

The continuous homomorphism of presented pro-p groups induced by a continuous homomorphism of the underlying free pro-p groups that sends every relator into the closed normal closure of the target relators.

Equations

• TauCeti.presentedProP.map φ hφ = TauCeti.presentedProP.lift ((TauCeti.presentedProP.mk p rels').comp φ) hφ

@[simp]

theorem TauCeti.presentedProP.map_mk {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (φ : freeProP p X →ₜ* freeProP p Y) (hφ : ∀ r ∈ rels, (mk p rels') (φ r) = 1) (x : freeProP p X) : (map φ hφ) ((mk p rels) x) = (mk p rels') (φ x)

The induced homomorphism computes on classes as the homomorphism of free pro-p groups.

@[simp]

theorem TauCeti.presentedProP.map_of {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (φ : freeProP p X →ₜ* freeProP p Y) (hφ : ∀ r ∈ rels, (mk p rels') (φ r) = 1) (x : X) : (map φ hφ) (of p rels x) = (mk p rels') (φ (freeProP.of x))

The induced homomorphism sends a generator to the class of its image.

theorem TauCeti.presentedProP.mk_eq_one_of_mk_eq_one {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (φ : freeProP p X →ₜ* freeProP p Y) (hφ : ∀ r ∈ rels, (mk p rels') (φ r) = 1) {x : freeProP p X} (hx : (mk p rels) x = 1) : (mk p rels') (φ x) = 1

A continuous homomorphism of free pro-p groups that sends the relators into the closed normal closure of the target relators sends the whole closed normal closure into it.

@[simp]

theorem TauCeti.presentedProP.map_id {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} : map (ContinuousMonoidHom.id (freeProP p X)) ⋯ = ContinuousMonoidHom.id (presentedProP p X rels)

The identity of the free pro-p group induces the identity of a presented group.

theorem TauCeti.presentedProP.map_comp {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} {Z : Type w} {rels'' : Set (freeProP p Z)} (φ : freeProP p X →ₜ* freeProP p Y) (hφ : ∀ r ∈ rels, (mk p rels') (φ r) = 1) (ψ : freeProP p Y →ₜ* freeProP p Z) (hψ : ∀ r ∈ rels', (mk p rels'') (ψ r) = 1) : (map ψ hψ).comp (map φ hφ) = map (ψ.comp φ) ⋯

The homomorphisms induced by a composite are the composite of the induced homomorphisms.

theorem TauCeti.presentedProP.map_surjective {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} {φ : freeProP p X →ₜ* freeProP p Y} (hφ : ∀ r ∈ rels, (mk p rels') (φ r) = 1) (hs : Function.Surjective ⇑φ) : Function.Surjective ⇑(map φ hφ)

A surjection of free pro-p groups induces a surjection of presented pro-p groups.

noncomputable def TauCeti.presentedProP.congr {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (e : freeProP p X ≃ₜ* freeProP p Y) (h : ∀ r ∈ rels, (mk p rels') (e r) = 1) (h' : ∀ r ∈ rels', (mk p rels) (e.symm r) = 1) : presentedProP p X rels ≃ₜ* presentedProP p Y rels'

A topological isomorphism of the free pro-p groups sending each set of relators into the closed normal closure of the other induces a topological isomorphism of the presented pro-p groups.

Equations

• TauCeti.presentedProP.congr e h h' = e.quotientCongr (Subgroup.normalClosure rels).topologicalClosure (Subgroup.normalClosure rels').topologicalClosure ⋯

@[simp]

theorem TauCeti.presentedProP.congr_mk {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (e : freeProP p X ≃ₜ* freeProP p Y) (h : ∀ r ∈ rels, (mk p rels') (e r) = 1) (h' : ∀ r ∈ rels', (mk p rels) (e.symm r) = 1) (x : freeProP p X) : (congr e h h') ((mk p rels) x) = (mk p rels') (e x)

The induced isomorphism computes on classes as the isomorphism of free pro-p groups.

@[simp]

theorem TauCeti.presentedProP.congr_symm_mk {p : ℕ} {X : Type u} {rels : Set (freeProP p X)} {Y : Type v} {rels' : Set (freeProP p Y)} (e : freeProP p X ≃ₜ* freeProP p Y) (h : ∀ r ∈ rels, (mk p rels') (e r) = 1) (h' : ∀ r ∈ rels', (mk p rels) (e.symm r) = 1) (y : freeProP p Y) : (congr e h h').symm ((mk p rels') y) = (mk p rels) (e.symm y)

The inverse of the induced isomorphism computes on classes as the inverse isomorphism of free pro-p groups.

noncomputable def TauCeti.presentedProP.congrSingleton {p : ℕ} {X : Type u} {Y : Type v} (e : freeProP p X ≃ₜ* freeProP p Y) {r : freeProP p X} {r' : freeProP p Y} (h : e r = r') : presentedProP p X {r} ≃ₜ* presentedProP p Y {r'}

A topological isomorphism of the free pro-p groups carrying the relator r to the relator r' induces a topological isomorphism of the one-relator presented pro-p groups ⟨X ∣ r⟩ ≃ₜ* ⟨Y ∣ r'⟩.

Equations

• TauCeti.presentedProP.congrSingleton e h = TauCeti.presentedProP.congr e ⋯ ⋯

@[simp]

theorem TauCeti.presentedProP.congrSingleton_mk {p : ℕ} {X : Type u} {Y : Type v} (e : freeProP p X ≃ₜ* freeProP p Y) {r : freeProP p X} {r' : freeProP p Y} (h : e r = r') (x : freeProP p X) : (congrSingleton e h) ((mk p {r}) x) = (mk p {r'}) (e x)

The isomorphism of one-relator presented groups induced by e computes on classes as e.

@[simp]

theorem TauCeti.presentedProP.congrSingleton_symm_mk {p : ℕ} {X : Type u} {Y : Type v} (e : freeProP p X ≃ₜ* freeProP p Y) {r : freeProP p X} {r' : freeProP p Y} (h : e r = r') (y : freeProP p Y) : (congrSingleton e h).symm ((mk p {r'}) y) = (mk p {r}) (e.symm y)

The inverse of the isomorphism of one-relator presented groups induced by e computes on classes as e⁻¹.

noncomputable def TauCeti.presentedProP.congrOfClosureEq {p : ℕ} {X : Type u} {rels rels₂ : Set (freeProP p X)} (h : (Subgroup.normalClosure rels).topologicalClosure = (Subgroup.normalClosure rels₂).topologicalClosure) : presentedProP p X rels ≃ₜ* presentedProP p X rels₂

Two sets of relators with the same closed normal closure present the same pro-p group, by an isomorphism matching the classes of every element of the free pro-p group.

Equations

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

@[simp]

theorem TauCeti.presentedProP.congrOfClosureEq_mk {p : ℕ} {X : Type u} {rels rels₂ : Set (freeProP p X)} (h : (Subgroup.normalClosure rels).topologicalClosure = (Subgroup.normalClosure rels₂).topologicalClosure) (x : freeProP p X) : (congrOfClosureEq h) ((mk p rels) x) = (mk p rels₂) x

The isomorphism between presentations with the same closed normal closure fixes the class of every element of the free pro-p group.

@[simp]

theorem TauCeti.presentedProP.congrOfClosureEq_symm_mk {p : ℕ} {X : Type u} {rels rels₂ : Set (freeProP p X)} (h : (Subgroup.normalClosure rels).topologicalClosure = (Subgroup.normalClosure rels₂).topologicalClosure) (x : freeProP p X) : (congrOfClosureEq h).symm ((mk p rels₂) x) = (mk p rels) x

The inverse of the isomorphism between presentations with the same closed normal closure also fixes the class of every element of the free pro-p group.

The empty set of relators

noncomputable def TauCeti.presentedProP.equivFreeProP {p : ℕ} {X : Type u} : presentedProP p X ∅ ≃ₜ* freeProP p X

With no relators, the presented pro-p group is the free pro-p group: the canonical quotient map is a topological isomorphism.

Equations

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

@[simp]

theorem TauCeti.presentedProP.equivFreeProP_symm_apply {p : ℕ} {X : Type u} (x : freeProP p X) : equivFreeProP.symm x = (mk p ∅) x

The inverse of the isomorphism with the free pro-p group is the canonical quotient map.

@[simp]

theorem TauCeti.presentedProP.equivFreeProP_mk {p : ℕ} {X : Type u} (x : freeProP p X) : equivFreeProP ((mk p ∅) x) = x

The isomorphism with the free pro-p group sends the class of an element to that element.

@[simp]

theorem TauCeti.presentedProP.equivFreeProP_of {p : ℕ} {X : Type u} (x : X) : equivFreeProP (of p ∅ x) = freeProP.of x

The isomorphism with the free pro-p group matches the generators.

Continuous images of free pro-p groups are presented

noncomputable def TauCeti.presentedProP.equivOfSurjective {p : ℕ} {X : Type u} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] (φ : freeProP p X →ₜ* G) (hφ : Function.Surjective ⇑φ) : presentedProP p X ↑(↑φ).ker ≃ₜ* G

A Hausdorff group that is a continuous image of the free pro-p group on X is presented on X, with the kernel as its set of relators. Algebraically this is the first isomorphism theorem, QuotientGroup.liftEquiv.

Equations

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

@[simp]

theorem TauCeti.presentedProP.equivOfSurjective_mk {p : ℕ} {X : Type u} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] (φ : freeProP p X →ₜ* G) (hφ : Function.Surjective ⇑φ) (x : freeProP p X) : (equivOfSurjective φ hφ) ((mk p ↑(↑φ).ker) x) = φ x

The presentation isomorphism of a continuous image sends the class of an element to its image.

@[simp]

theorem TauCeti.presentedProP.equivOfSurjective_of {p : ℕ} {X : Type u} {G : Type v} [Group G] [TopologicalSpace G] [T2Space G] (φ : freeProP p X →ₜ* G) (hφ : Function.Surjective ⇑φ) (x : X) : (equivOfSurjective φ hφ) (of p (↑(↑φ).ker) x) = φ (freeProP.of x)

The presentation isomorphism of a continuous image matches the generators.

From a profinite presentation to a pro-p presentation

noncomputable def TauCeti.presentedProfiniteGroup.toPresentedProP {X : Type u} (p : ℕ) (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) : presentedProfiniteGroup X rels →ₜ* presentedProP p X (⇑(freeProP.fromFreeProfiniteGroup p X) '' rels)

The canonical continuous homomorphism from a presented profinite group to the pro-p group presented on the same generators by the images of the relators in the free pro-p group.

Equations

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

@[simp]

theorem TauCeti.presentedProfiniteGroup.toPresentedProP_mk {X : Type u} (p : ℕ) (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (toPresentedProP p rels) ((mk rels) x) = (presentedProP.mk p (⇑(freeProP.fromFreeProfiniteGroup p X) '' rels)) ((freeProP.fromFreeProfiniteGroup p X) x)

The comparison homomorphism computes on classes through the canonical map to the free pro-p group.

@[simp]

theorem TauCeti.presentedProfiniteGroup.toPresentedProP_of {X : Type u} (p : ℕ) (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) (x : X) : (toPresentedProP p rels) (of rels x) = presentedProP.of p (⇑(freeProP.fromFreeProfiniteGroup p X) '' rels) x

The comparison homomorphism matches the canonical generators.

theorem TauCeti.presentedProfiniteGroup.toPresentedProP_surjective {X : Type u} (p : ℕ) (rels : Set ↑(freeProfiniteGroup X).toProfinite.toTop) : Function.Surjective ⇑(toPresentedProP p rels)

A presented profinite group maps onto the pro-p group presented by the images of its relators.

Presentations of topologically finitely generated pro-p groups

theorem TauCeti.IsProP.exists_continuousMulEquiv_presentedProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (h : IsTopologicallyFinitelyGenerated G) (X : Type u) [Finite X] (hX : topologicalGeneratorRankNat G h ≤ Nat.card X) : ∃ (rels : Set (freeProP p X)), Nonempty (presentedProP p X rels ≃ₜ* G)

Every topologically finitely generated pro-p group has a presentation on any finite type with at least topologicalGeneratorRankNat G elements, in particular on a type with exactly topologicalGeneratorRankNat G elements, which is what a minimal presentation means.

The generators of a presentation on Fin n, indexed by ℕ

noncomputable def TauCeti.presentedProPGen (p n : ℕ) (rels : Set (freeProP p (Fin n))) (i : ℕ) : presentedProP p (Fin n) rels

The generators of a pro-p group presented on Fin n, indexed by ℕ with value 1 out of range: the images of TauCeti.freeProPGen.

Equations

• TauCeti.presentedProPGen p n rels i = (TauCeti.presentedProP.mk p rels) (TauCeti.freeProPGen p n i)

@[simp]

theorem TauCeti.presentedProP.mk_freeProPGen (p n : ℕ) (rels : Set (freeProP p (Fin n))) (i : ℕ) : (mk p rels) (freeProPGen p n i) = presentedProPGen p n rels i

The quotient map carries freeProPGen to presentedProPGen.

@[simp]

theorem TauCeti.presentedProPGen_of_lt (p n : ℕ) (rels : Set (freeProP p (Fin n))) {i : ℕ} (h : i < n) : presentedProPGen p n rels i = presentedProP.of p rels ⟨i, h⟩

In range, presentedProPGen p n rels i is the i-th canonical generator.

@[simp]

theorem TauCeti.presentedProPGen_eq_one_of_le (p n : ℕ) (rels : Set (freeProP p (Fin n))) {i : ℕ} (h : n ≤ i) : presentedProPGen p n rels i = 1

Out of range, presentedProPGen p n rels i is 1.

theorem TauCeti.presentedProPGen_val (p n : ℕ) (rels : Set (freeProP p (Fin n))) (i : Fin n) : presentedProPGen p n rels ↑i = presentedProP.of p rels i

On the values of Fin n, presentedProPGen p n rels is the canonical generator.

theorem TauCeti.map_presentedProPGen (p n : ℕ) (rels : Set (freeProP p (Fin n))) {K : Type u_1} {F : Type u_2} [Group K] [FunLike F (presentedProP p (Fin n) rels) K] [MonoidHomClass F (presentedProP p (Fin n) rels) K] (φ : F) (i : ℕ) : φ (presentedProPGen p n rels i) = if h : i < n then φ (presentedProP.of p rels ⟨i, h⟩) else 1

The value of a homomorphism on the ℕ-indexed generators of a presented group.

@[simp]

theorem TauCeti.presentedProP.mk_comp_freeProPGen (p n : ℕ) (rels : Set (freeProP p (Fin n))) : ⇑(mk p rels) ∘ freeProPGen p n = presentedProPGen p n rels

The quotient map carries the tuple freeProPGen to the tuple presentedProPGen: the function-level form of TauCeti.presentedProP.mk_freeProPGen, which lets a word read on presentedProPGen be pulled back along the quotient map to the same word on freeProPGen.

theorem TauCeti.presentedProP.comp_mk_freeProPGen (p n : ℕ) (rels : Set (freeProP p (Fin n))) {K : Type u_1} [Monoid K] [TopologicalSpace K] (φ : presentedProP p (Fin n) rels →ₜ* K) (i : ℕ) : (φ.comp (mk p rels)) (freeProPGen p n i) = φ (presentedProPGen p n rels i)

A continuous homomorphism of the presented group, pulled back to the free group along the quotient map, takes on the ℕ-indexed free generators its values on presentedProPGen.