Joël Riou
Joël Riou
In this PR, we obtain the basic behaviour of lifting properties with respect to adjunctions. --- [](https://gitpod.io/from-referrer/)
This PR introduces variations on the statements of simplicial relations which makes it easier to use. This is demonstrated in `algebraic_topology.dold_kan.faces`. The attribute `reassoc` is also added to the simplicial...
feat: the homological functor on the homotopy category of cochain complexes in an abelian category
The homology functors on the homotopy category of cochain complexes in an abelian category are homological functors (in the sense that they send distinguished triangles to exact sequences). This PR...
This PR contains a redefinition of homology, theorems about localization of categories, including triangulated categories, a construction of the derived category of an abelian category, derived functors, spectral sequences, etc....
--- - [ ] depends on: #11740 [](https://gitpod.io/from-referrer/)
This PR defines the type `Triangulated.Subcategory C` when `C` is a pretriangulated category. It also introduces a type class `Set.RespectsIso` for set of objects in a category `C` that is...
In this file, it is shown that if a class of morphisms `W` in a pretriangulated category is compatible with the triangulation and has a left calculus of fractions, then...
In this PR, it is shown that if `W : MorphismProperty C` has a left calculus of fractions and `C` is preadditive, then the localized category is also preadditive. ---...
We introduce lemmas on fractions which shall be useful when construction the preadditive structure on the localized category. --- - [ ] depends on: #11721 [](https://gitpod.io/from-referrer/)
Given two complex shapes `c : ComplexShape ι` and `c' : ComplexShape ι'` for homological complexes, an embedding from `c` to `c'` (`e : c.Embedding c'`) consists of the data...