Theorems · Theorem · category theory
CategoryTheory.Functor.map_isZero
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X : C},
CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero (F.obj X)- Cited by
- 16 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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.Homproof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapproof · cited by 8,698
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Functor.map_idproof · cited by 616
- CategoryTheory.Functor.PreservesZeroMorphismsstatement and proof · cited by 458
- CategoryTheory.Limits.IsZerostatement and proof · cited by 306
- CategoryTheory.Functor.map_zeroproof · cited by 85
Cited by16
Results whose statement or proof uses this declaration.
- CategoryTheory.Abelian.Ext.zero_homproof · cited by 6
- CategoryTheory.Functor.isZero_leftDerived_obj_projective_succproof · cited by 3
- CochainComplex.degreewiseEpiWithInjectiveKernel_iff_of_isZeroproof · cited by 2
- CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁proof · cited by 2
- CategoryTheory.JointlyReflectIsomorphisms.isZero_iffproof · cited by 1
- CategoryTheory.ObjectProperty.le_extensionProduct_rightproof · cited by 1
- CategoryTheory.Triangulated.TStructure.isLE_of_isZeroproof · cited by 1
- CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedByproof · cited by 1
- TopCat.Sheaf.isZero_iff_stalkFunctor_obj_isZeroproof · cited by 1
- CategoryTheory.Triangulated.TStructure.isGE_of_isZeroproof · cited by 1
- CategoryTheory.Sheaf.subsingleton_H_of_isZeroproof · cited by 0