instFaithfulFunctorOppositeAbToPresheaf

English

The functor toPresheaf R is faithful: it reflects distinct morphisms, i.e., if two morphisms become equal after applying toPresheaf R, they were equal originally.

Русский

Функтор toPresheaf R верен: он сохраняет различие морфизмов, то есть если после применения toPresheaf R два морфизма совпадают, то они были равны изначально.

LaTeX

$$$\mathrm{toPresheaf}(R)\text{ is faithful, hence } f=g \Rightarrow (\!f.app\;X = g.app\;X)$.$$

Lean4

instance : (toPresheaf R).Faithful where
  map_injective {_ _ f g}
    h := by
    ext X x
    exact congr_fun (((evaluation _ _).obj X ⋙ forget _).congr_map h) x

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