English
The shift of a distinguished triangle is again distinguished.
Русский
Сдвиг распознаваемого треугольника снова является распознаваемым.
LaTeX
$$$\\forall n \\in \\mathbb{Z}, (\\mathrm{shiftFunctor} \\, C \\, n).\\mathrm{obj} T \\in \\mathrm{distTriang} \\ C$$$
Lean4
theorem shift_distinguished (n : ℤ) : (CategoryTheory.shiftFunctor (Triangle C) n).obj T ∈ distTriang C :=
by
revert T hT
let H : ℤ → Prop := fun n =>
∀ (T : Triangle C) (_ : T ∈ distTriang C), (Triangle.shiftFunctor C n).obj T ∈ distTriang C
change H n
have H_zero : H 0 := fun T hT => isomorphic_distinguished _ hT _ ((Triangle.shiftFunctorZero C).app T)
have H_one : H 1 := fun T hT =>
isomorphic_distinguished _ (rot_of_distTriang _ (rot_of_distTriang _ (rot_of_distTriang _ hT))) _
((rotateRotateRotateIso C).symm.app T)
have H_neg_one : H (-1) := fun T hT =>
isomorphic_distinguished _ (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ hT))) _
((invRotateInvRotateInvRotateIso C).symm.app T)
have H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c := fun {a b c} ha hb hc T hT =>
isomorphic_distinguished _ (hb _ (ha _ hT)) _ ((Triangle.shiftFunctorAdd' C _ _ _ hc).app T)
obtain (n | n) := n
·
induction n with
| zero => exact H_zero
| succ n hn => exact H_add hn H_one rfl
·
induction n with
| zero => exact H_neg_one
| succ n hn => exact H_add hn H_neg_one rfl
