Documentation

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

Existence of Kan extensions and Kan lifts in bicategories #

We provide the propositional typeclass HasLeftKanExtension f g, which asserts that there exists a left Kan extension of g along f. See CategoryTheory.Bicategory.Kan.IsKan for the definition of left Kan extensions. Under the assumption that HasLeftKanExtension f g, we define the left Kan extension lan f g by using the axiom of choice.

Main definitions #

These notations are inspired by [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006].

TODO #

class CategoryTheory.Bicategory.HasLeftKanExtension {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : a c) :

The existence of a left Kan extension of g along f.

Instances

    The left Kan extension of g along f at the level of structured arrows.

    Equations
    Instances For
      def CategoryTheory.Bicategory.lan {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : a c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] :
      b c

      The left Kan extension of g along f.

      Equations
      Instances For

        f⁺ g is the left Kan extension of g along f.

          b
          △ \
          |   \ f⁺ g
        f |     \
          |       ◿
          a - - - ▷ c
              g
        
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Evidence that the Lan.extension f g is a Kan extension.

          Equations
          Instances For

            The family of 2-morphisms out of the left Kan extension f⁺ g.

            Equations
            Instances For
              class CategoryTheory.Bicategory.Lan.CommuteWith {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : a c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c x) :

              We say that a 1-morphism h commutes with the left Kan extension f⁺ g if the whiskered left extension for f⁺ g by h is a Kan extension of g ≫ h along f.

              Instances

                Evidence that h commutes with the left Kan extension f⁺ g.

                Equations
                Instances For
                  def CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : a c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] (t : CategoryTheory.Bicategory.LeftExtension f g) (H : t.IsKan) {x : B} (h : c x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] :
                  (t.whisker h).IsKan

                  If h commutes with f⁺ g and t is another left Kan extension of g along f, then t.whisker h is a left Kan extension of g ≫ h along f.

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

                    The isomorphism f⁺ (g ≫ h) ≅ f⁺ g ≫ h at the level of structured arrows.

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

                      We say that there exists an absolute left Kan extension of g along f if any 1-morphism h commutes with the left Kan extension f⁺ g.

                      Instances
                        Equations
                        • =
                        class CategoryTheory.Bicategory.HasLeftKanLift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : b a) (g : c a) :

                        The existence of a left kan lift of g along f.

                        Instances

                          The left Kan lift of g along f at the level of structured arrows.

                          Equations
                          Instances For
                            def CategoryTheory.Bicategory.lanLift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : b a) (g : c a) [CategoryTheory.Bicategory.HasLeftKanLift f g] :
                            c b

                            The left Kan lift of g along f.

                            Equations
                            Instances For

                              f₊ g is the left Kan lift of g along f.

                                          b
                                        ◹ |
                                 f₊ g /   |
                                    /     | f
                                  /       ▽
                                c - - - ▷ a
                                     g
                              
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Evidence that the LanLift.lift f g is a Kan lift.

                                Equations
                                Instances For

                                  The family of 2-morphisms out of the left Kan lift f₊ g.

                                  Equations
                                  Instances For
                                    class CategoryTheory.Bicategory.LanLift.CommuteWith {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : b a) (g : c a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x c) :

                                    We say that a 1-morphism h commutes with the left Kan lift f₊ g if the whiskered left lift for f₊ g by h is a Kan lift of h ≫ g along f.

                                    Instances

                                      Evidence that h commutes with the left Kan lift f₊ g.

                                      Equations
                                      Instances For
                                        def CategoryTheory.Bicategory.LanLift.CommuteWith.isKanWhisker {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : b a) (g : c a) [CategoryTheory.Bicategory.HasLeftKanLift f g] (t : CategoryTheory.Bicategory.LeftLift f g) (H : t.IsKan) {x : B} (h : x c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] :
                                        (t.whisker h).IsKan

                                        If h commutes with f₊ g and t is another left Kan lift of g along f, then t.whisker h is a left Kan lift of h ≫ g along f.

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

                                          The isomorphism f₊ (h ≫ g) ≅ h ≫ f₊ g at the level of structured arrows.

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

                                            We say that there exists an absolute left Kan lift of g along f if any 1-morphism h commutes with the left Kan lift f₊ g.

                                            Instances
                                              Equations
                                              • =