Finitely Presented Groups

This file defines finitely presented groups.

Main definitions

• Subgroup.IsNormalClosureFG N: says that the subgroup N is the normal closure of a finitely generated subgroup.
• IsFinitelyPresented: defines when a group is finitely presented.

Main results

• Subgroup.IsNormalClosureFG_map: Being the normal closure of a finite set is preserved under surjective homomorphism.
• IsFinitelyPresented.equiv: finitely presented groups are closed under isomorphism.

Tags

finitely presented group, finitely generated normal closure

def Subgroup.IsNormalClosureFG {G : Type u_1} [Group G] (N : Subgroup G) : Prop

IsNormalClosureFG N says that the subgroup N is the normal closure of a finitely-generated subgroup.

Equations

• N.IsNormalClosureFG = ∃ (S : Set G), S.Finite ∧ Subgroup.normalClosure S = N

theorem Subgroup.IsNormalClosureFG.map {G : Type u_1} {H : Type u_2} [Group G] [Group H] {N : Subgroup G} (hN : N.IsNormalClosureFG) {f : G →* H} (hf : Function.Surjective ⇑f) : (map f N).IsNormalClosureFG

Being the normal closure of a finite set is invariant under surjective homomorphism.

class Group.IsFinitelyPresented (G : Type u_5) [Group G] : Prop

A group is finitely presented if it has a finite generating set such that the kernel of the induced map from the free group on that set is the normal closure of finitely many relations.

• out : ∃ (n : ℕ) (φ : FreeGroup (Fin n) →* G), Function.Surjective ⇑φ ∧ φ.ker.IsNormalClosureFG

theorem Group.isFinitelyPresented_iff (G : Type u_5) [Group G] : IsFinitelyPresented G ↔ ∃ (n : ℕ) (φ : FreeGroup (Fin n) →* G), Function.Surjective ⇑φ ∧ φ.ker.IsNormalClosureFG

theorem Group.IsFinitelyPresented.equiv {G : Type u_1} {H : Type u_2} [Group G] [Group H] (iso : G ≃* H) (h : IsFinitelyPresented G) : IsFinitelyPresented H

Finitely presented groups are closed under isomorphism.