Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations
ProCGroups/ReidemeisterSchreier/Discrete/Presentations/Relators/Operations

ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations

28 Theorems | 1 Definition

This module proves invariance and closure lemmas for changing relator sets, conjugating and cyclically rotating words, products of lists, and ordered finite products.

imports
Imported by

Declarations

Theorem ReidemeisterSchreier.Discrete.Presentations.normalClosure_eq_of_relatorEquivalent 
theorem normalClosure_eq_of_relatorEquivalent
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    Subgroup.normalClosure R = Subgroup.normalClosure S

If every relator on each side is trivial modulo the other side, the normal closures are equal.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.normalClosure_insert_eq_of_mem 
theorem normalClosure_insert_eq_of_mem
    (hr : r ∈ Subgroup.normalClosure R) :
    Subgroup.normalClosure (insert r R) = Subgroup.normalClosure R

Inserting an element already in the normal closure does not change the normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.normalClosure_diff_singleton_eq_of_mem 
theorem normalClosure_diff_singleton_eq_of_mem
    (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
    Subgroup.normalClosure R = Subgroup.normalClosure (R \ {r})

Removing a relator that already lies in the normal closure of the remaining relators does not change the normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.normalClosure_eq_of_subset_normalClosure 
theorem normalClosure_eq_of_subset_normalClosure
    (hR_to_S : R ⊆ Subgroup.normalClosure S)
    (hS_to_R : S ⊆ Subgroup.normalClosure R) :
    Subgroup.normalClosure R = Subgroup.normalClosure S

Two relator normal closures are equal when each relator family is contained in the normal closure generated by the other.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.conjugate_mem_normalClosure_of_mem 
theorem conjugate_mem_normalClosure_of_mem
    (hr : r ∈ R) (a : G) :
    a * r * a⁻¹ ∈ Subgroup.normalClosure R

Every conjugate of a relator belongs to the normal closure of the relator set.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.conjugate_mem_normalClosure 
theorem conjugate_mem_normalClosure
    (hr : r ∈ Subgroup.normalClosure R) (a : G) :
    a * r * a⁻¹ ∈ Subgroup.normalClosure R

A conjugate of a relator belongs to the normal closure of the relator set.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure 
theorem cyclic_rotation_mem_normalClosure
    (h : a * b ∈ Subgroup.normalClosure R) :
    b * a ∈ Subgroup.normalClosure R

Cyclically rotating a relator keeps it in the same normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.mem_of_left_mul_mem_normalClosure 
theorem mem_of_left_mul_mem_normalClosure
    {a b : G}
    (ha : a ∈ Subgroup.normalClosure R)
    (hab : a * b ∈ Subgroup.normalClosure R) :
    b ∈ Subgroup.normalClosure R

If left multiplication by a relator-normal-closure element gives membership, then the original element has the same membership property.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_pow_mem_normalClosure 
theorem cyclic_rotation_pow_mem_normalClosure
    {a b : G} {n : ℕ}
    (h : (a * b) ^ n ∈ Subgroup.normalClosure R) :
    (b * a) ^ n ∈ Subgroup.normalClosure R

A cyclic rotation of a power relator belongs to the normal closure of the original relator set.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.pow_mem_normalClosure_of_mul_inv_mem 
theorem pow_mem_normalClosure_of_mul_inv_mem
    {u v : G} {n : ℕ}
    (huv : u * v⁻¹ ∈ Subgroup.normalClosure R)
    (hv : v ^ n ∈ Subgroup.normalClosure R) :
    u ^ n ∈ Subgroup.normalClosure R

If u and v are congruent modulo the normal closure and a power of v lies in it, then the same power of u lies in it.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_mem_normalClosure 
theorem list_prod_mem_normalClosure
    {l : List G}
    (h : ∀ x ∈ l, x ∈ Subgroup.normalClosure R) :
    l.prod ∈ Subgroup.normalClosure R

The product of a list of relators belongs to the normal closure of the relator set.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_map_relatorEquivalent 
theorem list_prod_map_relatorEquivalent
    {ι : Type*} (l : List ι) {f g : ι → G}
    (h : ∀ i ∈ l, RelatorEquivalent R (f i) (g i)) :
    RelatorEquivalent R (l.map f).prod (l.map g).prod

Mapping a list through relator-equivalent entries preserves relator equivalence of the product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_map_relatorEquivalent_one 
theorem list_prod_map_relatorEquivalent_one
    {ι : Type*} (l : List ι) {f : ι → G}
    (h : ∀ i ∈ l, RelatorEquivalent R (f i) 1) :
    RelatorEquivalent R (l.map f).prod 1

A list product is relator-equivalent to the identity when every mapped entry is relator-equivalent to the identity.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_map_inv_reverse 
theorem list_prod_map_inv_reverse (l : List G) :
    (l.map Inv.inv).reverse.prod = l.prod⁻¹

Mapping inversion over a list and then reversing it gives a product equal to the inverse product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_reverse_map_inv 
theorem list_prod_reverse_map_inv (l : List G) :
    (l.reverse.map Inv.inv).prod = l.prod⁻¹

Reversing a list and then inverting its entries gives a product equal to the inverse product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_reverse_inv_relatorEquivalent 
theorem list_prod_reverse_inv_relatorEquivalent
    {l m : List G}
    (h : RelatorEquivalent R l.prod m.prod) :
    RelatorEquivalent R (l.reverse.map Inv.inv).prod
      (m.reverse.map Inv.inv).prod

A list product is relator-equivalent to the inverse of the reversed inverse list product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_append_relatorEquivalent 
theorem list_prod_append_relatorEquivalent
    {l₁ l₂ m₁ m₂ : List G}
    (h₁ : RelatorEquivalent R l₁.prod m₁.prod)
    (h₂ : RelatorEquivalent R l₂.prod m₂.prod) :
    RelatorEquivalent R (l₁ ++ l₂).prod (m₁ ++ m₂).prod

Appending relator-equivalent list products preserves relator equivalence.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_append_left_relatorEquivalent 
theorem list_prod_append_left_relatorEquivalent
    (l : List G) {m n : List G}
    (h : RelatorEquivalent R m.prod n.prod) :
    RelatorEquivalent R (l ++ m).prod (l ++ n).prod

Left-appending the same list product preserves relator equivalence.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_middle_eq_one_relatorEquivalent 
theorem list_prod_middle_eq_one_relatorEquivalent
    (l m : List G) {u : G}
    (h : RelatorEquivalent R u 1) :
    RelatorEquivalent R (l ++ u :: m).prod (l ++ m).prod

Removing a middle subproduct equal to one preserves relator equivalence of the list product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_middle_mul_inv_relatorEquivalent 
theorem list_prod_middle_mul_inv_relatorEquivalent
    (l m : List G) {u v : G}
    (h : RelatorEquivalent R u v) :
    RelatorEquivalent R (l ++ (u * v⁻¹) :: m).prod
      (l ++ m).prod

Inserting or removing a middle product multiplied by its inverse preserves relator equivalence.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_append_rotate_mem_normalClosure 
theorem list_prod_append_rotate_mem_normalClosure
    {l m : List G}
    (h : (l ++ m).prod ∈ Subgroup.normalClosure R) :
    (m ++ l).prod ∈ Subgroup.normalClosure R

Rotating an appended list product gives an element of the relator normal closure.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_append_rotate_relatorEquivalent 
theorem list_prod_append_rotate_relatorEquivalent
    {l m : List G}
    (h : RelatorEquivalent R (l ++ m).prod 1) :
    RelatorEquivalent R (m ++ l).prod 1

A rotated append decomposition of a list product is relator-equivalent to the original product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_take_drop_rotate_relatorEquivalent 
theorem list_prod_take_drop_rotate_relatorEquivalent
    (l : List G) (n : ℕ)
    (h : RelatorEquivalent R l.prod 1) :
    RelatorEquivalent R ((l.drop n) ++ (l.take n)).prod 1

The take/drop rotation of a list product is relator-equivalent to the original product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.list_prod_take_drop_rotate_mem_normalClosure 
theorem list_prod_take_drop_rotate_mem_normalClosure
    (l : List G) (n : ℕ)
    (h : l.prod ∈ Subgroup.normalClosure R) :
    ((l.drop n) ++ (l.take n)).prod ∈ Subgroup.normalClosure R

A take-drop rotation of a list product belongs to the relator normal closure.

Show Lean proof
Definition ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct 
def orderedFinsetProduct (s : Finset ι) (f : ι → G) : G :=
  ((s.sort (· ≤ ·)).map f).prod

A noncommutative product indexed by a finite set, with multiplication ordered by the ambient \(LinearOrder\).

Theorem ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_mem_normalClosure 
theorem orderedFinsetProduct_mem_normalClosure
    (s : Finset ι) {f : ι → G}
    (h : ∀ i ∈ s, f i ∈ Subgroup.normalClosure R) :
    orderedFinsetProduct s f ∈ Subgroup.normalClosure R

An ordered finite product of relators belongs to the normal closure of the relator set.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_relatorEquivalent 
theorem orderedFinsetProduct_relatorEquivalent
    (s : Finset ι) {f g : ι → G}
    (h : ∀ i ∈ s, RelatorEquivalent R (f i) (g i)) :
    RelatorEquivalent R (orderedFinsetProduct s f)
      (orderedFinsetProduct s g)

Replacing each term of an ordered finite product by a relator-equivalent term preserves relator equivalence.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_relatorEquivalent_one 
theorem orderedFinsetProduct_relatorEquivalent_one
    (s : Finset ι) {f : ι → G}
    (h : ∀ i ∈ s, RelatorEquivalent R (f i) 1) :
    RelatorEquivalent R (orderedFinsetProduct s f) 1

An ordered finite product is relator-equivalent to the identity when every term is relator-equivalent to the identity.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_congr 
theorem orderedFinsetProduct_congr
    (s : Finset ι) {f g : ι → G}
    (h : ∀ i ∈ s, f i = g i) :
    orderedFinsetProduct s f = orderedFinsetProduct s g

Pointwise equality on a finite index set gives equality of the corresponding ordered products.

Show Lean proof