Documentation

DerivedAlgGeo.Algebra.Homology.HomologicalComplexLeftExact

Degree-zero homology under preserved kernels #

For an ℕ-indexed cochain complex, degree-zero homology is its degree-zero cycle object: there is no incoming differential. A functor preserving the outgoing kernel of this complex preserves these cycles, so its degreewise extension commutes with degree-zero homology. The comparison is natural in the complex when the corresponding kernel is preserved at each endpoint.

This is a statement about ordinary complexes. It does not identify degree-zero homology of a right-derived functor with its underived functor; that requires an injective-resolution comparison.

Main definitions #

Main results #

Implementation notes #

The incoming differential at zero vanishes. Mathlib's canonical isomorphism from cycles to homology and its preserved-cycles isomorphism give the result. An additive left-exact functor between abelian categories supplies the local homology and preservation instances in this statement.

References #

Tags #

homological algebra, preserved kernel, degree-zero homology

source
noncomputable def CategoryTheory.Functor.mapCochainComplexHomologyZeroIso {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (K : CochainComplex C ℕ) [HomologicalComplex.HasHomology K 0] [((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K).HasHomology 0] [Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc K 0).g 0) F] :
((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K).homology 0 ≅ F.obj (HomologicalComplex.homology K 0)

Mapping an ℕ-indexed cochain complex through a functor that preserves its outgoing degree-zero kernel commutes with degree-zero homology, when both homology objects exist.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Functor.mapCochainComplexHomologyZeroIso_naturality {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {K L : CochainComplex C ℕ} (φ : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] [((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K).HasHomology 0] [((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj L).HasHomology 0] [Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc K 0).g 0) F] [Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc L 0).g 0) F] :
    CategoryStruct.comp (HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0) (F.mapCochainComplexHomologyZeroIso L).hom = CategoryStruct.comp (F.mapCochainComplexHomologyZeroIso K).hom (F.map (HomologicalComplex.homologyMap φ 0))

    The degree-zero homology comparison respects cochain maps through naturality of the cycles-to-homology and preserved-cycles isomorphisms.

    source
    theorem CategoryTheory.Functor.mapCochainComplexHomologyZeroIso_naturality_assoc {C : Type u} {D : Type v} [Category.{u_1, u} C] [Category.{u_2, v} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {K L : CochainComplex C ℕ} (φ : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] [((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K).HasHomology 0] [((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj L).HasHomology 0] [Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc K 0).g 0) F] [Limits.PreservesLimit (Limits.parallelPair (HomologicalComplex.sc L 0).g 0) F] {Z : D} (h : F.obj (HomologicalComplex.homology L 0) ⟶ Z) :
    CategoryStruct.comp (HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0) (CategoryStruct.comp (F.mapCochainComplexHomologyZeroIso L).hom h) = CategoryStruct.comp (F.mapCochainComplexHomologyZeroIso K).hom (CategoryStruct.comp (F.map (HomologicalComplex.homologyMap φ 0)) h)

    The degree-zero homology comparison respects cochain maps through naturality of the cycles-to-homology and preserved-cycles isomorphisms.