Theorems · Theorem · category theory
HomologicalComplex.shape
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) (i j : ι),
¬c.Rel i j → self.d i j = 0- Cited by
- 59 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
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
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- HomologicalComplex.Xstatement · cited by 1,839
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- HomologicalComplex.dstatement · cited by 598
- ComplexShape.Relstatement · cited by 518
Cited by59
Results whose statement or proof uses this declaration.
- HomologicalComplex.d_comp_dproof · cited by 36
- HomologicalComplex.Hom.commproof · cited by 29
- CochainComplex.HomComplex.δ_shapeproof · cited by 11
- HomologicalComplex₂.d₂_eq_zeroproof · cited by 8
- CategoryTheory.ShortComplex.ShortExact.homology_exact₂proof · cited by 6
- HomologicalComplex.epi_homologyMap_of_epi_of_not_relproof · cited by 3
- HomologicalComplex.fromOpcycles_eq_zeroproof · cited by 2
- HomologicalComplex.mapBifunctor₂₃.d₃_eq_zeroproof · cited by 2
- HomologicalComplex.d_pOpcyclesproof · cited by 2
- HomologicalComplex.mapBifunctor₂₃.d₂_eq_zeroproof · cited by 2
- HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundaryproof · cited by 2
- HomologicalComplex₂.shape_fproof · cited by 2