instIsCompatibleWithShiftTrWIntOfIsStableUnderShift

Mathlib.CategoryTheory.Triangulated.Subcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instIsCompatibleWithShiftTrWIntOfIsStableUnderShift

← MathLib Explorer

English

The instance of RespectsIso for trW holds for any P with trW.

Русский

Существование инстанса, удовлетворяющего свойству RespectsIso для trW.

LaTeX

$$$P.trW.RespectsIso$$$

Lean4

instance [P.IsStableUnderShift ℤ] : P.trW.IsCompatibleWithShift ℤ where
  condition
    n := by
    ext K L f
    exact ⟨fun hf => hf.unshift, fun hf => hf.shift n⟩

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

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

Разделы

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

Аффилиация

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