Documentation

Mathlib.CategoryTheory.Functor.KanExtension.AdjunctionPreserves

Adjoint functors preserve Kan extensions #

In this file, it is shown that left adjoint functors preserve left Kan extensions, and that right adjoint functors preserve right Kan extensions. In particuliar, this applies to equivalences of categories.

source
def CategoryTheory.Adjunction.leftExtensionPostCompose₂RightAdjoint {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) :
Functor (L.LeftExtension (F.comp G₁)) (L.LeftExtension F)

The right adjoint of LeftExtension.postcompose₂ L F G₁ when G₁ is part of an adjunction adj : G₁ ⊣ G₂.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Adjunction.leftExtensionPostCompose₂RightAdjoint_obj_hom_app {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) (X : Comma (Functor.fromPUnit (F.comp G₁)) ((Functor.whiskeringLeft C D H₂).obj L)) (X✝ : C) :
    ((adj.leftExtensionPostCompose₂RightAdjoint F L).obj X).hom.app X✝ = CategoryStruct.comp (adj.unit.app (F.obj X✝)) (G₂.map (X.hom.app X✝))
    source
    @[simp]
    theorem CategoryTheory.Adjunction.leftExtensionPostCompose₂RightAdjoint_obj_right_map {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) (X : Comma (Functor.fromPUnit (F.comp G₁)) ((Functor.whiskeringLeft C D H₂).obj L)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
    ((adj.leftExtensionPostCompose₂RightAdjoint F L).obj X).right.map f = G₂.map (X.right.map f)
    source
    @[simp]
    theorem CategoryTheory.Adjunction.leftExtensionPostCompose₂RightAdjoint_map_right_app {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) {X Y : Comma (Functor.fromPUnit (F.comp G₁)) ((Functor.whiskeringLeft C D H₂).obj L)} (φ : X ⟶ Y) (X✝ : D) :
    ((adj.leftExtensionPostCompose₂RightAdjoint F L).map φ).right.app X✝ = G₂.map (φ.right.app X✝)
    source
    @[simp]
    theorem CategoryTheory.Adjunction.leftExtensionPostCompose₂RightAdjoint_obj_right_obj {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) (X : Comma (Functor.fromPUnit (F.comp G₁)) ((Functor.whiskeringLeft C D H₂).obj L)) (X✝ : D) :
    ((adj.leftExtensionPostCompose₂RightAdjoint F L).obj X).right.obj X✝ = G₂.obj (X.right.obj X✝)
    source
    def CategoryTheory.Adjunction.leftExtensionPostcompose₂ {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) :
    Functor.LeftExtension.postcompose₂ L F G₁ ⊣ adj.leftExtensionPostCompose₂RightAdjoint F L

    The adjunction exhibiting that LeftExtension.postcompose₂ L F G₁ has a right adjoint when G₁ has.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Adjunction.preservesLeftKanExtension {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₁) (L : Functor C D) :
      G₁.PreservesLeftKanExtension F L
      source
      def CategoryTheory.Adjunction.rightExtensionPostCompose₂LeftAdjoint {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) :
      Functor (L.RightExtension (F.comp G₂)) (L.RightExtension F)

      The left adjoint of RightExtension.postcompose₂ L F G₂ when G₂ is part of an adjunction adj : G₁ ⊣ G₂.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Adjunction.rightExtensionPostCompose₂LeftAdjoint_map_left_app {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) {X Y : Comma ((Functor.whiskeringLeft C D H₁).obj L) (Functor.fromPUnit (F.comp G₂))} (φ : X ⟶ Y) (X✝ : D) :
        ((adj.rightExtensionPostCompose₂LeftAdjoint F L).map φ).left.app X✝ = G₁.map (φ.left.app X✝)
        source
        @[simp]
        theorem CategoryTheory.Adjunction.rightExtensionPostCompose₂LeftAdjoint_obj_left_obj {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) (X : Comma ((Functor.whiskeringLeft C D H₁).obj L) (Functor.fromPUnit (F.comp G₂))) (X✝ : D) :
        ((adj.rightExtensionPostCompose₂LeftAdjoint F L).obj X).left.obj X✝ = G₁.obj (X.left.obj X✝)
        source
        @[simp]
        theorem CategoryTheory.Adjunction.rightExtensionPostCompose₂LeftAdjoint_obj_hom_app {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) (X : Comma ((Functor.whiskeringLeft C D H₁).obj L) (Functor.fromPUnit (F.comp G₂))) (X✝ : C) :
        ((adj.rightExtensionPostCompose₂LeftAdjoint F L).obj X).hom.app X✝ = CategoryStruct.comp (G₁.map (X.hom.app X✝)) (adj.counit.app (F.obj X✝))
        source
        @[simp]
        theorem CategoryTheory.Adjunction.rightExtensionPostCompose₂LeftAdjoint_obj_left_map {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) (X : Comma ((Functor.whiskeringLeft C D H₁).obj L) (Functor.fromPUnit (F.comp G₂))) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
        ((adj.rightExtensionPostCompose₂LeftAdjoint F L).obj X).left.map f = G₁.map (X.left.map f)
        source
        def CategoryTheory.Adjunction.rightExtensionPostcompose₂ {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) :
        adj.rightExtensionPostCompose₂LeftAdjoint F L ⊣ Functor.RightExtension.postcompose₂ L F G₂

        The adjunction exhibiting that RightExtension.postcompose₂ L F G₂ has a left adjoint when G₂ has.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem CategoryTheory.Adjunction.preservesRightKanExtension {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} {G₂ : Functor H₂ H₁} (adj : G₁ ⊣ G₂) (F : Functor C H₂) (L : Functor C D) :
          G₂.PreservesRightKanExtension F L
          source
          instance CategoryTheory.Functor.instPreservesLeftKanExtensionOfIsLeftAdjoint {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₁ : Functor H₁ H₂} [G₁.IsLeftAdjoint] (F : Functor C H₁) (L : Functor C D) :
          G₁.PreservesLeftKanExtension F L
          source
          instance CategoryTheory.Functor.instPreservesRightKanExtensionOfIsRightAdjoint {C : Type u_1} {D : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} H₁] [Category.{v_4, u_4} H₂] {G₂ : Functor H₂ H₁} [G₂.IsRightAdjoint] (F : Functor C H₂) (L : Functor C D) :
          G₂.PreservesRightKanExtension F L