The scalars of a monoidal category commute

The endomorphisms of the tensor unit form a commutative monoid. The tensor product is a second unital multiplication on End (𝟙_ C), and the interchange law makes it compatible with composition, so the Eckmann–Hilton argument applies: conjugating by the unitor writes an endomorphism of the unit either as a right whiskering or as a left whiskering, and whiskerings on opposite sides commute.

theorem RS.unit_comp_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp g f

Endomorphisms of the tensor unit commute.

@[instance_reducible]

instance RS.endUnitCommMonoid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CommMonoid (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

The scalars form a commutative monoid.

Equations

• RS.endUnitCommMonoid = { toMonoid := inferInstance, mul_comm := ⋯ }

theorem RS.braiding_unit_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

The unit braids trivially with itself.