mapConePostcomposeEquivalenceFunctor

Mathlib.CategoryTheory.Limits.Cones

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

Lean4

/-- `mapCone` commutes with `postcomposeEquivalence`
-/
@[simps!]
def mapConePostcomposeEquivalenceFunctor {α : F ≅ G} {c} :
    mapCone H ((Cones.postcomposeEquivalence α).functor.obj c) ≅
      (Cones.postcomposeEquivalence (isoWhiskerRight α H :)).functor.obj (mapCone H c) :=
  Cones.ext (Iso.refl _)

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

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

Разделы

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

Аффилиация

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