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 https://ncatlab.org/nlab/show/cartesian+category.)

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.

TODO #

Once we have cocartesian-monoidal categories, replace monoidalOfHasFiniteCoproducts and symmetricOfHasFiniteCoproducts with CocartesianMonoidalCategory.ofHasFiniteCoproducts.

source
@[implicit_reducible]
noncomputable def CategoryTheory.monoidalOfHasFiniteCoproducts (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] :
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) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y : C) :
    MonoidalCategoryStruct.tensorObj X Y = (X ⨿ Y)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
    MonoidalCategoryStruct.tensorHom f g = Limits.coprod.map f g
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) {Y Z : C} (f : Y ⟶ Z) :
    MonoidalCategoryStruct.whiskerLeft X f = Limits.coprod.map (CategoryStruct.id X) f
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] {X Y : C} (f : X ⟶ Y) (Z : C) :
    MonoidalCategoryStruct.whiskerRight f Z = Limits.coprod.map f (CategoryStruct.id Z)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) :
    (MonoidalCategoryStruct.leftUnitor X).hom = Limits.coprod.desc (Limits.initial.to X) (CategoryStruct.id X)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) :
    (MonoidalCategoryStruct.rightUnitor X).hom = Limits.coprod.desc (CategoryStruct.id X) (Limits.initial.to X)
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) :
    (MonoidalCategoryStruct.leftUnitor X).inv = Limits.coprod.inr
    source
    @[simp]
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) :
    (MonoidalCategoryStruct.rightUnitor X).inv = Limits.coprod.inl
    source
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y Z : C) :
    (MonoidalCategoryStruct.associator X Y Z).hom = Limits.coprod.desc (Limits.coprod.desc Limits.coprod.inl (CategoryStruct.comp Limits.coprod.inl Limits.coprod.inr)) (CategoryStruct.comp Limits.coprod.inr Limits.coprod.inr)
    source
    theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y Z : C) :
    (MonoidalCategoryStruct.associator X Y Z).inv = Limits.coprod.desc (CategoryStruct.comp Limits.coprod.inl Limits.coprod.inl) (Limits.coprod.desc (CategoryStruct.comp Limits.coprod.inr Limits.coprod.inl) Limits.coprod.inr)
    source
    @[implicit_reducible]
    noncomputable def CategoryTheory.symmetricOfHasFiniteCoproducts (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] :
    SymmetricCategory C

    The monoidal structure coming from finite coproducts is symmetric.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.symmetricOfHasFiniteCoproducts_braiding (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (P Q : C) :
      β_ P Q = Limits.coprod.braiding P Q