Lifting properties and adjunction

In this file, we obtain Adjunction.HasLiftingProperty_iff, which states that when we have an adjunction adj : G ⊣ F between two functors G : C ⥤ D and F : D ⥤ C, then a morphism of the form G.map i has the left lifting property in D with respect to a morphism p if and only the morphism i has the left lifting property in C with respect to F.map p.

theorem CategoryTheory.CommSq.right_adjoint {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y} (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F) : CategoryTheory.CommSq ((adj.homEquiv A X) u) i (F.map p) ((adj.homEquiv B Y) v)

When we have an adjunction G ⊣ F, any commutative square where the left map is of the form G.map i and the right map is p has an "adjoint" commutative square whose left map is i and whose right map is F.map p.

def CategoryTheory.CommSq.rightAdjointLiftStructEquiv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y} (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F) : CategoryTheory.CommSq.LiftStruct sq ≃ CategoryTheory.CommSq.LiftStruct ⋯

The liftings of a commutative are in bijection with the liftings of its (right) adjoint square.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.CommSq.right_adjoint_hasLift_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y} (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F) : CategoryTheory.CommSq.HasLift ⋯ ↔ CategoryTheory.CommSq.HasLift sq

A square has a lifting if and only if its (right) adjoint square has a lifting.

instance CategoryTheory.CommSq.instHasLiftObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCoeEquivHomObjToPrefunctorHomInstFunLikeEquivHomEquivMapRight_adjoint {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y} (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F) [CategoryTheory.CommSq.HasLift sq] : CategoryTheory.CommSq.HasLift ⋯

Equations

• ⋯ = ⋯

theorem CategoryTheory.CommSq.left_adjoint {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y} (sq : CategoryTheory.CommSq u i (F.map p) v) (adj : G ⊣ F) : CategoryTheory.CommSq ((adj.homEquiv A X).symm u) (G.map i) p ((adj.homEquiv B Y).symm v)

When we have an adjunction G ⊣ F, any commutative square where the left map is of the form i and the right map is F.map p has an "adjoint" commutative square whose left map is G.map i and whose right map is p.

def CategoryTheory.CommSq.leftAdjointLiftStructEquiv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y} (sq : CategoryTheory.CommSq u i (F.map p) v) (adj : G ⊣ F) : CategoryTheory.CommSq.LiftStruct sq ≃ CategoryTheory.CommSq.LiftStruct ⋯

The liftings of a commutative are in bijection with the liftings of its (left) adjoint square.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.CommSq.left_adjoint_hasLift_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y} (sq : CategoryTheory.CommSq u i (F.map p) v) (adj : G ⊣ F) : CategoryTheory.CommSq.HasLift ⋯ ↔ CategoryTheory.CommSq.HasLift sq

A (left) adjoint square has a lifting if and only if the original square has a lifting.

instance CategoryTheory.CommSq.instHasLiftObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCoeEquivHomObjToPrefunctorHomInstFunLikeEquivSymmHomEquivMapLeft_adjoint {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {A : C} {B : C} {X : D} {Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y} (sq : CategoryTheory.CommSq u i (F.map p) v) (adj : G ⊣ F) [CategoryTheory.CommSq.HasLift sq] : CategoryTheory.CommSq.HasLift ⋯

Equations

• ⋯ = ⋯

theorem CategoryTheory.Adjunction.hasLiftingProperty_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} (adj : G ⊣ F) {A : C} {B : C} {X : D} {Y : D} (i : A ⟶ B) (p : X ⟶ Y) : CategoryTheory.HasLiftingProperty (G.map i) p ↔ CategoryTheory.HasLiftingProperty i (F.map p)