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](#29657 (comment)). 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

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: jcreinhold

Mathlib.lean

@@ -2566,6 +2566,7 @@ import Mathlib.CategoryTheory.Monoidal.Cartesian.Over
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
+import Mathlib.CategoryTheory.Monoidal.CommComon_
 import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Comon_

Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

@@ -70,7 +70,7 @@ end
 
 @[simps! counit]
 instance {a : B} : Comonad (𝟙 a) :=
-  inferInstanceAs <| ComonObj (MonoidalCategory.tensorUnit (a ⟶ a))
+  ComonObj.instTensorUnit (a ⟶ a)
 
 /-- An oplax functor from the trivial bicategory to `B` defines a comonad in `B`. -/
 def ofOplaxFromUnit (F : OplaxFunctor (LocallyDiscrete (Discrete Unit)) B) :

Mathlib/CategoryTheory/Monoidal/Bimon_.lean

@@ -142,6 +142,7 @@ theorem ofMonComonObjX_mul (M : Mon (Comon C)) :
 
 @[deprecated (since := "2025-09-15")] alias ofMon_Comon_ObjX_mul := ofMonComonObjX_mul
 
+attribute [local instance] ComonObj.instTensorUnit in
 attribute [local simp] MonObj.tensorObj.one_def MonObj.tensorObj.mul_def tensorμ in
 /-- The object level part of the backward direction of `Comon (Mon C) ≌ Mon (Comon C)` -/
 @[simps]

Mathlib/CategoryTheory/Monoidal/CommComon_.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2025 Jacob Reinhold. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacob Reinhold
+-/
+import Mathlib.CategoryTheory.Monoidal.Comon_
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
+import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
+
+/-!
+# The category of commutative comonoids in a braided monoidal category.
+
+We define the category of commutative comonoid objects in a braided monoidal category `C`.
+
+## Main definitions
+
+* `CommComon C` - The bundled structure of commutative comonoid objects
+
+## Tags
+
+comonoid, commutative, braided
+-/
+
+universe v₁ v₂ v₃ u₁ u₂ u₃ u
+
+namespace CategoryTheory
+
+open MonoidalCategory ComonObj Functor
+
+variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory.{v₁} C]
+
+variable (C) in
+/-- A commutative comonoid object internal to a monoidal category. -/
+structure CommComon where
+  /-- The underlying object in the ambient monoidal category -/
+  X : C
+  [comon : ComonObj X]
+  [comm : IsCommComonObj X]
+
+attribute [instance] CommComon.comon CommComon.comm
+
+namespace CommComon
+
+/-- A commutative comonoid object is a comonoid object. -/
+@[simps X]
+def toComon (A : CommComon C) : Comon C := ⟨A.X⟩
+
+section
+
+attribute [local instance] ComonObj.instTensorUnit in
+/-- The trivial comonoid on the unit object is commutative. -/
+instance instCommComonObjUnit : IsCommComonObj (𝟙_ C) where
+  comul_comm := by simp [← unitors_equal]
+
+end
+
+attribute [local instance] ComonObj.instTensorUnit in
+variable (C) in
+/-- The trivial commutative comonoid object. We later show this is initial in `CommComon C`. -/
+@[simps!]
+def trivial : CommComon C := mk (𝟙_ C)
+
+instance : Inhabited (CommComon C) :=
+  ⟨trivial C⟩
+
+variable {M : CommComon C}
+
+instance : Category (CommComon C) :=
+  InducedCategory.category CommComon.toComon
+
+@[simp]
+theorem id_hom (A : CommComon C) : Comon.Hom.hom (𝟙 A) = 𝟙 A.X :=
+  rfl
+
+@[simp]
+theorem comp_hom {R S T : CommComon C} (f : R ⟶ S) (g : S ⟶ T) :
+    Comon.Hom.hom (f ≫ g) = f.hom ≫ g.hom :=
+  rfl
+
+@[ext]
+lemma hom_ext {A B : CommComon C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g :=
+  Comon.Hom.ext h
+
+section
+
+variable (C)
+
+/-- The forgetful functor from commutative comonoid objects to comonoid objects. -/
+@[simps!]
+def forget₂Comon : CommComon C ⥤ Comon C :=
+  inducedFunctor _
+
+end
+
+end CommComon
+
+end CategoryTheory

Mathlib/CategoryTheory/Monoidal/Comon_.lean

@@ -53,8 +53,10 @@ namespace ComonObj
 
 attribute [reassoc (attr := simp)] counit_comul comul_counit comul_assoc
 
+/-- The canonical comonoid structure on the monoidal unit.
+This is not a global instance to avoid conflicts with other comonoid structures. -/
 @[simps]
-instance (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] : ComonObj (𝟙_ C) where
+def instTensorUnit (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] : ComonObj (𝟙_ C) where
   counit := 𝟙 _
   comul := (λ_ _).inv
   counit_comul := by simp
@@ -102,6 +104,7 @@ attribute [instance] Comon.comon
 
 namespace Comon
 
+attribute [local instance] ComonObj.instTensorUnit in
 variable (C) in
 /-- The trivial comonoid object. We later show this is terminal in `Comon C`.
 -/
@@ -442,3 +445,16 @@ def mapComon (F : C ⥤ D) [F.OplaxMonoidal] : Comon C ⥤ Comon D where
 -- and so can't state `mapComonFunctor : OplaxMonoidalFunctor C D ⥤ Comon C ⥤ Comon D`.
 
 end CategoryTheory.Functor
+
+section
+variable [BraidedCategory.{v₁} C]
+
+/-- Predicate for a comonoid object to be commutative. -/
+class IsCommComonObj (X : C) [ComonObj X] where
+  comul_comm (X) : Δ ≫ (β_ X X).hom = Δ := by cat_disch
+
+open scoped ComonObj
+
+attribute [reassoc (attr := simp)] IsCommComonObj.comul_comm
+
+end