opToUnderOp — Mathlib

English

The canonical functor by reversing structure arrows from Over to Under is defined (deprecated).

Русский

Канонический функтор из Over в Under определён (устарел).

LaTeX

$$$\mathrm{opToUnderOp}(X): \Over(X)^{\mathrm{op}} \to \Under(\mathrm{op}X)$$$

Lean4

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

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