fac_apply

Mathlib.CategoryTheory.Limits.Types.ColimitType

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.CoconeTypes.IsColimit.fac_apply

English

If c is a colimit cocone, then desc c' followed by injection at j equals c'.ι j x.

Русский

Если c является коллимитным коконом, то desc c' затем инъекция на j даёт c'.ι j x.

LaTeX

$$$hc.desc c' (c.ι j x) = c'.ι j x$$$

Lean4

@[simp]
theorem fac_apply (c' : CoconeTypes.{w₂} F) (j : J) (x : F.obj j) : hc.desc c' (c.ι j x) = c'.ι j x :=
  congr_fun (hc.fac c' j) x

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

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

Разделы

Аффилиация

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