opEquiv — Mathlib

English

There is a natural equivalence between the arrow category of the opposite category and the arrow category of the original category.

Русский

Существует естественная эквивалентность между категорией стрелок в противоположной категории и категорией стрелок в исходной категории.

LaTeX

$$$\\\\operatorname{Arrow}(C^{op}) \\simeq \\\\operatorname{Arrow}(C)$$$

Lean4

/-- The bijection `Arrow Cᵒᵖ ≃ Arrow C`. -/
def opEquiv (C : Type u) [Category.{v} C] : Arrow Cᵒᵖ ≃ Arrow C
    where
  toFun f := Arrow.mk f.hom.unop
  invFun g := Arrow.mk g.hom.op

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