Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Derived Hom Triangle

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. The actual Hom diagram chase needed to extend the protected generator comparison through finite complex filtrations. This proves a transfer across a distinguished triangle; it assumes no derived adjunction, unbounded resolution, or full faithfulness of the functor. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1. The chase uses Mathlib’s proved yoneda exactness at commit 5e0c4e5239cb0a2d86d68a884bf52cfd963fce22 (Joël Riou, Apache-2.0).

Theorem 1.1 (map Hom bijective triangle middle).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedHomTriangle.mapHom_bijective_triangle_middle

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/DerivedHomTriangle.mapHom_bijective_triangle_middle (✓ std3). ∎

Source. Repository-derived.

Commentary.

A five-term Hom chase, with the comparison the literal functor map. Only the four adjacent source Hom comparisons are used.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/DerivedHomTriangle.mapHom_bijective_triangle_middle