Documentation Verification Report

Refinements

📁 Source: Mathlib/Algebra/Homology/Refinements.lean

Statistics

Metric	Count
Definitions	0
Theorems `comp_homologyπ_eq_iff_up_to_refinements`, `comp_homologyπ_eq_zero_iff_up_to_refinements`, `comp_pOpcycles_eq_zero_iff_up_to_refinements`, `epi_homologyMap_iff_up_to_refinements`, `eq_liftCycles_homologyπ_up_to_refinements`, `exactAt_iff_exact_up_to_refinements`, `liftCycles_comp_homologyπ_eq_iff_up_to_refinements`, `liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements`, `mono_homologyMap_iff_up_to_refinements`	9
Total	9

HomologicalComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_homologyπ_eq_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `homology` `homologyπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Epi` `X` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `toCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.comp_homologyπ_eq_iff_up_to_refinements`
`comp_homologyπ_eq_zero_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `homology` `homologyπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Epi` `X` `toCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements`
`comp_pOpcycles_eq_zero_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `opcycles` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `pOpcycles` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Epi` `d`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements`
`epi_homologyMap_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.Epi` `homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `homologyMap` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.CategoryStruct.comp` `d` `CategoryTheory.Limits.HasZeroMorphisms.zero` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `Hom.f`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.epi_homologyMap_iff_up_to_refinements`
`eq_liftCycles_homologyπ_up_to_refinements` 📖	mathematical	`ComplexShape.next`	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Epi` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryStruct.comp` `d` `CategoryTheory.Limits.HasZeroMorphisms.zero` `homology` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `cycles` `liftCycles` `homologyπ`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements`
`exactAt_iff_exact_up_to_refinements` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next`	`ExactAt` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Epi` `X` `CategoryTheory.CategoryStruct.comp` `d`	—	`exactAt_iff'` `CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements`
`liftCycles_comp_homologyπ_eq_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `homology` `liftCycles` `homologyπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Epi` `X` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `d`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements`
`liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `cycles` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `homology` `liftCycles` `homologyπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Epi` `X` `d`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements`
`mono_homologyMap_iff_up_to_refinements` 📖	mathematical	`ComplexShape.prev` `ComplexShape.next`	`CategoryTheory.Mono` `homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `homologyMap` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Epi` `X` `CategoryTheory.CategoryStruct.comp` `d`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements`

---

← Back to Index