isSeparator_iff_faithful_preadditiveCoyoneda

English

IsSeparating G iff the preadditive Coyoneda functor at G is faithful.

Русский

IsSeparating G эквивалентно тому, что Coyoneda-функтор относительно G верен.

LaTeX

$$$\mathrm{IsSeparating}(G) \iff (\text{preadditiveCoyoneda.obj } { unop := G }).\mathrm{Faithful}$$$

Lean4

theorem isSeparator_iff_faithful_preadditiveCoyoneda (G : C) :
    IsSeparator G ↔ (preadditiveCoyoneda.obj (op G)).Faithful :=
  by
  rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrpCat), fun h => Functor.Faithful.comp _ _⟩

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