opToOverOp

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.opToOverOp

← MathLib Explorer

English

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

Русский

Канонический функтор From Under to Over устарел.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru