English
Similarly for mor₃, there exists a b making the morphism square commute with mor₁ and mor₂, respecting a certain rotated structure.
Русский
Аналогично для mor₃ существует b, делающий квадрат морфизмов коммутирующим, совместимый с mor₁ и mor₂ и с учётом вращенной структуры.
LaTeX
$$complete_distinguished_triangle_morphism₂$$
Lean4
/-- A commutative square involving the morphisms `mor₃` of two distinguished triangles
can be extended as morphism of triangles -/
theorem complete_distinguished_triangle_morphism₂ (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distTriang C)
(hT₂ : T₂ ∈ distTriang C) (a : T₁.obj₁ ⟶ T₂.obj₁) (c : T₁.obj₃ ⟶ T₂.obj₃)
(comm : T₁.mor₃ ≫ a⟦(1 : ℤ)⟧' = c ≫ T₂.mor₃) :
∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂ :=
by
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ :=
complete_distinguished_triangle_morphism _ _ (inv_rot_of_distTriang _ hT₁) (inv_rot_of_distTriang _ hT₂)
(c⟦(-1 : ℤ)⟧') a
(by
dsimp
simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm, Functor.map_comp, shift_shift_neg',
Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])
refine ⟨a, ⟨ha₁, ?_⟩⟩
dsimp only [Triangle.invRotate, Triangle.mk] at ha₂
rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]
simp only [shiftEquiv'_counitIso, shift_neg_shift', assoc, Iso.inv_hom_id_app_assoc]
