Defining a group given by generators and relations

Given a subset rels of relations of the free group on a type α, this file constructs the group given by generators x : α and relations r ∈ rels.

Main definitions

• PresentedGroup rels: the quotient group of the free group on a type α by a subset rels of relations of the free group on α.
• of: The canonical map from α to a presented group with generators α.
• toGroup f: the canonical group homomorphism PresentedGroup rels → G, given a function f : α → G from a type α to a group G which satisfies the relations rels.

Tags

generators, relations, group presentations

def PresentedGroup {α : Type u_1} (rels : Set (FreeGroup α)) : Type u_1

Given a set of relations, rels, over a type α, PresentedGroup constructs the group with generators x : α and relations rels as a quotient of FreeGroup α.

Equations

• PresentedGroup rels = (FreeGroup α ⧸ Subgroup.normalClosure rels)

def PresentedAddGroup {α : Type u_1} (rels : Set (FreeAddGroup α)) : Type u_1

Given a set of relations, rels, over a type α, PresentedAddGroup constructs the additive group with generators x : α and relations rels as a quotient of FreeAddGroup α.

Equations

• PresentedAddGroup rels = (FreeAddGroup α ⧸ AddSubgroup.normalClosure rels)

@[instance_reducible]

instance instGroupPresentedGroup {α : Type u_1} (rels : Set (FreeGroup α)) : Group (PresentedGroup rels)

Equations

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

@[instance_reducible]

instance instAddGroupPresentedAddGroup {α : Type u_1} (rels : Set (FreeAddGroup α)) : AddGroup (PresentedAddGroup rels)

Equations

• instAddGroupPresentedAddGroup rels = QuotientAddGroup.Quotient.addGroup (AddSubgroup.normalClosure rels)

def PresentedGroup.mk {α : Type u_1} (rels : Set (FreeGroup α)) : FreeGroup α →* PresentedGroup rels

The canonical map from the free group on α to a presented group with generators x : α, where x is mapped to its equivalence class under the given set of relations rels

Equations

• PresentedGroup.mk rels = { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯ }

def PresentedAddGroup.mk {α : Type u_1} (rels : Set (FreeAddGroup α)) : FreeAddGroup α →+ PresentedAddGroup rels

The canonical map from the free additive group on α to a presented additive group with generators x : α, where x is mapped to its equivalence class under the given set of relations rels

Equations

• PresentedAddGroup.mk rels = { toFun := QuotientAddGroup.mk, map_zero' := ⋯, map_add' := ⋯ }

theorem PresentedGroup.mk_surjective {α : Type u_1} (rels : Set (FreeGroup α)) : Function.Surjective ⇑(mk rels)

theorem PresentedAddGroup.mk_surjective {α : Type u_1} (rels : Set (FreeAddGroup α)) : Function.Surjective ⇑(mk rels)

def PresentedGroup.of {α : Type u_1} {rels : Set (FreeGroup α)} (x : α) : PresentedGroup rels

of is the canonical map from α to a presented group with generators x : α. The term x is mapped to the equivalence class of the image of x in FreeGroup α.

Equations

• PresentedGroup.of x = (PresentedGroup.mk rels) (FreeGroup.of x)

def PresentedAddGroup.of {α : Type u_1} {rels : Set (FreeAddGroup α)} (x : α) : PresentedAddGroup rels

of is the canonical map from α to a presented additive group with generators x : α. The term x is mapped to the equivalence class of the image of x in FreeGroup α.

Equations

• PresentedAddGroup.of x = (PresentedAddGroup.mk rels) (FreeAddGroup.of x)

def PresentedGroup.map {α : Type u_1} {β : Type u_2} (f : FreeGroup α →* FreeGroup β) {s : Set (FreeGroup α)} {t : Set (FreeGroup β)} (hst : Set.MapsTo (⇑f) s t) : PresentedGroup s →* PresentedGroup t

FreeGroup α →* FreeGroup β induces a homomorphism PresentedGroup s →* PresentedGroup t if the image of s is contained in t.

Equations

• PresentedGroup.map f hst = QuotientGroup.map (Subgroup.normalClosure s) (Subgroup.normalClosure t) f ⋯

def PresentedAddGroup.map {α : Type u_1} {β : Type u_2} (f : FreeAddGroup α →+ FreeAddGroup β) {s : Set (FreeAddGroup α)} {t : Set (FreeAddGroup β)} (hst : Set.MapsTo (⇑f) s t) : PresentedAddGroup s →+ PresentedAddGroup t

FreeAddGroup α →* FreeAddGroup β induces a homomorphism PresentedAddGroup s →* PresentedAddGroup t if the image of s is contained in t.

Equations

• PresentedAddGroup.map f hst = QuotientAddGroup.map (AddSubgroup.normalClosure s) (AddSubgroup.normalClosure t) f ⋯

theorem PresentedGroup.mk_eq_one_iff {α : Type u_1} {rels : Set (FreeGroup α)} {x : FreeGroup α} : (mk rels) x = 1 ↔ x ∈ Subgroup.normalClosure rels

theorem PresentedAddGroup.mk_eq_zero_iff {α : Type u_1} {rels : Set (FreeAddGroup α)} {x : FreeAddGroup α} : (mk rels) x = 0 ↔ x ∈ AddSubgroup.normalClosure rels

theorem PresentedGroup.one_of_mem {α : Type u_1} {rels : Set (FreeGroup α)} {x : FreeGroup α} (hx : x ∈ rels) : (mk rels) x = 1

theorem PresentedAddGroup.zero_of_mem {α : Type u_1} {rels : Set (FreeAddGroup α)} {x : FreeAddGroup α} (hx : x ∈ rels) : (mk rels) x = 0

theorem PresentedGroup.mk_eq_mk_of_mul_inv_mem {α : Type u_1} {rels : Set (FreeGroup α)} {x y : FreeGroup α} (hx : x * y⁻¹ ∈ rels) : (mk rels) x = (mk rels) y

theorem PresentedAddGroup.mk_eq_mk_of_add_neg_mem {α : Type u_1} {rels : Set (FreeAddGroup α)} {x y : FreeAddGroup α} (hx : x + -y ∈ rels) : (mk rels) x = (mk rels) y

theorem PresentedGroup.mk_eq_mk_of_inv_mul_mem {α : Type u_1} {rels : Set (FreeGroup α)} {x y : FreeGroup α} (hx : x⁻¹ * y ∈ rels) : (mk rels) x = (mk rels) y

theorem PresentedAddGroup.mk_eq_mk_of_neg_add_mem {α : Type u_1} {rels : Set (FreeAddGroup α)} {x y : FreeAddGroup α} (hx : -x + y ∈ rels) : (mk rels) x = (mk rels) y

@[simp]

theorem PresentedGroup.closure_range_of {α : Type u_1} (rels : Set (FreeGroup α)) : Subgroup.closure (Set.range of) = ⊤

The generators of a presented group generate the presented group. That is, the subgroup closure of the set of generators equals ⊤.

@[simp]

theorem PresentedAddGroup.closure_range_of {α : Type u_1} (rels : Set (FreeAddGroup α)) : AddSubgroup.closure (Set.range of) = ⊤

The generators of a presented additive group generate the presented group. That is, the subgroup closure of the set of generators equals ⊤.

theorem PresentedGroup.induction_on {α : Type u_1} {rels : Set (FreeGroup α)} {C : PresentedGroup rels → Prop} (x : PresentedGroup rels) (H : ∀ (z : FreeGroup α), C ((mk rels) z)) : C x

theorem PresentedAddGroup.induction_on {α : Type u_1} {rels : Set (FreeAddGroup α)} {C : PresentedAddGroup rels → Prop} (x : PresentedAddGroup rels) (H : ∀ (z : FreeAddGroup α), C ((mk rels) z)) : C x

theorem PresentedGroup.generated_by {α : Type u_1} (rels : Set (FreeGroup α)) (H : Subgroup (PresentedGroup rels)) (h : ∀ (j : α), of j ∈ H) (x : PresentedGroup rels) : x ∈ H

theorem PresentedAddGroup.generated_by {α : Type u_1} (rels : Set (FreeAddGroup α)) (H : AddSubgroup (PresentedAddGroup rels)) (h : ∀ (j : α), of j ∈ H) (x : PresentedAddGroup rels) : x ∈ H

theorem PresentedGroup.closure_rels_subset_ker {α : Type u_1} {G : Type u_3} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) : Subgroup.normalClosure rels ≤ (FreeGroup.lift f).ker

theorem PresentedAddGroup.closure_rels_subset_ker {α : Type u_1} {G : Type u_3} [AddGroup G] {f : α → G} {rels : Set (FreeAddGroup α)} (h : ∀ r ∈ rels, (FreeAddGroup.lift f) r = 0) : AddSubgroup.normalClosure rels ≤ (FreeAddGroup.lift f).ker

theorem PresentedGroup.to_group_eq_one_of_mem_closure {α : Type u_1} {G : Type u_3} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) (x : FreeGroup α) : x ∈ Subgroup.normalClosure rels → (FreeGroup.lift f) x = 1

theorem PresentedAddGroup.to_addGroup_eq_zero_of_mem_closure {α : Type u_1} {G : Type u_3} [AddGroup G] {f : α → G} {rels : Set (FreeAddGroup α)} (h : ∀ r ∈ rels, (FreeAddGroup.lift f) r = 0) (x : FreeAddGroup α) : x ∈ AddSubgroup.normalClosure rels → (FreeAddGroup.lift f) x = 0

def PresentedGroup.toGroup {α : Type u_1} {G : Type u_3} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) : PresentedGroup rels →* G

The extension of a map f : α → G that satisfies the given relations to a group homomorphism from PresentedGroup rels → G.

Equations

• PresentedGroup.toGroup h = QuotientGroup.lift (Subgroup.normalClosure rels) (FreeGroup.lift f) ⋯

def PresentedAddGroup.toAddGroup {α : Type u_1} {G : Type u_3} [AddGroup G] {f : α → G} {rels : Set (FreeAddGroup α)} (h : ∀ r ∈ rels, (FreeAddGroup.lift f) r = 0) : PresentedAddGroup rels →+ G

The extension of a map f : α → G that satisfies the given relations to an additive group homomorphism from PresentedGroup rels → G.

Equations

• PresentedAddGroup.toAddGroup h = QuotientAddGroup.lift (AddSubgroup.normalClosure rels) (FreeAddGroup.lift f) ⋯

@[simp]

theorem PresentedGroup.toGroup.of {α : Type u_1} {G : Type u_3} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) {x : α} : (toGroup h) (PresentedGroup.of x) = f x

@[simp]

theorem PresentedAddGroup.toAddGroup.of {α : Type u_1} {G : Type u_3} [AddGroup G] {f : α → G} {rels : Set (FreeAddGroup α)} (h : ∀ r ∈ rels, (FreeAddGroup.lift f) r = 0) {x : α} : (toAddGroup h) (PresentedAddGroup.of x) = f x

theorem PresentedGroup.toGroup.unique {α : Type u_1} {G : Type u_3} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) (g : PresentedGroup rels →* G) (hg : ∀ (x : α), g (PresentedGroup.of x) = f x) {x : PresentedGroup rels} : g x = (toGroup h) x

theorem PresentedAddGroup.toAddGroup.unique {α : Type u_1} {G : Type u_3} [AddGroup G] {f : α → G} {rels : Set (FreeAddGroup α)} (h : ∀ r ∈ rels, (FreeAddGroup.lift f) r = 0) (g : PresentedAddGroup rels →+ G) (hg : ∀ (x : α), g (PresentedAddGroup.of x) = f x) {x : PresentedAddGroup rels} : g x = (toAddGroup h) x

theorem PresentedGroup.ext {α : Type u_1} {G : Type u_3} [Group G] {rels : Set (FreeGroup α)} {φ ψ : PresentedGroup rels →* G} (hx : ∀ (x : α), φ (of x) = ψ (of x)) : φ = ψ

theorem PresentedAddGroup.ext {α : Type u_1} {G : Type u_3} [AddGroup G] {rels : Set (FreeAddGroup α)} {φ ψ : PresentedAddGroup rels →+ G} (hx : ∀ (x : α), φ (of x) = ψ (of x)) : φ = ψ

theorem PresentedGroup.ext_iff {α : Type u_1} {G : Type u_3} [Group G] {rels : Set (FreeGroup α)} {φ ψ : PresentedGroup rels →* G} : φ = ψ ↔ ∀ (x : α), φ (of x) = ψ (of x)

theorem PresentedAddGroup.ext_iff {α : Type u_1} {G : Type u_3} [AddGroup G] {rels : Set (FreeAddGroup α)} {φ ψ : PresentedAddGroup rels →+ G} : φ = ψ ↔ ∀ (x : α), φ (of x) = ψ (of x)

def PresentedGroup.equivPresentedGroup {α : Type u_1} {β : Type u_2} (rels : Set (FreeGroup α)) (e : α ≃ β) : PresentedGroup rels ≃* PresentedGroup (⇑(FreeGroup.freeGroupCongr e) '' rels)

Presented groups of isomorphic types are isomorphic.

Equations

• PresentedGroup.equivPresentedGroup rels e = QuotientGroup.congr (Subgroup.normalClosure rels) (Subgroup.normalClosure (⇑(FreeGroup.freeGroupCongr e) '' rels)) (FreeGroup.freeGroupCongr e) ⋯

def PresentedAddGroup.equivPresentedAddGroup {α : Type u_1} {β : Type u_2} (rels : Set (FreeAddGroup α)) (e : α ≃ β) : PresentedAddGroup rels ≃+ PresentedAddGroup (⇑(FreeAddGroup.freeAddGroupCongr e) '' rels)

Presented additive groups of isomorphic types are isomorphic.

Equations

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

theorem PresentedGroup.equivPresentedGroup_apply_of {α : Type u_1} {β : Type u_2} (x : α) (rels : Set (FreeGroup α)) (e : α ≃ β) : (equivPresentedGroup rels e) (of x) = of (e x)

theorem PresentedAddGroup.equivPresentedAddGroup_apply_of {α : Type u_1} {β : Type u_2} (x : α) (rels : Set (FreeAddGroup α)) (e : α ≃ β) : (equivPresentedAddGroup rels e) (of x) = of (e x)

theorem PresentedGroup.equivPresentedGroup_symm_apply_of {α : Type u_1} {β : Type u_2} (x : β) (rels : Set (FreeGroup α)) (e : α ≃ β) : (equivPresentedGroup rels e).symm (of x) = of (e.symm x)

theorem PresentedAddGroup.equivPresentedAddGroup_symm_apply_of {α : Type u_1} {β : Type u_2} (x : β) (rels : Set (FreeAddGroup α)) (e : α ≃ β) : (equivPresentedAddGroup rels e).symm (of x) = of (e.symm x)

@[instance_reducible]

instance PresentedGroup.instInhabited {α : Type u_1} (rels : Set (FreeGroup α)) : Inhabited (PresentedGroup rels)

Equations

• PresentedGroup.instInhabited rels = { default := 1 }

@[instance_reducible]

instance PresentedAddGroup.instInhabited {α : Type u_1} (rels : Set (FreeAddGroup α)) : Inhabited (PresentedAddGroup rels)

Equations

• PresentedAddGroup.instInhabited rels = { default := 0 }

def PresentedGroup.toCoprod {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)) : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)

The canonical inclusion map from the disjoint union of types to the free product of the relations

Equations

• PresentedGroup.toCoprod rels₁ rels₂ = Sum.elim (⇑Monoid.Coprod.inl ∘ PresentedGroup.of) (⇑Monoid.Coprod.inr ∘ PresentedGroup.of)

def PresentedAddGroup.toCoprod {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeAddGroup α)) (rels₂ : Set (FreeAddGroup β)) : α ⊕ β → AddMonoid.Coprod (PresentedAddGroup rels₁) (PresentedAddGroup rels₂)

The canonical inclusion map from the disjoint union of types to the free product of the relations

Equations

• PresentedAddGroup.toCoprod rels₁ rels₂ = Sum.elim (⇑AddMonoid.Coprod.inl ∘ PresentedAddGroup.of) (⇑AddMonoid.Coprod.inr ∘ PresentedAddGroup.of)

@[simp]

theorem PresentedGroup.lift_toCoprod_inl_eq_inl_mk {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)) : (FreeGroup.lift (toCoprod rels₁ rels₂)).comp (FreeGroup.map Sum.inl) = Monoid.Coprod.inl.comp (mk rels₁)

@[simp]

theorem PresentedAddGroup.lift_toCoprod_inl_eq_inl_mk {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeAddGroup α)) (rels₂ : Set (FreeAddGroup β)) : (FreeAddGroup.lift (toCoprod rels₁ rels₂)).comp (FreeAddGroup.map Sum.inl) = AddMonoid.Coprod.inl.comp (mk rels₁)

@[simp]

theorem PresentedGroup.lift_toCoprod_inr_eq_inr_mk {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)) : (FreeGroup.lift (toCoprod rels₁ rels₂)).comp (FreeGroup.map Sum.inr) = Monoid.Coprod.inr.comp (mk rels₂)

@[simp]

theorem PresentedAddGroup.lift_toCoprod_inr_eq_inr_mk {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeAddGroup α)) (rels₂ : Set (FreeAddGroup β)) : (FreeAddGroup.lift (toCoprod rels₁ rels₂)).comp (FreeAddGroup.map Sum.inr) = AddMonoid.Coprod.inr.comp (mk rels₂)

theorem PresentedGroup.lift_toCoprod_eq_one {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)) (r : FreeGroup (α ⊕ β)) (hr : r ∈ ⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂) : (FreeGroup.lift (toCoprod rels₁ rels₂)) r = 1

theorem PresentedAddGroup.lift_toCoprod_eq_zero {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeAddGroup α)) (rels₂ : Set (FreeAddGroup β)) (r : FreeAddGroup (α ⊕ β)) (hr : r ∈ ⇑(FreeAddGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeAddGroup.map Sum.inr) '' rels₂) : (FreeAddGroup.lift (toCoprod rels₁ rels₂)) r = 0

def PresentedGroup.coprodPresentations {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)) : PresentedGroup (⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂) ≃* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)

The free product (Coproduct) of presentations is isomorphic to the presentation of the union over the FreeGroup (α ⊕ β)

Equations

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

def PresentedAddGroup.coprodPresentations {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeAddGroup α)) (rels₂ : Set (FreeAddGroup β)) : PresentedAddGroup (⇑(FreeAddGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeAddGroup.map Sum.inr) '' rels₂) ≃+ AddMonoid.Coprod (PresentedAddGroup rels₁) (PresentedAddGroup rels₂)

The free product (Coproduct) of presentations is isomorphic to the presentation of the union over the FreeAddGroup (α ⊕ β)

Equations

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