Functoriality laws for short-exact derived triangles

Mathlib constructs a morphism between the distinguished triangles associated to a morphism of short exact sequences. This file records the identity and composition laws for that construction, so downstream geometry can use it as a functorial interface rather than unfold its three components.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_id {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) : map hS hS (CategoryStruct.id S) = CategoryStruct.id hS.singleTriangle

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_comp {C : Type u} [Category.{v, u} C] [Abelian C] {S₁ S₂ S₃ : ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact) (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) : map h₁ h₃ (CategoryStruct.comp f g) = CategoryStruct.comp (map h₁ h₂ f) (map h₂ h₃ g)

theorem CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_comp_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {S₁ S₂ S₃ : ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact) (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : Pretriangulated.Triangle (DerivedCategory C)} (h : h₃.singleTriangle ⟶ Z) : CategoryStruct.comp (map h₁ h₃ (CategoryStruct.comp f g)) h = CategoryStruct.comp (map h₁ h₂ f) (CategoryStruct.comp (map h₂ h₃ g) h)