English
The map that sends a coalgebra equivalence e: A ≃ₗc[R] B to its underlying coalgebra homomorphism e.toCoalgHom is injective; i.e., two coalgebra equivalences are equal whenever their underlying coalgebra homomorphisms are equal.
Русский
Отображение, отправляющее коалгебраическую эквивалентность e: A ≃ₗc[R] B в соответствующий коалгебраический гомоморфизм e.toCoalgHom, инъективно; т.е. две коалгебраические эквивалентности совпадают, если совпадают их соответствующие коалгебраические гомоморфизмы.
LaTeX
$$$\\operatorname{toCoalgHom}(e_1) = \\operatorname{toCoalgHom}(e_2) \\iff e_1 = e_2$$$
Lean4
theorem toCoalgHom_injective : Function.Injective (toCoalgHom : (A ≃ₗc[R] B) → A →ₗc[R] B) := fun _ _ H =>
toEquiv_injective <| Equiv.ext <| CoalgHom.congr_fun H
