Commit 2024-08-20 10:06 5f2879ac

View on Github →

feat(CategoryTheory/Monoidal): Cat is monoidal with the cartesian product of categories (#15258) feat(CategoryTheory/Monoidal): Cat, the category of categories, is monoidal with the cartesian product of categories Co-authored-by : atopaz@fastmail.com Co-authored-by : yael.dillies@gmail.com

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ChosenFiniteProducts/Cat.lean

added def CategoryTheory.Cat.chosenTerminalIsTerminal

added def CategoryTheory.Cat.isLimitProdCone

added def CategoryTheory.Cat.prodCone

added theorem CategoryTheory.Monoidal.associator_hom

added theorem CategoryTheory.Monoidal.associator_inv

added theorem CategoryTheory.Monoidal.leftUnitor_hom

added theorem CategoryTheory.Monoidal.leftUnitor_inv

added theorem CategoryTheory.Monoidal.rightUnitor_hom

added theorem CategoryTheory.Monoidal.rightUnitor_inv

added theorem CategoryTheory.Monoidal.tensorHom

added theorem CategoryTheory.Monoidal.tensorObj

added theorem CategoryTheory.Monoidal.tensorUnit

added theorem CategoryTheory.Monoidal.whiskerLeft

added theorem CategoryTheory.Monoidal.whiskerLeft_fst

added theorem CategoryTheory.Monoidal.whiskerLeft_snd

added theorem CategoryTheory.Monoidal.whiskerRight

added theorem CategoryTheory.Monoidal.whiskerRight_fst

added theorem CategoryTheory.Monoidal.whiskerRight_snd