English
If P isIsStableUnderShift, then P.trW is compatible with triangulation under integer shifts.
Русский
Если P IsStableUnderShift, то P.trW совместима с треугольной структурой при целочисленном сдвиге.
LaTeX
$$$[P.IsStableUnderShift Int] \\Rightarrow P.trW.IsCompatibleWithShift Int$$$
Lean4
theorem exists_triangle (A : C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
∃ (X Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ X⟦(1 : ℤ)⟧),
Triangle.mk f g h ∈ distTriang C :=
by
obtain ⟨X, Y, hX, hY, f, g, h, mem⟩ := t.exists_triangle_zero_one (A⟦n₀⟧)
let T := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
let e := (shiftEquiv C n₀).unitIso.symm.app A
have hT' : Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ∈ distTriang C :=
by
refine isomorphic_distinguished _ (Triangle.shift_distinguished _ mem (-n₀)) _ ?_
refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_
all_goals simp [T]
exact ⟨_, _, t.le_shift _ _ _ (neg_add_cancel n₀) _ hX, t.ge_shift _ _ _ (by cutsat) _ hY, _, _, _, hT'⟩
