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.

source

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.MonoidalCategory.tensorObj X X
The comultiplication morphism of a comonoid object.
counit_comul' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.counit X) = (CategoryTheory.MonoidalCategory.leftUnitor X).inv
comul_counit' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft X Comon_Class.counit) = (CategoryTheory.MonoidalCategory.rightUnitor X).inv
comul_assoc' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft X Comon_Class.comul) = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.comul X) (CategoryTheory.MonoidalCategory.associator X X X).hom)

Instances

source

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

Instances For

source

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.

Instances For

source

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

Instances For

source

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.

Instances For

source

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.MonoidalCategory.tensorObj (𝟙_ C) X ⟶ Z) :

CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.counit X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv h

source

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.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj X X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Comon_Class.comul) h) = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.comul X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X X X).hom h))

source

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.MonoidalCategory.tensorObj X (𝟙_ C) ⟶ Z) :

CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Comon_Class.counit) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv h

source

@[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 Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.counit X) = (CategoryTheory.MonoidalCategory.leftUnitor X).inv

source

@[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.MonoidalCategory.tensorObj (𝟙_ C) X ⟶ Z) :

source

@[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 Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft X Comon_Class.counit) = (CategoryTheory.MonoidalCategory.rightUnitor X).inv

source

@[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.MonoidalCategory.tensorObj X (𝟙_ C) ⟶ Z) :

source

@[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 Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft X Comon_Class.comul) = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.comul X) (CategoryTheory.MonoidalCategory.associator X X X).hom)

source

@[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.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj X X) ⟶ Z) :

source

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.MonoidalCategory.tensorHom f f)

Instances

source

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

source

@[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.MonoidalCategory.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.MonoidalCategory.tensorHom f f) h)

source

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.MonoidalCategory.tensorObj self.X self.X
The comultiplication morphism of a comonoid object.
counit_comul : CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.MonoidalCategory.whiskerRight self.counit self.X) = (CategoryTheory.MonoidalCategory.leftUnitor self.X).inv
comul_counit : CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.counit) = (CategoryTheory.MonoidalCategory.rightUnitor self.X).inv
comul_assoc : CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.comul) = CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.comul self.X) (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom)

Instances For

source

@[simp]

theorem Comon_.counit_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Comon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) self.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.counit self.X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).inv h

source

@[simp]

theorem Comon_.comul_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Comon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj self.X (𝟙_ C) ⟶ Z) :

CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.counit) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor self.X).inv h

source

@[simp]

theorem Comon_.comul_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Comon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj self.X (CategoryTheory.MonoidalCategory.tensorObj self.X self.X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.comul) h) = CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.comul self.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom h))

source

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

Instances For

source

@[simp]

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

(Comon_.mk' X).counit = Comon_Class.counit

source

@[simp]

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

(Comon_.mk' X).comul = Comon_Class.comul

source

@[simp]

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

(Comon_.mk' X).X = X

source

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' := ⋯ }

source

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.

Instances For

source

@[simp]

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

(Comon_.trivial C).X = 𝟙_ C

source

@[simp]

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

(Comon_.trivial C).comul = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv

source

@[simp]

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

(Comon_.trivial C).counit = CategoryTheory.CategoryStruct.id (𝟙_ C)

source

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 }

source

@[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.MonoidalCategory.tensorHom M.counit f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor Z).inv

source

@[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.MonoidalCategory.tensorObj (𝟙_ C) Z ⟶ Z✝) :

CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.counit f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor Z).inv h)

source

@[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.MonoidalCategory.tensorHom f M.counit) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor Z).inv

source

@[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.MonoidalCategory.tensorObj Z (𝟙_ C) ⟶ Z✝) :

CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f M.counit) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Z).inv h)

source

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.MonoidalCategory.whiskerRight M.comul M.X) = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X M.comul) (CategoryTheory.MonoidalCategory.associator M.X M.X M.X).inv)

source

theorem Comon_.comul_assoc_flip_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj M.X M.X) M.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight M.comul M.X) h) = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X M.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X M.X M.X).inv h))

source

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.MonoidalCategory.tensorHom self.hom self.hom)

Instances For

source

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

source

@[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.MonoidalCategory.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.MonoidalCategory.tensorHom self.hom self.hom) h)

source

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

source

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

Instances For

source

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

source

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 }

source

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

Instances For

source

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

(Comon_.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

source

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

source

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

source

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

source

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

source

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

Instances For

source

@[simp]

theorem Comon_.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) :

(Comon_.forget C).obj A = A.X

source

@[simp]

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

(Comon_.forget C).map f = f.hom

source

instance Comon_.forget_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(Comon_.forget C).Faithful

Equations

⋯ = ⋯

source

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

CategoryTheory.IsIso f.hom

Equations

⋯ = e

source

instance Comon_.instReflectsIsomorphismsForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(Comon_.forget C).ReflectsIsomorphisms

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

Equations

⋯ = ⋯

source

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.MonoidalCategory.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.

Instances For

source

@[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.MonoidalCategory.tensorHom f.hom f.hom) := by aesop_cat) :

(Comon_.mkIso f f_counit f_comul).inv.hom = f.inv

source

@[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.MonoidalCategory.tensorHom f.hom f.hom) := by aesop_cat) :

(Comon_.mkIso f f_counit f_comul).hom.hom = f.hom

source

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

Unique (A ⟶ Comon_.trivial C)

Equations

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

source

@[simp]

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

default.hom = A.counit

source

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

CategoryTheory.Limits.HasTerminal (Comon_ C)

Equations

⋯ = ⋯

source

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

Instances For

source

@[simp]

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

(Comon_.Comon_ToMon_OpOp_obj' C A).X = Opposite.op A.X

source

@[simp]

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

(Comon_.Comon_ToMon_OpOp_obj' C A).mul = A.comul.op

source

@[simp]

theorem Comon_.Comon_ToMon_OpOp_obj'_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) :

(Comon_.Comon_ToMon_OpOp_obj' C A).one = A.counit.op

source

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.

Instances For

source

@[simp]

theorem Comon_.Comon_ToMon_OpOp_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Comon_ C) :

(Comon_.Comon_ToMon_OpOp C).obj A = Opposite.op (Comon_.Comon_ToMon_OpOp_obj' C A)

source

@[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_.Comon_ToMon_OpOp C).map f = Opposite.op { hom := f.hom.op, one_hom := ⋯, mul_hom := ⋯ }

source

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

Instances For

source

@[simp]

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

(Comon_.Mon_OpOpToComon_obj' C A).counit = A.one.unop

source

@[simp]

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

(Comon_.Mon_OpOpToComon_obj' C A).X = Opposite.unop A.X

source

@[simp]

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

(Comon_.Mon_OpOpToComon_obj' C A).comul = A.mul.unop

source

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.

Instances For

source

@[simp]

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

(Comon_.Mon_OpOpToComon_ C).obj A = Comon_.Mon_OpOpToComon_obj' C (Opposite.unop A)

source

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

((Comon_.Mon_OpOpToComon_ C).map f).hom = f.unop.hom.unop

source

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.

Instances For

source

@[simp]

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

(Comon_.Comon_EquivMon_OpOp C).inverse = Comon_.Mon_OpOpToComon_ C

source

@[simp]

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

(Comon_.Comon_EquivMon_OpOp C).unitIso = CategoryTheory.NatIso.ofComponents (fun (x : Comon_ C) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (Comon_ C)).obj x)) ⋯

source

@[simp]

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

(Comon_.Comon_EquivMon_OpOp C).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : (Mon_ Cᵒᵖ)ᵒᵖ) => CategoryTheory.Iso.refl (((Comon_.Mon_OpOpToComon_ C).comp (Comon_.Comon_ToMon_OpOp C)).obj x)) ⋯

source

@[simp]

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

(Comon_.Comon_EquivMon_OpOp C).functor = Comon_.Comon_ToMon_OpOp C

source

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

source

@[simp]

theorem Comon_.monoidal_tensorUnit_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(𝟙_ (Comon_ C)).X = 𝟙_ C

source

@[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.MonoidalCategory.whiskerLeft X f).hom = CategoryTheory.MonoidalCategory.whiskerLeft X.X f.hom

source

@[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.MonoidalCategory.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.X).hom

source

@[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.MonoidalCategory.whiskerRight f X).hom = CategoryTheory.MonoidalCategory.whiskerRight f.hom X.X

source

@[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.MonoidalCategory.tensorObj X Y).X = CategoryTheory.MonoidalCategory.tensorObj X.X Y.X

source

@[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.MonoidalCategory.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.X).inv

source

@[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.MonoidalCategory.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.X).inv

source

@[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.MonoidalCategory.tensorObj X Y).counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom X.counit Y.counit) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom

source

@[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.MonoidalCategory.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategory.associator X.X Y.X Z.X).inv

source

@[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.MonoidalCategory.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategory.associator X.X Y.X Z.X).hom

source

@[simp]

theorem Comon_.monoidal_tensorUnit_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(𝟙_ (Comon_ C)).comul = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv

source

@[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.MonoidalCategory.tensorHom f g).hom = CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom

source

@[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.MonoidalCategory.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.X).hom

source

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

source

@[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.MonoidalCategory.tensorObj X Y).comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom X.comul Y.comul) (CategoryTheory.MonoidalCategory.tensorμ X.X X.X Y.X Y.X)

source

theorem Comon_.tensorObj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : Comon_ C) :

(CategoryTheory.MonoidalCategory.tensorObj A B).X = CategoryTheory.MonoidalCategory.tensorObj A.X B.X

source

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.MonoidalCategory.tensorObj A B)

Equations

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

source

theorem Comon_.tensorObj_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : Comon_ C) :

(CategoryTheory.MonoidalCategory.tensorObj A B).counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.counit B.counit) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom

source

theorem Comon_.tensorObj_comul' (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : Comon_ C) :

(CategoryTheory.MonoidalCategory.tensorObj A B).comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.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.

source

theorem Comon_.tensorObj_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A B : Comon_ C) :

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

source