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
⊢ IsSplitMono (F.map f) → IsSplitMono 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
⊢ IsSplitMono f → IsSplitMono (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
⊢ IsSplitMono (F.map f) ↔ IsSplitMono 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 : IsSplitMono (F.map f)
⊢ IsSplitMono 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
⊢ IsSplitMono (F.map f) → IsSplitMono 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 : IsSplitMono (F.map f)
⊢ IsSplitMono f
exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.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 : IsSplitMono f
⊢ IsSplitMono (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
⊢ IsSplitMono f → IsSplitMono (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 : IsSplitMono f
⊢ IsSplitMono (F.map f)
exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)