ofPullbackCone

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

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

Lean4

/-- This is a helper construction that can be useful when verifying that a category has all
pullbacks. Given `F : WalkingCospan ⥤ C`, which is really the same as
`cospan (F.map inl) (F.map inr)`, and a pullback cone on `F.map inl` and `F.map inr`, we
get a cone on `F`.

If you're thinking about using this, have a look at `hasPullbacks_of_hasLimit_cospan`,
which you may find to be an easier way of achieving your goal. -/
@[simps]
def ofPullbackCone {F : WalkingCospan ⥤ C} (t : PullbackCone (F.map inl) (F.map inr)) : Cone F
    where
  pt := t.pt
  π := t.π ≫ (diagramIsoCospan F).inv

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

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

Разделы

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

Аффилиация

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