Documentation

Mathlib.Algebra.Homology.Additive

Homology is an additive functor #

When V is preadditive, HomologicalComplex V c is also preadditive, and homologyFunctor is additive.

TODO: similarly for R-linear.

The i-th component of a chain map, as an additive map from chain maps to morphisms.

Instances For

    An additive functor induces a functor between homological complexes. This is sometimes called the "prolongation".

    Instances For

      The functor on homological complexes induced by the identity functor is isomorphic to the identity functor.

      Instances For

        A natural transformation between functors induces a natural transformation between those functors applied to homological complexes.

        Instances For

          A natural isomorphism between functors induces a natural isomorphism between those functors applied to homological complexes.

          Instances For

            An equivalence of categories induces an equivalences between the respective categories of homological complex.

            Instances For
              theorem ChainComplex.map_chain_complex_of {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_4, u_2} W] [CategoryTheory.Preadditive W] {α : Type u_3} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] (X : αV) (d : (n : α) → X (n + 1) X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) :
              (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (ChainComplex.of X d sq) = ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) (_ : ∀ (n : α), CategoryTheory.CategoryStruct.comp ((fun n => F.map (d n)) (n + 1)) ((fun n => F.map (d n)) n) = 0)