isCoseparator_iff_faithful_yoneda_obj

English

Let G be an object. G is a coseparator iff the Yoneda image of G is faithful, i.e., the contravariant Yoneda functor at G is faithful.

Русский

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

LaTeX

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

Lean4

theorem isCoseparator_iff_faithful_yoneda_obj (G : C) : IsCoseparator G ↔ (yoneda.obj G).Faithful :=
  ⟨fun hG => ⟨fun hfg => Quiver.Hom.unop_inj (hG.def _ _ (congr_fun hfg))⟩, fun _ =>
    (isCoseparator_def _).2 fun _ _ _ _ hfg => Quiver.Hom.op_inj <| (yoneda.obj G).map_injective (funext hfg)⟩

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