mathlib3 documentation

category_theory.lifting_properties.adjunction

Lifting properties and adjunction #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we obtain adjunction.has_lifting_property_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 category_theory.comm_sq.right_adjoint {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : G.obj A X} {v : G.obj B Y} (sq : category_theory.comm_sq u (G.map i) p v) (adj : G F) :
category_theory.comm_sq ((adj.hom_equiv A X) u) i (F.map p) ((adj.hom_equiv 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.

Instances for category_theory.comm_sq.right_adjoint
def category_theory.comm_sq.right_adjoint_lift_struct_equiv {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : G.obj A X} {v : G.obj B Y} (sq : category_theory.comm_sq u (G.map i) p v) (adj : G F) :

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

Equations
theorem category_theory.comm_sq.right_adjoint_has_lift_iff {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : G.obj A X} {v : G.obj B Y} (sq : category_theory.comm_sq u (G.map i) p v) (adj : G F) :

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

@[protected, instance]
def category_theory.comm_sq.right_adjoint.has_lift {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : G.obj A X} {v : G.obj B Y} (sq : category_theory.comm_sq u (G.map i) p v) (adj : G F) [sq.has_lift] :
theorem category_theory.comm_sq.left_adjoint {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : A F.obj X} {v : B F.obj Y} (sq : category_theory.comm_sq u i (F.map p) v) (adj : G F) :
category_theory.comm_sq (((adj.hom_equiv A X).symm) u) (G.map i) p (((adj.hom_equiv 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.

Instances for category_theory.comm_sq.left_adjoint
def category_theory.comm_sq.left_adjoint_lift_struct_equiv {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : A F.obj X} {v : B F.obj Y} (sq : category_theory.comm_sq u i (F.map p) v) (adj : G F) :

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

Equations
theorem category_theory.comm_sq.left_adjoint_has_lift_iff {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : A F.obj X} {v : B F.obj Y} (sq : category_theory.comm_sq u i (F.map p) v) (adj : G F) :

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

@[protected, instance]
def category_theory.comm_sq.left_adjoint.has_lift {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} {A B : C} {X Y : D} {i : A B} {p : X Y} {u : A F.obj X} {v : B F.obj Y} (sq : category_theory.comm_sq u i (F.map p) v) (adj : G F) [sq.has_lift] :
theorem category_theory.adjunction.has_lifting_property_iff {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {G : C D} {F : D C} (adj : G F) {A B : C} {X Y : D} (i : A B) (p : X Y) :