Commit 2026-08-25 11:58 2c0cf72f

View on Github →

feat(CategoryTheory/Triangulated): applying a homological functor to a spectral object (#42936) In this file, we show that one may obtain a spectral object in an abelian category by applying a homological functor to a triangulated spectral object. We also fix some (not all) transparency issues with ComposableArrows.

Estimated changes

Modified Mathlib/CategoryTheory/ComposableArrows/Basic.lean

Modified Mathlib/CategoryTheory/ComposableArrows/One.lean

Modified Mathlib/CategoryTheory/ComposableArrows/Two.lean

deleted def CategoryTheory.ComposableArrows.twoδ₁Toδ₀

deleted def CategoryTheory.ComposableArrows.twoδ₂Toδ₁

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Modified Mathlib/CategoryTheory/Triangulated/SpectralObject.lean

deleted theorem CategoryTheory.Triangulated.SpectralObject.comp_hom

deleted theorem CategoryTheory.Triangulated.SpectralObject.id_hom

added theorem CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_δ

modified def CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor

added def CategoryTheory.Triangulated.SpectralObject.triangleMap

added theorem CategoryTheory.Triangulated.SpectralObject.δ_naturality