Commit 2024-04-29 20:47 9cbb31ee
View on Github →feat(CategoryTheory/Triangulated): homological functors (#11759)
A functor F : C ⥤ A from a pretriangulated category to an abelian category is homological iff it sends distinguished triangles in C to exact sequences in A. In this PR, we define the corresponding type class F.IsHomological. If F is a homological functor, we introduce the strictly full triangulated subcategory F.homologicalKernel.