tensorLeftMopIso — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\text{tensorIso}(C) :\\; \\text{tensor } C^{\\mathrm{op}} \\cong (\\mathrm{unmop}(C) ∘\\; \\text{tensorRight } X \\; ∘\\; \\text{mopFunctor } C) $$$$

Lean4

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

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