English
If F is triangulated and ess-surjective on 2-arrow composable patterns, then D is triangulated when C is.
Русский
Если F трангулирован и эс-суръективен на композиции из двух стрелок, то D трангулирован, если C трангулирован.
LaTeX
$$$IsTriangulated D$ given $IsTriangulated C$ and essSurj on 2-arrow compositions$$
Lean4
/-- If `F : C ⥤ D` is a triangulated functor from a triangulated category, then `D`
is also triangulated if tuples of composables arrows in `D` can be lifted to `C`. -/
theorem isTriangulated_of_essSurj_mapComposableArrows_two (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated]
[(F.mapComposableArrows 2).EssSurj] [IsTriangulated C] : IsTriangulated D :=
by
apply IsTriangulated.mk
intro Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ u₁₂ u₂₃ u₁₃ comm v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃ v₁₃ w₁₃ h₁₃
obtain ⟨α, ⟨e⟩⟩ :
∃ (α : ComposableArrows C 2), Nonempty ((F.mapComposableArrows 2).obj α ≅ ComposableArrows.mk₂ u₁₂ u₂₃) :=
⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
obtain ⟨X₁, X₂, X₃, f, g, rfl⟩ := ComposableArrows.mk₂_surjective α
obtain ⟨_, _, _, h₁₂'⟩ := distinguished_cocone_triangle f
obtain ⟨_, _, _, h₂₃'⟩ := distinguished_cocone_triangle g
obtain ⟨_, _, _, h₁₃'⟩ := distinguished_cocone_triangle (f ≫ g)
exact
⟨Octahedron.ofIso (e₁ := (e.app 0).symm) (e₂ := (e.app 1).symm) (e₃ := (e.app 2).symm) (comm₁₂ :=
ComposableArrows.naturality' e.inv 0 1) (comm₂₃ := ComposableArrows.naturality' e.inv 1 2) (H :=
(someOctahedron rfl h₁₂' h₂₃' h₁₃').map F) ..⟩
