ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.FreeGroupLift
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.
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)A free-group element is relator-equivalent to the word built from a list when its word representation reduces to that list.
Show Lean proof
by
apply RelatorEquivalent.of_eq
rw [← FreeGroup.toWord_inj]
simp only [h, FreeGroup.toWord_mk]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) uA free-group word is relator-equivalent to the word built from a list when their reduced words agree.
Show Lean proof
(freeGroup_relatorEquivalent_of_toWord_eq_reduce
(R := R) (u := u) (w := w) h.symm).symmdef 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 xsExpand each signed source letter to the reduced word of its image, reversing and inverting negative letters.
@[simp]
theorem freeGroupSubstitutionWord_nil {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) :
freeGroupSubstitutionWord f [] = []Substitution sends the empty word to the empty word.
Show Lean proof
rfl@[simp]
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 xsSubstitution of a positive letter prepends the reduced word of its image.
Show Lean proof
rfl@[simp]
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 xsSubstitution of a negative letter prepends the inverse-reversal of its image word.
Show Lean proof
rfltheorem freeGroupSubstitutionWord_append {Y : Type*} [DecidableEq Y]
(f : X → FreeGroup Y) (xs ys : List (X × Bool)) :
freeGroupSubstitutionWord f (xs ++ ys) =
freeGroupSubstitutionWord f xs ++ freeGroupSubstitutionWord f ysSubstitution preserves concatenation of signed words.
Show Lean proof
by
induction xs with
| nil => simp
| cons xb xs ih =>
rcases xb with ⟨x, b⟩
cases b
· simp only [List.cons_append, freeGroupSubstitutionWord_cons_false, ih, List.append_assoc]
· simp only [List.cons_append, freeGroupSubstitutionWord_cons_true, ih, List.append_assoc]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)Evaluating a substitution word agrees with applying the free-group lift.
Show Lean proof
by
induction xs with
| nil => exact FreeGroup.one_eq_mk.symm
| cons xb xs ih =>
rcases xb with ⟨x, b⟩
cases b
· rw [freeGroupSubstitutionWord_cons_false, ← FreeGroup.mul_mk,
← FreeGroup.inv_mk, FreeGroup.mk_toWord, ih]
simp only [FreeGroup.lift_mk, List.map_cons, cond_false, List.prod_cons]
· rw [freeGroupSubstitutionWord_cons_true, ← FreeGroup.mul_mk,
FreeGroup.mk_toWord, ih]
simp only [FreeGroup.lift_mk, List.map_cons, cond_true, List.prod_cons]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)The lifted generator maps to the corresponding word in the free-group presentation.
Show Lean proof
by
rw [← freeGroup_mk_substitutionWord (f := f) (xs := xs)]
simp only [FreeGroup.toWord_mk]
Theorem
ReidemeisterSchreier.Discrete.Presentations.freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq
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 ysThe free-group lift of a reduced substitution word agrees with the corresponding generator.
Show Lean proof
by
rw [← FreeGroup.toWord_inj]
rw [freeGroup_toWord_lift_mk, FreeGroup.toWord_mk, h]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)A lifted generator word is relator-equivalent to the corresponding word when the substitution word has the stated reduction.
Show Lean proof
RelatorEquivalent.of_eq
(freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq h)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)) 1A lifted generator word is relator-equivalent to the identity when its substitution word reduces to the empty word.
Show Lean proof
(freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq
(R := R) h).trans hytheorem 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)A free-group lift preserves relator equivalence when the generator images are relator-equivalent.
Show Lean proof
by
let N : Subgroup G := Subgroup.normalClosure R
let F : FreeGroup X →* G ⧸ N :=
(QuotientGroup.mk' N).comp (FreeGroup.lift f)
let K : FreeGroup X →* G ⧸ N :=
(QuotientGroup.mk' N).comp (FreeGroup.lift g)
have hhom : F = K := by
ext x
dsimp [F, K]
simp only [FreeGroup.lift_apply_of]
rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
exact h x
have hw := congrArg (fun φ : FreeGroup X →* G ⧸ N => φ w) hhom
change ((FreeGroup.lift f w : G) : G ⧸ N) =
((FreeGroup.lift g w : G) : G ⧸ N) at hw
exact relatorEquivalent_iff_eq_in_presentedQuotient.2 hwtheorem 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) 1A free-group lift sends the word to a relator-equivalent trivial word when the generator images are relator-equivalent to one.
Show Lean proof
by
let trivialLift : FreeGroup X →* G :=
FreeGroup.lift (fun _ : X => (1 : G))
have htrivial : trivialLift w = 1 := by
have hhom : trivialLift = 1 := by
ext x
simp only [FreeGroup.lift_apply_of, MonoidHom.one_apply, trivialLift]
exact congrArg (fun φ : FreeGroup X →* G => φ w) hhom
simpa [trivialLift, htrivial] using
freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
(R := R) (f := f) (g := fun _ : X => (1 : G)) h w
Theorem
ReidemeisterSchreier.Discrete.Presentations.freeGroup_lift_relatorEquivalent_of_generator_eq
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)A free-group lift preserves relator equivalence when the generator images are equal.
Show Lean proof
freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
(R := R) (f := f) (g := g)
(fun x => RelatorEquivalent.of_eq (h x)) w