instPreservesLimitsOfShapeπ₁

Mathlib.Algebra.Homology.ShortComplex.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₁

English

For a functor F : J ⥤ ShortComplex C with π₁ having limits for F, π₂ and π₃, F preserves limits of shape J for π₁.

Русский

Для функтера F : J ⥤ ShortComplex C, если для F существуют пределы π₁, π₂, π₃, F сохраняет пределы формы J для π₁.

LaTeX

$$$ \text{PreservesLimitsOfShape } J \pi_1 $$$

Lean4

noncomputable instance : PreservesLimitsOfShape J (π₁ : _ ⥤ C) where

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

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

Разделы

Аффилиация

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