Acyclic

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

Statistics

Metric	Count
Definitions subcategoryAcyclic	1
Theorems instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, instIsTriangulatedIntUpSubcategoryAcyclic, mem_subcategoryAcyclic_iff, quasiIso_eq_subcategoryAcyclic_W, quotient_obj_mem_subcategoryAcyclic_iff_acyclic, quotient_obj_mem_subcategoryAcyclic_iff_exactAt	6
Total	7

HomotopyCategory

Definitions

Name	Category	Theorems
subcategoryAcyclic 📖	CompOp	11 math math: CochainComplex.IsKInjective.rightOrthogonal, instIsTriangulatedIntUpSubcategoryAcyclic, quasiIso_eq_subcategoryAcyclic_W, CochainComplex.IsKProjective.leftOrthogonal, CochainComplex.isKProjective_iff_leftOrthogonal, mem_subcategoryAcyclic_iff, quotient_obj_mem_subcategoryAcyclic_iff_acyclic, CochainComplex.isKInjective_iff_rightOrthogonal, quotient_obj_mem_subcategoryAcyclic_iff_exactAt, instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms 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 subcategoryAcyclic	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.instIsClosedUnderIsomorphismsHomologicalKernel
instIsTriangulatedIntUpSubcategoryAcyclic 📖	mathematical	—	CategoryTheory.ObjectProperty.IsTriangulated 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 instHasZeroObject CategoryTheory.Abelian.hasZeroObject hasShift instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp CategoryTheory.Abelian.hasBinaryBiproducts subcategoryAcyclic	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject CategoryTheory.Abelian.hasZeroObject instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.instIsTriangulatedHomologicalKernel instIsHomologicalIntUpHomologyFunctor
mem_subcategoryAcyclic_iff 📖	mathematical	—	subcategoryAcyclic CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj 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 homologyFunctor CategoryTheory.categoryWithHomology_of_abelian	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.mem_homologicalKernel_iff CategoryTheory.categoryWithHomology_of_abelian
quasiIso_eq_subcategoryAcyclic_W 📖	mathematical	—	quasiIso ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Abelian.toPreadditive CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ObjectProperty.trW HomotopyCategory instCategoryHomotopyCategory instHasZeroObject CategoryTheory.Abelian.hasZeroObject hasShift instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp CategoryTheory.Abelian.hasBinaryBiproducts subcategoryAcyclic	—	CategoryTheory.MorphismProperty.ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instHasZeroObject CategoryTheory.Abelian.hasZeroObject instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Functor.mem_homologicalKernel_trW_iff instIsHomologicalIntUpHomologyFunctor
quotient_obj_mem_subcategoryAcyclic_iff_acyclic 📖	mathematical	—	subcategoryAcyclic CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient HomologicalComplex.Acyclic AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup	—	quotient_obj_mem_subcategoryAcyclic_iff_exactAt
quotient_obj_mem_subcategoryAcyclic_iff_exactAt 📖	mathematical	—	subcategoryAcyclic CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient HomologicalComplex.ExactAt AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian mem_subcategoryAcyclic_iff CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Iso.isZero_iff

---

← Back to Index