op

Mathlib.CategoryTheory.Limits.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Fan.op

English

The inverse composed with the i-th sigma injection equals the i-th projection.

Русский

Обратное композиции с i-й внедрением равняется i-й проекции.

LaTeX

$$$(\mathrm{opProductIsoCoproduct Z).inv} \circ (\Sigma i)^{\mathrm{op}} = \Pi i$$$

Lean4

/-- A `Fan` gives a `Cofan` in the opposite category. -/
@[simp]
def op (f : Fan Z) : Cofan (op <| Z ·) :=
  Cofan.mk _ (fun a ↦ (f.proj a).op)

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

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

Разделы

Аффилиация

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