feat(CategoryTheory): the monoidal category structure on graded objects

[joelriou]

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.

Co-authored-by: Kim Morrison

---

• [ ] depends on: #14343

[github-actions[bot]]

PR summary 779ef7d15f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.GradedObject.Monoidal	453	528	+75 (+16.56%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.GradedObject.Monoidal	75

---

Declarations diff

+ instance (F : C ⥤ D) (J : Type*) [Finite J] [PreservesFiniteCoproducts F] : + instance (n : ℕ) : Finite ((fun (i : ℕ × ℕ) => i.1 + i.2) ⁻¹' {n}) := by + instance (n : ℕ) : Finite ({ i : (ℕ × ℕ × ℕ) | i.1 + i.2.1 + i.2.2 = n }) := by + left_tensor_tensorObj₃_ext + monoidalCategory + pentagon + pentagon_inv + tensorObj₄_ext + whiskerLeft_whiskerLeft_associator_inv + ιTensorObj₄ + ιTensorObj₄_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#14343~~ By Dependent Issues (🤖). Happy coding!

[kim-em]

Excited to see that you've finished this @joelriou, it's great!

bors d+

[mathlib-bors[bot]]

:v: joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style