Theorems · Theorem · category theory
CategoryTheory.Iso.isZero_iff
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y),
CategoryTheory.Limits.IsZero X ↔ CategoryTheory.Limits.IsZero Y- Cited by
- 11 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
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.Isostatement and proof · cited by 3,963
- CategoryTheory.Iso.symmproof · cited by 993
- CategoryTheory.Limits.IsZerostatement and proof · cited by 306
- CategoryTheory.Limits.IsZero.of_isoproof · cited by 35
Cited by11
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.LeftHomologyData.exact_iffproof · cited by 8
- CategoryTheory.ShortComplex.RightHomologyData.exact_iffproof · cited by 6
- DerivedCategory.isGE_Q_obj_iffproof · cited by 2
- CategoryTheory.Functor.mem_homologicalKernel_iffproof · cited by 1
- CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedByproof · cited by 1
- CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_iffproof · cited by 1
- HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAtproof · cited by 1
- CategoryTheory.ShortComplex.QuasiIso.exact_iffproof · cited by 0
- CochainComplex.mappingCone.isZero_X_iffproof · cited by 0
- DerivedCategory.isLE_Q_obj_iffproof · cited by 0
- HomologicalComplex.extend_exactAt_iffproof · cited by 0