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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono (F.map f) → Mono 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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono f → Mono (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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono (F.map f) ↔ Mono 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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono (F.map f) → Mono f
exact F.mono_of_mono_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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
h : Mono f
⊢ Mono (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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
⊢ Mono f → Mono (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₁ : PreservesMonomorphisms F
hF₂ : ReflectsMonomorphisms F
h : Mono f
⊢ Mono (F.map f)
exact F.map_mono f