map_surjective — Mathlib

English

Let F be a fully faithful functor. Then for any objects X and Y in the source category, the map on hom-sets F.map : Hom_C(X,Y) → Hom_D(FX,FY) is surjective; i.e., every morphism between F X and F Y in D arises as the image of some morphism between X and Y in C.

Русский

Пусть F — полностью полнофункциональный (полный и верный) функтор. Тогда для любых объектов X, Y в исходной категории отображение F.map : Hom_C(X,Y) → Hom_D(FX,FY) является сюръективным; то есть любой морфизм между FX и FY в D есть образом некоторого морфизма между X и Y в C.

LaTeX

$$$\forall X,Y:\;\operatorname{Surjective}\big(F.map : (X \to Y) \to (F X \to F Y)\big)$$$

Lean4

theorem map_surjective {X Y : C} : Function.Surjective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  hF.homEquiv.surjective

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