case mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi (F.map f) → Epi f

case mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi f → Epi (F.map f)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi (F.map f) ↔ Epi f
constructor
no goals
case mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi (F.map f) → Epi f
exact F.epi_of_epi_map
case mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
h : Epi f
⊢ Epi (F.map f)
case mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
⊢ Epi f → Epi (F.map f)
intro h
no goals
case mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : PreservesEpimorphisms F
hF₂ : ReflectsEpimorphisms F
h : Epi f
⊢ Epi (F.map f)
exact F.map_epi f