pullbackObjIso

Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.pullbackObjIso

Lean4

/-- Evaluating a pullback amounts to taking the pullback of the evaluations. -/
noncomputable def pullbackObjIso (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullback f g).obj d ≅ pullback (f.app d) (g.app d) :=
  limitObjIsoLimitCompEvaluation (cospan f g) d ≪≫ HasLimit.isoOfNatIso (diagramIsoCospan _)

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

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

Разделы

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

Аффилиация

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