mathlib4 feat(CategoryTheory/Monoidal): Hopf monoids

Defines Hopf monoids in a braided category.

Proves two facts (antipode is an antihomomorphism, morphisms intertwine antipode) that are not yet proved for unbundled Hopf algebras. Once we prove Hopf_ (ModuleCat R) is equivalent to HopfAlgebraCat (having defined that!), we will get those two facts for free.

We should also check later that Hopf_ C in a cartesian monoidal category is equivalent GroupObject_ C (being defined independently elsewhere).

[ ] depends on: #13313
[ ] depends on: #13312 (probably doesn't actually depend, but I don't want to sort out the git history now)
[x] depends on: #13315

May 28 '24 15:05 kim-em

PR summary 94b3b98c1d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Monoidal.Hopf_`	476

Declarations diff

+ Hopf_ + antipode_antipode + antipode_comul + antipode_comul₁ + antipode_comul₂ + antipode_counit + compatibility + comul_assoc_flip_hom + comul_assoc_hom + comul_counit_hom + counit_comul_hom + hom_antipode + hom_comul_hom + hom_counit_hom + instance : Category (Hopf_ C) := inferInstanceAs <| Category (InducedCategory (Bimon_ C) Hopf_.X) + mul_antipode + mul_antipode₁ + mul_antipode₂ + mul_counit + one_antipode + one_comul + to_trivial + trivial + trivial_to

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.

Jun 13 '24 04:06 github-actions[bot]

This PR/issue depends on:

~~leanprover-community/mathlib4#13313~~
~~leanprover-community/mathlib4#13312~~
~~leanprover-community/mathlib4#13315~~ By Dependent Issues (🤖). Happy coding!