HomologicalFunctor

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/HomologicalFunctor.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsHomologicalIntUpHomologyFunctor	1
Total	1

HomotopyCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsHomologicalIntUpHomologyFunctor 📖	mathematical	—	CategoryTheory.Functor.IsHomological HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory hasShift homologyFunctor CategoryTheory.categoryWithHomology_of_abelian instHasZeroObject CategoryTheory.Abelian.hasZeroObject instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp CategoryTheory.Abelian.hasBinaryBiproducts	—	CategoryTheory.Functor.IsHomological.mk' AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instHasZeroObject CategoryTheory.Abelian.hasZeroObject instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveHomologyFunctor HomologicalComplex.instPreservesZeroMorphismsEval CategoryTheory.Pretriangulated.isomorphic_distinguished distinguished_iff_iso_trianglehOfDegreewiseSplit HomologicalComplex.shortExact_of_degreewise_shortExact CategoryTheory.ShortComplex.Splitting.shortExact CategoryTheory.Functor.preservesZeroMorphisms_comp instAdditiveHomologicalComplexQuotient HomologicalComplex.instPreservesZeroMorphismsHomologyFunctor CategoryTheory.ShortComplex.exact_iff_of_iso CategoryTheory.ShortComplex.ShortExact.homology_exact₂

---

← Back to Index