feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category

[robin-carlier]

Show that in the augmented simplex category, ⦋0⦌ is an internal monoid object.

Future work will show that this is in fact the universal monoid object: for any monoidal category C, evaluation at ⦋0⦌ induces an equivalence of categories between Mon_ C and the category of monoidal functors from AugmentedSimplexCategory to C. The resulting augmented cosimplicial object one gets from this construction is sometimes called the "monoidal bar construction" attached to a monoid.

This PR was split from #25743.

---

• depends on: feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on AugmentedSimplexCategory #25743

[github-actions]

PR summary cdf36433a2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplexCategory.Augmented	1
Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic (new file)	890
Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (new file)	893
Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Mon_ (new file)	911

---

Declarations diff

+ associator
+ id_star_whiskerRight
+ id_tensorHom
+ instance : MonoidalCategory AugmentedSimplexCategory
+ instance : MonoidalCategoryStruct AugmentedSimplexCategory
+ leftUnitor
+ mon_
+ rightUnitor
+ tensorHom
+ tensorHomOf
+ tensorHom_id
+ tensorObj
+ tensorObjOf
+ tensorObj_hom_ext
+ tensorUnit
+ tensor_comp
+ tensor_id
+ whiskerLeft_id_star
+ φ₁
+ φ₁'
+ φ₁'_eval
+ φ₁_comp_tensorHom
+ φ₁_comp_φ₁_comp_associator
+ φ₂
+ φ₂'
+ φ₂'_eval
+ φ₂_comp_associator
+ φ₂_comp_tensorHom
+ φ₂_comp_φ₁_comp_associator
++ eqToHom_toOrderHom

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on AugmentedSimplexCategory #25743
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.