Documentation

Mathlib.CategoryTheory.Limits.KanExtension

Kan extensions #

This file defines the right and left Kan extensions of a functor. They exist under the assumption that the target category has enough limits resp. colimits.

The main definitions are Ran ι and Lan ι, where ι : S ⥤ L is a functor. Namely, Ran ι is the right Kan extension, while Lan ι is the left Kan extension, both as functors (S ⥤ D) ⥤ (L ⥤ D).

To access the right resp. left adjunction associated to these, use Ran.adjunction resp. Lan.adjunction.

Projects #

A lot of boilerplate could be generalized by defining and working with pseudofunctors.

source
@[inline, reducible]
abbrev CategoryTheory.Ran.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) (x : L) :
CategoryTheory.Functor (CategoryTheory.StructuredArrow x ι) D

The diagram indexed by Ran.index ι x used to define Ran.

Equations
Instances For
    source
    def CategoryTheory.Ran.cone {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] {ι : CategoryTheory.Functor S L} {F : CategoryTheory.Functor S D} {G : CategoryTheory.Functor L D} (x : L) (f : CategoryTheory.Functor.comp ι G ⟶ F) :
    CategoryTheory.Limits.Cone (CategoryTheory.Ran.diagram ι F x)

    A cone over Ran.diagram ι F x used to define Ran.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Ran.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] {X : L} {Y : L} (f : X ⟶ Y) :
      (CategoryTheory.Ran.loc ι F).toPrefunctor.map f = CategoryTheory.Limits.limit.pre (CategoryTheory.Ran.diagram ι F X) (CategoryTheory.StructuredArrow.map f)
      source
      @[simp]
      theorem CategoryTheory.Ran.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (x : L) :
      (CategoryTheory.Ran.loc ι F).toPrefunctor.obj x = CategoryTheory.Limits.limit (CategoryTheory.Ran.diagram ι F x)
      source
      def CategoryTheory.Ran.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] :
      CategoryTheory.Functor L D

      An auxiliary definition used to define Ran.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Ran.equiv_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (G : CategoryTheory.Functor L D) (f : G ⟶ CategoryTheory.Ran.loc ι F) (x : S) :
        ((CategoryTheory.Ran.equiv ι F G) f).app x = CategoryTheory.CategoryStruct.comp (f.app (ι.toPrefunctor.obj x)) (CategoryTheory.Limits.limit.π (CategoryTheory.Ran.diagram ι F (ι.toPrefunctor.obj x)) (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (ι.toPrefunctor.obj x))))
        source
        @[simp]
        theorem CategoryTheory.Ran.equiv_symm_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (G : CategoryTheory.Functor L D) (f : ((CategoryTheory.whiskeringLeft S L D).toPrefunctor.obj ι).toPrefunctor.obj G ⟶ F) (x : L) :
        ((CategoryTheory.Ran.equiv ι F G).symm f).app x = CategoryTheory.Limits.limit.lift (CategoryTheory.Ran.diagram ι F x) (CategoryTheory.Ran.cone x f)
        source
        def CategoryTheory.Ran.equiv {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (G : CategoryTheory.Functor L D) :
        (G ⟶ CategoryTheory.Ran.loc ι F) ≃ (((CategoryTheory.whiskeringLeft S L D).toPrefunctor.obj ι).toPrefunctor.obj G ⟶ F)

        An auxiliary definition used to define Ran and Ran.adjunction.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ran_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] (G : CategoryTheory.Functor S D) (x : L) :
          ((CategoryTheory.ran ι).toPrefunctor.obj G).toPrefunctor.obj x = CategoryTheory.Limits.limit (CategoryTheory.Ran.diagram ι G x)
          source
          @[simp]
          theorem CategoryTheory.ran_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] (G : CategoryTheory.Functor S D) {X : L} {Y : L} (f : X ⟶ Y) :
          ((CategoryTheory.ran ι).toPrefunctor.obj G).toPrefunctor.map f = CategoryTheory.Limits.limit.pre (CategoryTheory.Ran.diagram ι G X) (CategoryTheory.StructuredArrow.map f)
          source
          @[simp]
          theorem CategoryTheory.ran_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] {Y : CategoryTheory.Functor S D} {Y' : CategoryTheory.Functor S D} (g : Y ⟶ Y') (x : L) :
          ((CategoryTheory.ran ι).toPrefunctor.map g).app x = CategoryTheory.Limits.limit.lift (CategoryTheory.Ran.diagram ι Y' x) { pt := CategoryTheory.Limits.limit (CategoryTheory.Ran.diagram ι Y x), π := CategoryTheory.NatTrans.mk fun (i : CategoryTheory.StructuredArrow x ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre (CategoryTheory.Ran.diagram ι Y x) (CategoryTheory.StructuredArrow.map i.hom)) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Ran.equiv ι Y (CategoryTheory.Ran.loc ι Y)) (CategoryTheory.CategoryStruct.id (CategoryTheory.Ran.loc ι Y))).app i.right) (g.app i.right)) }
          source
          def CategoryTheory.ran {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] :
          CategoryTheory.Functor (CategoryTheory.Functor S D) (CategoryTheory.Functor L D)

          The right Kan extension of a functor.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CategoryTheory.Ran.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] :
            (CategoryTheory.whiskeringLeft S L D).toPrefunctor.obj ι ⊣ CategoryTheory.ran ι

            The adjunction associated to Ran.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem CategoryTheory.Ran.reflective {S : Type u₁} {L : Type u₂} (D : Type u₃) [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [CategoryTheory.Full ι] [CategoryTheory.Faithful ι] [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] :
              CategoryTheory.IsIso (CategoryTheory.Ran.adjunction D ι).counit
              source
              @[inline, reducible]
              abbrev CategoryTheory.Lan.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) (x : L) :
              CategoryTheory.Functor (CategoryTheory.CostructuredArrow ι x) D

              The diagram indexed by Lan.index ι x used to define Lan.

              Equations
              Instances For
                source
                def CategoryTheory.Lan.cocone {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] {ι : CategoryTheory.Functor S L} {F : CategoryTheory.Functor S D} {G : CategoryTheory.Functor L D} (x : L) (f : F ⟶ CategoryTheory.Functor.comp ι G) :
                CategoryTheory.Limits.Cocone (CategoryTheory.Lan.diagram ι F x)

                A cocone over Lan.diagram ι F x used to define Lan.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Lan.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [I : ∀ (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] {x : L} {y : L} (f : x ⟶ y) :
                  (CategoryTheory.Lan.loc ι F).toPrefunctor.map f = CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram ι F y) (CategoryTheory.CostructuredArrow.map f)
                  source
                  @[simp]
                  theorem CategoryTheory.Lan.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [I : ∀ (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] (x : L) :
                  (CategoryTheory.Lan.loc ι F).toPrefunctor.obj x = CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram ι F x)
                  source
                  def CategoryTheory.Lan.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [I : ∀ (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] :
                  CategoryTheory.Functor L D

                  An auxiliary definition used to define Lan.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Lan.equiv_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [I : ∀ (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] (G : CategoryTheory.Functor L D) (f : CategoryTheory.Lan.loc ι F ⟶ G) (x : S) :
                    ((CategoryTheory.Lan.equiv ι F G) f).app x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Lan.diagram ι F (ι.toPrefunctor.obj x)) (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (ι.toPrefunctor.obj x)))) (f.app (ι.toPrefunctor.obj x))
                    source
                    @[simp]
                    theorem CategoryTheory.Lan.equiv_symm_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [I : ∀ (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] (G : CategoryTheory.Functor L D) (f : F ⟶ ((CategoryTheory.whiskeringLeft S L D).toPrefunctor.obj ι).toPrefunctor.obj G) (x : L) :
                    ((CategoryTheory.Lan.equiv ι F G).symm f).app x = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram ι F x) (CategoryTheory.Lan.cocone x f)
                    source
                    def CategoryTheory.Lan.equiv {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [I : ∀ (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] (G : CategoryTheory.Functor L D) :
                    (CategoryTheory.Lan.loc ι F ⟶ G) ≃ (F ⟶ ((CategoryTheory.whiskeringLeft S L D).toPrefunctor.obj ι).toPrefunctor.obj G)

                    An auxiliary definition used to define Lan and Lan.adjunction.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.lan_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (F : CategoryTheory.Functor S D) (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] (F : CategoryTheory.Functor S D) (x : L) :
                      ((CategoryTheory.lan ι).toPrefunctor.obj F).toPrefunctor.obj x = CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram ι F x)
                      source
                      @[simp]
                      theorem CategoryTheory.lan_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (F : CategoryTheory.Functor S D) (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] (F : CategoryTheory.Functor S D) {x : L} {y : L} (f : x ⟶ y) :
                      ((CategoryTheory.lan ι).toPrefunctor.obj F).toPrefunctor.map f = CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram ι F y) (CategoryTheory.CostructuredArrow.map f)
                      source
                      @[simp]
                      theorem CategoryTheory.lan_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (F : CategoryTheory.Functor S D) (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] {X : CategoryTheory.Functor S D} {X' : CategoryTheory.Functor S D} (f : X ⟶ X') (x : L) :
                      ((CategoryTheory.lan ι).toPrefunctor.map f).app x = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram ι X x) { pt := CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram ι X' x), ι := CategoryTheory.NatTrans.mk fun (i : CategoryTheory.CostructuredArrow ι x) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (f.app i.left) (((CategoryTheory.Lan.equiv ι X' (CategoryTheory.Lan.loc ι X')) (CategoryTheory.CategoryStruct.id (CategoryTheory.Lan.loc ι X'))).app i.left)) (CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram ι X' x) (CategoryTheory.CostructuredArrow.map i.hom)) }
                      source
                      def CategoryTheory.lan {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (F : CategoryTheory.Functor S D) (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] :
                      CategoryTheory.Functor (CategoryTheory.Functor S D) (CategoryTheory.Functor L D)

                      The left Kan extension of a functor.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def CategoryTheory.Lan.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (F : CategoryTheory.Functor S D) (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] :
                        CategoryTheory.lan ι ⊣ (CategoryTheory.whiskeringLeft S L D).toPrefunctor.obj ι

                        The adjunction associated to Lan.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem CategoryTheory.Lan.coreflective {S : Type u₁} {L : Type u₂} (D : Type u₃) [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [CategoryTheory.Full ι] [CategoryTheory.Faithful ι] [∀ (F : CategoryTheory.Functor S D) (x : L), CategoryTheory.Limits.HasColimit (CategoryTheory.Lan.diagram ι F x)] :
                          CategoryTheory.IsIso (CategoryTheory.Lan.adjunction D ι).unit