preservesColimitNatIso

Mathlib.CategoryTheory.Limits.Preserves.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.preservesColimitNatIso

Lean4

/-- If `C, D` has all colimits of shape `J`, and `G` preserves them, then `preservesColimitIso`
is functorial w.r.t. `F`. -/
@[simps!]
def preservesColimitNatIso : colim ⋙ G ≅ (Functor.whiskeringRight J C D).obj G ⋙ colim :=
  NatIso.ofComponents (fun F => preservesColimitIso G F)
    (by
      intro _ _ f
      rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]
      apply colimit.hom_ext; intro j
      dsimp
      rw [ι_colimMap_assoc]
      simp only [ι_preservesColimitIso_inv, Functor.whiskerRight_app, ι_preservesColimitIso_inv_assoc, ← G.map_comp]
      rw [ι_colimMap])

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

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

Разделы

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

Аффилиация

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