toBialgEquiv_toBialgHom

Mathlib.Algebra.Category.BialgCat.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.toBialgEquiv_toBialgHom

English

Further associativity/compatibility of composed isomorphisms in BialgCat.

Русский

Дополнительная ассоциативность совместимоcти составляемых изоморфизмов в BialgCat.

LaTeX

$$$toBialgIso((e.trans f)) = toBialgIso(e) \circ toBialgIso(f)$$$

Lean4

@[simp]
theorem toBialgEquiv_toBialgHom (i : X ≅ Y) : (i.toBialgEquiv : X →ₐc[R] Y) = i.hom.1 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru