English
If IsTriangulated C and P.IsTriangulated, then P.trW is multiplicative with respect to composition of triangles.
Русский
Если IsTriangulated C и P.IsTriangulated, то P.trW мультипликативна по композиции треугольников.
LaTeX
$$$[IsTriangulated C] [P.IsTriangulated] : P.trW.IsMultiplicative$$$
Lean4
instance [IsTriangulated C] [P.IsTriangulated] : P.trW.IsCompatibleWithTriangulation :=
⟨by
rintro T₁ T₃ mem₁ mem₃ a b ⟨Z₅, g₅, h₅, mem₅, mem₅'⟩ ⟨Z₄, g₄, h₄, mem₄, mem₄'⟩ comm
obtain ⟨Z₂, g₂, h₂, mem₂⟩ := distinguished_cocone_triangle (T₁.mor₁ ≫ b)
have H := someOctahedron rfl mem₁ mem₄ mem₂
have H' := someOctahedron comm.symm mem₅ mem₃ mem₂
let φ : T₁ ⟶ T₃ := H.triangleMorphism₁ ≫ H'.triangleMorphism₂
exact
⟨φ.hom₃, P.trW.comp_mem _ _ (trW.mk P H.mem mem₄') (trW.mk' P H'.mem mem₅'), by simpa [φ] using φ.comm₂, by
simpa [φ] using φ.comm₃⟩⟩
