C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) (_ : F.map f ≫ F.map (𝟙 Y) = F.map f ≫ F.map (𝟙 Y)))
⊢ Epi (F.map f)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
⊢ Epi (F.map f)
have := isColimitPushoutCoconeMapOfIsColimit F _ (PushoutCocone.isColimitMkIdId f)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) (_ : F.map f ≫ 𝟙 (F.obj Y) = F.map f ≫ 𝟙 (F.obj Y)))
⊢ Epi (F.map f)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) (_ : F.map f ≫ F.map (𝟙 Y) = F.map f ≫ F.map (𝟙 Y)))
⊢ Epi (F.map f)
simp_rw [F.map_id] at this
no goals
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) (_ : F.map f ≫ 𝟙 (F.obj Y) = F.map f ≫ 𝟙 (F.obj Y)))
⊢ Epi (F.map f)
apply PushoutCocone.epi_of_isColimitMkIdId _ this