ι_post

Mathlib.CategoryTheory.Limits.HasLimits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.colimit.ι_post

Lean4

@[reassoc (attr := simp)]
theorem ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) :=
  by
  erw [IsColimit.fac]
  rfl

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

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

Разделы

Аффилиация

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