Documentation

Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Lifting properties and parametrized adjunctions #

If we have a parametrized adjunction adj₂ : F ⊣₂ G, sq₁₂ : F.PushoutObjObj f₁ f₂ and sq₁₃ : G.PullbackObjObj f₁ f₃, we show that sq₁₂.ι has the left lifting property with respect to f₃ if and only if f₂ has the left lifting property with respect to sq₁₃.π: this is the lemma ParametrizedAdjunction.hasLiftingProperty_iff.

source
noncomputable def CategoryTheory.ParametrizedAdjunction.arrowHomEquiv {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) :
(Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) ≃ (Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π)

Given a parametrized adjunction F ⊣₂ G between bifunctors, and structures sq₁₂ : F.PushoutObjObj f₁ f₂ and sq₁₃ : G.PullbackObjObj f₁ f₃, there are as many commutative squares with left map sq₁₂.ι and right map f₃ as commutative squares with left map f₂ and right map sq₁₃.π.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) :
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β).right = adj₂.homEquiv.symm (CategoryStruct.comp (Arrow.Hom.right β) sq₁₃.snd)
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) :
    ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).left = adj₂.homEquiv (CategoryStruct.comp sq₁₂.inl (Arrow.Hom.left α))
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) :
    CategoryStruct.comp (Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)) sq₁₃.fst = adj₂.homEquiv (CategoryStruct.comp sq₁₂.inr (Arrow.Hom.left α))
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z) :
    CategoryStruct.comp (Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)) (CategoryStruct.comp sq₁₃.fst h) = CategoryStruct.comp (adj₂.homEquiv (CategoryStruct.comp sq₁₂.inr (Arrow.Hom.left α))) h
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) :
    CategoryStruct.comp (Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)) sq₁₃.snd = adj₂.homEquiv (Arrow.Hom.right α)
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) {Z : C₂} (h : (G.obj (Opposite.op Y₁)).obj Y₃ ⟶ Z) :
    CategoryStruct.comp (Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)) (CategoryStruct.comp sq₁₃.snd h) = CategoryStruct.comp (adj₂.homEquiv (Arrow.Hom.right α)) h
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) :
    CategoryStruct.comp sq₁₂.inl (Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) = adj₂.homEquiv.symm (Arrow.Hom.left β)
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) {Z : C₃} (h : (Arrow.mk f₃).left ⟶ Z) :
    CategoryStruct.comp sq₁₂.inl (CategoryStruct.comp (Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) h) = CategoryStruct.comp (adj₂.homEquiv.symm (Arrow.Hom.left β)) h
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) :
    CategoryStruct.comp sq₁₂.inr (Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) = adj₂.homEquiv.symm (CategoryStruct.comp (Arrow.Hom.right β) sq₁₃.fst)
    source
    @[simp]
    theorem CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π) {Z : C₃} (h : (Arrow.mk f₃).left ⟶ Z) :
    CategoryStruct.comp sq₁₂.inr (CategoryStruct.comp (Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) h) = CategoryStruct.comp (adj₂.homEquiv.symm (CategoryStruct.comp (Arrow.Hom.right β) sq₁₃.fst)) h
    source
    noncomputable def CategoryTheory.ParametrizedAdjunction.liftStructEquiv {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) :
    Arrow.LiftStruct α ≃ Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)

    Given a parametrized adjunction F ⊣₂ G between bifunctors, structures sq₁₂ : F.PushoutObjObj f₁ f₂ and sq₁₃ : G.PullbackObjObj f₁ f₃, there are as many liftings for the commutative square given by a map α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃ as there are liftings for the square given by the corresponding map Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃) :
      HasLiftingProperty sq₁₂.ι f₃ ↔ HasLiftingProperty f₂ sq₁₃.π