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 β.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 α.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).right sq₁₃.fst = adj₂.homEquiv (CategoryStruct.comp sq₁₂.inr α.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).right (CategoryStruct.comp sq₁₃.fst h) = CategoryStruct.comp (adj₂.homEquiv (CategoryStruct.comp sq₁₂.inr α.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).right sq₁₃.snd = adj₂.homEquiv α.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α).right (CategoryStruct.comp sq₁₃.snd h) = CategoryStruct.comp (adj₂.homEquiv α.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β).left = adj₂.homEquiv.symm β.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β).left h) = CategoryStruct.comp (adj₂.homEquiv.symm β.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β).left = adj₂.homEquiv.symm (CategoryStruct.comp β.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 ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β).left h) = CategoryStruct.comp (adj₂.homEquiv.symm (CategoryStruct.comp β.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₁₃.π