The category of comonoids in a monoidal category.

We define comonoids in a monoidal category C, and show that they are equivalently monoid objects in the opposite category.

We construct the monoidal structure on Comon C, when C is braided.

An oplax monoidal functor takes comonoid objects to comonoid objects. That is, a oplax monoidal functor F : C ⥤ D induces a functor Comon C ⥤ Comon D.

TODO

• Comonoid objects in C are "just" oplax monoidal functors from the trivial monoidal category to C.

class ComonObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type v₁

A comonoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".

• counit : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C

  The counit morphism of a comonoid object.

• comul : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X

  The comultiplication morphism of a comonoid object.

• counit_comul : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerRight counit X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
• comul_counit : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X counit) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
• comul_assoc : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X comul) = CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul X) (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom)

def ComonObj.termΔ : Lean.ParserDescr

The comultiplication morphism of a comonoid object.

Equations

• ComonObj.termΔ = Lean.ParserDescr.node `ComonObj.termΔ 1024 (Lean.ParserDescr.symbol "Δ")

def ComonObj.«termΔ[_]» : Lean.ParserDescr

The comultiplication morphism of a comonoid object.

Equations

• One or more equations did not get rendered due to their size.

def ComonObj.termε : Lean.ParserDescr

The counit morphism of a comonoid object.

Equations

• ComonObj.termε = Lean.ParserDescr.node `ComonObj.termε 1024 (Lean.ParserDescr.symbol "ε")

def ComonObj.«termε[_]» : Lean.ParserDescr

The counit morphism of a comonoid object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ComonObj.comul_counit_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : ComonObj X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X counit) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h

@[simp]

theorem ComonObj.comul_assoc_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : ComonObj X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) ⟶ Z) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X comul) h) = CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom h))

@[simp]

theorem ComonObj.counit_comul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : ComonObj X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ⟶ Z) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight counit X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv h

def ComonObj.instTensorUnit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : ComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The canonical comonoid structure on the monoidal unit. This is not a global instance to avoid conflicts with other comonoid structures.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

class IsComonHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [ComonObj M] [ComonObj N] (f : M ⟶ N) : Prop

The property that a morphism between comonoid objects is a comonoid morphism.

• hom_counit : CategoryTheory.CategoryStruct.comp f ComonObj.counit = ComonObj.counit
• hom_comul : CategoryTheory.CategoryStruct.comp f ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)

@[deprecated IsComonHom (since := "2025-09-15")]

def IsComon_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [ComonObj M] [ComonObj N] (f : M ⟶ N) : Prop

Alias of IsComonHom.

---

The property that a morphism between comonoid objects is a comonoid morphism.

Equations

• @IsComon_Hom = @IsComonHom

@[simp]

theorem IsComonHom.hom_counit_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : C} {inst✝² : ComonObj M} {inst✝³ : ComonObj N} (f : M ⟶ N) [self : IsComonHom f] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ComonObj.counit h) = CategoryTheory.CategoryStruct.comp ComonObj.counit h

@[simp]

theorem IsComonHom.hom_comul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : C} {inst✝² : ComonObj M} {inst✝³ : ComonObj N} (f : M ⟶ N) [self : IsComonHom f] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj N N ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ComonObj.comul h) = CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) h)

instance instIsComonHomId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [ComonObj M] : IsComonHom (CategoryTheory.CategoryStruct.id M)

instance instIsComonHomComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : C} [ComonObj M] [ComonObj N] [ComonObj O] (f : M ⟶ N) (g : N ⟶ O) [IsComonHom f] [IsComonHom g] : IsComonHom (CategoryTheory.CategoryStruct.comp f g)

instance instIsComonHomInvOfHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [ComonObj M] [ComonObj N] (f : M ≅ N) [IsComonHom f.hom] : IsComonHom f.inv

instance instIsComonHomInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [ComonObj M] [ComonObj N] (f : M ⟶ N) [IsComonHom f] [CategoryTheory.IsIso f] : IsComonHom (CategoryTheory.inv f)

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

A comonoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".

• X : C

  The underlying object of a comonoid object.

• comon : ComonObj self.X

@[deprecated Comon (since := "2025-09-15")]

def Comon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max u₁ v₁)

Alias of Comon.

---

A comonoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".

Equations

• Comon_ = Comon

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

The trivial comonoid object. We later show this is terminal in Comon C.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• Comon.instInhabited = { default := Comon.trivial C }

@[simp]

theorem ComonObj.counit_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [ComonObj M] {Z : C} (f : M ⟶ Z) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.tensorHom counit f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv

@[simp]

theorem ComonObj.counit_comul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [ComonObj M] {Z : C} (f : M ⟶ Z) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom counit f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv h)

@[simp]

theorem ComonObj.comul_counit_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [ComonObj M] {Z : C} (f : M ⟶ Z) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f counit) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv

@[simp]

theorem ComonObj.comul_counit_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [ComonObj M] {Z : C} (f : M ⟶ Z) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f counit) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv h)

theorem ComonObj.comul_assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [ComonObj X] : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul X) = CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X comul) (CategoryTheory.MonoidalCategoryStruct.associator X X X).inv)

theorem ComonObj.comul_assoc_flip_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [ComonObj X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) X ⟶ Z) : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul X) h) = CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).inv h))

structure Comon.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M N : Comon C) : Type v₁

A morphism of comonoid objects.

• hom : M.X ⟶ N.X

  The underlying morphism of a morphism of comonoid objects.

• isComonHom_hom : IsComonHom self.hom

theorem Comon.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : Comon C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem Comon.Hom.ext_iff {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : Comon C} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

@[reducible, inline]

abbrev Comon.Hom.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ⟶ N.X) (f_counit : CategoryTheory.CategoryStruct.comp f ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) := by cat_disch) : M.Hom N

Construct a morphism M ⟶ N of Comon C from a map f : M ⟶ N and a IsComonHom f instance.

Equations

• Comon.Hom.mk' f f_counit f_comul = { hom := f, isComonHom_hom := ⋯ }

def Comon.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Comon C) : M.Hom M

The identity morphism on a comonoid object.

Equations

• M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isComonHom_hom := ⋯ }

@[simp]

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

instance Comon.homInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Comon C) : Inhabited (M.Hom M)

Equations

• M.homInhabited = { default := M.id }

def Comon.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : Comon C} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Composition of morphisms of monoid objects.

Equations

• Comon.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isComonHom_hom := ⋯ }

@[simp]

theorem Comon.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : Comon C} (f : M.Hom N) (g : N.Hom O) : (comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

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

Equations

• One or more equations did not get rendered due to their size.

instance Comon.instIsComonHomHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M ⟶ N) : IsComonHom f.hom

theorem Comon.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X Y : Comon C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g

theorem Comon.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X Y : Comon C} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

@[simp]

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

@[simp]

theorem Comon.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N K : Comon C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

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

The forgetful functor from comonoid objects to the ambient category.

Equations

• Comon.forget C = { obj := fun (A : Comon C) => A.X, map := fun {X Y : Comon C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Comon.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Comon C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.hom

@[simp]

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

instance Comon.forget_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (forget C).Faithful

instance Comon.instIsIsoHomOfMapForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Comon C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((forget C).map f)] : CategoryTheory.IsIso f.hom

instance Comon.instReflectsIsomorphismsForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (forget C).ReflectsIsomorphisms

The forgetful functor from comonoid objects to the ambient category reflects isomorphisms.

def Comon.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) [IsComonHom f.hom] : M ≅ N

Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects and checking compatibility with counit and comultiplication only in the forward direction.

Equations

• Comon.mkIso' f = { hom := { hom := f.hom, isComonHom_hom := inst✝ }, inv := { hom := f.inv, isComonHom_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Comon.mkIso'_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) [IsComonHom f.hom] : (mkIso' f).inv.hom = f.inv

@[simp]

theorem Comon.mkIso'_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) [IsComonHom f.hom] : (mkIso' f).hom.hom = f.hom

def Comon.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) (f_counit : CategoryTheory.CategoryStruct.comp f.hom ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f.hom ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : M ≅ N

Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects and checking compatibility with counit and comultiplication only in the forward direction.

Equations

• Comon.mkIso f f_counit f_comul = { hom := { hom := f.hom, isComonHom_hom := ⋯ }, inv := { hom := f.inv, isComonHom_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Comon.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) (f_counit : CategoryTheory.CategoryStruct.comp f.hom ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f.hom ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : (mkIso f f_counit f_comul).hom.hom = f.hom

@[simp]

theorem Comon.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) (f_counit : CategoryTheory.CategoryStruct.comp f.hom ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f.hom ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : (mkIso f f_counit f_comul).inv.hom = f.inv

instance Comon.uniqueHomToTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : Unique (A ⟶ trivial C)

Equations

• A.uniqueHomToTrivial = { default := { hom := ComonObj.counit, isComonHom_hom := ⋯ }, uniq := ⋯ }

@[simp]

theorem Comon.uniqueHomToTrivial_default_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : default.hom = ComonObj.counit

instance Comon.instHasTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.HasTerminal (Comon C)

@[reducible, inline]

abbrev Comon.ComonToMonOpOpObjMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : MonObj (Opposite.op A.X)

Auxiliary definition for ComonToMonOpOpObj.

Equations

• A.ComonToMonOpOpObjMon = { one := ComonObj.counit.op, mul := ComonObj.comul.op, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[deprecated Comon.ComonToMonOpOpObjMon (since := "2025-09-15")]

def Comon.Comon_ToMon_OpOpObjMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : MonObj (Opposite.op A.X)

Alias of Comon.ComonToMonOpOpObjMon.

---

Auxiliary definition for ComonToMonOpOpObj.

Equations

• @Comon.Comon_ToMon_OpOpObjMon = @Comon.ComonToMonOpOpObjMon

def Comon.ComonToMonOpOpObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : Mon Cᵒᵖ

Turn a comonoid object into a monoid object in the opposite category.

Equations

• A.ComonToMonOpOpObj = { X := Opposite.op A.X, mon := A.ComonToMonOpOpObjMon }

@[simp]

theorem Comon.ComonToMonOpOpObj_mon_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : MonObj.one = ComonObj.counit.op

@[simp]

theorem Comon.ComonToMonOpOpObj_mon_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : MonObj.mul = ComonObj.comul.op

@[simp]

theorem Comon.ComonToMonOpOpObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : A.ComonToMonOpOpObj.X = Opposite.op A.X

@[deprecated Comon.ComonToMonOpOpObj (since := "2025-09-15")]

def Comon.Comon_ToMon_OpOpObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : Mon Cᵒᵖ

Alias of Comon.ComonToMonOpOpObj.

---

Turn a comonoid object into a monoid object in the opposite category.

Equations

• @Comon.Comon_ToMon_OpOpObj = @Comon.ComonToMonOpOpObj

def Comon.ComonToMonOpOp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (Comon C) (Mon Cᵒᵖ)ᵒᵖ

The contravariant functor turning comonoid objects into monoid objects in the opposite category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Comon.ComonToMonOpOp_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Comon C} (f : X✝ ⟶ Y✝) : (ComonToMonOpOp C).map f = Opposite.op { hom := f.hom.op, isMonHom_hom := ⋯ }

@[simp]

theorem Comon.ComonToMonOpOp_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon C) : (ComonToMonOpOp C).obj A = Opposite.op A.ComonToMonOpOpObj

@[deprecated Comon.ComonToMonOpOp (since := "2025-09-15")]

def Comon.Comon_ToMon_OpOp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (Comon C) (Mon Cᵒᵖ)ᵒᵖ

Alias of Comon.ComonToMonOpOp.

---

The contravariant functor turning comonoid objects into monoid objects in the opposite category.

Equations

• Comon.Comon_ToMon_OpOp = Comon.ComonToMonOpOp

@[reducible, inline]

abbrev Comon.MonOpOpToComonObjComon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj (Opposite.unop A.X)

Auxiliary definition for MonOpOpToComonObj.

Equations

• Comon.MonOpOpToComonObjComon A = { counit := MonObj.one.unop, comul := MonObj.mul.unop, counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }

@[deprecated Comon.MonOpOpToComonObjComon (since := "2025-09-15")]

def Comon.Mon_OpOpToComonObjComon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj (Opposite.unop A.X)

Alias of Comon.MonOpOpToComonObjComon.

---

Auxiliary definition for MonOpOpToComonObj.

Equations

• @Comon.Mon_OpOpToComonObjComon = @Comon.MonOpOpToComonObjComon

def Comon.MonOpOpToComonObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : Comon C

Turn a monoid object in the opposite category into a comonoid object.

Equations

• Comon.MonOpOpToComonObj A = { X := Opposite.unop A.X, comon := Comon.MonOpOpToComonObjComon A }

@[simp]

theorem Comon.MonOpOpToComonObj_comon_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj.comul = MonObj.mul.unop

@[simp]

theorem Comon.MonOpOpToComonObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : (MonOpOpToComonObj A).X = Opposite.unop A.X

@[simp]

theorem Comon.MonOpOpToComonObj_comon_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj.counit = MonObj.one.unop

@[deprecated Comon.MonOpOpToComonObj (since := "2025-09-15")]

def Comon.Mon_OpOpToComonObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon Cᵒᵖ) : Comon C

Alias of Comon.MonOpOpToComonObj.

---

Turn a monoid object in the opposite category into a comonoid object.

Equations

• @Comon.Mon_OpOpToComonObj = @Comon.MonOpOpToComonObj

def Comon.MonOpOpToComon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (Mon Cᵒᵖ)ᵒᵖ (Comon C)

The contravariant functor turning monoid objects in the opposite category into comonoid objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Comon.MonOpOpToComon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((MonOpOpToComon C).map f).hom = f.unop.hom.unop

@[simp]

theorem Comon.MonOpOpToComon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : (Mon Cᵒᵖ)ᵒᵖ) : (MonOpOpToComon C).obj A = MonOpOpToComonObj (Opposite.unop A)

@[deprecated Comon.MonOpOpToComon (since := "2025-09-15")]

def Comon.Mon_OpOpToComon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (Mon Cᵒᵖ)ᵒᵖ (Comon C)

Alias of Comon.MonOpOpToComon.

---

The contravariant functor turning monoid objects in the opposite category into comonoid objects.

Equations

• Comon.Mon_OpOpToComon_ = Comon.MonOpOpToComon

def Comon.Comon_EquivMon_OpOp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Comon C ≌ (Mon Cᵒᵖ)ᵒᵖ

Comonoid objects are contravariantly equivalent to monoid objects in the opposite category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Comon.Comon_EquivMon_OpOp_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Comon_EquivMon_OpOp C).functor = ComonToMonOpOp C

@[simp]

theorem Comon.Comon_EquivMon_OpOp_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Comon_EquivMon_OpOp C).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : (Mon Cᵒᵖ)ᵒᵖ) => CategoryTheory.Iso.refl (((MonOpOpToComon C).comp (ComonToMonOpOp C)).obj x)) ⋯

@[simp]

theorem Comon.Comon_EquivMon_OpOp_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Comon_EquivMon_OpOp C).unitIso = CategoryTheory.NatIso.ofComponents (fun (x : Comon C) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (Comon C)).obj x)) ⋯

@[simp]

theorem Comon.Comon_EquivMon_OpOp_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Comon_EquivMon_OpOp C).inverse = MonOpOpToComon C

instance Comon.monoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalCategory (Comon C)

Comonoid objects in a braided category form a monoidal category.

This definition is via transporting back and forth to monoids in the opposite category.

Equations

• Comon.monoidal C = CategoryTheory.Monoidal.transport (Comon.Comon_EquivMon_OpOp C).symm

@[simp]

theorem Comon.monoidal_whiskerLeft_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X x✝ x✝¹ : Comon C) (f : x✝ ⟶ x✝¹) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom

@[simp]

theorem Comon.monoidal_leftUnitor_hom_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Comon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom

@[simp]

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

@[simp]

theorem Comon.monoidal_rightUnitor_inv_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Comon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv

@[simp]

theorem Comon.monoidal_tensorObj_comon_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon C) : ComonObj.comul = MonObj.mul.unop

@[simp]

theorem Comon.monoidal_tensorHom_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Comon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

theorem Comon.monoidal_tensorObj_comon_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon C) : ComonObj.counit = MonObj.one.unop

@[simp]

theorem Comon.monoidal_whiskerRight_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ X₂✝ : Comon C} (f : X₁✝ ⟶ X₂✝) (X : Comon C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.X

@[simp]

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

@[simp]

theorem Comon.monoidal_rightUnitor_hom_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Comon C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom

@[simp]

theorem Comon.monoidal_tensorObj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).X = CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X

@[simp]

theorem Comon.monoidal_associator_hom_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : Comon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom

@[simp]

theorem Comon.monoidal_leftUnitor_inv_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Comon C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv

@[simp]

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

@[simp]

theorem Comon.monoidal_associator_inv_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : Comon C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv

theorem Comon.tensorObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : Comon C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B).X = CategoryTheory.MonoidalCategoryStruct.tensorObj A.X B.X

instance Comon.instComonObjTensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : C) [ComonObj A] [ComonObj B] : ComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

Equations

• Comon.instComonObjTensorObj A B = inferInstanceAs (ComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj { X := A, comon := inst✝¹ } { X := B, comon := inst✝ }).X)

@[simp]

theorem Comon.tensorObj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : C) [ComonObj A] [ComonObj B] : ComonObj.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

theorem Comon.tensorObj_comul' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : C) [ComonObj A] [ComonObj B] : ComonObj.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryTheory.MonoidalCategory.tensorμ (Opposite.op A) (Opposite.op B) (Opposite.op A) (Opposite.op B)).unop

Preliminary statement of the comultiplication for a tensor product of comonoids. This version is the definitional equality provided by transport, and not quite as good as the version provided in tensorObj_comul below.

@[simp]

theorem Comon.tensorObj_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : C) [ComonObj A] [ComonObj B] : ComonObj.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryTheory.MonoidalCategory.tensorμ A A B B)

The comultiplication on the tensor product of two comonoids is the tensor product of the comultiplications followed by the tensor strength (to shuffle the factors back into order).

instance Comon.instMonoidalForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget C).Monoidal

The forgetful functor from Comon C to C is monoidal when C is monoidal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Comon.forget_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (forget C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem Comon.forget_η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.OplaxMonoidal.η (forget C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem Comon.forget_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon C) : CategoryTheory.Functor.LaxMonoidal.μ (forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem Comon.forget_δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon C) : CategoryTheory.Functor.OplaxMonoidal.δ (forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)

@[reducible, inline]

abbrev CategoryTheory.Functor.obj.instComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : C) [ComonObj A] (F : Functor C D) [F.OplaxMonoidal] : ComonObj (F.obj A)

The image of a comonoid object under a oplax monoidal functor is a comonoid object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.obj.ε_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] : ComonObj.counit = CategoryStruct.comp (F.map ComonObj.counit) (OplaxMonoidal.η F)

theorem CategoryTheory.Functor.obj.ε_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp ComonObj.counit h = CategoryStruct.comp (F.map ComonObj.counit) (CategoryStruct.comp (OplaxMonoidal.η F) h)

@[simp]

theorem CategoryTheory.Functor.obj.Δ_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] : ComonObj.comul = CategoryStruct.comp (F.map ComonObj.comul) (OplaxMonoidal.δ F X X)

theorem CategoryTheory.Functor.obj.Δ_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj X) ⟶ Z) : CategoryStruct.comp ComonObj.comul h = CategoryStruct.comp (F.map ComonObj.comul) (CategoryStruct.comp (OplaxMonoidal.δ F X X) h)

instance CategoryTheory.Functor.map.instIsComon_Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y : C} [ComonObj X] [ComonObj Y] (f : X ⟶ Y) [IsComonHom f] : IsComonHom (F.map f)

def CategoryTheory.Functor.mapComon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] : Functor (Comon C) (Comon D)

A oplax monoidal functor takes comonoid objects to comonoid objects.

That is, a oplax monoidal functor F : C ⥤ D induces a functor Comon C ⥤ Comon D.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.mapComon_obj_comon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (A : Comon C) : ComonObj.counit = CategoryStruct.comp (F.map ComonObj.counit) (OplaxMonoidal.η F)

@[simp]

theorem CategoryTheory.Functor.mapComon_obj_comon_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (A : Comon C) : ComonObj.comul = CategoryStruct.comp (F.map ComonObj.comul) (OplaxMonoidal.δ F A.X A.X)

@[simp]

theorem CategoryTheory.Functor.mapComon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X✝ Y✝ : Comon C} (f : X✝ ⟶ Y✝) : (F.mapComon.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapComon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (A : Comon C) : (F.mapComon.obj A).X = F.obj A.X

class IsCommComonObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [ComonObj X] : Prop

Predicate for a comonoid object to be commutative.

• comul_comm : CategoryTheory.CategoryStruct.comp ComonObj.comul (β_ X X).hom = ComonObj.comul

@[simp]

theorem IsCommComonObj.comul_comm_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) {inst✝³ : ComonObj X} [self : IsCommComonObj X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ Z) : CategoryTheory.CategoryStruct.comp ComonObj.comul (CategoryTheory.CategoryStruct.comp (β_ X X).hom h) = CategoryTheory.CategoryStruct.comp ComonObj.comul h