Theorems · Theorem · category theory

CategoryTheory.Functor.zero_obj

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject D] (X : C),
  CategoryTheory.Limits.IsZero (CategoryTheory.Functor.obj 0 X)

Defined in: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Cited by: 2 results in Mathlib
Foundations: Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category CategoryTheory.Limits.HasZeroObject

Mathlib docs Source Loogle LeanSearch

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
CategoryTheory.Functor.objstatement · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Limits.HasZeroObjectstatement and proof · cited by 1,298
CategoryTheory.Limits.IsZerostatement · cited by 306
CategoryTheory.Limits.HasZeroObject.zero'statement · cited by 115
CategoryTheory.Limits.isZero_zeroproof · cited by 34
CategoryTheory.Limits.IsZero.objproof · cited by 3

Cited by2

Results whose statement or proof uses this declaration.

CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguishedproof · cited by 1
CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_obj_objproof · cited by 0