comp_yonedaPresheaf'

Mathlib.Topology.Category.TopCat.Yoneda

URI: https://scilib.ai/kg/mathlib#ContinuousMap.comp_yonedaPresheaf'

English

The Yoneda presheaf composed with F.op equals F.op composed with yonedaPresheaf'.

Русский

Точное равенство: yonedaPresheaf F Y = F.op ⋙ yonedaPresheaf' Y.

LaTeX

$$$\\text{yonedaPresheaf}(F,Y) = F^{op} \\circ \\text{yonedaPresheaf}'(Y).$$$

Lean4

theorem comp_yonedaPresheaf' : yonedaPresheaf F Y = F.op ⋙ yonedaPresheaf' Y :=
  rfl

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

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

Разделы

Аффилиация

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