Theorems · Definition · category theory
CochainComplex.HomComplex
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Preadditive C] → CochainComplex C ℤ → CochainComplex C ℤ → CochainComplex AddCommGrpCat ℤThe cochain complex of homomorphisms between two cochain complexes F and G.
In degree n : ℤ, it consists of the abelian group HomComplex.Cochain F G n.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- ComplexShape.upproof · cited by 1,123
- CochainComplexstatement and proof · cited by 1,016
- ComplexShape.Relproof · cited by 518
- AddCommGrpCatstatement · cited by 462
- CochainComplex.HomComplex.Cochainproof · cited by 341
- AddMonoidHomClass.toAddMonoidHomproof · cited by 232
- AddCommGrpCat.ofproof · cited by 97
- AddCommGrpCat.ofHomproof · cited by 72
- CochainComplex.HomComplex.δ_homproof · cited by 6
Cited by14
Results whose statement or proof uses this declaration.
- CochainComplex.HomComplex.leftHomologyDatastatement · cited by 4
- CochainComplex.HomComplex.leftHomologyData'statement and proof · cited by 4
- CochainComplex.HomComplex.homologyAddEquivstatement · cited by 0
- CochainComplex.HomComplex.leftHomologyData'_H_coestatement · cited by 0
- CochainComplex.HomComplex.leftHomologyData'_K_coestatement · cited by 0
- CochainComplex.HomComplex.leftHomologyData'_istatement · cited by 0
- CochainComplex.HomComplex.leftHomologyData'_πstatement · cited by 0
- CochainComplex.HomComplex.leftHomologyData_H_coestatement · cited by 0
- CochainComplex.HomComplex.leftHomologyData_K_coestatement · cited by 0
- CochainComplex.HomComplex_Xstatement and proof · cited by 0
- CochainComplex.HomComplex_d_hom_applystatement and proof · cited by 0
- CochainComplex.HomComplex.leftHomologyData_i_hom_applystatement · cited by 0