The free commutative magma

FreeCommMagma α is the free magma on α modulo the congruence generated by commutativity: the nonassociative commutative products of generators, Marcolli, Chomsky and Berwick's binary unordered rooted trees with leaves in α. lift is the universal property, by which maps from α into a commutative magma correspond to magma homomorphisms out of FreeCommMagma α. [UPSTREAM] candidate for Mathlib/Algebra/Free.lean.

Main definitions

• FreeCommMagma: the free commutative magma on a type.
• FreeCommMagma.of, FreeCommMagma.ofMagma: the generators, and the projection from the free magma.
• FreeCommMagma.lift: the universal property.

Main results

• FreeCommMagma.hom_ext: magma homomorphisms agreeing on the generators are equal.
• FreeCommMagma.of_injective: the generators are distinct.

References

• [MCB25]

def FreeMagma.commCon (α : Type u) : Con (FreeMagma α)

The congruence on the free magma generated by commutativity.

Equations

• FreeMagma.commCon α = conGen fun (x y : FreeMagma α) => ∃ (a : FreeMagma α) (b : FreeMagma α), x = a * b ∧ y = b * a

@[simp]

theorem FreeMagma.commCon_of_iff {α : Type u} {a : α} {y : FreeMagma α} : (commCon α) (of a) y ↔ y = of a

theorem FreeMagma.lift_congr {α : Type u} {M : Type v} [CommMagma M] (f : α → M) {x y : FreeMagma α} (h : (commCon α) x y) : (lift f) x = (lift f) y

def FreeCommMagma (α : Type u) : Type u

The free commutative magma on α, the free magma modulo commutativity.

Equations

• FreeCommMagma α = (FreeMagma.commCon α).Quotient

@[instance_reducible]

instance FreeCommMagma.instMul {α : Type u} : Mul (FreeCommMagma α)

Equations

• FreeCommMagma.instMul = { mul := FreeCommMagma.instMul._aux_1 }

@[instance_reducible]

instance FreeCommMagma.instCommMagma {α : Type u} : CommMagma (FreeCommMagma α)

Equations

• FreeCommMagma.instCommMagma = { toMul := FreeCommMagma.instMul, mul_comm := ⋯ }

def FreeCommMagma.ofMagma {α : Type u} : FreeMagma α →ₙ* FreeCommMagma α

The projection from the free magma, forgetting the bracketing order.

Equations

• FreeCommMagma.ofMagma = { toFun := fun (x : FreeMagma α) => ↑x, map_mul' := ⋯ }

def FreeCommMagma.of {α : Type u} (a : α) : FreeCommMagma α

The generator a.

Equations

• FreeCommMagma.of a = FreeCommMagma.ofMagma (FreeMagma.of a)

@[instance_reducible]

instance FreeCommMagma.instInhabited {α : Type u} [Inhabited α] : Inhabited (FreeCommMagma α)

Equations

• FreeCommMagma.instInhabited = { default := FreeCommMagma.of default }

@[simp]

theorem FreeCommMagma.ofMagma_of {α : Type u} (a : α) : ofMagma (FreeMagma.of a) = of a

theorem FreeCommMagma.ofMagma_surjective {α : Type u} : Function.Surjective ⇑ofMagma

theorem FreeCommMagma.inductionOn {α : Type u} {motive : FreeCommMagma α → Prop} (x : FreeCommMagma α) (of : ∀ (a : α), motive (of a)) (mul : ∀ (x y : FreeCommMagma α), motive x → motive y → motive (x * y)) : motive x

theorem FreeCommMagma.hom_ext {α : Type u} {M : Type v} [Mul M] {f g : FreeCommMagma α →ₙ* M} (h : ∀ (a : α), f (of a) = g (of a)) : f = g

Magma homomorphisms out of a free commutative magma agreeing on the generators are equal.

theorem FreeCommMagma.hom_ext_iff {α : Type u} {M : Type v} [Mul M] {f g : FreeCommMagma α →ₙ* M} : f = g ↔ ∀ (a : α), f (of a) = g (of a)

def FreeCommMagma.lift {α : Type u} {M : Type v} [CommMagma M] : (α → M) ≃ (FreeCommMagma α →ₙ* M)

The universal property of the free commutative magma: maps from α into a commutative magma correspond to magma homomorphisms out of FreeCommMagma α.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FreeCommMagma.lift_of {α : Type u} {M : Type v} [CommMagma M] (f : α → M) (a : α) : (lift f) (of a) = f a

@[simp]

theorem FreeCommMagma.lift_comp_of {α : Type u} {M : Type v} [CommMagma M] (f : α → M) : ⇑(lift f) ∘ of = f

@[simp]

theorem FreeCommMagma.lift_ofMagma {α : Type u} {M : Type v} [CommMagma M] (f : α → M) (x : FreeMagma α) : (lift f) (ofMagma x) = (FreeMagma.lift f) x

@[simp]

theorem FreeCommMagma.lift_symm_apply {α : Type u} {M : Type v} [CommMagma M] (F : FreeCommMagma α →ₙ* M) : lift.symm F = ⇑F ∘ of

def FreeCommMagma.map {α : Type u} {β : Type v} (f : α → β) : FreeCommMagma α →ₙ* FreeCommMagma β

The functorial action on generators.

Equations

• FreeCommMagma.map f = FreeCommMagma.lift (FreeCommMagma.of ∘ f)

@[simp]

theorem FreeCommMagma.map_of {α : Type u} {β : Type v} (f : α → β) (a : α) : (map f) (of a) = of (f a)

theorem FreeCommMagma.of_injective {α : Type u} : Function.Injective of