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 Comon_Class {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 Comon_Class.termΔ : Lean.ParserDescr

The comultiplication morphism of a comonoid object.

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

The comultiplication morphism of a comonoid object.

def Comon_Class.termε : Lean.ParserDescr

The counit morphism of a comonoid object.

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

The counit morphism of a comonoid object.

@[simp]

theorem Comon_Class.comul_counit_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : Comon_Class 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 Comon_Class.counit_comul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : Comon_Class 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

@[simp]

theorem Comon_Class.comul_assoc_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : Comon_Class 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))

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

instance instIsComon_HomId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Comon_Class M] : IsComon_Hom (CategoryTheory.CategoryStruct.id M)

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

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

instance instIsComon_HomInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [Comon_Class M] [Comon_Class N] (f : M ⟶ N) [IsComon_Hom f] [CategoryTheory.IsIso f] : IsComon_Hom (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 : Comon_Class self.X

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.

@[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_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Comon_Class.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem Comon_.trivial_comon_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Comon_Class.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)

@[simp]

theorem Comon_Class.counit_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Comon_Class 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 Comon_Class.counit_comul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Comon_Class 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 Comon_Class.comul_counit_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Comon_Class 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 Comon_Class.comul_counit_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Comon_Class 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 Comon_Class.comul_assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class 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 Comon_Class.comul_assoc_flip_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class 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.

• is_comon_hom : IsComon_Hom 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 Comon_Class.counit = Comon_Class.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f Comon_Class.comul = CategoryTheory.CategoryStruct.comp Comon_Class.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 IsComon_Hom f instance.

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.

@[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)

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.

@[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)

instance Comon_.instIsComon_HomHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon_ C} (f : M ⟶ N) : IsComon_Hom 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.

@[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) [IsComon_Hom 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.

@[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) [IsComon_Hom 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) [IsComon_Hom 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 Comon_Class.counit = Comon_Class.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f.hom Comon_Class.comul = CategoryTheory.CategoryStruct.comp Comon_Class.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.

@[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 Comon_Class.counit = Comon_Class.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f.hom Comon_Class.comul = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : (mkIso f f_counit f_comul).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) (f_counit : CategoryTheory.CategoryStruct.comp f.hom Comon_Class.counit = Comon_Class.counit := by cat_disch) (f_comul : CategoryTheory.CategoryStruct.comp f.hom Comon_Class.comul = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : (mkIso f f_counit f_comul).hom.hom = f.hom

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

@[simp]

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

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

@[reducible, inline]

abbrev Comon_.Comon_ToMon_OpOpObjMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : Mon_Class (Opposite.op A.X)

Auxiliary definition for Comon_ToMon_OpOpObj.

def Comon_.Comon_ToMon_OpOpObj {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.

@[simp]

theorem Comon_.Comon_ToMon_OpOpObj_mon_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : Mon_Class.one = Comon_Class.counit.op

@[simp]

theorem Comon_.Comon_ToMon_OpOpObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : A.Comon_ToMon_OpOpObj.X = Opposite.op A.X

@[simp]

theorem Comon_.Comon_ToMon_OpOpObj_mon_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : Mon_Class.mul = Comon_Class.comul.op

def Comon_.Comon_ToMon_OpOp (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.

@[simp]

theorem Comon_.Comon_ToMon_OpOp_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Comon_ C} (f : X✝ ⟶ Y✝) : (Comon_ToMon_OpOp C).map f = Opposite.op { hom := f.hom.op, is_mon_hom := ⋯ }

@[simp]

theorem Comon_.Comon_ToMon_OpOp_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : (Comon_ToMon_OpOp C).obj A = Opposite.op A.Comon_ToMon_OpOpObj

@[reducible, inline]

abbrev Comon_.Mon_OpOpToComonObjComon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ Cᵒᵖ) : Comon_Class (Opposite.unop A.X)

Auxiliary definition for Mon_OpOpToComonObj.

def Comon_.Mon_OpOpToComonObj {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.

@[simp]

theorem Comon_.Mon_OpOpToComonObj_comon_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ Cᵒᵖ) : Comon_Class.counit = Mon_Class.one.unop

@[simp]

theorem Comon_.Mon_OpOpToComonObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ Cᵒᵖ) : (Mon_OpOpToComonObj A).X = Opposite.unop A.X

@[simp]

theorem Comon_.Mon_OpOpToComonObj_comon_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ Cᵒᵖ) : Comon_Class.comul = Mon_Class.mul.unop

def Comon_.Mon_OpOpToComon_ (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.

@[simp]

theorem Comon_.Mon_OpOpToComon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : (Mon_ Cᵒᵖ)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((Mon_OpOpToComon_ C).map f).hom = f.unop.hom.unop

@[simp]

theorem Comon_.Mon_OpOpToComon__obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : (Mon_ Cᵒᵖ)ᵒᵖ) : (Mon_OpOpToComon_ C).obj A = Mon_OpOpToComonObj (Opposite.unop A)

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.

@[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 (((Mon_OpOpToComon_ C).comp (Comon_ToMon_OpOp 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 = Mon_OpOpToComon_ C

@[simp]

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

@[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)) ⋯

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.

@[simp]

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

@[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_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_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_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_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_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

@[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_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_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_tensorObj_comon_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon_ C) : Comon_Class.counit = Mon_Class.one.unop

@[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_tensorUnit_comon_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Comon_Class.comul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).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) : Comon_Class.comul = Mon_Class.mul.unop

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_.instComon_ClassTensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : C) [Comon_Class A] [Comon_Class B] : Comon_Class (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

@[simp]

theorem Comon_.tensorObj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : C) [Comon_Class A] [Comon_Class B] : Comon_Class.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.counit Comon_Class.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) [Comon_Class A] [Comon_Class B] : Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.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) [Comon_Class A] [Comon_Class B] : Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.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.

@[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.instComon_Class {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : C) [Comon_Class A] (F : Functor C D) [F.OplaxMonoidal] : Comon_Class (F.obj A)

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

@[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) [Comon_Class X] : Comon_Class.counit = CategoryStruct.comp (F.map Comon_Class.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) [Comon_Class X] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp Comon_Class.counit h = CategoryStruct.comp (F.map Comon_Class.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) [Comon_Class X] : Comon_Class.comul = CategoryStruct.comp (F.map Comon_Class.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) [Comon_Class X] {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj X) ⟶ Z) : CategoryStruct.comp Comon_Class.comul h = CategoryStruct.comp (F.map Comon_Class.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} [Comon_Class X] [Comon_Class Y] (f : X ⟶ Y) [IsComon_Hom f] : IsComon_Hom (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.

@[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) : Comon_Class.comul = CategoryStruct.comp (F.map Comon_Class.comul) (OplaxMonoidal.δ F A.X A.X)

@[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

@[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) : Comon_Class.counit = CategoryStruct.comp (F.map Comon_Class.counit) (OplaxMonoidal.η F)

@[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