instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated

English

If f is an isomorphism, then P.trW f holds (for any P with ContainsZero).

Русский

Если f изоморфизм, то P.trW f истинно (при P.ContainsZero).

LaTeX

$$$[P.ContainsZero] \\Rightarrow \\forall X Y, f: X \\to Y, [\\text{IsIso } f] \\Rightarrow P.trW f$$$

Lean4

instance [IsTriangulated C] [P.IsTriangulated] : P.trW.IsMultiplicative where
  comp_mem := by
    rw [← trW_isoClosure]
    rintro X₁ X₂ X₃ u₁₂ u₂₃ ⟨Z₁₂, v₁₂, w₁₂, H₁₂, mem₁₂⟩ ⟨Z₂₃, v₂₃, w₂₃, H₂₃, mem₂₃⟩
    obtain ⟨Z₁₃, v₁₃, w₁₂, H₁₃⟩ := distinguished_cocone_triangle (u₁₂ ≫ u₂₃)
    exact ⟨_, _, _, H₁₃, P.isoClosure.ext_of_isTriangulatedClosed₂ _ (someOctahedron rfl H₁₂ H₂₃ H₁₃).mem mem₁₂ mem₂₃⟩

Похожие утверждения