Documentation Verification Report

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` `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` `subcategoryAcyclic`	—	`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` `CategoryTheory.Functor.instIsClosedUnderIsomorphismsHomologicalKernel`
`instIsTriangulatedIntUpSubcategoryAcyclic` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsTriangulated` `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` `instHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `hasShift` `instPreadditive` `instAdditiveIntUpShiftFunctor` `instPretriangulatedIntUp` `CategoryTheory.Abelian.hasBinaryBiproducts` `subcategoryAcyclic`	—	`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` `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` `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` `homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian`	—	`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.Functor.mem_homologicalKernel_iff` `CategoryTheory.categoryWithHomology_of_abelian`
`quasiIso_eq_subcategoryAcyclic_W` 📖	mathematical	—	`quasiIso` `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` `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` `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.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` `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` `HomologicalComplex.instCategory` `HomotopyCategory` `instCategoryHomotopyCategory` `quotient` `HomologicalComplex.Acyclic` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd`	—	`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` `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` `HomologicalComplex.instCategory` `HomotopyCategory` `instCategoryHomotopyCategory` `quotient` `HomologicalComplex.ExactAt` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd`	—	`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` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `mem_subcategoryAcyclic_iff` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.Iso.isZero_iff`

---

← Back to Index