opEquiv — Mathlib

English

There is a natural equivalence between arrows X → Y and opposites op Y → op X.

Русский

Существует естественное эквивалентное соответствие между стрелами X → Y и противоположными стрелами op Y → op X.

LaTeX

$$$\\text{Equiv}(X \\to Y,\\; \\mathrm{op}\\,Y \\to \\mathrm{op}\\,X)$$$

Lean4

/-- The bijection `(X ⟶ Y) ≃ (op Y ⟶ op X)`. -/
@[simps]
def opEquiv {V} [Quiver V] {X Y : V} : (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X)
    where
  toFun := Opposite.op
  invFun := Opposite.unop

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