Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Prelax functors #

This file defines lax prefunctors and prelax functors between bicategories. The point of these definitions is to provide some common API that will be helpful in the development of both lax and oplax functors.

Main definitions #

PrelaxFunctorStruct B C:

A PrelaxFunctorStruct F between quivers B and C, such that both have been equipped with quiver structures on the hom-types, consists of

PrelaxFunctor B C:

A prelax functor F between bicategories B and C is a PrelaxFunctorStruct such that the associated prefunctors between the hom types are all functors. In other words, it is a PrelaxFunctorStruct that satisfies

mkOfHomFunctor: constructs a PrelaxFunctor from a map on objects and functors between the corresponding hom types.

structure CategoryTheory.PrelaxFunctorStruct (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a b)] (C : Type u₂) [Quiver C] [(a b : C) → Quiver (a b)] extends Prefunctor :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A PrelaxFunctorStruct between bicategories consists of functions between objects, 1-morphisms, and 2-morphisms. This structure will be extended to define PrelaxFunctor.

  • obj : BC
  • map : {X Y : B} → (X Y)(self.obj X self.obj Y)
  • map₂ : {a b : B} → {f g : a b} → (f g)(self.map f self.map g)

    The action of a lax prefunctor on 2-morphisms.

Instances For
    @[simp]
    theorem CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_obj {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] (F : BC) (F' : (a b : B) → (a b) ⥤q (F a F b)) :
    @[simp]
    theorem CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_map {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] (F : BC) (F' : (a b : B) → (a b) ⥤q (F a F b)) {a : B} {b : B} :
    ∀ (a_1 : a b), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map a_1 = (F' a b).obj a_1
    @[simp]
    theorem CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_map₂ {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] (F : BC) (F' : (a b : B) → (a b) ⥤q (F a F b)) {a : B} {b : B} :
    ∀ {f g : a b} (a_1 : f g), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map₂ a_1 = (F' a b).map a_1
    def CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] (F : BC) (F' : (a b : B) → (a b) ⥤q (F a F b)) :

    Construct a lax prefunctor from a map on objects, and prefunctors between the corresponding hom types.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.PrelaxFunctorStruct.id_map₂ (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a b)] :
      ∀ {a b : B} {f g : a b} (η : f g), (CategoryTheory.PrelaxFunctorStruct.id B).map₂ η = η
      @[simp]

      The identity lax prefunctor.

      Equations
      Instances For
        Equations
        @[simp]
        theorem CategoryTheory.PrelaxFunctorStruct.comp_toPrefunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a b)] (F : CategoryTheory.PrelaxFunctorStruct B C) (G : CategoryTheory.PrelaxFunctorStruct C D) :
        (F.comp G).toPrefunctor = F.toPrefunctor ⋙q G.toPrefunctor
        @[simp]
        theorem CategoryTheory.PrelaxFunctorStruct.comp_map₂ {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a b)] (F : CategoryTheory.PrelaxFunctorStruct B C) (G : CategoryTheory.PrelaxFunctorStruct C D) :
        ∀ {a b : B} {f g : a b} (η : f g), (F.comp G).map₂ η = G.map₂ (F.map₂ η)
        def CategoryTheory.PrelaxFunctorStruct.comp {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a b)] (F : CategoryTheory.PrelaxFunctorStruct B C) (G : CategoryTheory.PrelaxFunctorStruct C D) :

        Composition of lax prefunctors.

        Equations
        • F.comp G = { toPrefunctor := F.toPrefunctor ⋙q G.toPrefunctor, map₂ := fun {a b : B} {f g : a b} (η : f g) => G.map₂ (F.map₂ η) }
        Instances For
          structure CategoryTheory.PrelaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctorStruct :
          Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

          A prelax functor between bicategories is a lax prefunctor such that map₂ is a functor. This structure will be extended to define LaxFunctor and OplaxFunctor.

          Instances For
            @[simp]

            Prelax functors preserves identity 2-morphisms.

            @[simp]
            theorem CategoryTheory.PrelaxFunctor.map₂_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} {h : a b} (η : f g) (θ : g h) :
            self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)

            Prelax functors preserves compositions of 2-morphisms.

            theorem CategoryTheory.PrelaxFunctor.map₂_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} {h : a b} (η : f g) (θ : g h✝) {Z : self.obj a self.obj b} (h : self.map h✝ Z) :
            @[simp]
            theorem CategoryTheory.PrelaxFunctor.mkOfHomFunctors_toPrelaxFunctorStruct {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : BC) (F' : (a b : B) → CategoryTheory.Functor (a b) (F a F b)) :
            (CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').toPrelaxFunctorStruct = CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F fun (a b : B) => (F' a b).toPrefunctor

            Construct a prelax functor from a map on objects, and functors between the corresponding hom types.

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

              The identity prelax functor.

              Equations
              Instances For
                Equations
                @[simp]
                theorem CategoryTheory.PrelaxFunctor.comp_toPrelaxFunctorStruct {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :
                (F.comp G).toPrelaxFunctorStruct = F.comp G.toPrelaxFunctorStruct

                Composition of prelax functors.

                Equations
                • F.comp G = { toPrelaxFunctorStruct := F.comp G.toPrelaxFunctorStruct, map₂_id := , map₂_comp := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.PrelaxFunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) (a : B) (b : B) :
                  ∀ {X Y : a b} (η : X Y), (F.mapFunctor a b).map η = F.map₂ η
                  @[simp]
                  theorem CategoryTheory.PrelaxFunctor.mapFunctor_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) (a : B) (b : B) (f : a b) :
                  (F.mapFunctor a b).obj f = F.map f

                  Function between 1-morphisms as a functor.

                  Equations
                  • F.mapFunctor a b = { obj := fun (f : a b) => F.map f, map := fun {X Y : a b} (η : X Y) => F.map₂ η, map_id := , map_comp := }
                  Instances For
                    @[simp]
                    theorem CategoryTheory.PrelaxFunctor.mkOfHomFunctors_mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : BC) (F' : (a b : B) → CategoryTheory.Functor (a b) (F a F b)) (a : B) (b : B) :
                    (CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').mapFunctor a b = F' a b
                    @[simp]
                    theorem CategoryTheory.PrelaxFunctor.map₂Iso_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) :
                    (F.map₂Iso η).inv = F.map₂ η.inv
                    @[simp]
                    theorem CategoryTheory.PrelaxFunctor.map₂Iso_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) :
                    (F.map₂Iso η).hom = F.map₂ η.hom
                    @[reducible, inline]
                    abbrev CategoryTheory.PrelaxFunctor.map₂Iso {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) :
                    F.map f F.map g

                    A prelaxfunctor F sends 2-isomorphisms η : f ≅ f to 2-isomorphisms F.map f ≅ F.map g.

                    Equations
                    • F.map₂Iso η = (F.mapFunctor a b).mapIso η
                    Instances For
                      instance CategoryTheory.PrelaxFunctor.map₂_isIso {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) [CategoryTheory.IsIso η] :
                      CategoryTheory.IsIso (F.map₂ η)
                      Equations
                      • =
                      @[simp]
                      theorem CategoryTheory.PrelaxFunctor.map₂_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) [CategoryTheory.IsIso η] :
                      F.map₂ (CategoryTheory.inv η) = CategoryTheory.inv (F.map₂ η)
                      theorem CategoryTheory.PrelaxFunctor.map₂_hom_inv_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) {Z : F.obj a F.obj b} (h : F.map f Z) :
                      @[simp]
                      theorem CategoryTheory.PrelaxFunctor.map₂_hom_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) :
                      CategoryTheory.CategoryStruct.comp (F.map₂ η.hom) (F.map₂ η.inv) = CategoryTheory.CategoryStruct.id (F.map f)
                      theorem CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) [CategoryTheory.IsIso η] {Z : F.obj a F.obj b} (h : F.map f Z) :
                      theorem CategoryTheory.PrelaxFunctor.map₂_inv_hom_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) {Z : F.obj a F.obj b} (h : F.map g Z) :
                      @[simp]
                      theorem CategoryTheory.PrelaxFunctor.map₂_inv_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) :
                      CategoryTheory.CategoryStruct.comp (F.map₂ η.inv) (F.map₂ η.hom) = CategoryTheory.CategoryStruct.id (F.map g)
                      theorem CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (η : f g) [CategoryTheory.IsIso η] {Z : F.obj a F.obj b} (h : F.map g Z) :