isSeparator_iff_faithful_preadditiveCoyonedaObj

English

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

Русский

IsSeparating G тогда и только тогда, когда Coyoneda-объект в G верен.

LaTeX

$$$\mathrm{IsSeparating}(G) \iff (\text{preadditiveCoyonedaObj } G).\mathrm{Faithful}$$$

Lean4

theorem isSeparator_iff_faithful_preadditiveCoyonedaObj (G : C) : IsSeparator G ↔ (preadditiveCoyonedaObj G).Faithful :=
  by
  rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}), fun h => Functor.Faithful.comp _ _⟩

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