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 (↑(CategoryTheory.Adjunction.homEquiv adj A X) u) i (F.map p)
(↑(CategoryTheory.Adjunction.homEquiv adj 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
(_ :
CategoryTheory.CommSq (↑(CategoryTheory.Adjunction.homEquiv adj A X) u) i (F.map p)
(↑(CategoryTheory.Adjunction.homEquiv adj B Y) v))
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.
Instances For
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 (↑(CategoryTheory.Adjunction.homEquiv adj A X) u) i (F.map p)
(↑(CategoryTheory.Adjunction.homEquiv adj B Y) v)) ↔ 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
(_ :
CategoryTheory.CommSq (↑(CategoryTheory.Adjunction.homEquiv adj A X) u) i (F.map p)
(↑(CategoryTheory.Adjunction.homEquiv adj B Y) v))
Equations
- One or more equations did not get rendered due to their size.
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 (↑(CategoryTheory.Adjunction.homEquiv adj A X).symm u) (G.map i) p
(↑(CategoryTheory.Adjunction.homEquiv adj 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
(_ :
CategoryTheory.CommSq (↑(CategoryTheory.Adjunction.homEquiv adj A X).symm u) (G.map i) p
(↑(CategoryTheory.Adjunction.homEquiv adj B Y).symm v))
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.
Instances For
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 (↑(CategoryTheory.Adjunction.homEquiv adj A X).symm u) (G.map i) p
(↑(CategoryTheory.Adjunction.homEquiv adj B Y).symm v)) ↔ 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
(_ :
CategoryTheory.CommSq (↑(CategoryTheory.Adjunction.homEquiv adj A X).symm u) (G.map i) p
(↑(CategoryTheory.Adjunction.homEquiv adj B Y).symm v))
Equations
- One or more equations did not get rendered due to their size.
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)