Theorems · Inductive type · group theory

FreeSemigroup

Type u → Type u

If α is a type, then FreeSemigroup α is the free semigroup generated by α. This is a semigroup equipped with a function FreeSemigroup.of : α → FreeSemigroup α which has the following universal property: if M is any semigroup, and f : α → M is any function, then this function is the composite of FreeSemigroup.of and a unique semigroup homomorphism FreeSemigroup.lift f : FreeSemigroup α →ₙ* M. A typical element of FreeSemigroup α is a nonempty formal product of elements of α. For example if x and y are terms of type α then x * y * y * x is a "typical" element of FreeSemigroup α. In particular if α is empty then FreeSemigroup α is also empty, and if α has one term then FreeSemigroup α is isomorphic to Multiplicative ℕ+. If α has two or more terms then FreeSemigroup α is not commutative. One can think of FreeSemigroup α as the type of nonempty lists of α, with multiplication given by concatenation.

Defined in

Mathlib.Algebra.Free

Cited by

43 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms