monoidalCategoryOp — Mathlib

Lean4
instance monoidalCategoryOp : MonoidalCategory Cᵒᵖ
    where
  tensorObj X Y := op (unop X ⊗ unop Y)
  whiskerLeft X _ _ f := (X.unop ◁ f.unop).op
  whiskerRight f X := (f.unop ▷ X.unop).op
  tensorHom f g := (f.unop ⊗ₘ g.unop).op
  tensorHom_def _ _ := Quiver.Hom.unop_inj (tensorHom_def' _ _)
  tensorHom_comp_tensorHom _ _ _ _ := Quiver.Hom.unop_inj <| by simp
  tensorUnit := op (𝟙_ C)
  associator X Y Z := (α_ (unop X) (unop Y) (unop Z)).symm.op
  leftUnitor X := (λ_ (unop X)).symm.op
  rightUnitor X := (ρ_ (unop X)).symm.op
  associator_naturality f g h := Quiver.Hom.unop_inj <| by simp
  leftUnitor_naturality f := Quiver.Hom.unop_inj <| by simp
  rightUnitor_naturality f := Quiver.Hom.unop_inj <| by simp
  triangle X Y := Quiver.Hom.unop_inj <| by dsimp; monoidal_coherence
  pentagon W X Y Z := Quiver.Hom.unop_inj <| by dsimp; monoidal_coherence
Похожие утверждения