Documentation

Mathlib.CategoryTheory.Monoidal.Conv

The convolution monoid. #

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

source
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 have a (set-theoretic) monoid structure.

Equations
    Instances For
      source
      instance CategoryTheory.Conv.instOne {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [ComonObj M] [MonObj N] :
      One (Conv M N)
      Equations
        source
        theorem CategoryTheory.Conv.one_eq {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [ComonObj M] [MonObj N] :
        1 = CategoryStruct.comp ComonObj.counit MonObj.one
        source
        instance CategoryTheory.Conv.instMul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [ComonObj M] [MonObj N] :
        Mul (Conv M N)
        Equations
          source
          theorem CategoryTheory.Conv.mul_eq {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [ComonObj M] [MonObj N] (f g : Conv M N) :
          f * g = CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f M) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft N g) MonObj.mul))
          source
          instance CategoryTheory.Conv.instMonoid {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [ComonObj M] [MonObj N] :
          Monoid (Conv M N)
          Equations