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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Comon_ C) (N : Mon_ 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.X ⟶ N.X)

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

Equations

• CategoryTheory.Conv.instOne = { one := CategoryTheory.CategoryStruct.comp M.counit N.one }

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

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

Equations

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

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

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

Equations

• CategoryTheory.Conv.instMonoid = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯