Documentation

Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

The natural monoidal structure on any category with finite (co)products. #

A category with a monoidal structure provided in this way is sometimes called a (co)cartesian category, although this is also sometimes used to mean a finitely complete category. (See .)

As this works with either products or coproducts, and sometimes we want to think of a different monoidal structure entirely, we don't set up either construct as an instance.

Implementation #

We had previously chosen to rely on HasTerminal and HasBinaryProducts instead of HasBinaryProducts, because we were later relying on the definitional form of the tensor product. Now that has_limit has been refactored to be a Prop, this issue is irrelevant and we could simplify the construction here.

See CategoryTheory.monoidalOfChosenFiniteProducts for a variant of this construction which allows specifying a particular choice of terminal object and binary products.

source
def CategoryTheory.monoidalOfHasFiniteProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] :
CategoryTheory.MonoidalCategory C

A category with a terminal object and binary products has a natural monoidal structure.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorObj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) :
    CategoryTheory.MonoidalCategory.tensorObj X Y = (X ⨯ Y)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
    CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.Limits.prod.map f g
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerLeft (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) {Y : C} {Z : C} (f : Y ⟶ Z) :
    CategoryTheory.MonoidalCategory.whiskerLeft X f = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) :
    CategoryTheory.MonoidalCategory.whiskerRight f Z = CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Z)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :
    (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.Limits.prod.snd
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :
    (CategoryTheory.MonoidalCategory.leftUnitor X).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X) (CategoryTheory.CategoryStruct.id X)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :
    (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.Limits.prod.fst
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :
    (CategoryTheory.MonoidalCategory.rightUnitor X).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.terminal.from X)
    source
    theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) (Z : C) :
    (CategoryTheory.MonoidalCategory.associator X Y Z).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
    source
    theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) (Z : C) :
    (CategoryTheory.MonoidalCategory.associator X Y Z).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
    source
    @[simp]
    theorem CategoryTheory.symmetricOfHasFiniteProducts_braiding (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) :
    β_ X Y = CategoryTheory.Limits.prod.braiding X Y
    source
    def CategoryTheory.symmetricOfHasFiniteProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] :
    CategoryTheory.SymmetricCategory C

    The monoidal structure coming from finite products is symmetric.

    Equations
    Instances For
      source
      def CategoryTheory.monoidalOfHasFiniteCoproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] :
      CategoryTheory.MonoidalCategory C

      A category with an initial object and binary coproducts has a natural monoidal structure.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorObj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) (Y : C) :
        CategoryTheory.MonoidalCategory.tensorObj X Y = (X ⨿ Y)
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
        CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.Limits.coprod.map f g
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {Y : C} {Z : C} (f : Y ⟶ Z) :
        CategoryTheory.MonoidalCategory.whiskerLeft X f = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) :
        CategoryTheory.MonoidalCategory.whiskerRight f Z = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Z)
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) :
        (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to X) (CategoryTheory.CategoryStruct.id X)
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) :
        (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.initial.to X)
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) :
        (CategoryTheory.MonoidalCategory.leftUnitor X).inv = CategoryTheory.Limits.coprod.inr
        source
        @[simp]
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) :
        (CategoryTheory.MonoidalCategory.rightUnitor X).inv = CategoryTheory.Limits.coprod.inl
        source
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) (Y : C) (Z : C) :
        (CategoryTheory.MonoidalCategory.associator X Y Z).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
        source
        theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) (Y : C) (Z : C) :
        (CategoryTheory.MonoidalCategory.associator X Y Z).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)
        source
        @[simp]
        theorem CategoryTheory.symmetricOfHasFiniteCoproducts_braiding (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P : C) (Q : C) :
        β_ P Q = CategoryTheory.Limits.coprod.braiding P Q
        source
        def CategoryTheory.symmetricOfHasFiniteCoproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] :
        CategoryTheory.SymmetricCategory C

        The monoidal structure coming from finite coproducts is symmetric.

        Equations
        Instances For