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.

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

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

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

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

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

Equations

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

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

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

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

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.

Equations

• Comon_.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, comon := Comon_Class.instTensorUnit 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)

Equations

• Comon_.instInhabited = { default := Comon_.trivial 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.

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

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

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

@[reducible, inline]

abbrev Comon_.Hom.mk' {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] : { X := M, comon := inst✝ }.Hom { X := N, comon := inst✝¹ }

Construct a morphism M ⟶ N of Comon_ C from a map f : M ⟶ N and a IsComon_Hom f instance.

Equations

• Comon_.Hom.mk' f = { hom := f, hom_counit := ⋯, hom_comul := ⋯ }

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 : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = CategoryTheory.CategoryStruct.comp Comon_Class.counit h

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 Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom self.hom self.hom) h)

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

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

instance Comon_.instIsComon_HomHom_1 {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.

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

Equations

• Comon_.mkIso' f = { hom := Comon_.Hom.mk' f.hom, inv := Comon_.Hom.mk' f.inv, 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) [IsComon_Hom f.hom] : (mkIso' f).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) [IsComon_Hom f.hom] : (mkIso' f).inv.hom = f.inv

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

Equations

• A.Comon_ToMon_OpOpObjMon = { one := Comon_Class.counit.op, mul := Comon_Class.comul.op, one_mul' := ⋯, mul_one' := ⋯, mul_assoc' := ⋯ }

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.

Equations

• A.Comon_ToMon_OpOpObj = { X := Opposite.op A.X, mon := A.Comon_ToMon_OpOpObjMon }

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

@[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_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) : Mon_Class.one = Comon_Class.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_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 := ⋯ }

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

Equations

• Comon_.Mon_OpOpToComonObjComon A = { counit := Mon_Class.one.unop, comul := Mon_Class.mul.unop, counit_comul' := ⋯, comul_counit' := ⋯, comul_assoc' := ⋯ }

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.

Equations

• Comon_.Mon_OpOpToComonObj A = { X := Opposite.unop A.X, comon := Comon_.Mon_OpOpToComonObjComon A }

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

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

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_OpOpToComonObj (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_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_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)) ⋯

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_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_comon_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon_ C) : Comon_Class.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.counit Comon_Class.counit) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

@[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_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_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_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_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_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_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_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_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_tensorObj_comon_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Comon_ C) : Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.MonoidalCategory.tensorμ X.X X.X Y.X Y.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_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_.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 A B = inferInstanceAs (Comon_Class (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) [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.

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)

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

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