Mathlib Map

Theorems · Theorem · category theory

CategoryTheory.ShortComplex.Exact.condition

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → ∃ h, CategoryTheory.Limits.IsZero h.left.H

the condition that there exists a homology data whose left.H field is zero

Defined in
Mathlib.Algebra.Homology.ShortComplex.Exact
Cited by
2 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.Exact.hasHomology · cited by 12Exact.hasHomologyCategoryTheory.ShortComplex.Exact.hasZeroObject · cited by 4Exact.hasZeroObjectCategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.ShortComplex · cited by 1850CategoryTheory.ShortCompl…CategoryTheory.Limits.IsZero · cited by 306Limits.IsZeroCategoryTheory.ShortComplex.Exact · cited by 292ShortComplex.ExactCategoryTheory.ShortComplex.LeftHomologyData.H · cited by 236LeftHomologyData.HCategoryTheory.ShortComplex.HomologyData.left · cited by 130HomologyData.leftCategoryTheory.ShortComplex.HomologyData · cited by 102ShortComplex.HomologyDataExact.conditionCITED BYCITES

Cites8

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

Cited by2

Results whose statement or proof uses this declaration.