Mathlib Map

Theorems · Theorem · category theory

CategoryTheory.ShortComplex.LeftHomologyData.wi

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

the kernel condition for i

Defined in
Mathlib.Algebra.Homology.ShortComplex.LeftHomology
Cited by
7 results in Mathlib
Foundations
Depth 6 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.map · cited by 25LeftHomologyData.mapCategoryTheory.ShortComplex.LeftHomologyData.op · cited by 13LeftHomologyData.opCategoryTheory.ShortComplex.iCycles_g · cited by 12ShortComplex.iCycles_gCategoryTheory.ShortComplex.LeftHomologyData.hi · cited by 5LeftHomologyData.hiCategoryTheory.ShortComplex.LeftHomologyData.wπ · cited by 3LeftHomologyData.wπCategoryTheory.ShortComplex.LeftHomologyData.hπ · cited by 3LeftHomologyData.hπCategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso_of_mono · cited by 1ShortComplex.isIso_cycles…CategoryTheory.ShortComplex.Exact.shortExact · cited by 1Exact.shortExactCategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc · cited by 0LeftHomologyData.wπ_assocCategoryTheory.ShortComplex.HasLeftHomology.hasKernel · cited by 0HasLeftHomology.hasKernelCategoryTheory.ShortComplex.LeftHomologyData.wi_assoc · cited by 0LeftHomologyData.wi_assocCategoryTheory.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 876ShortComplex.X₃CategoryTheory.ShortComplex.g · cited by 658ShortComplex.gCategoryTheory.ShortComplex.LeftHomologyData.K · cited by 233LeftHomologyData.KCategoryTheory.ShortComplex.LeftHomologyData · cited by 212ShortComplex.LeftHomology…CategoryTheory.ShortComplex.LeftHomologyData.i · cited by 144LeftHomologyData.iLeftHomologyData.wiCITED BYCITES

Cites11

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

Cited by11

Results whose statement or proof uses this declaration.