Commit 2025-09-25 12:38 7ef00670

feat(CategoryTheory/Monoidal): Add commutative comonoid objects (#29919) This PR adds commutative comonoid objects and removes the problematic global comonoid instance (see #29657).

Main changes

1. Add CommComonObj class

Added Mathlib/CategoryTheory/Monoidal/CommComon_.lean defining commutative comonoids. This captures the mathematical notion that swapping the two copies produced by comultiplication gives the same result. In cartesian categories, all comonoids are automatically commutative (copying data has no preferred order).

2. Remove global ComonObj instance for unit object

The global ComonObj (𝟙_ C) instance interfered in related proofs. This PR removes it and updates affected code:

• Bicategory/Monad/Basic.lean: Now uses ComonObj.instTensorUnit for the identity monad's comonad structure
• Monoidal/Bimon_.lean: Added explicit proofs the global instance previously resolved, verifying unit morphisms preserve comonoid structure

Design notes

• CommComonObj extends ComonObj and requires BraidedCategory for the braiding
• Unlike the removed global instance, CommComonObj stays a class (it describes a property, not a structure)
• The explicit instTensorUnit lets users control when to use the trivial comonoid structure