C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝ : StrongEpi f
X Y : D
Z : X ⟶ Y
⊢ ∀ [inst : Mono Z], HasLiftingProperty (F.map f) Z
intro
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z
rw [adj.hasLiftingProperty_iff]
no goals
C : Type u_3
D : Type u_4
inst✝³ : Category C
inst✝² : Category D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
h₁ : Functor.PreservesMonomorphisms F'
h₂ : Functor.PreservesEpimorphisms F
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
infer_instance