English
Given distinguished triangles T₁ and T₂ and a commutative square on their mor₂s, there exists a morphism a making the square commute and compatible with mor₃ under a shift.
Русский
Имеются выделенные треугольники T₁ и T₂ и коммутабельная решётка морфизмов mor₂; тогда существует морфизм a, обеспечивающий совместимость квадратa и mor₃ после сдвига.
LaTeX
$$complete_distinguished_triangle_morphism1$$
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) (b : T₁.obj₂ ⟶ T₂.obj₂) (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂) :
∃ (a : T₁.obj₁ ⟶ T₂.obj₁), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ a⟦(1 : ℤ)⟧' = c ≫ T₂.mor₃ :=
by
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ :=
complete_distinguished_triangle_morphism _ _ (rot_of_distTriang _ hT₁) (rot_of_distTriang _ hT₂) b c comm
refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩
· apply (shiftFunctor C (1 : ℤ)).map_injective
dsimp at ha₂
rw [neg_comp, comp_neg, neg_inj] at ha₂
simpa only [Functor.map_comp, Functor.map_preimage] using ha₂
· simpa only [Functor.map_preimage] using ha₁
