Commit 2024-07-16 09:12 63ed47e7

View on Github →

feat(CategoryTheory): the monoidal category structure on graded objects (#14457) Under suitable conditions on a monoidal category C, we define an instance of MonoidalCategory (GradedObject ℕ C). The construction is actually more general, and it shall be used in order to get monoidal category structures on homological complexes in future PRs.

Estimated changes

Modified Mathlib/CategoryTheory/EffectiveEpi/Extensive.lean

Modified Mathlib/CategoryTheory/GradedObject/Monoidal.lean

added theorem CategoryTheory.GradedObject.Monoidal.left_tensor_tensorObj₃_ext

added theorem CategoryTheory.GradedObject.Monoidal.pentagon

added theorem CategoryTheory.GradedObject.Monoidal.pentagon_inv

added theorem CategoryTheory.GradedObject.Monoidal.tensorObj₄_ext

added theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₄_eq

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

deleted def CategoryTheory.Limits.preservesFiniteCoproductsOfReflectsOfPreserves

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

added theorem CategoryTheory.MonoidalCategory.whiskerLeft_whiskerLeft_associator_inv