[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
[PROOFSTEP]
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (yoneda.obj J) ↔ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
[PROOFSTEP]
refine' ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGroupCat)).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : Functor.PreservesEpimorphisms (preadditiveYoneda.obj J ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (preadditiveYoneda.obj J) → Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : Functor.PreservesEpimorphisms (preadditiveYoneda.obj J)
⊢ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (yoneda.obj J) ↔ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
refine' ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : Functor.PreservesEpimorphisms (preadditiveYonedaObj J ⋙ forget (ModuleCat (End J)))
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J) → Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)
