tensorRightMopIso — Mathlib

English

The identification - ⊗ mop X = mop (- ⊗ unmop X) as a natural isomorphism.

Русский

Идентификация - ⊗ mop X = mop (- ⊗ unmop X) как естественный изоморфизм.

LaTeX

$$$$ \\text{tensorRightMopIso}(X) :\\; \\text{tensorRight }(\\mathrm{mop} X) \\cong \\mathrm{unmopFunctor}(C) ∘ \\text{tensorLeft } X ∘ \\text{mopFunctor } C $$$$

Lean4

/-- The identification `- ⊗ mop X = mop (- ⊗ unmop X)` as a natural isomorphism. -/
@[simps!]
def tensorRightMopIso (X : C) : tensorRight (mop X) ≅ unmopFunctor C ⋙ tensorLeft X ⋙ mopFunctor C :=
  Iso.refl _

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