[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ 0
[PROOFSTEP]
simpa only [Limits.comp_zero] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ (f - g) = 0
[PROOFSTEP]
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h
[PROOFSTEP]
simpa only [Limits.zero_comp] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), (f - g) ≫ h = 0
[PROOFSTEP]
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsSeparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (h : G ⟶ X), h ≫ f = h ≫ 0
[PROOFSTEP]
simpa only [Limits.comp_zero] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (h : G ⟶ X), h ≫ (f - g) = 0
[PROOFSTEP]
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsCoseparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h
[PROOFSTEP]
simpa only [Limits.zero_comp] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (h : Y ⟶ G), (f - g) ≫ h = 0
[PROOFSTEP]
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ Faithful (preadditiveCoyoneda.obj (op G))
[PROOFSTEP]
rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj, whiskeringRight_obj_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyoneda.obj (op G) ⋙ forget AddCommGroupCat) ↔ Faithful (preadditiveCoyoneda.obj (op G))
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget AddCommGroupCat), fun h => Faithful.comp _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ Faithful (preadditiveCoyonedaObj (op G))
[PROOFSTEP]
rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyonedaObj (op G) ⋙ forget₂ (ModuleCat (End (op G))) AddCommGroupCat) ↔
    Faithful (preadditiveCoyonedaObj (op G))
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => Faithful.comp _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ Faithful (preadditiveYoneda.obj G)
[PROOFSTEP]
rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj, whiskeringRight_obj_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveYoneda.obj G ⋙ forget AddCommGroupCat) ↔ Faithful (preadditiveYoneda.obj G)
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget AddCommGroupCat), fun h => Faithful.comp _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ Faithful (preadditiveYonedaObj G)
[PROOFSTEP]
rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGroupCat) ↔ Faithful (preadditiveYonedaObj G)
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => Faithful.comp _ _⟩
