Documentation

InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Tensors

Tensors in an enriched category #

Let C be a V-enriched category.

This file defines a pretensor of v : V and c : C as an object obj : C, together with a morphism cone : v ⟶ (x ⟶[V] obj). Based on this, it defines a family of morphisms coneNatTrans : (obj ⟶[V] y) ⟶ (x ⟶[V] y)^v.

It defines a tensor "v ⊗ c" as a pretensor where the coneNatTrans morphisms are isomorphisms. Subsequently, it constructs the left and right whiskering of morphisms.

Most of this file is devoted to showing that tensoring, together with whiskering, constitutes a V-enriched functor tensor_bifunc : V ⊗ C ⟶ C.

source
structure CategoryTheory.Enriched.Pretensor {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] (v : V) (x : C) :
Type (max u₁ v)

A pretensor is an object obj : C, together with a morphism cone : v ⟶ (x ⟶[V] obj).

Instances For
    source
    def CategoryTheory.Enriched.Pretensor.coneNatTrans {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} (vx : Pretensor v x) (y : C) :
    Ehom V C vx.obj y ⟶ Ihom V v (Ehom V C x y)

    The family of morphisms from vx ⟶[V] y to (x ⟶[V] y)^v

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Enriched.Pretensor.uncurry_coneNatTrans {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} (vx : Pretensor v x) (y : C) :
      MonoidalClosed.uncurry (vx.coneNatTrans y) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight vx.cone (vx.obj ⟶[V] y)) (eComp V x vx.obj y)

      Since Pretensor.coneNatTrans is defined by currying, its uncurrying can be simplified.

      source
      structure CategoryTheory.Enriched.Tensor {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] (v : V) (x : C) extends CategoryTheory.Enriched.Pretensor v x :
      Type (max u₁ v)

      A Tensor is a Pretensor such that coneNatTransInv is an inverse to coneNatTrans.

      Instances For
        source
        instance CategoryTheory.Enriched.Tensor.instIsIsoConeNatTrans {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} {vx : Tensor v x} {y : C} :
        IsIso (vx.coneNatTrans y)

        For a tensor, the morphisms Pretensor.coneNatTrans are isomorphisms, with inverses given by Tensor.coneNatTransInv.

        source
        instance CategoryTheory.Enriched.Tensor.instIsIsoConeNatTransInv {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} {vx : Tensor v x} {y : C} :
        IsIso (vx.coneNatTransInv y)

        For a tensor, the morphisms Tensor.coneNatTransInv are isomorphisms, with inverses given by Pretensor.coneNatTrans.

        source
        def CategoryTheory.Enriched.Tensor.whiskerRight (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {v w : V} (vx : Tensor v x) (wx : Tensor w x) :
        Ehom V V v w ⟶ Ehom V C vx.obj wx.obj

        Whiskering on the right by x : C turns a morphism v ⟶ w into a morphism v ⊗ x ⟶ w ⊗ x.

        Equations
        Instances For
          source
          theorem CategoryTheory.Enriched.Tensor.whiskerRight_coneNatTrans (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v w : V} {x : C} (vx : Tensor v x) (wx : Tensor w x) :
          CategoryStruct.comp (whiskerRight V vx wx) (vx.coneNatTrans wx.obj) = (ihom v).map wx.cone

          Since right whiskering is defined by postcomposition with Tensor.coneNatTransInv, its postcomposition with Pretensor.coneNatTrans can be simplified.

          source
          theorem CategoryTheory.Enriched.Tensor.whiskerRight_id (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} (vx : Tensor v x) :
          CategoryStruct.comp (eId V v) (whiskerRight V vx vx) = eId V vx.obj

          Whiskering the identity on the right yields the identity again.

          source
          theorem CategoryTheory.Enriched.Tensor.cone_comp_whiskerRight_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Tensor w x) (vx : Tensor v x) :
          CategoryStruct.comp (MonoidalCategoryStruct.tensorHom wx.cone (whiskerRight V wx vx)) (eComp V x wx.obj vx.obj) = CategoryStruct.comp ((ihom.ev w).app v) vx.cone

          An auxiliary lemma for what is to come.

          source
          theorem CategoryTheory.Enriched.Tensor.whiskerRight_comp (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {u v w : V} {x : C} (ux : Tensor u x) (vx : Tensor v x) (wx : Tensor w x) :
          CategoryStruct.comp (eComp V u v w) (whiskerRight V ux wx) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (whiskerRight V ux vx) (whiskerRight V vx wx)) (eComp V ux.obj vx.obj wx.obj)

          Whiskering on the right commutes with morphism composition.

          source
          def CategoryTheory.Enriched.Tensor.whiskerLeft (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] {x y : C} {v : V} (vx : Tensor v x) (vy : Tensor v y) :
          Ehom V C x y ⟶ Ehom V C vx.obj vy.obj

          Whiskering on the left by v : V turns a morphism x ⟶ y into a morphism v ⊗ x ⟶ v ⊗ y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem CategoryTheory.Enriched.Tensor.whiskerLeft_coneNatTrans_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] {x y : C} {v : V} (vx : Tensor v x) (vy : Tensor v y) :
            CategoryStruct.comp (whiskerLeft V vx vy) (vx.coneNatTrans vy.obj) = MonoidalClosed.curry (CategoryStruct.comp (β_ v (x ⟶[V] y)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (x ⟶[V] y) vy.cone) (eComp V x y vy.obj)))

            Since left whiskering is defined by postcomposition with Tensor.coneNatTransInv, its postcomposition with Pretensor.coneNatTrans can be simplified.

            source
            theorem CategoryTheory.Enriched.Tensor.whiskerLeft_id (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] {v : V} {x : C} (vx : Tensor v x) :
            CategoryStruct.comp (eId V x) (whiskerLeft V vx vx) = eId V vx.obj

            Whiskering the identity on the left yields the identity again.

            source
            theorem CategoryTheory.Enriched.Tensor.cone_comp_whiskerLeft_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] {x y : C} {v : V} (vx : Tensor v x) (vy : Tensor v y) :
            CategoryStruct.comp (β_ (Ehom V C x y) v).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom vx.cone (whiskerLeft V vx vy)) (eComp V x vx.obj vy.obj)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Ehom V C x y) vy.cone) (eComp V x y vy.obj)

            An auxiliary lemma for what is to come.

            source
            theorem CategoryTheory.Enriched.Tensor.whiskerLeft_comp (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] {v : V} {x y z : C} (vx : Tensor v x) (vy : Tensor v y) (vz : Tensor v z) :
            CategoryStruct.comp (eComp V x y z) (whiskerLeft V vx vz) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (whiskerLeft V vx vy) (whiskerLeft V vy vz)) (eComp V vx.obj vy.obj vz.obj)

            Whiskering on the left commutes with morphism composition.

            source
            theorem CategoryTheory.Enriched.Tensor.whiskerRight_right_eq_whiskerLeft_left (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] {v w : V} {x y : C} (vx : Tensor v x) (wx : Tensor w x) (vy : Tensor v y) (wy : Tensor w y) :
            CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (whiskerRight V vx wx) (whiskerLeft V wx wy)) (eComp V vx.obj wx.obj wy.obj) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (whiskerRight V vy wy) (whiskerLeft V vx vy)) (CategoryStruct.comp (β_ (Ehom V C vy.obj wy.obj) (Ehom V C vx.obj vy.obj)).hom (eComp V vx.obj vy.obj wy.obj))

            Right whiskering commutes with left whiskering.

            source
            class CategoryTheory.Enriched.Tensor.TensoredCategory (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] [SymmetricCategory V] (C : Type v) [EnrichedCategory V C] :
            Type (max (max u u₁) v)
            • tensor (v : V) (x : C) : Tensor v x
            Instances
              source
              def CategoryTheory.Enriched.Tensor.tensor_bifunc (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [SymmetricCategory V] [TensoredCategory V C] :
              EnrichedFunctor V (V ⊗[V] C) C

              Tensoring, together with whiskering, constitutes a V-enriched functor tensor_bifunc : V ⊗ C ⟶ C -

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