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

ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Presentation

5 Theorems

This module expands conjugated list products and promotes generatorwise normal-closure relations to all words under a free-group endomorphism.

import
Imported by

Declarations

Theorem ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod 
theorem conjugate_list_prod {G : Type*} [Group G] (x : G) :
    ∀ l : List G, x * l.prod * x⁻¹ = (l.map fun t => x * t * x⁻¹).prod

Conjugating a list product is the product of the conjugated entries.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.nested_conjugate_list_prod 
theorem nested_conjugate_list_prod {G : Type*} [Group G]
    (x : G) {p n : ℕ} (f : Fin p → Fin n → G) :
    (List.ofFn (fun b : Fin p =>
      (List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)).prod =
        x * (List.ofFn (fun b : Fin p =>
          (List.ofFn (fun j : Fin n => f b j)).prod)).prod * x⁻¹

A rectangular product of conjugated entries is the conjugate of the corresponding rectangular product.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.subgroup_list_prod_val 
theorem subgroup_list_prod_val {G : Type*} [Group G]
    {H : Subgroup G} {n : ℕ} (f : Fin n → H) :
    (((List.ofFn f).prod : H) : G) =
      (List.ofFn (fun i : Fin n => ((f i : H) : G))).prod

The value of a subgroup list product is the product of the underlying subgroup elements.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.subgroup_nested_list_prod_val 
theorem subgroup_nested_list_prod_val {G : Type*} [Group G]
    {H : Subgroup G} {p n : ℕ} (f : Fin p → Fin n → H) :
    (((List.ofFn (fun b : Fin p =>
      (List.ofFn (fun j : Fin n => f b j)).prod)).prod : H) : G) =
        (List.ofFn (fun b : Fin p =>
          (List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prod

The subgroup nested list product underlying value is evaluated by the displayed coordinate or generator-level formula in the Reidemeister--Schreier rewriting system.

Show Lean proof
Theorem ReidemeisterSchreier.Discrete.Presentations.freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv 
theorem freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv
    {Y : Type*} (R : Set (FreeGroup Y)) (F : FreeGroup Y →* FreeGroup Y)
    (hgen :
      ∀ y : Y,
        F (FreeGroup.of y) * (FreeGroup.of y)⁻¹ ∈ Subgroup.normalClosure R) :
    ∀ w : FreeGroup Y, F w * w⁻¹ ∈ Subgroup.normalClosure R

If an endomorphism is congruent to the identity on generators modulo a normal closure, then it is congruent to the identity on every free-group word.

Show Lean proof