shift — Mathlib

English

If P is stable under shift, then shifting f by n preserves membership: P.trW (f⟦n⟧') holds whenever P.trW f holds.

Русский

Если P стабильно относительно сдвига, то сдвиг f на n сохраняет принадлежность: P.trW (f⟦n⟧') при P.trW f.

LaTeX

$$$[P.IsStableUnderShift \\mathbb Z] \\Rightarrow (P.trW f \\Rightarrow P.trW (f \\langle n \\rangle '))$$$

Lean4

theorem shift [P.IsStableUnderShift ℤ] {X₁ X₂ : C} {f : X₁ ⟶ X₂} (hf : P.trW f) (n : ℤ) : P.trW (f⟦n⟧') :=
  by
  rw [← smul_mem_trW_iff _ _ (n.negOnePow)]
  obtain ⟨X₃, g, h, hT, mem⟩ := hf
  exact ⟨_, _, _, Pretriangulated.Triangle.shift_distinguished _ hT n, P.le_shift _ _ mem⟩

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