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

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

@[simp]

theorem Comon_Class.comul_counit_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : Comon_Class X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z) :

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

source

@[simp]

theorem Comon_Class.counit_comul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : Comon_Class X] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ⟶ Z) :

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

source

@[simp]

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

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

source

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.

source

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

source

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

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.MonoidalCategoryStruct.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 : CategoryTheory.MonoidalCategoryStruct.tensorUnit 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.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)

source

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

IsComon_Hom (CategoryTheory.CategoryStruct.id M)

source

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

IsComon_Hom (CategoryTheory.CategoryStruct.comp f g)

source

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

source

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

IsComon_Hom (CategoryTheory.inv f)

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.
comon : Comon_Class self.X

Instances For

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

Comon_.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, comon := Comon_Class.instTensorUnit C }

Instances For

source

@[simp]

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

(trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C

source

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

source

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

source

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

Inhabited (Comon_ C)

Equations

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

source

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

source

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

source

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

source

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

source

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)

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.
is_comon_hom : IsComon_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

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

source

@[reducible, inline]

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

M.Hom N

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 f_counit f_comul = { hom := f, is_comon_hom := ⋯ }

Instances For

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

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

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

(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

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

source

instance Comon_.instIsComon_HomHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Comon_ C} (f : M ⟶ N) :

IsComon_Hom f.hom

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

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

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

source

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

source

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

(forget C).Faithful

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 ((forget C).map f)] :

CategoryTheory.IsIso f.hom

source

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.

source

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 := { hom := f.hom, is_comon_hom := inst✝ }, inv := { hom := f.inv, is_comon_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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) [IsComon_Hom f.hom] :

(mkIso' f).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) [IsComon_Hom f.hom] :

(mkIso' f).hom.hom = f.hom

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

Comon_.mkIso f f_counit f_comul = { hom := { hom := f.hom, is_comon_hom := ⋯ }, inv := { hom := f.inv, is_comon_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

source

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

source

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

source

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

CategoryTheory.Limits.HasTerminal (Comon_ C)

source

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

Instances For

source

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 }

Instances For

source

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

source

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

source

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

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_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Comon_ C} (f : X✝ ⟶ Y✝) :

(Comon_ToMon_OpOp C).map f = Opposite.op { hom := f.hom.op, is_mon_hom := ⋯ }

source

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

source

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

Instances For

source

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 }

Instances For

source

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

source

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

source

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

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

source

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

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

source

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

source

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

source

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

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

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.MonoidalCategoryStruct.tensorObj X Y).X = CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X

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

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

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

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.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.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.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv

source

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

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.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom

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

source

@[simp]

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

Comon_Class.counit = Mon_Class.one.unop

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

source

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

source

@[simp]

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

Comon_Class.comul = Mon_Class.mul.unop

source

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

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

source

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

source

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.

source

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

source