opToOpUnder — Mathlib

English

The equivalence respects identities and compositions, making the correspondence canonical.

Русский

Эквивалентность сохраняет тождественные отображения и композиции, образуя каноническое соответствие.

LaTeX

$$$\mathrm{opEquivOpUnder}(X): \mathrm{Over}(\mathrm{op}X) \simeq \mathrm{Under}(X)^{\mathrm{op}}$$$

Lean4

/-- The canonical functor by reversing structure arrows. -/
@[deprecated Over.opEquivOpUnder (since := "2025-04-08")]
def opToOpUnder : Over (op X) ⥤ (Under X)ᵒᵖ :=
  (Over.opEquivOpUnder X).functor

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