Evaluation of signed words in free groups

A signed word is a list of pairs (x, b), with true denoting a generator and false its inverse. This file gives product formulas for evaluating such words under a homomorphism out of a free group.

Main results

• MonoidHom.apply_freeGroup_mk: a homomorphism evaluates a signed word letter by letter.
• FreeGroup.lift_inv_mk: inverting the image of every generator flips every sign in a word.

theorem MonoidHom.apply_freeGroup_mk {α : Type u_1} {M : Type u_2} [DivisionMonoid M] (F : FreeGroup α →* M) (L : List (α × Bool)) : F (FreeGroup.mk L) = (List.map (fun (p : α × Bool) => bif p.2 then F (FreeGroup.of p.1) else (F (FreeGroup.of p.1))⁻¹) L).prod

A homomorphism out of a free group into a division monoid evaluates on the word L as the product of the images of its signed letters. For a group target and a homomorphism given as a lift, this is FreeGroup.lift_mk.

theorem FreeGroup.lift_inv_mk {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (L : List (α × Bool)) : (lift fun (x : α) => (f x)⁻¹) (mk L) = (lift f) (mk (List.map (fun (p : α × Bool) => (p.1, !p.2)) L))

Lifting the pointwise inverse of f evaluates on the word L as lifting f evaluates on the word with every sign flipped.