instEssSurjId

Mathlib.CategoryTheory.EssentialImage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instEssSurjId

English

The identity functor on any category is essentially surjective.

Русский

Тождественный функтор на любой категории по существу сюръжен.

LaTeX

$$$\operatorname{EssSurj}(\mathrm{Id}_C)$$$

Lean4

instance instEssSurjId : EssSurj (𝟭 C) where mem_essImage Y := ⟨Y, ⟨Iso.refl _⟩⟩

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

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

Разделы

Аффилиация

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