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, an 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 CategoryTheory.ComonObj {C : Type u₁} [Category.{v₁, u₁} C] [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 ⟶ MonoidalCategoryStruct.tensorUnit C

  The counit morphism of a comonoid object.

• comul : X ⟶ MonoidalCategoryStruct.tensorObj X X

  The comultiplication morphism of a comonoid object.

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

def CategoryTheory.ComonObj.termΔ : Lean.ParserDescr

The comultiplication morphism of a comonoid object.

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

The comultiplication morphism of a comonoid object.

def CategoryTheory.ComonObj.termε : Lean.ParserDescr

The counit morphism of a comonoid object.

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

The counit morphism of a comonoid object.

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

The canonical comonoid structure on the monoidal unit. This is not a global instance to avoid conflicts with other comonoid structures.

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

instance CategoryTheory.instIsComonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [ComonObj M] : IsComonHom (CategoryStruct.id M)

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

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

instance CategoryTheory.instIsComonHomInv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [ComonObj M] [ComonObj N] (f : M ⟶ N) [IsComonHom f] [IsIso f] : IsComonHom (inv f)

structure CategoryTheory.Comon (C : Type u₁) [Category.{v₁, u₁} C] [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 : ComonObj self.X

def CategoryTheory.Comon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Comon C

The trivial comonoid object. We later show this is terminal in Comon C.

@[simp]

theorem CategoryTheory.Comon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (trivial C).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

structure CategoryTheory.Comon.Hom {C : Type u₁} [Category.{v₁, u₁} C] [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.

• isComonHom_hom : IsComonHom self.hom

theorem CategoryTheory.Comon.Hom.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : Comon C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Comon.Hom.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : Comon C} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

@[reducible, inline]

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

Construct a morphism M ⟶ N of Comon C from a map f : M ⟶ N and a IsComonHom f instance.

def CategoryTheory.Comon.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Comon C) : M.Hom M

The identity morphism on a comonoid object.

@[simp]

theorem CategoryTheory.Comon.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Comon C) : M.id.hom = CategoryStruct.id M.X

@[implicit_reducible]

instance CategoryTheory.Comon.homInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Comon C) : Inhabited (M.Hom M)

def CategoryTheory.Comon.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : Comon C} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Composition of morphisms of monoid objects.

@[simp]

theorem CategoryTheory.Comon.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : Comon C} (f : M.Hom N) (g : N.Hom O) : (comp f g).hom = CategoryStruct.comp f.hom g.hom

@[implicit_reducible]

instance CategoryTheory.Comon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Category.{v₁, max u₁ v₁} (Comon C)

instance CategoryTheory.Comon.instIsComonHomHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M ⟶ N) : IsComonHom f.hom

theorem CategoryTheory.Comon.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : Comon C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g

theorem CategoryTheory.Comon.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : Comon C} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

@[simp]

theorem CategoryTheory.Comon.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Comon C) : (CategoryStruct.id M).hom = CategoryStruct.id M.X

@[simp]

theorem CategoryTheory.Comon.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N K : Comon C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

def CategoryTheory.Comon.forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (Comon C) C

The forgetful functor from comonoid objects to the ambient category.

@[simp]

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

@[simp]

theorem CategoryTheory.Comon.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : (forget C).obj A = A.X

instance CategoryTheory.Comon.forget_faithful {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (forget C).Faithful

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

instance CategoryTheory.Comon.instReflectsIsomorphismsForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (forget C).ReflectsIsomorphisms

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

def CategoryTheory.Comon.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) [IsComonHom f.hom] : M ≅ N

Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects and checking compatibility with counit and comultiplication only in the forward direction.

@[simp]

theorem CategoryTheory.Comon.mkIso'_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) [IsComonHom f.hom] : (mkIso' f).inv.hom = f.inv

@[simp]

theorem CategoryTheory.Comon.mkIso'_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) [IsComonHom f.hom] : (mkIso' f).hom.hom = f.hom

def CategoryTheory.Comon.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) (f_counit : CategoryStruct.comp f.hom ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryStruct.comp f.hom ComonObj.comul = CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : M ≅ N

Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects and checking compatibility with counit and comultiplication only in the forward direction.

@[simp]

theorem CategoryTheory.Comon.mkIso_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) (f_counit : CategoryStruct.comp f.hom ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryStruct.comp f.hom ComonObj.comul = CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : (mkIso f f_counit f_comul).inv.hom = f.inv

@[simp]

theorem CategoryTheory.Comon.mkIso_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Comon C} (f : M.X ≅ N.X) (f_counit : CategoryStruct.comp f.hom ComonObj.counit = ComonObj.counit := by cat_disch) (f_comul : CategoryStruct.comp f.hom ComonObj.comul = CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom f.hom f.hom) := by cat_disch) : (mkIso f f_counit f_comul).hom.hom = f.hom

@[implicit_reducible]

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

@[simp]

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

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

@[reducible, inline]

abbrev CategoryTheory.Comon.ComonToMonOpOpObjMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : MonObj (Opposite.op A.X)

Auxiliary definition for ComonToMonOpOpObj.

def CategoryTheory.Comon.ComonToMonOpOpObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : Mon Cᵒᵖ

Turn a comonoid object into a monoid object in the opposite category.

@[simp]

theorem CategoryTheory.Comon.ComonToMonOpOpObj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : MonObj.mul = ComonObj.comul.op

@[simp]

theorem CategoryTheory.Comon.ComonToMonOpOpObj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : MonObj.one = ComonObj.counit.op

@[simp]

theorem CategoryTheory.Comon.ComonToMonOpOpObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : A.ComonToMonOpOpObj.X = Opposite.op A.X

def CategoryTheory.Comon.ComonToMonOpOp (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (Comon C) (Mon Cᵒᵖ)ᵒᵖ

The contravariant functor turning comonoid objects into monoid objects in the opposite category.

@[simp]

theorem CategoryTheory.Comon.ComonToMonOpOp_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : Comon C} (f : X✝ ⟶ Y✝) : (ComonToMonOpOp C).map f = Opposite.op { hom := f.hom.op, isMonHom_hom := ⋯ }

@[simp]

theorem CategoryTheory.Comon.ComonToMonOpOp_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Comon C) : (ComonToMonOpOp C).obj A = Opposite.op A.ComonToMonOpOpObj

@[reducible, inline]

abbrev CategoryTheory.Comon.MonOpOpToComonObjComon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj (Opposite.unop A.X)

Auxiliary definition for MonOpOpToComonObj.

def CategoryTheory.Comon.MonOpOpToComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon Cᵒᵖ) : Comon C

Turn a monoid object in the opposite category into a comonoid object.

@[simp]

theorem CategoryTheory.Comon.MonOpOpToComonObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon Cᵒᵖ) : (MonOpOpToComonObj A).X = Opposite.unop A.X

@[simp]

theorem CategoryTheory.Comon.MonOpOpToComonObj_comon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj.counit = MonObj.one.unop

@[simp]

theorem CategoryTheory.Comon.MonOpOpToComonObj_comon_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon Cᵒᵖ) : ComonObj.comul = MonObj.mul.unop

def CategoryTheory.Comon.MonOpOpToComon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (Mon Cᵒᵖ)ᵒᵖ (Comon C)

The contravariant functor turning monoid objects in the opposite category into comonoid objects.

@[simp]

theorem CategoryTheory.Comon.MonOpOpToComon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : (Mon Cᵒᵖ)ᵒᵖ) : (MonOpOpToComon C).obj A = MonOpOpToComonObj (Opposite.unop A)

@[simp]

theorem CategoryTheory.Comon.MonOpOpToComon_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((MonOpOpToComon C).map f).hom = f.unop.hom.unop

def CategoryTheory.Comon.Comon_EquivMon_OpOp (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Comon C ≌ (Mon Cᵒᵖ)ᵒᵖ

Comonoid objects are contravariantly equivalent to monoid objects in the opposite category.

@[simp]

theorem CategoryTheory.Comon.Comon_EquivMon_OpOp_inverse (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (Comon_EquivMon_OpOp C).inverse = MonOpOpToComon C

@[simp]

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

@[simp]

theorem CategoryTheory.Comon.Comon_EquivMon_OpOp_unitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (Comon_EquivMon_OpOp C).unitIso = NatIso.ofComponents (fun (x : Comon C) => Iso.refl ((Functor.id (Comon C)).obj x)) ⋯

@[simp]

theorem CategoryTheory.Comon.Comon_EquivMon_OpOp_counitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (Comon_EquivMon_OpOp C).counitIso = NatIso.ofComponents (fun (x : (Mon Cᵒᵖ)ᵒᵖ) => Iso.refl (((MonOpOpToComon C).comp (ComonToMonOpOp C)).obj x)) ⋯

@[implicit_reducible]

instance CategoryTheory.Comon.monoidal (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonoidalCategory (Comon C)

Comonoid objects in a braided category form a monoidal category.

This definition is via transporting back and forth to monoids in the opposite category.

@[simp]

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

@[simp]

theorem CategoryTheory.Comon.monoidal_associator_inv_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : Comon C) : (MonoidalCategoryStruct.associator X Y Z).inv.hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X.X (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop) (CategoryStruct.comp (MonoidalCategoryStruct.associator X.X Y.X Z.X).inv (MonoidalCategoryStruct.whiskerRight (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop Z.X))

@[simp]

theorem CategoryTheory.Comon.monoidal_tensorUnit_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (MonoidalCategoryStruct.tensorUnit (Comon C)).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.Comon.monoidal_rightUnitor_hom_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Comon C) : (MonoidalCategoryStruct.rightUnitor X).hom.hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X.X (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorUnit (Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop) (MonoidalCategoryStruct.rightUnitor X.X).hom

@[simp]

theorem CategoryTheory.Comon.monoidal_leftUnitor_hom_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Comon C) : (MonoidalCategoryStruct.leftUnitor X).hom.hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorUnit (Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop X.X) (MonoidalCategoryStruct.leftUnitor X.X).hom

@[simp]

theorem CategoryTheory.Comon.monoidal_rightUnitor_inv_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Comon C) : (MonoidalCategoryStruct.rightUnitor X).inv.hom = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X.X).inv (MonoidalCategoryStruct.whiskerLeft X.X (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorUnit (Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop)

@[simp]

theorem CategoryTheory.Comon.monoidal_whiskerLeft_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X x✝ x✝¹ : Comon C) (f : x✝ ⟶ x✝¹) : (MonoidalCategoryStruct.whiskerLeft X f).hom = MonoidalCategoryStruct.whiskerLeft X.X f.hom

@[simp]

theorem CategoryTheory.Comon.monoidal_associator_hom_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : Comon C) : (MonoidalCategoryStruct.associator X Y Z).hom.hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop Z.X) (CategoryStruct.comp (MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (MonoidalCategoryStruct.whiskerLeft X.X (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop))

@[simp]

theorem CategoryTheory.Comon.monoidal_tensorHom_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Comon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (MonoidalCategoryStruct.tensorHom f g).hom = MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

theorem CategoryTheory.Comon.monoidal_whiskerRight_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X₁✝ X₂✝ : Comon C} (f : X₁✝ ⟶ X₂✝) (X : Comon C) : (MonoidalCategoryStruct.whiskerRight f X).hom = MonoidalCategoryStruct.whiskerRight f.hom X.X

@[simp]

theorem CategoryTheory.Comon.monoidal_leftUnitor_inv_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Comon C) : (MonoidalCategoryStruct.leftUnitor X).inv.hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X.X).inv (MonoidalCategoryStruct.whiskerRight (CategoryStruct.id (Opposite.op (MonOpOpToComonObj (MonoidalCategoryStruct.tensorUnit (Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop X.X)

@[simp]

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

@[simp]

theorem CategoryTheory.Comon.monoidal_tensorObj_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Comon C) : (MonoidalCategoryStruct.tensorObj X Y).X = MonoidalCategoryStruct.tensorObj X.X Y.X

@[simp]

theorem CategoryTheory.Comon.monoidal_tensorObj_comon_comul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Comon C) : ComonObj.comul = MonObj.mul.unop

theorem CategoryTheory.Comon.tensorObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A B : Comon C) : (MonoidalCategoryStruct.tensorObj A B).X = MonoidalCategoryStruct.tensorObj A.X B.X

@[implicit_reducible]

instance CategoryTheory.Comon.instComonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A B : C) [ComonObj A] [ComonObj B] : ComonObj (MonoidalCategoryStruct.tensorObj A B)

@[simp]

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

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

@[implicit_reducible]

instance CategoryTheory.Comon.instMonoidalForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (forget C).Monoidal

The forgetful functor from Comon C to C is monoidal when C is monoidal.

@[simp]

theorem CategoryTheory.Comon.forget_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor.LaxMonoidal.ε (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Comon.forget_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor.OplaxMonoidal.η (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Comon.forget_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Comon C) : Functor.LaxMonoidal.μ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem CategoryTheory.Comon.forget_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Comon C) : Functor.OplaxMonoidal.δ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

@[reducible, inline]

abbrev CategoryTheory.Functor.obj.instComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : C) [ComonObj A] (F : Functor C D) [F.OplaxMonoidal] : ComonObj (F.obj A)

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

@[simp]

theorem CategoryTheory.Functor.obj.ε_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] : ComonObj.counit = CategoryStruct.comp (F.map ComonObj.counit) (OplaxMonoidal.η F)

theorem CategoryTheory.Functor.obj.ε_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp ComonObj.counit h = CategoryStruct.comp (F.map ComonObj.counit) (CategoryStruct.comp (OplaxMonoidal.η F) h)

@[simp]

theorem CategoryTheory.Functor.obj.Δ_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] : ComonObj.comul = CategoryStruct.comp (F.map ComonObj.comul) (OplaxMonoidal.δ F X X)

theorem CategoryTheory.Functor.obj.Δ_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) [ComonObj X] {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj X) ⟶ Z) : CategoryStruct.comp ComonObj.comul h = CategoryStruct.comp (F.map ComonObj.comul) (CategoryStruct.comp (OplaxMonoidal.δ F X X) h)

instance CategoryTheory.Functor.map.instIsComon_Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y : C} [ComonObj X] [ComonObj Y] (f : X ⟶ Y) [IsComonHom f] : IsComonHom (F.map f)

def CategoryTheory.Functor.mapComon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] : Functor (Comon C) (Comon D)

An oplax monoidal functor takes comonoid objects to comonoid objects.

That is, an oplax monoidal functor F : C ⥤ D induces a functor Comon C ⥤ Comon D.

@[simp]

theorem CategoryTheory.Functor.mapComon_obj_comon_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (A : Comon C) : ComonObj.comul = CategoryStruct.comp (F.map ComonObj.comul) (OplaxMonoidal.δ F A.X A.X)

@[simp]

theorem CategoryTheory.Functor.mapComon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (A : Comon C) : (F.mapComon.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapComon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X✝ Y✝ : Comon C} (f : X✝ ⟶ Y✝) : (F.mapComon.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapComon_obj_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) : ComonObj.counit = CategoryStruct.comp (F.map ComonObj.counit) (OplaxMonoidal.η F)

class CategoryTheory.IsCommComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [ComonObj X] : Prop

Predicate for a comonoid object to be commutative.

• comul_comm : CategoryStruct.comp ComonObj.comul (β_ X X).hom = ComonObj.comul

@[simp]

theorem CategoryTheory.IsCommComonObj.comul_comm_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (X : C) {inst✝³ : ComonObj X} [self : IsCommComonObj X] {Z : C} (h : MonoidalCategoryStruct.tensorObj X X ⟶ Z) : CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (β_ X X).hom h) = CategoryStruct.comp ComonObj.comul h