Mathlib Map

Theorems · Inductive type · category theory

CategoryTheory.ShortComplex.HomologyData

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Type (max u v)

A homology data for a short complex consists of two compatible left and right homology data

Defined in
Mathlib.Algebra.Homology.ShortComplex.Homology
Cited by
102 results in Mathlib
Foundations
Depth 3 from the axioms, rests on 4 definitions · uses no axioms
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.ShortComplex.HomologyData.left · cited by 130HomologyData.leftCategoryTheory.ShortComplex.HomologyData.right · cited by 99HomologyData.rightCategoryTheory.ShortComplex.HomologyData.iso · cited by 45HomologyData.isoCategoryTheory.ShortComplex.homologyData · cited by 33ShortComplex.homologyDataCategoryTheory.ShortComplex.HomologyMapData · cited by 27ShortComplex.HomologyMapD…CategoryTheory.ShortComplex.HomologyMapData.left · cited by 25HomologyMapData.leftCategoryTheory.ShortComplex.HomologyMapData.right · cited by 23HomologyMapData.rightCategoryTheory.ShortComplex.exact_of_iso · cited by 18ShortComplex.exact_of_isoCategoryTheory.ShortComplex.homologyMap' · cited by 16ShortComplex.homologyMap'CategoryTheory.Abelian.SpectralObject.homologyDataIdId · cited by 15SpectralObject.homologyDa…HomologicalComplex.extend.homologyData' · cited by 13extend.homologyData'CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData · cited by 12SpectralObject.spectralSe…CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono · cited by 11ShortComplex.exact_iff_of…CategoryTheory.ShortComplex.HomologyData.ofIso · cited by 11HomologyData.ofIsoCategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData · cited by 11SpectralSequence.homology…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.ShortComplex · cited by 1850CategoryTheory.ShortCompl…ShortComplex.HomologyDataCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by167

Results whose statement or proof uses this declaration.