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 ⟶ 𝟙_ 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.

Equations

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

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

The comultiplication morphism of a comonoid object.

Equations

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

def Comon_Class.termε : Lean.ParserDescr

The counit morphism of a comonoid object.

Equations

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

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

The counit morphism of a comonoid object.

Equations

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

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 (𝟙_ 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

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

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 (𝟙_ 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 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerRight counit X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv

@[simp]

theorem Comon_Class.counit_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (𝟙_ 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_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X counit) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv

@[simp]

theorem Comon_Class.comul_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (𝟙_ 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.comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : 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)

@[simp]

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

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 : 𝟙_ 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)

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.

• counit : self.X ⟶ 𝟙_ C

  The counit of a comonoid object.

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

  The comultiplication morphism of a comonoid object.

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

@[simp]

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

@[simp]

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

@[simp]

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

def Comon_.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : Comon_ C

Construct an object of Comon_ C from an object X : C and Comon_Class X instance.

Equations

• Comon_.mk' X = { X := X, counit := Comon_Class.counit, comul := Comon_Class.comul, counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }

@[simp]

theorem Comon_.mk'_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : (mk' X).counit = Comon_Class.counit

@[simp]

theorem Comon_.mk'_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : (mk' X).comul = Comon_Class.comul

@[simp]

theorem Comon_.mk'_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Comon_Class X] : (mk' X).X = X

instance Comon_.instComon_ClassX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} : Comon_Class M.X

Equations

• Comon_.instComon_ClassX = { counit := M.counit, comul := M.comul, counit_comul' := ⋯, comul_counit' := ⋯, comul_assoc' := ⋯ }

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

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

@[simp]

theorem Comon_.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (trivial C).X = 𝟙_ C

@[simp]

theorem Comon_.trivial_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (trivial C).comul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).inv

@[simp]

theorem Comon_.trivial_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (trivial C).counit = CategoryTheory.CategoryStruct.id (𝟙_ C)

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Comon_.comul_assoc_flip_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X M.X) M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.comul M.X) h) = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X M.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M.X M.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.

• hom_counit : CategoryTheory.CategoryStruct.comp self.hom N.counit = M.counit
• hom_comul : CategoryTheory.CategoryStruct.comp self.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom self.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

@[simp]

theorem Comon_.Hom.hom_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon_ C} (self : M.Hom N) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj N.X N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp N.comul h) = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom self.hom self.hom) h)

@[simp]

theorem Comon_.Hom.hom_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon_ C} (self : M.Hom N) {Z : C} (h : 𝟙_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp N.counit h) = CategoryTheory.CategoryStruct.comp M.counit h

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, hom_counit := ⋯, hom_comul := ⋯ }

@[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, hom_counit := ⋯, hom_comul := ⋯ }

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

• Comon_.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

@[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_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : (forget C).obj A = A.X

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

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) (f_counit : CategoryTheory.CategoryStruct.comp f.hom N.counit = M.counit := by aesop_cat) (f_comul : CategoryTheory.CategoryStruct.comp f.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by aesop_cat) : 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

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

@[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 N.counit = M.counit := by aesop_cat) (f_comul : CategoryTheory.CategoryStruct.comp f.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by aesop_cat) : (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 N.counit = M.counit := by aesop_cat) (f_comul : CategoryTheory.CategoryStruct.comp f.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) := by aesop_cat) : (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)

Equations

• A.uniqueHomToTrivial = { default := { hom := A.counit, hom_counit := ⋯, hom_comul := ⋯ }, uniq := ⋯ }

@[simp]

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

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

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

• Comon_.Comon_ToMon_OpOp_obj' C A = { X := Opposite.op A.X, one := A.counit.op, mul := A.comul.op, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Comon_.Comon_ToMon_OpOp_obj'_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : (Comon_ToMon_OpOp_obj' C A).one = A.counit.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.

Equations

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

@[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 (Comon_ToMon_OpOp_obj' C A)

@[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, one_hom := ⋯, mul_hom := ⋯ }

def Comon_.Mon_OpOpToComon_obj' (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_.Mon_OpOpToComon_obj' C A = { X := Opposite.unop A.X, counit := A.one.unop, comul := A.mul.unop, counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Comon_.Mon_OpOpToComon_obj'_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ Cᵒᵖ) : (Mon_OpOpToComon_obj' C A).comul = A.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.

Equations

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

@[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_OpOpToComon_obj' C (Opposite.unop A)

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

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_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_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_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_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Comon_EquivMon_OpOp C).functor = Comon_ToMon_OpOp 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_tensorUnit_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (𝟙_ (Comon_ C)).X = 𝟙_ 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_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_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_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_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_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon_ C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom X.counit Y.counit) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).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_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_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (𝟙_ (Comon_ C)).comul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).inv

@[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_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_tensorUnit_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (𝟙_ (Comon_ C)).counit = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Comon_.monoidal_tensorObj_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon_ C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom X.comul Y.comul) (CategoryTheory.MonoidalCategory.tensorμ X.X X.X Y.X Y.X)

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)

Equations

• Comon_.instComon_ClassTensorObj C A B = inferInstanceAs (Comon_Class (CategoryTheory.MonoidalCategoryStruct.tensorObj (Comon_.mk' A) (Comon_.mk' B)).X)

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

theorem Comon_.tensorObj_comul' (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : Comon_ C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B).comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom A.comul B.comul) (CategoryTheory.MonoidalCategory.tensorμ (Opposite.op A.X) (Opposite.op B.X) (Opposite.op A.X) (Opposite.op B.X)).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.

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

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 (𝟙_ 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 (𝟙_ 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)

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_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_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) : (F.mapComon.obj A).comul = CategoryStruct.comp (F.map A.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_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) : (F.mapComon.obj A).counit = CategoryStruct.comp (F.map A.counit) (OplaxMonoidal.η F)