Finitely Presented Groups

This file defines finitely presented groups.

Main definitions

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

Main results

• Subgroup.IsFinitelyNormallyGenerated.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.IsFinitelyNormallyGenerated {G : Type u_1} [Group G] (N : Subgroup G) : Prop

N.IsFinitelyNormallyGenerated says that the subgroup N is the normal closure of a finite set.

Equations

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

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

N.IsFinitelyNormallyGenerated says that the additive subgroup N is the normal closure of a finite set.

Equations

• N.IsFinitelyNormallyGenerated = ∃ (S : Set G), S.Finite ∧ AddSubgroup.normalClosure S = N

@[deprecated Subgroup.IsFinitelyNormallyGenerated (since := "2026-06-25")]

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

Alias of Subgroup.IsFinitelyNormallyGenerated.

---

N.IsFinitelyNormallyGenerated says that the subgroup N is the normal closure of a finite set.

Equations

• @Subgroup.IsNormalClosureFG = @Subgroup.IsFinitelyNormallyGenerated

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

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

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

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

theorem Subgroup.IsFinitelyNormallyGenerated.of_FG {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [h : Group.FG ↥N] : N.IsFinitelyNormallyGenerated

theorem AddSubgroup.IsFinitelyNormallyGenerated.of_FG {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [N.Normal] [h : AddGroup.FG ↥N] : N.IsFinitelyNormallyGenerated

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

The preimage of a finitely generated normal subgroup by a surjective homomorphism with a finitely generated kernel is finitely generated.

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

The preimage of a finitely generated normal subgroup by a surjective additive homomorphism with a finitely generated kernel is finitely generated.

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

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

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

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.IsFinitelyNormallyGenerated

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.IsFinitelyNormallyGenerated

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

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.

theorem Group.IsFinitelyPresented.of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] [hG : IsFinitelyPresented G] (f : G →* H) (hf_surj : Function.Surjective ⇑f) (hf_ker : f.ker.IsFinitelyNormallyGenerated) : IsFinitelyPresented H

The image of a finitely presented group under a surjective homomorphism whose kernel is finitely generated as a normal subgroup is finitely presented.

theorem AddGroup.IsFinitelyPresented.of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [hG : IsFinitelyPresented G] (f : G →+ H) (hf_surj : Function.Surjective ⇑f) (hf_ker : f.ker.IsFinitelyNormallyGenerated) : IsFinitelyPresented H

The image of a finitely presented additive group under a surjective additive homomorphism whose kernel is finitely generated as a normal subgroup is finitely presented.

theorem Group.IsFinitelyPresented.quotient {G : Type u_1} [Group G] [hG : IsFinitelyPresented G] (N : Subgroup G) [N.Normal] (hN : N.IsFinitelyNormallyGenerated) : IsFinitelyPresented (G ⧸ N)

The quotient of a finitely presented group by a subgroup which is finitely generated as a normal subgroup is finitely presented.

theorem AddGroup.IsFinitelyPresented.quotient {G : Type u_1} [AddGroup G] [hG : IsFinitelyPresented G] (N : AddSubgroup G) [N.Normal] (hN : N.IsFinitelyNormallyGenerated) : IsFinitelyPresented (G ⧸ N)

The quotient of a finitely presented additive group by an additive subgroup which is finitely generated as a normal subgroup is finitely presented.

theorem Group.IsFinitelyPresented.exists_mulEquiv_presentedGroup {G : Type u_1} [Group G] [hg : IsFinitelyPresented G] : ∃ (n : ℕ) (s : Set (FreeGroup (Fin n))), s.Finite ∧ Nonempty (G ≃* PresentedGroup s)

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.instPresentedGroupOfFiniteElemFreeGroup {α : Type u_3} [Finite α] (s : Set (FreeGroup α)) [Finite ↑s] : IsFinitelyPresented (PresentedGroup s)

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

Multiplicative ℤ is finitely presented.

instance Group.IsFinitelyPresented.instIsFinitelyPresentedInt : AddGroup.IsFinitelyPresented ℤ

ℤ is finitely presented

instance Group.IsFinitelyPresented.instCoprod {G : Type u_1} {H : Type u_2} [Group G] [Group H] [IsFinitelyPresented G] [IsFinitelyPresented H] : IsFinitelyPresented (Monoid.Coprod G H)

The free product of finitely presented groups is finitely presented

instance Group.IsFinitelyPresented.instOfFinite (G : Type u_1) [Group G] [Finite G] : IsFinitelyPresented G

Any finite group is finitely presented.

instance AddGroup.IsFinitelyPresented.instOfFinite (G : Type u_1) [AddGroup G] [Finite G] : IsFinitelyPresented G