Given a set of relations, rels, over a type α, presented_group constructs the group with generators α and relations rels as a quotient of free_group α.
Equations
@[instance]
Equations
of x is the canonical map from α to a presented group with generators α. The term x is
mapped to the equivalence class of the image of x in free_group α.
Equations
theorem
presented_group.closure_rels_subset_ker
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)} :
(∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1) → subgroup.normal_closure rels ≤ (free_group.to_group f).ker
theorem
presented_group.to_group_eq_one_of_mem_closure
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)}
(h : ∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1)
(x : free_group α) :
x ∈ subgroup.normal_closure rels → ⇑(free_group.to_group f) x = 1
def
presented_group.to_group
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)} :
(∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1) → presented_group rels →* β
The extension of a map f : α → β that satisfies the given relations to a group homomorphism from presented_group rels → β.
Equations
@[simp]
theorem
presented_group.to_group.of
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)}
(h : ∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1)
{x : α} :
⇑(presented_group.to_group h) (presented_group.of x) = f x
@[simp]
theorem
presented_group.to_group.mul
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)}
(h : ∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1)
{x y : presented_group rels} :
⇑(presented_group.to_group h) (x * y) = ⇑(presented_group.to_group h) x * ⇑(presented_group.to_group h) y
@[simp]
theorem
presented_group.to_group.one
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)}
(h : ∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1) :
⇑(presented_group.to_group h) 1 = 1
@[simp]
theorem
presented_group.to_group.inv
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)}
(h : ∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1)
{x : presented_group rels} :
⇑(presented_group.to_group h) x⁻¹ = (⇑(presented_group.to_group h) x)⁻¹
theorem
presented_group.to_group.unique
{α β : Type}
[group β]
{f : α → β}
{rels : set (free_group α)}
(h : ∀ (r : free_group α), r ∈ rels → ⇑(free_group.to_group f) r = 1)
(g : presented_group rels →* β)
(hg : ∀ (x : α), ⇑g (presented_group.of x) = f x)
{x : presented_group rels} :
⇑g x = ⇑(presented_group.to_group h) x