Theorem CategoryTheory.Triangulated.SpectralObject.id_hom

Modification history

2026-08-25 11:58

Mathlib/CategoryTheory/Triangulated/SpectralObject.lean

feat(CategoryTheory/Triangulated): applying a homological functor to a spectral object (#42936) …

Deleted CategoryTheory.Triangulated.SpectralObject.id_hom View on Github →

2025-11-28 17:46

Mathlib/CategoryTheory/Triangulated/SpectralObject.lean

feat(CategoryTheory/Triangulated): spectral objects (#31586) …

Added CategoryTheory.Triangulated.SpectralObject.id_hom View on Github →