English
The minimal congruence on FreeMonoid (M ⊕ N) making the two injections sum.inl and sum.inr into the coproduct into a pair of monoid homomorphisms is given by the infimum of all c with the listed relations: x*y on the left, x*y on the right, and the unit elements map to the unit.
Русский
Минимальная конгруэнция на FreeMonoid (M ⊕ N), такая что инъекции в левые и правые суммы образуют моноид-гомоморфизмы в копрод, равна infimum всех c, удовлетворяющих указанным отношениям: произведение слева и справа, единицы соответствуют единице.
LaTeX
$$$\text{coprodCon}(M,N) = \; \inf \{c \mid \forall x,y:\, c(out) \text{ и т.д.} \}$$$
Lean4
/-- The minimal congruence relation `c` on `FreeMonoid (M ⊕ N)`
such that `FreeMonoid.of ∘ Sum.inl` and `FreeMonoid.of ∘ Sum.inr` are monoid homomorphisms
to the quotient by `c`. -/
@[to_additive /-- The minimal additive congruence relation `c` on `FreeAddMonoid (M ⊕ N)`
such that `FreeAddMonoid.of ∘ Sum.inl` and `FreeAddMonoid.of ∘ Sum.inr`
are additive monoid homomorphisms to the quotient by `c`. -/
]
def coprodCon (M N : Type*) [MulOneClass M] [MulOneClass N] : Con (FreeMonoid (M ⊕ N)) :=
sInf
{c |
(∀ x y : M, c (of (Sum.inl (x * y))) (of (Sum.inl x) * of (Sum.inl y))) ∧
(∀ x y : N, c (of (Sum.inr (x * y))) (of (Sum.inr x) * of (Sum.inr y))) ∧
c (of <| Sum.inl 1) 1 ∧ c (of <| Sum.inr 1) 1}
