instCreatesLimitsOfShapeProjOfIsConnected

Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CostructuredArrow.instCreatesLimitsOfShapeProjOfIsConnected

Lean4

/-- The projection from `CostructuredArrow K B` to `C` creates any connected limit. -/
instance [IsConnected J] {B : D} : CreatesLimitsOfShape J (CostructuredArrow.proj K B) where
  CreatesLimit :=
    createsLimitOfReflectsIso fun c t =>
      { liftedCone := CreatesConnected.raiseCone c
        validLift := eqToIso (CreatesConnected.mapCone_raiseCone c)
        makesLimit := CreatesConnected.isLimitRaiseCone t }

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

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

Разделы

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

Аффилиация

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