mapCoconePrecompose

Mathlib.CategoryTheory.Limits.Cones

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

Lean4

/-- `map_cocone` commutes with `precompose`. In particular, for `F : J ⥤ C`, given a cocone
`c : Cocone F`, a natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious
ways of producing a cocone over `G ⋙ H`, and they are both isomorphic.
-/
@[simps!]
def mapCoconePrecompose {α : F ⟶ G} {c} :
    mapCocone H ((Cocones.precompose α).obj c) ≅ (Cocones.precompose (whiskerRight α H :)).obj (mapCocone H c) :=
  Cocones.ext (Iso.refl _)

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

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

Разделы

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

Аффилиация

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