monoidalCategoryMop — Mathlib

Lean4
instance monoidalCategoryMop : MonoidalCategory Cᴹᵒᵖ
    where
  tensorObj X Y := mop (unmop Y ⊗ unmop X)
  whiskerLeft X _ _ f := (f.unmop ▷ X.unmop).mop
  whiskerRight f X := (X.unmop ◁ f.unmop).mop
  tensorHom f g := (g.unmop ⊗ₘ f.unmop).mop
  tensorHom_def _ _ := Quiver.Hom.unmop_inj (tensorHom_def' _ _)
  tensorHom_comp_tensorHom _ _ _ _ := Quiver.Hom.unmop_inj <| by simp
  tensorUnit := mop (𝟙_ C)
  associator X Y Z := (α_ (unmop Z) (unmop Y) (unmop X)).symm.mop
  leftUnitor X := (ρ_ (unmop X)).mop
  rightUnitor X := (λ_ (unmop X)).mop
  associator_naturality f g h := Quiver.Hom.unmop_inj <| by simp
  leftUnitor_naturality f := Quiver.Hom.unmop_inj <| by simp
  rightUnitor_naturality f := Quiver.Hom.unmop_inj <| by simp
  triangle X Y := Quiver.Hom.unmop_inj <| by dsimp; monoidal_coherence
  pentagon W X Y
    Z :=
    Quiver.Hom.unmop_inj <| by dsimp;
      monoidal_coherence
        -- it would be nice if we could autogenerate all of these somehow
Похожие утверждения