Theorems · Definition · category theory
HomologicalComplex.Acyclic
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
{ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → PropA homological complex K is acyclic if it is exact at i for any i.
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- HomologicalComplex.ExactAtproof · cited by 44
Cited by34
Results whose statement or proof uses this declaration.
- CochainComplex.IsKInjective.homotopyZerostatement · cited by 4
- HomologicalComplex.acyclic_truncGE_iff_isSupportedOutsidestatement and proof · cited by 3
- CochainComplex.IsKProjective.homotopyZerostatement · cited by 3
- HomologicalComplex.acyclic_truncLE_iff_isSupportedOutsidestatement and proof · cited by 2
- CochainComplex.IsKInjective.nonempty_homotopy_zerostatement · cited by 2
- HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclicstatement · cited by 2
- CochainComplex.isKProjective_iff_leftOrthogonalproof · cited by 1
- CochainComplex.isKProjective_of_opproof · cited by 1
- HomologicalComplex.acyclic_iffstatement · cited by 1
- HomologicalComplex.acyclic_op_iffstatement and proof · cited by 1
- CochainComplex.acyclic_opstatement and proof · cited by 1
- HomologicalComplex.Acyclic.opstatement and proof · cited by 1