toCat_full

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#MonCat.toCat_full

English

The instance asserts that the forgetful functor from MonCat toCat is full.

Русский

Экземпляр утверждает, что функтор забывания MonCat→Cat является полным.

LaTeX

$$$\\text{toCat Full}$$$

Lean4

instance toCat_full : toCat.Full where
  map_surjective
    y :=
    let ⟨x, h⟩ := (SingleObj.mapHom _ _).surjective y
    ⟨ofHom x, h⟩

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

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

Разделы

Аффилиация

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