Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
feat(category_theory): finite products give a monoidal structure (#1340)
* providing minimal API for limits of special shapes

* apis for special shapes

* start

* fintype instances

* copy-paste from monoidal-categories-reboot

* associators, unitors, braidings for binary product

* minor

* minor

* map

* minor

* instances

* blah

* chore(category_theory/monoidal): monoidal_category doesn't extend category

* minor

* minor

* assoc lemma

* coprod

* done?

* fix import

* names

* cleanup

* fix reassoc

* comments

* comments
  • Loading branch information
semorrison authored and mergify[bot] committed Sep 4, 2019
1 parent 8cd16b9 commit 5d59e8b
Show file tree
Hide file tree
Showing 5 changed files with 66 additions and 13 deletions.
4 changes: 2 additions & 2 deletions src/category_theory/limits/limits.lean
Expand Up @@ -454,7 +454,7 @@ def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
@[simp] lemma limit.is_limit_lift {F : J ⥤ C} [has_limit F] (c : cone F) :
(limit.is_limit F).lift c = limit.lift F c := rfl

@[simp,reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
@[simp, reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
limit.lift F c ≫ limit.π F j = c.π.app j :=
is_limit.fac _ c j

Expand Down Expand Up @@ -617,7 +617,7 @@ def lim : (J ⥤ C) ⥤ C :=

variables {F} {G : J ⥤ C} (α : F ⟶ G)

@[simp,reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
@[simp, reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
by apply is_limit.fac

@[simp] lemma limit.lift_map (c : cone F) :
Expand Down
@@ -0,0 +1 @@
-- TODO construct finite limits from finite products and equalizers
@@ -0,0 +1 @@
-- TODO construct limits from products and equalizers
57 changes: 57 additions & 0 deletions src/category_theory/monoidal/of_has_finite_products.lean
@@ -0,0 +1,57 @@
/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Simon Hudon
-/
import category_theory.monoidal.category
import category_theory.limits.shapes.finite_products
import category_theory.limits.shapes.binary_products
import category_theory.limits.shapes.terminal
import category_theory.limits.types

/-!
# 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, we don't set up either construct as an instance.
-/

open category_theory.limits

universes v u

namespace category_theory

section
variables (C : Type u) [𝒞 : category.{v+1} C]
include 𝒞

local attribute [tidy] tactic.case_bash

/-- A category with finite products has a natural monoidal structure. -/
def monoidal_of_has_finite_products [has_finite_products.{v} C] : monoidal_category C :=
{ tensor_unit := terminal C,
tensor_obj := λ X Y, limits.prod X Y,
tensor_hom := λ _ _ _ _ f g, limits.prod.map f g,
associator := prod.associator,
left_unitor := prod.left_unitor,
right_unitor := prod.right_unitor }

/-- A category with finite coproducts has a natural monoidal structure. -/
def monoidal_of_has_finite_coproducts [has_finite_coproducts.{v} C] : monoidal_category C :=
{ tensor_unit := initial C,
tensor_obj := λ X Y, limits.coprod X Y,
tensor_hom := λ _ _ _ _ f g, limits.coprod.map f g,
associator := coprod.associator,
left_unitor := coprod.left_unitor,
right_unitor := coprod.right_unitor }

end

end category_theory

-- TODO in fact, a category with finite products is braided, and symmetric,
-- and we should say that here.
16 changes: 5 additions & 11 deletions src/category_theory/monoidal/types.lean
Expand Up @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Michael Jendrusch, Scott Morrison
-/
import category_theory.types
import category_theory.monoidal.category
import category_theory.limits.types
import category_theory.monoidal.of_has_finite_products

open category_theory
open tactic
Expand All @@ -13,16 +14,9 @@ universes u v

namespace category_theory.monoidal

instance types : monoidal_category.{u+1} (Type u) :=
{ tensor_obj := λ X Y, X × Y,
tensor_hom := λ _ _ _ _ f g, prod.map f g,
tensor_unit := punit,
left_unitor := λ X, (equiv.punit_prod X).to_iso,
right_unitor := λ X, (equiv.prod_punit X).to_iso,
associator := λ X Y Z, (equiv.prod_assoc X Y Z).to_iso,
..category_theory.types.{u+1} }
local attribute [instance] monoidal_of_has_finite_products
instance types : monoidal_category.{u+1} (Type u) := by apply_instance

-- TODO Once we add braided/symmetric categories, include the braiding.
-- TODO More generally, define the symmetric monoidal structure on any category with products.
-- TODO Once we add braided/symmetric categories, include the braiding/symmetry.

end category_theory.monoidal

0 comments on commit 5d59e8b

Please sign in to comment.