counitAlgHom_comp

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#BialgHomClass.counitAlgHom_comp

← MathLib Explorer

English

A variant of counit compatibility for a generic F in BialgHomClass.

Русский

Вариант совместимости counit для общего F в BialgHomClass.

LaTeX

$$$ (counitAlgHom R B) \\circ (AlgHomClass.toAlgHom f) = counitAlgHom R A $$$

Lean4

@[simp]
theorem counitAlgHom_comp (f : F) : (counitAlgHom R B).comp (f : A →ₐ[R] B) = counitAlgHom R A :=
  AlgHom.toLinearMap_injective (CoalgHomClass.counit_comp f)

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

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

Разделы

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

Аффилиация

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