English
The natural cone from the product-triangle to the family T_j is a limit cone, i.e., it exhibits the product as a limit of the diagram given by T_j.
Русский
Естественный конус от треугольника-произведения к семейству T_j является пределом, то есть треугольник выражает произведение как предел диаграммы T_j.
LaTeX
$$isLimitFan : IsLimit (productTriangle.fan T)$$
Lean4
theorem zero₃₁ [HasZeroMorphisms C] (h : ∀ j, (T j).mor₃ ≫ (T j).mor₁⟦(1 : ℤ)⟧' = 0) :
(productTriangle T).mor₃ ≫ (productTriangle T).mor₁⟦1⟧' = 0 :=
by
have : HasProduct (fun j => (T j).obj₂⟦(1 : ℤ)⟧) :=
⟨_, isLimitFanMkObjOfIsLimit (shiftFunctor C (1 : ℤ)) _ _ (productIsProduct (fun j => (T j).obj₂))⟩
dsimp
change _ ≫ (Pi.lift (fun j => Pi.π _ j ≫ (T j).mor₁))⟦(1 : ℤ)⟧' = 0
rw [assoc, ← cancel_mono (piComparison _ _), zero_comp, assoc, assoc]
ext j
simp only [map_lift_piComparison, assoc, limit.lift_π, Fan.mk_π_app, zero_comp, Functor.map_comp,
← piComparison_comp_π_assoc, IsIso.inv_hom_id_assoc, limMap_π_assoc, Discrete.natTrans_app, h j, comp_zero]
