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

structure CategoryTheory.CommComon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Type (max u₁ v₁)

A commutative comonoid object internal to a monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• comon : ComonObj self.X
• comm : IsCommComonObj self.X

def CategoryTheory.CommComon.toComon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommComon C) : Comon C

A commutative comonoid object is a comonoid object.

Equations

• A.toComon = { X := A.X, comon := A.comon }

@[simp]

theorem CategoryTheory.CommComon.toComon_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommComon C) : A.toComon.X = A.X

instance CategoryTheory.CommComon.instCommComonObjUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : IsCommComonObj (MonoidalCategoryStruct.tensorUnit C)

The trivial comonoid on the unit object is commutative.

def CategoryTheory.CommComon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : CommComon C

The trivial commutative comonoid object. We later show this is initial in CommComon C.

Equations

• CategoryTheory.CommComon.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, comon := ComonObj.instTensorUnit C, comm := ⋯ }

@[simp]

theorem CategoryTheory.CommComon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (trivial C).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.CommComon.trivial_comon_comul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : ComonObj.comul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv

@[simp]

theorem CategoryTheory.CommComon.trivial_comon_counit (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : ComonObj.counit = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

instance CategoryTheory.CommComon.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Inhabited (CommComon C)

Equations

• CategoryTheory.CommComon.instInhabited = { default := CategoryTheory.CommComon.trivial C }

instance CategoryTheory.CommComon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Category.{v₁, max u₁ v₁} (CommComon C)

Equations

• CategoryTheory.CommComon.instCategory = CategoryTheory.InducedCategory.category CategoryTheory.CommComon.toComon

@[simp]

theorem CategoryTheory.CommComon.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommComon C) : (CategoryStruct.id A).hom = CategoryStruct.id A.X

@[simp]

theorem CategoryTheory.CommComon.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {R S T : CommComon C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.CommComon.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommComon C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g

theorem CategoryTheory.CommComon.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommComon C} {f g : A ⟶ B} : f = g ↔ f.hom = g.hom

def CategoryTheory.CommComon.forget₂Comon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor (CommComon C) (Comon C)

The forgetful functor from commutative comonoid objects to comonoid objects.

Equations

• CategoryTheory.CommComon.forget₂Comon C = CategoryTheory.inducedFunctor CategoryTheory.CommComon.toComon

@[simp]

theorem CategoryTheory.CommComon.forget₂Comon_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : InducedCategory (Comon C) toComon} (f : X✝ ⟶ Y✝) : (forget₂Comon C).map f = f

@[simp]

theorem CategoryTheory.CommComon.forget₂Comon_obj_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommComon C) : ((forget₂Comon C).obj A).X = A.X

@[simp]

theorem CategoryTheory.CommComon.forget₂Comon_obj_comon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommComon C) : ((forget₂Comon C).obj A).comon = A.comon