---
tag: 4YN1TB9CXN
kind: statement
role: proposition
name: Universal property of the free magma
msc: [08B20, 20N02]
uses: [ZZF8XPBG3Z, 9689SFPVE9, KBXSZC6BV1]
about: [ZZF8XPBG3Z]
sources:
  - url: https://en.wikipedia.org/wiki/Magma_(algebra)
    locator: Free magma
---

## Statement

Let $X$ be a set, let $M(X)$ be the [[free magma|ZZF8XPBG3Z]] on $X$, and let $\iota \colon X \to M(X)$ be the inclusion of the generators.
Let $N$ be a [[magma|9689SFPVE9]] and let $f \colon X \to N$ be a map.
Then there is exactly one magma [[homomorphism|KBXSZC6BV1]] $h \colon M(X) \to N$ such that $h \circ \iota = f$.

## Remarks

Existence: define $h$ by recursion on the construction of elements, with $h(x) = f(x)$ for $x \in X$ and $h(u \cdot v) = h(u) \cdot h(v)$.
This recursion is valid because each element of $M(X)$ is either a generator or a product $u \cdot v$ for exactly one pair $(u, v)$.
Uniqueness: two homomorphisms that agree on $X$ agree on all elements, by induction on the construction.
Example: with $N = (\Z, +)$ and $f(x) = 1$ for all $x$, the homomorphism $h$ sends each element to its number of leaves.
With $N = (\N, \max(a, b) + 1)$ and $f(x) = 0$, the homomorphism $h$ sends each element to the height of its binary tree.
In Mathlib this is `FreeMagma.lift`, an equivalence between maps $X \to N$ and magma homomorphisms $M(X) \to N$.

## Explanations

### L1 human

To map the free magma into another magma, it is enough to say where each letter goes.
The image of every bracketed product is then forced: it is the same product, bracketed the same way, of the images of the letters.
Since the free magma has no rules, nothing can go wrong.

### L2 human

The proposition says that the free magma is the free algebra of the variety of all magmas.
The free semigroup on $X$ has the same kind of universal property, and it is the quotient of $M(X)$ by the congruence generated by associativity.
Recursive definitions on binary trees, such as size and height, are instances of this proposition.