English
The equalities relating the two sides of the isomorphisms, ensuring compatibility with the projections and injections, are standard results expressing the universal property of the unit-collapsed coproduct.
Русский
Согласование двух сторон изоморфизма через проекции и включения — стандартный результат, выражающий универсальное свойство копродукта с единицей.
LaTeX
$$$$ \\text{compatibility relations for CoprodPUnit isomorphisms with injections/projections.} $$$$
Lean4
/-- A relation on the free monoid on alphabet `Σ i, M i`,
relating `⟨i, 1⟩` with `1` and `⟨i, x⟩ * ⟨i, y⟩` with `⟨i, x * y⟩`. -/
inductive Rel : FreeMonoid (Σ i, M i) → FreeMonoid (Σ i, M i) → Prop
| of_one (i : ι) : Monoid.CoprodI.Rel (FreeMonoid.of ⟨i, 1⟩) 1
|
of_mul {i : ι} (x y : M i) :
Monoid.CoprodI.Rel (FreeMonoid.of ⟨i, x⟩ * FreeMonoid.of ⟨i, y⟩) (FreeMonoid.of ⟨i, x * y⟩)
