Documentation

Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Preservation of Kan extensions #

Given functors F : A ⥤ B, L : B ⥤ C, and G : B ⥤ D, we introduce a typeclass G.PreservesLeftKanExtension F L which encodes the fact that the left Kan extension of F along L is preserved by the functor G.

When the Kan extension is pointwise, it suffices that G preserves (co)limits of the relevant diagrams.

We introduce the dual typeclass G.PreservesRightKanExtension.

G.PreservesLeftKanExtension F L asserts that G preserves all left Kan extensions of F along L. See PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension for a constructor taking a single left Kan extension as input.

Instances

    Alternative constructor for PreservesLeftKanExtension, phrased in terms of LeftExtension.IsUniversal instead. See PreservesLeftKanExtension.mk_of_preserves_isUniversal for a similar constructor taking as input a single LeftExtension.

    Show that G preserves left Kan extensions if it maps some left Kan extension to a left Kan extension.

    Show that G preserves left Kan extensions if it maps some left Kan extension to a left Kan extension, phrased in terms of IsUniversal.

    G.PreservesLeftKanExtensionAt F L c asserts that G preserves all pointwise left Kan extensions of F along L at the point c.

    Instances
      @[reducible, inline]

      G.PreservesLeftKanExtension F L asserts that G preserves all pointwise left Kan extensions of F along L.

      Equations
      Instances For

        Given a pointwise left Kan extension of F along L at c, exhibits (LeftExtension.whiskerRight L F G).obj E as a pointwise left Kan extension of F ⋙ G along L at c.

        Equations
        Instances For

          Given a pointwise left Kan extension of F along L, exhibits (LeftExtension.whiskerRight L F G).obj E as a pointwise left Kan extension of F ⋙ G along L.

          Equations
          Instances For

            The cocone at a point of the whiskering right by Gof an extension is isomorphic to the action of G on the cocone at that point for the original extension.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              If G preserves any pointwise left Kan extension of F along L at c, then it preserves all of them.

              Extract an isomorphism (leftKanExtension L F) ⋙ G ≅ leftKanExtension L (F ⋙ G) when G preserves left Kan extensions.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                A functor that preserves the colimit of CostructuredArrow.proj L c ⋙ F preserves the pointwise left Kan extension of F along L at c.

                If there is a pointwise left Kan extension of F along L, and if G preserves them, then G preserves left Kan extensions of F along L.

                Extract an isomorphism (pointwiseLeftKanExtension L F) ⋙ G ≅ pointwiseLeftKanExtension L (F ⋙ G) when G preserves left Kan extensions.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[reducible, inline]

                  G.PreservesLeftKanExtensions L means that G : B ⥤ D preserves all left Kan extensions along L : A ⥤ C of every functor A ⥤ B.

                  Equations
                  Instances For
                    @[reducible, inline]

                    G.PreservesPointwiseLeftKanExtensions L means that G : B ⥤ D preserves all pointwise left Kan extensions along L : A ⥤ C of every functor A ⥤ B.

                    Equations
                    Instances For

                      Commuting a functor that preserves left Kan extensions with the lan functor.

                      Equations
                      Instances For

                        G.PreservesRightKanExtension F L asserts that G preserves all right Kan extensions of F along L. See PreservesRightKanExtension.mk_of_preserves_isRightKanExtension for a constructor taking a single right Kan extension as input.

                        Instances

                          Alternative constructor for PreservesRightKanExtension, phrased in terms of RightExtension.IsUniversal instead. See PreservesRightKanExtension.mk_of_preserves_isUniversal for a similar constructor taking as input a single RightExtension.

                          Show that G preserves right Kan extensions if it maps some right Kan extension to a right Kan extension.

                          Show that G preserves right Kan extensions if it maps some right Kan extension to a left Kan extension, phrased in terms of IsUniversal.

                          G.PreservesRightKanExtensionAt F L c asserts that G preserves all right pointwise right Kan extensions of F along L at c.

                          Instances
                            @[reducible, inline]

                            G.PreservesRightKanExtensions L asserts that G preserves all pointwise right Kan extensions of F along L for every F.

                            Equations
                            Instances For

                              Given a pointwise right Kan extension of F along L at c, exhibits (RightExtension.whiskerRight L F G).obj E as a pointwise right Kan extension of F ⋙ G along L at c.

                              Equations
                              Instances For

                                Given a pointwise right Kan extension of F along L, exhibits (RightExtension.whiskerRight L F G).obj E as a pointwise right Kan extension of F ⋙ G at L.

                                Equations
                                Instances For

                                  The cone at a point of the whiskering right by Gof an extension is isomorphic to the action of G on the cone at that point for the original extension.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    If G preserves any pointwise right Kan extension of F along L at c, then it preserves all of them.

                                    Extract an isomorphism rightKanExtension L F ⋙ G ≅ rightKanExtension L (F ⋙ G) when G preserves right Kan extensions.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      A functor that preserves the limit of (StructuredArrow.proj L c ⋙ F) preserves the pointwise right Kan extension of F along L at c.

                                      If there is a pointwise right Kan extension of F along L, and if G preserves them, then G preserves right Kan extensions of F along L.

                                      Extract an isomorphism L.pointwiseRightKanExtension F ⋙ G ≅ L.pointwiseRightKanExtension (F ⋙ G) when G preserves right Kan extensions.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[reducible, inline]

                                        G.PreservesRightKanExtensions L means that G : B ⥤ D preserves all right Kan extensions along L : A ⥤ C of every functor A ⥤ B.

                                        Equations
                                        Instances For
                                          @[reducible, inline]

                                          G.PreservesPointwiseRightKanExtensions L means that G : B ⥤ D preserves all pointwise right Kan extensions along L : A ⥤ C of every functor A ⥤ B.

                                          Equations
                                          Instances For

                                            Commuting a functor that preserves right Kan extensions with the ran functor.

                                            Equations
                                            Instances For