map_surjective

Mathlib.CategoryTheory.Functor.FullyFaithful

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

English

If F is full, the map on morphisms is surjective.

Русский

Если F полно(й) (full), отображение на морфизмах сюрьективно.

LaTeX

$$$\\operatorname{Full} F \\Rightarrow \\operatorname{Surjective}(F.map)$$$

Lean4

theorem map_surjective (F : C ⥤ D) [Full F] : Function.Surjective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  Full.map_surjective

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

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

Разделы

Аффилиация

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