Documentation

Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Lifting properties and parametrized adjunctions #

Let F : C₁ ⥤ C₂ ⥤ C₃. Given morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₂ : X₂ ⟶ Y₂ in C₂, we introduce a structure F.PushoutObjObj f₁ f₂ which contains the data of a pushout of (F.obj Y₁).obj X₂ and (F.obj X₁).obj Y₂ along (F.obj X₁).obj X₂. If sq₁₂ : F.PushoutObjObj f₁ f₂, we have a canonical "inclusion" sq₁₂.ι : sq₁₂.pt ⟶ (F.obj Y₁).obj Y₂.

Similarly, if we have a bifunctor G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂, and morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₃ : X₃ ⟶ Y₃ in C₃, we introduce a structure F.PullbackObjObj f₁ f₃ which contains the data of a pullback of (G.obj (op X₁)).obj X₃ and (G.obj (op Y₁)).obj Y₃ over (G.obj (op X₁)).obj Y₃. If sq₁₃ : F.PullbackObjObj f₁ f₃, we have a canonical projection sq₁₃.π : (G.obj Y₁).obj X₃ ⟶ sq₁₃.pt.

Now, 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
structure CategoryTheory.Functor.PushoutObjObj {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₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) :
Type (max u₃ v₃)

Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃, and morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₂ : X₂ ⟶ Y₂ in C₂, this structure contains the data of a pushout of (F.obj Y₁).obj X₂ and (F.obj X₁).obj Y₂ along (F.obj X₁).obj X₂.

Instances For
    source
    noncomputable def CategoryTheory.Functor.PushoutObjObj.ofHasPushout {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₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] :
    F.PushoutObjObj f₁ f₂

    The PushoutObjObj structure given by the pushout of the colimits API.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_pt {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₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] :
      (ofHasPushout F f₁ f₂).pt = Limits.pushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
      source
      @[simp]
      theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inr {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₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] :
      (ofHasPushout F f₁ f₂).inr = Limits.pushout.inr ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
      source
      @[simp]
      theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inl {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₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] :
      (ofHasPushout F f₁ f₂).inl = Limits.pushout.inl ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
      source
      noncomputable def CategoryTheory.Functor.PushoutObjObj.ι {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
      sq.pt ⟶ (F.obj Y₁).obj Y₂

      The "inclusion" sq.pt ⟶ (F.obj Y₁).obj Y₂ when sq : F.PushoutObjObj f₁ f₂.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.PushoutObjObj.inl_ι {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
        CategoryStruct.comp sq.inl sq.ι = (F.obj Y₁).map f₂
        source
        @[simp]
        theorem CategoryTheory.Functor.PushoutObjObj.inl_ι_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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) {Z : C₃} (h : (F.obj Y₁).obj Y₂ ⟶ Z) :
        CategoryStruct.comp sq.inl (CategoryStruct.comp sq.ι h) = CategoryStruct.comp ((F.obj Y₁).map f₂) h
        source
        @[simp]
        theorem CategoryTheory.Functor.PushoutObjObj.inr_ι {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
        CategoryStruct.comp sq.inr sq.ι = (F.map f₁).app Y₂
        source
        @[simp]
        theorem CategoryTheory.Functor.PushoutObjObj.inr_ι_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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) {Z : C₃} (h : (F.obj Y₁).obj Y₂ ⟶ Z) :
        CategoryStruct.comp sq.inr (CategoryStruct.comp sq.ι h) = CategoryStruct.comp ((F.map f₁).app Y₂) h
        source
        def CategoryTheory.Functor.PushoutObjObj.flip {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
        F.flip.PushoutObjObj f₂ f₁

        Given sq : F.PushoutObjObj f₁ f₂, flipping the pushout square gives sq.flip : F.flip.PushoutObjObj f₂ f₁.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.PushoutObjObj.flip_pt {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
          sq.flip.pt = sq.pt
          source
          @[simp]
          theorem CategoryTheory.Functor.PushoutObjObj.flip_inl {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
          sq.flip.inl = sq.inr
          source
          @[simp]
          theorem CategoryTheory.Functor.PushoutObjObj.flip_inr {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
          sq.flip.inr = sq.inl
          source
          @[simp]
          theorem CategoryTheory.Functor.PushoutObjObj.ι_flip {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) :
          sq.flip.ι = sq.ι
          source
          structure CategoryTheory.Functor.PullbackObjObj {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) :
          Type (max u₂ v₂)

          Given a bifunctor G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂, and morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₃ : X₃ ⟶ Y₃ in C₃, this structure contains the data of a pullback of (G.obj (op X₁)).obj X₃ and (G.obj (op Y₁)).obj Y₃ over (G.obj (op X₁)).obj Y₃.

          Instances For
            source
            noncomputable def CategoryTheory.Functor.PullbackObjObj.ofHasPullback {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] :
            G.PullbackObjObj f₁ f₃

            The PullbackObjObj structure given by the pullback of the limits API.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_fst {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] :
              (ofHasPullback G f₁ f₃).fst = Limits.pullback.fst ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
              source
              @[simp]
              theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_pt {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] :
              (ofHasPullback G f₁ f₃).pt = Limits.pullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
              source
              @[simp]
              theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_snd {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] :
              (ofHasPullback G f₁ f₃).snd = Limits.pullback.snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
              source
              noncomputable def CategoryTheory.Functor.PullbackObjObj.π {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) :
              (G.obj (Opposite.op Y₁)).obj X₃ ⟶ sq.pt

              The projection (G.obj (op Y₁)).obj X₃ ⟶ sq.pt when sq : G.PullbackObjObj f₁ f₃.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Functor.PullbackObjObj.π_fst {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) :
                CategoryStruct.comp sq.π sq.fst = (G.map f₁.op).app X₃
                source
                @[simp]
                theorem CategoryTheory.Functor.PullbackObjObj.π_fst_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z) :
                CategoryStruct.comp sq.π (CategoryStruct.comp sq.fst h) = CategoryStruct.comp ((G.map f₁.op).app X₃) h
                source
                @[simp]
                theorem CategoryTheory.Functor.PullbackObjObj.π_snd {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) :
                CategoryStruct.comp sq.π sq.snd = (G.obj (Opposite.op Y₁)).map f₃
                source
                @[simp]
                theorem CategoryTheory.Functor.PullbackObjObj.π_snd_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) {Z : C₂} (h : (G.obj (Opposite.op Y₁)).obj Y₃ ⟶ Z) :
                CategoryStruct.comp sq.π (CategoryStruct.comp sq.snd h) = CategoryStruct.comp ((G.obj (Opposite.op Y₁)).map f₃) h
                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₁₃.π