orderDualEquivalence — Mathlib

English

For any preorder X, the category built from its order dual is equivalent to the opposite category of X.

Русский

Для любого частично упорядоченного множества X существует эквивалентность между категорией Xᵒᵈ и категорией Xᵒᵖ.

LaTeX

$$$(X^{\mathrm{OrderDual}}) \simeq (X)^{\mathrm{op}}$$$

Lean4

/-- The equivalence of categories from the order dual of a preordered type `X`
to the opposite category of the preorder `X`. -/
@[simps]
def orderDualEquivalence : Xᵒᵈ ≌ Xᵒᵖ
    where
  functor :=
    { obj := fun x => op (OrderDual.ofDual x)
      map := fun f => (homOfLE (leOfHom f)).op }
  inverse :=
    { obj := fun x => OrderDual.toDual x.unop
      map := fun f => (homOfLE (leOfHom f.unop)) }
  unitIso := Iso.refl _
  counitIso := Iso.refl _

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