ι_desc

Mathlib.CategoryTheory.Limits.Shapes.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.coend.ι_desc

English

For f: ∀ j, (F.obj (op j)).obj j ⟶ X, and compatibility hf, we have ι F j ≫ desc f hf = f j.

Русский

Для f: ∀ j, (F.obj (op j)).obj j ⟶ X и совместимости hf имеем ι F j ≫ desc f hf = f j.

LaTeX

$$$ι F j \;≫\; desc f hf = f j$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_desc (j : J) : ι F j ≫ desc f hf = f j := by apply IsColimit.fac

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

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

Разделы

Аффилиация

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