hasForgetToCommAlgCat

Mathlib.Algebra.Category.CommBialgCat

URI: https://scilib.ai/kg/mathlib#CommBialgCat.hasForgetToCommAlgCat

← MathLib Explorer

English

The forgetful object inherits a Bialgebra structure from A.

Русский

Объект забывания наследует структуру биалгебры от A.

LaTeX

$$$\forall A:\mathrm{CommBialgCat}(R),\ Bialgebra(R, (\mathrm{forget}(\mathrm{CommBialgCat})(R)).obj A)$$$

Lean4

instance hasForgetToCommAlgCat : HasForget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R)
    where
  forget₂.obj M := .of R M
  forget₂.map f := CommAlgCat.ofHom f.hom

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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