The convolution monoid.

When M : Comon_ C and N : Mon_ C, the morphisms M.X ⟶ N.X form a monoid (in Type).

def CategoryTheory.Conv {C : Type u₁} [Category.{v₁, u₁} C] (M N : C) : Type v₁

The morphisms in C between the underlying objects of a pair of bimonoids in C naturally has a (set-theoretic) monoid structure.

Equations

• CategoryTheory.Conv M N = (M ⟶ N)

instance CategoryTheory.Conv.instOne {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [Comon_Class M] [Mon_Class N] : One (Conv M N)

Equations

• CategoryTheory.Conv.instOne = { one := CategoryTheory.CategoryStruct.comp Comon_Class.counit Mon_Class.one }

theorem CategoryTheory.Conv.one_eq {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [Comon_Class M] [Mon_Class N] : 1 = CategoryStruct.comp Comon_Class.counit Mon_Class.one

instance CategoryTheory.Conv.instMul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [Comon_Class M] [Mon_Class N] : Mul (Conv M N)

Equations

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

theorem CategoryTheory.Conv.mul_eq {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [Comon_Class M] [Mon_Class N] (f g : Conv M N) : f * g = CategoryStruct.comp Comon_Class.comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f M) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft N g) Mon_Class.mul))

instance CategoryTheory.Conv.instMonoid {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [Comon_Class M] [Mon_Class N] : Monoid (Conv M N)

Equations

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