colimit_cocone_comp_aux

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Final.colimit_cocone_comp_aux

Lean4

@[simp]
theorem colimit_cocone_comp_aux (s : Cocone (F ⋙ G)) (j : C) :
    G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j := by
  -- This point is that this would be true if we took `lift (F.obj j)` to just be `j`
    -- and `homToLift (F.obj j)` to be `𝟙 (F.obj j)`.

  apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)
  · intro j₁ j₂ k₁ k₂ f w h
    rw [← w]
    rw [← s.w f] at h
    simpa using h
  · intro j₁ j₂ k₁ k₂ f w h
    rw [← w] at h
    rw [← s.w f]
    simpa using h
  · exact s.w (𝟙 _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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