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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono 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' instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono CategoryTheory.categoryWithHomology_of_abelian instHasZeroObject CategoryTheory.Abelian.hasZeroObject instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveHomologyFunctor AddRightCancelSemigroup.toIsRightCancelAdd 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