[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P)) ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
refine' ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P)) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P)) → Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P)) ↔ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
refine' ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat).PreservesEpimorphisms => _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGroupCat)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P)) (forget _)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P)) → Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
intro
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op P))
[PROOFSTEP]
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)
