toCoalgEquiv_toCoalgHom — Mathlib

English

Let e be a bialgebra equivalence A ≃ₐc[R] B. The underlying linear coalgebra map from A to B, viewed as a coalgebra hom, is exactly the same map as e viewed as a coalgebra hom.

Русский

Пусть e — биалгебровое эквивалентство A ≃ₐc[R] B. Найдём, что линейный коалгебраический гомоморфизм, лежащий в основе e, совпадает с гомоморфизмом коалгебры, полученным из e.

LaTeX

$$$((e : A \\to_{\\mathrm{coal}} B) = (e : A \\to_{\\mathrm{coal}} B))$$$

Lean4

theorem toCoalgEquiv_toCoalgHom : ((e : A ≃ₐc[R] B) : A →ₗc[R] B) = (e : A →ₐc[R] B) :=
  rfl

Похожие утверждения