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.
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
The liftings of a commutative are in bijection with the liftings of its (right) adjoint square.
Equations
- sq.right_adjoint_lift_struct_equiv adj = {to_fun := λ (l : sq.lift_struct), {l := ⇑(adj.hom_equiv B X) l.l, fac_left' := _, fac_right' := _}, inv_fun := λ (l : _.lift_struct), {l := ⇑((adj.hom_equiv B X).symm) l.l, fac_left' := _, fac_right' := _}, left_inv := _, right_inv := _}
A square has a lifting if and only if its (right) adjoint square has a lifting.
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
The liftings of a commutative are in bijection with the liftings of its (left) adjoint square.
Equations
- sq.left_adjoint_lift_struct_equiv adj = {to_fun := λ (l : sq.lift_struct), {l := ⇑((adj.hom_equiv B X).symm) l.l, fac_left' := _, fac_right' := _}, inv_fun := λ (l : _.lift_struct), {l := ⇑(adj.hom_equiv B X) l.l, fac_left' := _, fac_right' := _}, left_inv := _, right_inv := _}
A (left) adjoint square has a lifting if and only if the original square has a lifting.