instMonoidalCategoryStruct — Mathlib

Lean4

@[simps! tensorObj_X tensorHom_hom]
instance instMonoidalCategoryStruct : MonoidalCategoryStruct (Grp_ C)
    where
  tensorObj G H := ⟨G.X ⊗ H.X⟩
  tensorHom := tensorHom (C := Mon C)
  whiskerRight f G := whiskerRight (C := Mon C) f G.toMon
  whiskerLeft G _ _ f := MonoidalCategoryStruct.whiskerLeft (C := Mon C) G.toMon f
  tensorUnit := ⟨𝟙_ C⟩
  associator X Y Z := (Grp_.fullyFaithfulForget₂Mon C).preimageIso (associator X.toMon Y.toMon Z.toMon)
  leftUnitor G := (Grp_.fullyFaithfulForget₂Mon C).preimageIso (leftUnitor G.toMon)
  rightUnitor G := (Grp_.fullyFaithfulForget₂Mon C).preimageIso (rightUnitor G.toMon)

Похожие утверждения