C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi (F.map f)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi f
apply F.epi_of_epi_map
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
this : Epi (G.map f ≫ (α.app Y).inv)
⊢ Epi (F.map f)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi (F.map f)
haveI : Epi (G.map f ≫ (α.app Y).inv) := epi_comp _ _
case h.e'_5
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
this : Epi (G.map f ≫ (α.app Y).inv)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
this : Epi (G.map f ≫ (α.app Y).inv)
⊢ Epi (F.map f)
convert (epi_comp _ _ : Epi ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv))
no goals
case h.e'_5
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : ReflectsEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
this : Epi (G.map f ≫ (α.app Y).inv)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality]