Theorems · Definition · category theory
CochainComplex.HomComplex.coboundaries
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Preadditive C] →
(K L : CochainComplex C ℤ) → (n : ℤ) → AddSubgroup (CochainComplex.HomComplex.Cocycle K L n)The subgroup of Cocycle K L n consisting of coboundaries.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Set.ofPredproof · cited by 6,101
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- AddSubgroupstatement · cited by 3,232
- CochainComplexstatement and proof · cited by 1,016
- CochainComplex.HomComplex.Cochainproof · cited by 341
- CochainComplex.HomComplex.Cocyclestatement and proof · cited by 130
- CochainComplex.HomComplex.δproof · cited by 102
Cited by10
Results whose statement or proof uses this declaration.
- CochainComplex.HomComplex.CohomologyClassproof · cited by 49
- CochainComplex.HomComplex.CohomologyClass.mkproof · cited by 34
- CochainComplex.HomComplex.CohomologyClass.descAddMonoidHomstatement and proof · cited by 2
- CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iffstatement · cited by 2
- CochainComplex.HomComplex.mem_coboundaries_iffstatement · cited by 2
- CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iffstatement · cited by 1
- CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iffstatement · cited by 1
- CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iffstatement and proof · cited by 1
- CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom_cohomologyClassstatement and proof · cited by 0
- CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom.congr_simpstatement and proof · cited by 0