isCoseparator_iff_faithful_preadditiveYoneda

English

IsCoseparator G iff the faithful property holds for the preadditive Yoneda functor.

Русский

IsCoseparator G тогда и только тогда, когда сопутствующая предадитивная функциональность Yoneda верна.

LaTeX

$$$\mathrm{IsCoseparator}(G) \iff (\text{preadditiveYoneda.obj } G).\mathrm{Faithful}$$$

Lean4

theorem isCoseparator_iff_faithful_preadditiveYoneda (G : C) : IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful :=
  by
  rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrpCat), fun h => Functor.Faithful.comp _ _⟩

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