mop — Mathlib

English

For any morphism f: X → Y in C, mop f is the same morphism viewed in the opposite context.

Русский

Для морфизма f: X→Y в C mop f — тот же морфизм, рассматриваемый в противоположной категории.

LaTeX

$$$$ \\operatorname{mop}(f) = f $$$$

Lean4

/-- The monoidal opposite of a morphism `f : X ⟶ Y` is just `f`, thought of as `mop X ⟶ mop Y`. -/
def mop {X Y : C} (f : X ⟶ Y) : mop X ⟶ mop Y :=
  MonoidalOpposite.mop f

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