C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGroupCat) ↔ Faithful (preadditiveYonedaObj G)
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ Faithful (preadditiveYonedaObj G)
rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGroupCat) ↔ Faithful (preadditiveYonedaObj G)
exact ⟨fun h => Faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => Faithful.comp _ _⟩