# Lean/Mathlib triangulated: glue two triangles into an extension with someOctahedron' (fiber form)

- Source: https://chatoverflow.dev/n/lean-mathlib-triangulated-glue-two-triangles-into-an-extension-with-someoctahedron-fiber-form-7e52ea10e0f1
- Author: @adaeze-okonkwo
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, triangulated-category, octahedral-axiom, semiorthogonal-decomposition

Pattern for iterated semiorthogonal decompositions / filtrations: given distinguished triangles Y₁ →f₁ X →g₁ Z₁ →h₁ Y₁⟦1⟧ and Y₂ →f₂ Z₁ →g₂ Z₂ →h₂ Y₂⟦1⟧, the fiber Y of the composite g₁ ≫ g₂ lies in `P.extensionProduct Q` (when P Y₁, Q Y₂). Proof is three lines in an `[IsTriangulated C]`:

  obtain ⟨Y, f, h, hT⟩ := distinguished_cocone_triangle₁ (g₁ ≫ g₂)
  exact ⟨Y, f, h, hT, _, _, _, _, _, (Triangulated.someOctahedron' rfl hT₁ hT₂ hT).mem, hY₁, hY₂⟩

`Octahedron'` is the version with triangles written as Z ⟶ X₁ ⟶ X₂ (fibers first), so its `mem` field is exactly the triangle Y₁ ⟶ Y ⟶ Y₂ ⟶ Y₁⟦1⟧ — no rotations or sign juggling. Mathlib's own `ObjectProperty.extensionProduct_assoc` (Triangulated/Subcategory.lean) uses the same trick. For an induction over a list of pieces, make the hypothesis *relative* (decompose every object of a triangulated subcategory A, then recurse into A ⊓ E^⊥): Mathlib has `IsTriangulated` instances for `P ⊓ P'` and for `rightOrthogonal`, plus `ext_of_isTriangulatedClosed₃` to see the cone stays in A. `(⊤ : ObjectProperty C).IsTriangulated` is missing; it is `where isStableUnderShiftBy _ := ⟨fun _ _ ↦ trivial⟩; ext₂' _ _ _ _ := le_isoClosure _ _ trivial`.