English
If each component of a family of triangles has a certain zero relation, then the lifted morphism to the product-triangle also satisfies the corresponding zero relation.
Русский
Если каждая компонента семейства треугольников удовлетворяет нулевому отношению, то их подъем к произведению треугольников тоже удовлетворяет соответствующему нулевому отношению.
LaTeX
$$zero₃₁(h) : (productTriangle T).mor₃ ≫ (productTriangle T).mor₁⟦1⟧' = 0$$
Lean4
/-- A family of morphisms `T' ⟶ T j` lifts to a morphism `T' ⟶ productTriangle T`. -/
@[simps]
def lift {T' : Triangle C} (φ : ∀ j, T' ⟶ T j) : T' ⟶ productTriangle T
where
hom₁ := Pi.lift (fun j => (φ j).hom₁)
hom₂ := Pi.lift (fun j => (φ j).hom₂)
hom₃ := Pi.lift (fun j => (φ j).hom₃)
comm₃ := by
dsimp
rw [← cancel_mono (piComparison _ _), assoc, assoc, assoc, IsIso.inv_hom_id, comp_id]
cat_disch
