English
The Day convolution Conv M N carries a natural monoid structure; multiplication uses whiskering and the DayConvolution braiding, unit uses a unit object, and associativity holds.
Русский
DayConvolution Conv M N естественно образует моноид; умножение задаётся через whisker и braiding DayConvolution, единица через единичный объект, ассоциативность выполняется.
LaTeX
$$$\text{Conv } M N \text{ is a Monoid}$ with unit and multiplication defined by whiskering and DayConvolution braiding.$$
Lean4
instance : Monoid (Conv M N)
where
one_mul f := by simp [one_eq, mul_eq, ← whisker_exchange_assoc]
mul_one f := by simp [one_eq, mul_eq, ← whisker_exchange_assoc]
mul_assoc f g
h := by
simp only [mul_eq]
simp only [comp_whiskerRight, whisker_assoc, Category.assoc, MonoidalCategory.whiskerLeft_comp]
slice_lhs 7 8 => rw [← whisker_exchange]
slice_rhs 2 3 => rw [← whisker_exchange]
simp
