Module

Operations.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations

29 declarations indexed from sourceView source ↗

Module documentation

Operations on relator normal closures

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

Imports2

Mathlib.Tactic.Group
Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic

Imported by4

theorem

normalClosure_eq_of_relatorEquivalent

L29 ↗

ReidemeisterSchreier.Discrete.Presentations.normalClosure_eq_of_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

normalClosure_insert_eq_of_mem

L42 ↗

ReidemeisterSchreier.Discrete.Presentations.normalClosure_insert_eq_of_mem

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem normalClosure_insert_eq_of_mem
    (hr : r ∈ Subgroup.normalClosure R) :
    Subgroup.normalClosure (insert r R) = Subgroup.normalClosure R

theorem

normalClosure_diff_singleton_eq_of_mem

L59 ↗

ReidemeisterSchreier.Discrete.Presentations.normalClosure_diff_singleton_eq_of_mem

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem normalClosure_diff_singleton_eq_of_mem
    (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
    Subgroup.normalClosure R = Subgroup.normalClosure (R \ {r})

theorem

normalClosure_eq_of_subset_normalClosure

L76 ↗

ReidemeisterSchreier.Discrete.Presentations.normalClosure_eq_of_subset_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

conjugate_mem_normalClosure_of_mem

L85 ↗

ReidemeisterSchreier.Discrete.Presentations.conjugate_mem_normalClosure_of_mem

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem conjugate_mem_normalClosure_of_mem
    (hr : r ∈ R) (a : G) :
    a * r * a⁻¹ ∈ Subgroup.normalClosure R

theorem

conjugate_mem_normalClosure

L93 ↗

ReidemeisterSchreier.Discrete.Presentations.conjugate_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem conjugate_mem_normalClosure
    (hr : r ∈ Subgroup.normalClosure R) (a : G) :
    a * r * a⁻¹ ∈ Subgroup.normalClosure R

theorem

cyclic_rotation_mem_normalClosure

L100 ↗

ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem cyclic_rotation_mem_normalClosure
    (h : a * b ∈ Subgroup.normalClosure R) :
    b * a ∈ Subgroup.normalClosure R

theorem

mem_of_left_mul_mem_normalClosure

L110 ↗

ReidemeisterSchreier.Discrete.Presentations.mem_of_left_mul_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

cyclic_rotation_pow_mem_normalClosure

L122 ↗

ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_pow_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem cyclic_rotation_pow_mem_normalClosure
    {a b : G} {n : ℕ}
    (h : (a * b) ^ n ∈ Subgroup.normalClosure R) :
    (b * a) ^ n ∈ Subgroup.normalClosure R

theorem

pow_mem_normalClosure_of_mul_inv_mem

L144 ↗

ReidemeisterSchreier.Discrete.Presentations.pow_mem_normalClosure_of_mul_inv_mem

Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_mem_normalClosure

L163 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem list_prod_mem_normalClosure
    {l : List G}
    (h : ∀ x ∈ l, x ∈ Subgroup.normalClosure R) :
    l.prod ∈ Subgroup.normalClosure R

theorem

list_prod_map_relatorEquivalent

L181 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_map_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_map_relatorEquivalent_one

L200 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_map_relatorEquivalent_one

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_map_inv_reverse

L210 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_map_inv_reverse

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem list_prod_map_inv_reverse (l : List G) :
    (l.map Inv.inv).reverse.prod = l.prod⁻¹

theorem

list_prod_reverse_map_inv

L221 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_reverse_map_inv

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem list_prod_reverse_map_inv (l : List G) :
    (l.reverse.map Inv.inv).prod = l.prod⁻¹

theorem

list_prod_reverse_inv_relatorEquivalent

L226 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_reverse_inv_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_append_relatorEquivalent

L235 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_append_relatorEquivalent

Documentation

Appending relator-equivalent list products preserves relator equivalence.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_append_left_relatorEquivalent

L243 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_append_left_relatorEquivalent

Documentation

Left-appending the same list product preserves relator equivalence.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_middle_eq_one_relatorEquivalent

L252 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_middle_eq_one_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_middle_mul_inv_relatorEquivalent

L265 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_middle_mul_inv_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_append_rotate_mem_normalClosure

L274 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_append_rotate_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem list_prod_append_rotate_mem_normalClosure
    {l m : List G}
    (h : (l ++ m).prod ∈ Subgroup.normalClosure R) :
    (m ++ l).prod ∈ Subgroup.normalClosure R

theorem

list_prod_append_rotate_relatorEquivalent

L289 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_append_rotate_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

theorem list_prod_append_rotate_relatorEquivalent
    {l m : List G}
    (h : RelatorEquivalent R (l ++ m).prod 1) :
    RelatorEquivalent R (m ++ l).prod 1

theorem

list_prod_take_drop_rotate_relatorEquivalent

L298 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_take_drop_rotate_relatorEquivalent

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

theorem

list_prod_take_drop_rotate_mem_normalClosure

L308 ↗

ReidemeisterSchreier.Discrete.Presentations.list_prod_take_drop_rotate_mem_normalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}

Lean source · statement

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

def

orderedFinsetProduct

L324 ↗

ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}
section OrderedFinsetProduct
variable {ι : Type*} [LinearOrder ι]

Lean source · statement

def orderedFinsetProduct (s : Finset ι) (f : ι → G) : G

theorem

orderedFinsetProduct_mem_normalClosure

L328 ↗

ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_mem_normalClosure

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}
section OrderedFinsetProduct
variable {ι : Type*} [LinearOrder ι]

Lean source · statement

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

theorem

orderedFinsetProduct_relatorEquivalent

L343 ↗

ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_relatorEquivalent

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}
section OrderedFinsetProduct
variable {ι : Type*} [LinearOrder ι]

Lean source · statement

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)

theorem

orderedFinsetProduct_relatorEquivalent_one

L359 ↗

ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_relatorEquivalent_one

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}
section OrderedFinsetProduct
variable {ι : Type*} [LinearOrder ι]

Lean source · statement

theorem orderedFinsetProduct_relatorEquivalent_one
    (s : Finset ι) {f : ι → G}
    (h : ∀ i ∈ s, RelatorEquivalent R (f i) 1) :
    RelatorEquivalent R (orderedFinsetProduct s f) 1

theorem

orderedFinsetProduct_congr

L373 ↗

ReidemeisterSchreier.Discrete.Presentations.orderedFinsetProduct_congr

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete.Presentations
variable {G H : Type*} [Group G] [Group H]
section NormalClosure
variable {R S : Set G} {r a b : G}
section OrderedFinsetProduct
variable {ι : Type*} [LinearOrder ι]

Lean source · statement

theorem orderedFinsetProduct_congr
    (s : Finset ι) {f g : ι → G}
    (h : ∀ i ∈ s, f i = g i) :
    orderedFinsetProduct s f = orderedFinsetProduct s g

Module documentation

Operations on relator normal closures

Declarations