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

def AddSubgroup.IsNormalClosureFG {G : Type u_1} [AddGroup G] (N : AddSubgroup G) : Prop

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

Equations

• N.IsNormalClosureFG = ∃ (S : Set G), S.Finite ∧ AddSubgroup.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.

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

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

theorem Subgroup.IsNormalClosureFG.bot {G : Type u_1} [Group G] : ⊥.IsNormalClosureFG

The trivial group is the normal closure of a finite set of relations.

theorem AddSubgroup.IsNormalClosureFG.bot {G : Type u_1} [AddGroup G] : ⊥.IsNormalClosureFG

The trivial additive group is the normal closure of a finite set of relations.

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

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

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

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.

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

Finitely presented additive groups are closed under additive isomorphism.

instance Group.IsFinitelyPresented.instFreeGroupOfFinite {α : Type u_3} [Finite α] : IsFinitelyPresented (FreeGroup α)

A free group with a finite number of generators is finitely presented.

instance AddGroup.IsFinitelyPresented.instFreeAddGroupOfFinite {α : Type u_3} [Finite α] : IsFinitelyPresented (FreeAddGroup α)

A free additive group with a finite number of generators is finitely presented.

instance Group.IsFinitelyPresented.instMultiplicativeInt : IsFinitelyPresented (Multiplicative ℤ)

Multiplicative ℤ is finitely presented.

instance Group.IsFinitelyPresented.instIsFinitelyPresentedInt : AddGroup.IsFinitelyPresented ℤ

ℤ is finitely presented