Module

FreeGroupLift.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.FreeGroupLift

15 declarations indexed from sourceView source ↗

Module documentation

Free-group lifts modulo relators

This module relates reduced words and FreeGroup.mk, then proves that lifts whose generator images agree modulo a relator normal closure agree on every free-group word.

Imports1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic

Imported by2

theorem

freeGroup_relatorEquivalent_of_toWord_eq_reduce

L33 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_relatorEquivalent_of_toWord_eq_reduce

Documentation

A free-group element is relator-equivalent to the word built from a list when its word representation reduces to that list.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_relatorEquivalent_of_toWord_eq_reduce
    [DecidableEq X]
    {R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
    (h : u.toWord = FreeGroup.reduce w) :
    RelatorEquivalent R u (FreeGroup.mk w)

theorem

freeGroup_relatorEquivalent_mk_of_reduce_eq

L46 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_relatorEquivalent_mk_of_reduce_eq

Documentation

A free-group word is relator-equivalent to the word built from a list when their reduced words agree.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_relatorEquivalent_mk_of_reduce_eq
    [DecidableEq X]
    {R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
    (h : FreeGroup.reduce w = u.toWord) :
    RelatorEquivalent R (FreeGroup.mk w) u

def

freeGroupSubstitutionWord

L56 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroupSubstitutionWord

Documentation

Expand each signed source letter to the reduced word of its image, reversing and inverting negative letters.

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 FreeGroupLift
variable {X : Type*}

Lean source · full declaration

def freeGroupSubstitutionWord {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) :
    List (X × Bool) → List (Y × Bool)
  | [] => []
  | (x, true) :: xs => (f x).toWord ++ freeGroupSubstitutionWord f xs
  | (x, false) :: xs => FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs

theorem

freeGroupSubstitutionWord_nil

L65 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroupSubstitutionWord_nil

Documentation

Substitution sends the empty word to the empty word.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroupSubstitutionWord_nil {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) :
    freeGroupSubstitutionWord f [] = []

theorem

freeGroupSubstitutionWord_cons_true

L72 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroupSubstitutionWord_cons_true

Documentation

Substitution of a positive letter prepends the reduced word of its image.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroupSubstitutionWord_cons_true {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
    freeGroupSubstitutionWord f ((x, true) :: xs) =
      (f x).toWord ++ freeGroupSubstitutionWord f xs

theorem

freeGroupSubstitutionWord_cons_false

L80 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroupSubstitutionWord_cons_false

Documentation

Substitution of a negative letter prepends the inverse-reversal of its image word.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroupSubstitutionWord_cons_false {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
    freeGroupSubstitutionWord f ((x, false) :: xs) =
      FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs

theorem

freeGroupSubstitutionWord_append

L87 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroupSubstitutionWord_append

Documentation

Substitution preserves concatenation of signed words.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroupSubstitutionWord_append {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) (xs ys : List (X × Bool)) :
    freeGroupSubstitutionWord f (xs ++ ys) =
      freeGroupSubstitutionWord f xs ++ freeGroupSubstitutionWord f ys

theorem

freeGroup_mk_substitutionWord

L100 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_mk_substitutionWord

Documentation

Evaluating a substitution word agrees with applying the free-group lift.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_mk_substitutionWord {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) (xs : List (X × Bool)) :
    FreeGroup.mk (freeGroupSubstitutionWord f xs) =
      FreeGroup.lift f (FreeGroup.mk xs)

theorem

freeGroup_toWord_lift_mk

L117 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_toWord_lift_mk

Documentation

The lifted generator maps to the corresponding word in the free-group presentation.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_toWord_lift_mk {Y : Type*} [DecidableEq Y]
    (f : X → FreeGroup Y) (xs : List (X × Bool)) :
    (FreeGroup.lift f (FreeGroup.mk xs)).toWord =
      FreeGroup.reduce (freeGroupSubstitutionWord f xs)

theorem

freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq

L125 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq

Documentation

The free-group lift of a reduced substitution word agrees with the corresponding generator.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq
    {Y : Type*} [DecidableEq Y]
    {f : X → FreeGroup Y} {xs : List (X × Bool)}
    {ys : List (Y × Bool)}
    (h :
      FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
        FreeGroup.reduce ys) :
    FreeGroup.lift f (FreeGroup.mk xs) = FreeGroup.mk ys

theorem

freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq

L140 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq

Documentation

A lifted generator word is relator-equivalent to the corresponding word when the substitution word has the stated reduction.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq
    {Y : Type*} [DecidableEq Y]
    {R : Set (FreeGroup Y)}
    {f : X → FreeGroup Y} {xs : List (X × Bool)}
    {ys : List (Y × Bool)}
    (h :
      FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
        FreeGroup.reduce ys) :
    RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs))
      (FreeGroup.mk ys)

theorem

freeGroup_relatorEquivalent_lift_mk_one_of_substitutionWord_reduce_eq

L157 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_relatorEquivalent_lift_mk_one_of_substitutionWord_reduce_eq

Documentation

A lifted generator word is relator-equivalent to the identity when its substitution word reduces to the empty word.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_relatorEquivalent_lift_mk_one_of_substitutionWord_reduce_eq
    {Y : Type*} [DecidableEq Y]
    {R : Set (FreeGroup Y)}
    {f : X → FreeGroup Y} {xs : List (X × Bool)}
    {ys : List (Y × Bool)}
    (h :
      FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
        FreeGroup.reduce ys)
    (hy : RelatorEquivalent R (FreeGroup.mk ys) 1) :
    RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs)) 1

theorem

freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent

L174 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent

Documentation

A free-group lift preserves relator equivalence when the generator images are relator-equivalent.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
    {R : Set G} {f g : X → G}
    (h : ∀ x : X, RelatorEquivalent R (f x) (g x))
    (w : FreeGroup X) :
    RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w)

theorem

freeGroup_lift_relatorEquivalent_one_of_generator_relatorEquivalent

L199 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_lift_relatorEquivalent_one_of_generator_relatorEquivalent

Documentation

A free-group lift sends the word to a relator-equivalent trivial word when the generator images are relator-equivalent to one.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_lift_relatorEquivalent_one_of_generator_relatorEquivalent
    {R : Set G} {f : X → G}
    (h : ∀ x : X, RelatorEquivalent R (f x) 1)
    (w : FreeGroup X) :
    RelatorEquivalent R (FreeGroup.lift f w) 1

theorem

freeGroup_lift_relatorEquivalent_of_generator_eq

L216 ↗

ReidemeisterSchreier.Discrete.Presentations.freeGroup_lift_relatorEquivalent_of_generator_eq

Documentation

A free-group lift preserves relator equivalence when the generator images are equal.

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 FreeGroupLift
variable {X : Type*}

Lean source · statement

theorem freeGroup_lift_relatorEquivalent_of_generator_eq
    {R : Set G} {f g : X → G}
    (h : ∀ x : X, f x = g x)
    (w : FreeGroup X) :
    RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w)

Module documentation

Free-group lifts modulo relators

Declarations