isSeparator_iff_faithful_coyoneda_obj

English

Let G be an object. G is a separator iff the Yoneda image of G is faithful, i.e., the functor obtained from G via Yoneda reflects distinct morphisms.

Русский

Пусть G — объект. G является разделителем тогда и только тогда, когда образ G через Yoneda-функтор верен, то есть соответствующий функтор отражает разные морфизмы.

LaTeX

$$$\\mathrm{IsSeparator}(G) \\iff (\\mathrm{yoneda.obj}(\\mathrm{op}\,G)).\\mathrm{Faithful}$$$

Lean4

theorem isSeparator_iff_faithful_coyoneda_obj (G : C) : IsSeparator G ↔ (coyoneda.obj (op G)).Faithful :=
  ⟨fun hG => ⟨fun hfg => hG.def _ _ (congr_fun hfg)⟩, fun _ =>
    (isSeparator_def _).2 fun _ _ _ _ hfg => (coyoneda.obj (op G)).map_injective (funext hfg)⟩

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