pullback

Mathlib.CategoryTheory.Comma.Over.Pullback

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.pullback

Lean4

/-- In a category with pullbacks, a morphism `f : X ⟶ Y` induces a functor `Over Y ⥤ Over X`,
by pulling back a morphism along `f`. -/
@[simps! +simpRhs obj_left obj_hom map_left]
def pullback {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : Over Y ⥤ Over X
    where
  obj g := Over.mk (pullback.snd g.hom f)
  map := fun g {h} {k} =>
    Over.homMk (pullback.lift (pullback.fst _ _ ≫ k.left) (pullback.snd _ _) (by simp [pullback.condition]))

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

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

Разделы

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

Аффилиация

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