monoidalOfHasFiniteCoproducts — Mathlib

Lean4
/-- A category with an initial object and binary coproducts has a natural monoidal structure. -/
def monoidalOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : MonoidalCategory C :=
  letI : MonoidalCategoryStruct C :=
    { tensorObj := fun X Y ↦ X ⨿ Y
      whiskerLeft := fun _ _ _ g ↦ Limits.coprod.map (𝟙 _) g
      whiskerRight := fun {_ _} f _ ↦ Limits.coprod.map f (𝟙 _)
      tensorHom := fun f g ↦ Limits.coprod.map f g
      tensorUnit := ⊥_ C
      associator := coprod.associator
      leftUnitor := fun P ↦ coprod.leftUnitor P
      rightUnitor := fun P ↦ coprod.rightUnitor P }
  .ofTensorHom (pentagon := coprod.pentagon) (triangle := coprod.triangle) (associator_naturality :=
    @coprod.associator_naturality _ _ _)
Похожие утверждения