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
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi (F.map f) → IsSplitEpi 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
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi f → IsSplitEpi (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
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f
constructor
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
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f
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
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi (F.map f) → IsSplitEpi f
intro h
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
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f
exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
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
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitEpi f
⊢ IsSplitEpi (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
inst✝¹ : Full F
inst✝ : Faithful F
⊢ IsSplitEpi f → IsSplitEpi (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
inst✝¹ : Full F
inst✝ : Faithful F
h : IsSplitEpi f
⊢ IsSplitEpi (F.map f)
exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)