case mp.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift sq

case mpr.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift sq
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)
constructor <;> intro <;> constructor <;> intro f g sq
case mp.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X).symm f) (G.map i) p (↑(homEquiv adj B Y).symm g))
case mp.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift sq
rw [← sq.left_adjoint_hasLift_iff adj]
no goals
case mp.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X).symm f) (G.map i) p (↑(homEquiv adj B Y).symm g))
infer_instance
case mpr.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X) f) i (F.map p) (↑(homEquiv adj B Y) g))
case mpr.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift sq
rw [← sq.right_adjoint_hasLift_iff adj]
no goals
case mpr.sq_hasLift
C : Type u_3
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X) f) i (F.map p) (↑(homEquiv adj B Y) g))
infer_instance