Bracketings in a free magma

An element of a free magma is a bracketing of a nonempty list of generators. This file singles out the left combs, the bracketings ((a * b) * c) * d in which every product has a generator as its right factor, and shows that a homomorphism into a semigroup depends on the list of generators alone.

Main definitions

• FreeMagma.IsLeftComb: the element is a left comb.

Main results

• FreeMagma.isLeftComb_foldl_mul_of: multiplying on the right by generators preserves and reflects being a left comb.
• FreeMagma.toList_lift_foldl_mul_of: multiplying on the right by generators appends them to the list of generators.
• FreeMagma.lift_eq_lift_of_lift_of_eq: a homomorphism into a semigroup takes two elements with the same generators in the same order to the same value.

def FreeMagma.IsLeftComb {α : Type u_1} : FreeMagma α → Prop

An element of a free magma is a left comb when every product in it has a generator as its right factor.

Equations

• (FreeMagma.of a).IsLeftComb = True
• (x_1.mul (FreeMagma.of a)).IsLeftComb = x_1.IsLeftComb
• (a.mul (a_1.mul a_2)).IsLeftComb = False

@[instance_reducible]

instance FreeMagma.decidableIsLeftComb {α : Type u_1} (x : FreeMagma α) : Decidable x.IsLeftComb

Equations

• (FreeMagma.of a).decidableIsLeftComb = isTrue trivial
• (x_1.mul (FreeMagma.of a)).decidableIsLeftComb = x_1.decidableIsLeftComb
• (a.mul (a_1.mul a_2)).decidableIsLeftComb = isFalse ⋯

@[simp]

theorem FreeMagma.isLeftComb_of {α : Type u_1} (a : α) : (of a).IsLeftComb

@[simp]

theorem FreeMagma.isLeftComb_mul_of {α : Type u_1} (x : FreeMagma α) (a : α) : (x * of a).IsLeftComb ↔ x.IsLeftComb

@[simp]

theorem FreeMagma.not_isLeftComb_mul_mul {α : Type u_1} (x y z : FreeMagma α) : ¬(x * (y * z)).IsLeftComb

theorem FreeMagma.isLeftComb_foldl_mul_of {α : Type u_1} (x : FreeMagma α) (l : List α) : (List.foldl (fun (x1 : FreeMagma α) (x2 : α) => x1 * of x2) x l).IsLeftComb ↔ x.IsLeftComb

theorem FreeMagma.toList_lift_foldl_mul_of {α : Type u_1} (x : FreeMagma α) (l : List α) : FreeMonoid.toList ((lift FreeMonoid.of) (List.foldl (fun (x1 : FreeMagma α) (x2 : α) => x1 * of x2) x l)) = FreeMonoid.toList ((lift FreeMonoid.of) x) ++ l

theorem FreeMagma.lift_eq_lift_toFreeSemigroup {α : Type u_1} {β : Type u_2} [Semigroup β] (f : α → β) (x : FreeMagma α) : (lift f) x = (FreeSemigroup.lift f) (toFreeSemigroup x)

theorem FreeMagma.lift_of_eq_toFreeMonoid {α : Type u_1} (x : FreeMagma α) : (lift FreeMonoid.of) x = FreeSemigroup.toFreeMonoid (toFreeSemigroup x)

theorem FreeMagma.lift_eq_lift_of_lift_of_eq {α : Type u_1} {β : Type u_2} [Semigroup β] (f : α → β) {x y : FreeMagma α} (h : (lift FreeMonoid.of) x = (lift FreeMonoid.of) y) : (lift f) x = (lift f) y

A homomorphism from a free magma to a semigroup does not see the bracketing: it takes two elements with the same generators in the same order to the same value.