instPreservesLimitπ₁

Mathlib.Algebra.Homology.ShortComplex.Limits

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

English

For F: J ⥤ ShortComplex C with existing limits for π₁, π₂, π₃, F preserves the limit π₁.

Русский

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

LaTeX

$$$ \text{PreservesLimit } F \pi_1 $$$

Lean4

noncomputable instance : PreservesLimit F π₁ :=
  preservesLimit_of_preserves_limit_cone (isLimitLimitCone F) (isLimitπ₁MapConeLimitCone F)

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

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

Разделы

Аффилиация

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