English
The linear equivalence underlying the transitive composition of coalgebra equivalences e1₂ and e2₃ equals the usual composition of linear equivalences.
Русский
Линейное эквивалентное отображение, лежащее в основе траспозиции эквивалентностей коалгебр e12 и e23, равно обычному композиционному сочетанию линейных эквивалентностей.
LaTeX
$$$ (e_{12}.trans e_{23} : A \\to\\_{R} C) = (e_{12} : A \\to\\_{R} B) \\;\\widehat{\\otimes} \\; e_{23} $$$
Lean4
/-- Coalgebra equivalences are transitive. -/
@[trans, simps!]
def trans (e₁₂ : A ≃ₗc[R] B) (e₂₃ : B ≃ₗc[R] C) : A ≃ₗc[R] C :=
{ (e₂₃ : B →ₗc[R] C).comp (e₁₂ : A →ₗc[R] B), e₁₂.toLinearEquiv ≪≫ₗ e₂₃.toLinearEquiv with }
