limitsOfShape

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.limitsOfShape

Lean4

/-- The class of morphisms in `C` that are limits of shape `J` of
natural transformations involving morphisms in `W`. -/
inductive limitsOfShape : MorphismProperty C
  |
  mk (X₁ X₂ : J ⥤ C) (c₁ : Cone X₁) (c₂ : Cone X₂) (_ : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂)
    (_ : W.functorCategory J f) : limitsOfShape (h₂.lift (Cone.mk _ (c₁.π ≫ f)))

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

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

Разделы

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

Аффилиация

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