Theorems · Theorem · category theory
CategoryTheory.Functor.map_zero
∀ {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 Y : C), F.map 0 = 0- Cited by
- 85 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.Functor.objstatement · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapstatement · cited by 8,698
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Functor.PreservesZeroMorphismsstatement and proof · cited by 458
- CategoryTheory.Functor.PreservesZeroMorphisms.map_zeroproof · cited by 1
Cited by85
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.map_isZeroproof · cited by 16
- CategoryTheory.Abelian.Ext.mk₀_zeroproof · cited by 7
- CategoryTheory.Triangulated.TStructure.zeroproof · cited by 7
- CategoryTheory.Functor.homologySequence_compproof · cited by 6
- CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iffproof · cited by 5
- CategoryTheory.Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_posproof · cited by 4
- CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomologyproof · cited by 4
- CategoryTheory.Abelian.Ext.add_homproof · cited by 4
- CategoryTheory.Functor.exact_tfaeproof · cited by 3
- CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQproof · cited by 3
- CategoryTheory.ShortComplex.exact_map_iff_of_faithfulproof · cited by 3
- CategoryTheory.Functor.reflects_exact_of_faithfulproof · cited by 3