English
Let e: A ≃ₗc[R] B be a coalgebra equivalence. Then the linear map underlying its inverse coincides with the inverse of the underlying linear equivalence, i.e. the inverse expressed as a coalgebra hom is the same as the inverse linear map.
Русский
Пусть e: A ≃ₗc[R] B — эквивалентность коалгебр. Тогда линейное отображение, лежащее в основе его обратного отображения, совпадает с обратным отображением базового линейного отображения; то есть обратное в виде коалгомо́рхизмы равно обратному линейному отображению.
LaTeX
$$$((e.symm : B \to_{\mathrm{Coalgebra}} A) : B \to_{R} A) = (e : A \simeq_{R} B).symm$$$
Lean4
@[simp]
theorem symm_toCoalgHom (e : A ≃ₗc[R] B) : ((e.symm : B →ₗc[R] A) : B →ₗ[R] A) = (e : A ≃ₗ[R] B).symm :=
rfl
