Documentation

Mathlib.CategoryTheory.Enriched.EnrichedCat

The bicategory of V-enriched categories #

We define the bicategory EnrichedCat V of (bundled) V-enriched categories for a fixed monoidal category V.

Future work #

source
def CategoryTheory.EnrichedCat (V : Type v) [Category.{w, v} V] [MonoidalCategory V] :
Type (max (u + 1) (max u v) w)

Category of V-enriched categories for a monoidal category V.

Equations
Instances For
    source
    @[instance_reducible]
    instance CategoryTheory.EnrichedCat.instCoeSortType (V : Type v) [Category.{w, v} V] [MonoidalCategory V] :
    CoeSort (EnrichedCat V) (Type u)
    Equations
    source
    @[instance_reducible]
    instance CategoryTheory.EnrichedCat.str (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : EnrichedCat V) :
    EnrichedCategory V ↑C
    Equations
    source
    def CategoryTheory.EnrichedCat.of (V : Type v) [Category.{w, v} V] [MonoidalCategory V] (C : Type u) [EnrichedCategory V C] :
    EnrichedCat V

    Construct a bundled EnrichedCat from the underlying type and the typeclass.

    Equations
    Instances For
      source
      def CategoryTheory.EnrichedCat.whiskerLeft {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] (F : EnrichedFunctor V C D) {G H : EnrichedFunctor V D E} (α : G ⟶ H) :
      EnrichedFunctor.comp V F G ⟶ EnrichedFunctor.comp V F H

      Whisker a V-enriched natural transformation on the left.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.EnrichedCat.whiskerLeft_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] (F : EnrichedFunctor V C D) {G H : EnrichedFunctor V D E} (α : G ⟶ H) (X : ForgetEnrichment V C) :
        (whiskerLeft F α).out.app X = α.out.app (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))
        source
        def CategoryTheory.EnrichedCat.whiskerRight {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G : EnrichedFunctor V C D} (α : F ⟶ G) (H : EnrichedFunctor V D E) :
        EnrichedFunctor.comp V F H ⟶ EnrichedFunctor.comp V G H

        Whisker a V-enriched natural transformation on the right.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.EnrichedCat.whiskerRight_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G : EnrichedFunctor V C D} (α : F ⟶ G) (H : EnrichedFunctor V D E) (X : ForgetEnrichment V C) :
          (whiskerRight α H).out.app X = ForgetEnrichment.homOf V (CategoryStruct.comp (ForgetEnrichment.homTo V (α.out.app X)) (H.map (F.obj (ForgetEnrichment.to V X)) (G.obj (ForgetEnrichment.to V X))))
          source
          def CategoryTheory.EnrichedCat.leftUnitor {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) :
          EnrichedFunctor.comp V (EnrichedFunctor.id V C) F ≅ F

          Composing the V-enriched identity functor with any functor is isomorphic to that functor.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.EnrichedCat.leftUnitor_inv_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) :
            (leftUnitor F).inv.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))
            source
            @[simp]
            theorem CategoryTheory.EnrichedCat.leftUnitor_hom_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) :
            (leftUnitor F).hom.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))
            source
            def CategoryTheory.EnrichedCat.rightUnitor {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) :
            EnrichedFunctor.comp V F (EnrichedFunctor.id V D) ≅ F

            Composing any V-enriched functor with the identity functor is isomorphic to the former functor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.EnrichedCat.rightUnitor_inv_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) :
              (rightUnitor F).inv.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))
              source
              @[simp]
              theorem CategoryTheory.EnrichedCat.rightUnitor_hom_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] (F : EnrichedFunctor V C D) (X : ForgetEnrichment V C) :
              (rightUnitor F).hom.out.app X = CategoryStruct.id (ForgetEnrichment.of V (F.obj (ForgetEnrichment.to V X)))
              source
              def CategoryTheory.EnrichedCat.associator {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {E' : Type u₃} [EnrichedCategory V E'] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') :
              EnrichedFunctor.comp V (EnrichedFunctor.comp V F G) H ≅ EnrichedFunctor.comp V F (EnrichedFunctor.comp V G H)

              Composition of V-enriched functors is associative up to isomorphism.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.EnrichedCat.associator_inv_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {E' : Type u₃} [EnrichedCategory V E'] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') (X : ForgetEnrichment V C) :
                (associator F G H).inv.out.app X = CategoryStruct.id (ForgetEnrichment.of V (H.obj (G.obj (F.obj (ForgetEnrichment.to V X)))))
                source
                @[simp]
                theorem CategoryTheory.EnrichedCat.associator_hom_out_app {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {E' : Type u₃} [EnrichedCategory V E'] (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') (X : ForgetEnrichment V C) :
                (associator F G H).hom.out.app X = CategoryStruct.id (ForgetEnrichment.of V (H.obj (G.obj (F.obj (ForgetEnrichment.to V X)))))
                source
                theorem CategoryTheory.EnrichedCat.comp_whiskerRight {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G H : EnrichedFunctor V C D} (α : F ⟶ G) (β : G ⟶ H) (I : EnrichedFunctor V D E) :
                whiskerRight { out := CategoryStruct.comp α.out β.out } I = CategoryStruct.comp (whiskerRight α I) (whiskerRight β I)
                source
                theorem CategoryTheory.EnrichedCat.whisker_exchange {V : Type v} [Category.{w, v} V] [MonoidalCategory V] {C : Type u} [EnrichedCategory V C] {D : Type u₁} [EnrichedCategory V D] {E : Type u₂} [EnrichedCategory V E] {F G : EnrichedFunctor V C D} {H I : EnrichedFunctor V D E} (α : F ⟶ G) (β : H ⟶ I) :
                CategoryStruct.comp (whiskerLeft F β) (whiskerRight α I) = CategoryStruct.comp (whiskerRight α H) (whiskerLeft G β)
                source
                @[instance_reducible]
                instance CategoryTheory.EnrichedCat.bicategory {V : Type v} [Category.{w, v} V] [MonoidalCategory V] :
                Bicategory (EnrichedCat V)

                The bicategory structure on EnrichedCat V for a monoidal category V.

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