Documentation

Mathlib.CategoryTheory.Bicategory.Extension

Extensions and lifts in bicategories #

We introduce the concept of extensions and lifts within the bicategorical framework. These concepts are defined by commutative diagrams in the (1-)categorical context. Within the bicategorical framework, commutative diagrams are replaced by 2-morphisms. Depending on the orientation of the 2-morphisms, we define both left and right extensions (likewise for lifts). The use of left and right here is a common one in the theory of Kan extensions.

Implementation notes #

We define extensions and lifts as objects in certain comma categories (StructuredArrow for left, and CostructuredArrow for right). See the file CategoryTheory.StructuredArrow for properties about these categories. We introduce some intuitive aliases. For example, LeftExtension.extension is an alias for Comma.right.

References #

@[reducible, inline]
abbrev CategoryTheory.Bicategory.LeftExtension {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : a c) :
Type (max v w)

Triangle diagrams for (left) extensions.

  b
  △ \
  |   \ extension  △
f |     \          | unit
  |       ◿
  a - - - ▷ c
      g
Equations
Instances For
    @[reducible, inline]
    abbrev CategoryTheory.Bicategory.LeftExtension.extension {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} (t : CategoryTheory.Bicategory.LeftExtension f g) :
    b c

    The extension of g along f.

    Equations
    • t.extension = t.right
    Instances For
      @[reducible, inline]

      The 2-morphism filling the triangle diagram.

      Equations
      • t.unit = t.hom
      Instances For
        @[reducible, inline]

        Construct a left extension from a 1-morphism and a 2-morphism.

        Equations
        Instances For
          @[reducible, inline]

          To construct a morphism between left extensions, we need a 2-morphism between the extensions, and to check that it is compatible with the units.

          Equations
          Instances For

            Construct a left extension of g : a ⟶ c from a left extension of g ≫ 𝟙 c.

            Equations
            Instances For

              Whisker a 1-morphism to an extension.

                b
                △ \
                |   \ extension  △
              f |     \          | unit
                |       ◿
                a - - - ▷ c - - - ▷ x
                    g         h
              
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Bicategory.LeftExtension.whisker_extension {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} (t : CategoryTheory.Bicategory.LeftExtension f g) {x : B} (h : c x) :
                (t.whisker h).extension = CategoryTheory.CategoryStruct.comp t.extension h
                @[simp]
                @[simp]
                theorem CategoryTheory.Bicategory.LeftExtension.whiskering_obj {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} {x : B} (h : c x) (t : CategoryTheory.Bicategory.LeftExtension f g) :

                Whiskering a 1-morphism is a functor.

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

                  Define a morphism between left extensions by cancelling the whiskered identities.

                  Equations
                  Instances For
                    def CategoryTheory.Bicategory.LeftExtension.whiskerHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} {s : CategoryTheory.Bicategory.LeftExtension f g} {t : CategoryTheory.Bicategory.LeftExtension f g} (i : s t) {x : B} (h : c x) :
                    s.whisker h t.whisker h

                    Construct a morphism between whiskered extensions.

                    Equations
                    Instances For
                      def CategoryTheory.Bicategory.LeftExtension.whiskerIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} {s : CategoryTheory.Bicategory.LeftExtension f g} {t : CategoryTheory.Bicategory.LeftExtension f g} (i : s t) {x : B} (h : c x) :
                      s.whisker h t.whisker h

                      Construct an isomorphism between whiskered extensions.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_inv_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} (t : CategoryTheory.Bicategory.LeftExtension f g) :
                        t.whiskerOfCompIdIsoSelf.inv.right = (CategoryTheory.Bicategory.rightUnitor t.extension).inv
                        @[simp]
                        theorem CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_hom_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} (t : CategoryTheory.Bicategory.LeftExtension f g) :
                        t.whiskerOfCompIdIsoSelf.hom.right = (CategoryTheory.Bicategory.rightUnitor t.extension).hom

                        The isomorphism between left extensions induced by a right unitor.

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev CategoryTheory.Bicategory.LeftLift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : b a) (g : c a) :
                          Type (max v w)

                          Triangle diagrams for (left) lifts.

                                      b
                                    ◹ |
                             lift /   |      △
                                /     | f    | unit
                              /       ▽
                            c - - - ▷ a
                                 g
                          
                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev CategoryTheory.Bicategory.LeftLift.lift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : CategoryTheory.Bicategory.LeftLift f g) :
                            c b

                            The lift of g along f.

                            Equations
                            • t.lift = t.right
                            Instances For
                              @[reducible, inline]

                              The 2-morphism filling the triangle diagram.

                              Equations
                              • t.unit = t.hom
                              Instances For
                                @[reducible, inline]
                                abbrev CategoryTheory.Bicategory.LeftLift.mk {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (h : c b) (unit : g CategoryTheory.CategoryStruct.comp h f) :

                                Construct a left lift from a 1-morphism and a 2-morphism.

                                Equations
                                Instances For
                                  @[reducible, inline]

                                  To construct a morphism between left lifts, we need a 2-morphism between the lifts, and to check that it is compatible with the units.

                                  Equations
                                  Instances For
                                    Equations

                                    Construct a left lift along g : c ⟶ a from a left lift along 𝟙 c ≫ g.

                                    Equations
                                    Instances For

                                      Whisker a 1-morphism to a lift.

                                                          b
                                                        ◹ |
                                                 lift /   |      △
                                                    /     | f    | unit
                                                  /       ▽
                                      x - - - ▷ c - - - ▷ a
                                           h         g
                                      
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Bicategory.LeftLift.whisker_lift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : CategoryTheory.Bicategory.LeftLift f g) {x : B} (h : x c) :
                                        (t.whisker h).lift = CategoryTheory.CategoryStruct.comp h t.lift
                                        @[simp]
                                        @[simp]
                                        theorem CategoryTheory.Bicategory.LeftLift.whiskering_obj {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} {x : B} (h : x c) (t : CategoryTheory.Bicategory.LeftLift f g) :

                                        Whiskering a 1-morphism is a functor.

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

                                          Define a morphism between left lifts by cancelling the whiskered identities.

                                          Equations
                                          Instances For
                                            def CategoryTheory.Bicategory.LeftLift.whiskerHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : CategoryTheory.Bicategory.LeftLift f g} {t : CategoryTheory.Bicategory.LeftLift f g} (i : s t) {x : B} (h : x c) :
                                            s.whisker h t.whisker h

                                            Construct a morphism between whiskered lifts.

                                            Equations
                                            Instances For
                                              def CategoryTheory.Bicategory.LeftLift.whiskerIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : CategoryTheory.Bicategory.LeftLift f g} {t : CategoryTheory.Bicategory.LeftLift f g} (i : s t) {x : B} (h : x c) :
                                              s.whisker h t.whisker h

                                              Construct an isomorphism between whiskered lifts.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf_hom_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : CategoryTheory.Bicategory.LeftLift f g) :
                                                t.whiskerOfIdCompIsoSelf.hom.right = (CategoryTheory.Bicategory.leftUnitor t.lift).hom
                                                @[simp]
                                                theorem CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf_inv_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : CategoryTheory.Bicategory.LeftLift f g) :
                                                t.whiskerOfIdCompIsoSelf.inv.right = (CategoryTheory.Bicategory.leftUnitor t.lift).inv

                                                The isomorphism between left lifts induced by a left unitor.

                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev CategoryTheory.Bicategory.RightExtension {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a b) (g : a c) :
                                                  Type (max v w)

                                                  Triangle diagrams for (right) extensions.

                                                    b
                                                    △ \
                                                    |   \ extension  | counit
                                                  f |     \          ▽
                                                    |       ◿
                                                    a - - - ▷ c
                                                        g
                                                  
                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]

                                                    The extension of g along f.

                                                    Equations
                                                    • t.extension = t.left
                                                    Instances For
                                                      @[reducible, inline]

                                                      The 2-morphism filling the triangle diagram.

                                                      Equations
                                                      • t.counit = t.hom
                                                      Instances For
                                                        @[reducible, inline]

                                                        Construct a right extension from a 1-morphism and a 2-morphism.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev CategoryTheory.Bicategory.RightExtension.homMk {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a b} {g : a c} {s : CategoryTheory.Bicategory.RightExtension f g} {t : CategoryTheory.Bicategory.RightExtension f g} (η : s.extension t.extension) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) t.counit = s.counit) :
                                                          s t

                                                          To construct a morphism between right extensions, we need a 2-morphism between the extensions, and to check that it is compatible with the counits.

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev CategoryTheory.Bicategory.RightLift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : b a) (g : c a) :
                                                            Type (max v w)

                                                            Triangle diagrams for (right) lifts.

                                                                        b
                                                                      ◹ |
                                                               lift /   |      | counit
                                                                  /     | f    ▽
                                                                /       ▽
                                                              c - - - ▷ a
                                                                   g
                                                            
                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev CategoryTheory.Bicategory.RightLift.lift {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (t : CategoryTheory.Bicategory.RightLift f g) :
                                                              c b

                                                              The lift of g along f.

                                                              Equations
                                                              • t.lift = t.left
                                                              Instances For
                                                                @[reducible, inline]

                                                                The 2-morphism filling the triangle diagram.

                                                                Equations
                                                                • t.counit = t.hom
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev CategoryTheory.Bicategory.RightLift.mk {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} (h : c b) (counit : CategoryTheory.CategoryStruct.comp h f g) :

                                                                  Construct a right lift from a 1-morphism and a 2-morphism.

                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline]
                                                                    abbrev CategoryTheory.Bicategory.RightLift.homMk {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : b a} {g : c a} {s : CategoryTheory.Bicategory.RightLift f g} {t : CategoryTheory.Bicategory.RightLift f g} (η : s.lift t.lift) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η f) t.counit = s.counit) :
                                                                    s t

                                                                    To construct a morphism between right lifts, we need a 2-morphism between the lifts, and to check that it is compatible with the counits.

                                                                    Equations
                                                                    Instances For
                                                                      Equations