English
Let A and B be R-modules with coalgebra structures. The map that sends a coalgebra equivalence e: A ≃ₗc[R] B to its underlying linear equivalence e.toEquiv is injective; i.e., two coalgebra equivalences are equal whenever their underlying linear equivalences are equal.
Русский
Пусть A и B — модули над R с коалgebra-структурами. Отображение, отправляющее стех коалгебраические эквивалентности e: A ≃ₗc[R] B в соответствующую линейную эквивалентность e.toEquiv, инъективно; т.е. две коалгебраические эквивалентности совпадают, если совпадают их соответствующие линейные эквивалентности.
LaTeX
$$$\\forall e_1,e_2 : A \\simeq_{\\ell_c[R]} B,\; e_1^{\\mathrm{toEquiv}} = e_2^{\\mathrm{toEquiv}} \\Rightarrow e_1 = e_2$$$
Lean4
theorem toEquiv_injective : Function.Injective (toEquiv : (A ≃ₗc[R] B) → A ≃ B) := fun ⟨_, _, _, _⟩ ⟨_, _, _, _⟩ h =>
(CoalgEquiv.mk.injEq _ _ _ _ _ _ _ _).mpr ⟨CoalgHom.ext (congr_fun (Equiv.mk.inj h).1), (Equiv.mk.inj h).2⟩
