isCoseparator_iff_faithful_preadditiveYonedaObj

English

IsCoseparator G iff the faithful property holds for the preadditive Yoneda object at G.

Русский

IsCoseparator G тогда и только тогда, когда предадитивный Yoneda-объект в G верен.

LaTeX

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

Lean4

theorem isCoseparator_iff_faithful_preadditiveYonedaObj (G : C) : IsCoseparator G ↔ (preadditiveYonedaObj G).Faithful :=
  by
  rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}), fun h => Functor.Faithful.comp _ _⟩

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