Mathlib Map

Theorems · Theorem · category theory

CategoryTheory.ShortComplex.zero

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (self : CategoryTheory.ShortComplex C), CategoryTheory.CategoryStruct.comp self.f self.g = 0

the composition of the two given morphisms is zero

Defined in
Mathlib.Algebra.Homology.ShortComplex.Basic
Cited by
76 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.ShortComplex.LeftHomologyData.f' · cited by 61LeftHomologyData.f'CategoryTheory.ShortComplex.RightHomologyData.g' · cited by 43RightHomologyData.g'CategoryTheory.ShortComplex.exact_of_g_is_cokernel · cited by 25ShortComplex.exact_of_g_i…CategoryTheory.ShortComplex.exact_of_f_is_kernel · cited by 22ShortComplex.exact_of_f_i…CategoryTheory.ShortComplex.LeftHomologyData.f'_i · cited by 21LeftHomologyData.f'_iCategoryTheory.ShortComplex.Exact.exact_toComposableArrows · cited by 20Exact.exact_toComposableA…CategoryTheory.ShortComplex.RightHomologyData.p_g' · cited by 17RightHomologyData.p_g'CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork · cited by 14LeftHomologyData.ofIsLimi…CategoryTheory.ShortComplex.Exact.fIsKernel · cited by 12Exact.fIsKernelCategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork · cited by 12RightHomologyData.ofIsCol…CategoryTheory.ShortComplex.Exact.gIsCokernel · cited by 11Exact.gIsCokernelCategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' · cited by 11LeftHomologyData.ofEpiOfI…CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono · cited by 9LeftHomologyData.ofEpiOfI…CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel · cited by 5LeftHomologyData.ofHasKer…CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel · cited by 5RightHomologyData.ofHasCo…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.ShortComplex · cited by 1850CategoryTheory.ShortCompl…CategoryTheory.ShortComplex.X₂ · cited by 1115ShortComplex.X₂CategoryTheory.ShortComplex.X₁ · cited by 889ShortComplex.X₁CategoryTheory.ShortComplex.X₃ · cited by 876ShortComplex.X₃CategoryTheory.ShortComplex.g · cited by 658ShortComplex.gCategoryTheory.ShortComplex.f · cited by 653ShortComplex.fShortComplex.zeroCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by110

Results whose statement or proof uses this declaration.