ext'

Mathlib.CategoryTheory.Monad.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comonad.Coalgebra.Hom.ext'

English

Two morphisms of coalgebras are equal if their carrier maps are equal.

Русский

Два морфизма коалгебр равны, если их carrier-мappings равны.

LaTeX

$$$\\\\forall X,Y \\\\in G. Coalgebra, \\\\forall f,g: X \\\\to Y, \\\\ f.f = g.f \\\\Rightarrow \\\\ f = g.$$$

Lean4

@[ext]
theorem ext' (X Y : Coalgebra G) (f g : X ⟶ Y) (h : f.f = g.f) : f = g :=
  Hom.ext h

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

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

Разделы

Аффилиация

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