Documentation Verification Report

ShortExact

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

Statistics

Metric	Count
Definitions `descShortComplex`	1
Theorems `homologySequenceδ_quotient_mapTriangle_obj`, `homologySequenceδ_quotient_mapTriangle_obj_assoc`, `homologySequenceδ_triangleh`, `inl_v_descShortComplex_f`, `inl_v_descShortComplex_f_assoc`, `inr_descShortComplex`, `inr_descShortComplex_assoc`, `inr_f_descShortComplex_f`, `inr_f_descShortComplex_f_assoc`, `quasiIso_descShortComplex`	10
Total	11

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homologySequenceδ_quotient_mapTriangle_obj` 📖	mathematical	—	`CategoryTheory.Functor.homologySequenceδ` `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` `HomotopyCategory.hasShift` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `HomotopyCategory.quotient` `HomotopyCategory.commShiftQuotient` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CochainComplex` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `HomologicalComplex.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HomotopyCategory.homologyFunctorFactors` `CategoryTheory.Functor.shift` `Int.instAddMonoid` `instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat` `CategoryTheory.Functor.shiftMap` `CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Iso.inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomotopyCategory.homologyFunctor_shiftMap` `CategoryTheory.categoryWithHomology_of_abelian`
`homologySequenceδ_quotient_mapTriangle_obj_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `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` `CategoryTheory.Functor.shift` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `Int.instAddMonoid` `HomotopyCategory.hasShift` `HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `HomotopyCategory.quotient` `HomotopyCategory.commShiftQuotient` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Functor.homologySequenceδ` `HomologicalComplex.homologyFunctor` `CochainComplex` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HomotopyCategory.homologyFunctorFactors` `instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat` `CategoryTheory.Functor.shiftMap` `CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Iso.inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologySequenceδ_quotient_mapTriangle_obj`

CochainComplex.mappingCone

Definitions

Name	Category	Theorems
`descShortComplex` 📖	CompOp	8 math math: `homologySequenceδ_triangleh`, `inr_f_descShortComplex_f_assoc`, `inr_descShortComplex_assoc`, `quasiIso_descShortComplex`, `inl_v_descShortComplex_f_assoc`, `inr_descShortComplex`, `inl_v_descShortComplex_f`, `inr_f_descShortComplex_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homologySequenceδ_triangleh` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.Functor.homologySequenceδ` `HomotopyCategory` `instCategoryHomotopyCategory` `HomotopyCategory.hasShift` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat` `triangleh` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Functor.comp` `HomotopyCategory.quotient` `CochainComplex.mappingCone` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `HomologicalComplex.homologyFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HomotopyCategory.homologyFunctorFactors` `HomologicalComplex.homology` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.CategoryWithHomology.hasHomology` `HomologicalComplex.sc` `HomologicalComplex.homologyMap` `descShortComplex` `CategoryTheory.ShortComplex.ShortExact.δ` `CategoryTheory.Iso.inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Abelian.hasBinaryBiproducts` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.Functor.instIsSplitMonoApp` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Functor.map_injective` `CategoryTheory.Yoneda.yoneda_faithful` `CategoryTheory.NatTrans.ext'` `CategoryTheory.types_ext` `CochainComplex.next` `HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements` `CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc` `CategoryTheory.Category.comp_id` `Mathlib.Tactic.Reassoc.eq_whisker'` `HomologicalComplex.homologyπ_naturality_assoc` `HomologicalComplex.liftCycles_comp_cyclesMap_assoc` `decomp_to` `CategoryTheory.Preadditive.add_comp` `inl_v_descShortComplex_f` `CategoryTheory.Limits.comp_zero` `inr_f_descShortComplex_f` `zero_add` `HomologicalComplex.liftCycles.congr_simp` `CategoryTheory.Preadditive.neg_comp` `add_zero` `CategoryTheory.Limits.zero_comp` `inl_v_snd_v_assoc` `inl_v_fst_v_assoc` `CategoryTheory.Preadditive.comp_add` `d_snd_v` `inr_f_snd_v` `neg_eq_zero` `CategoryTheory.Preadditive.comp_neg` `d_fst_v` `inr_f_fst_v` `inr_f_d` `ext_to_iff` `ComplexShape.next_eq'` `CategoryTheory.ShortComplex.ShortExact.δ_eq` `CochainComplex.liftCycles_shift_homologyπ_assoc` `inl_v_triangle_mor₃_f_assoc` `CategoryTheory.Iso.inv_hom_id` `inr_f_triangle_mor₃_f_assoc`
`inl_v_descShortComplex_f` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.ShortComplex.X₁` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.ShortComplex.X₃` `CochainComplex.HomComplex.Cochain.v` `inl` `HomologicalComplex.Hom.f` `descShortComplex` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `inl_v_desc_f`
`inl_v_descShortComplex_f_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.ShortComplex.X₁` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CochainComplex.HomComplex.Cochain.v` `inl` `CategoryTheory.ShortComplex.X₃` `HomologicalComplex.Hom.f` `descShortComplex` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_v_descShortComplex_f`
`inr_descShortComplex` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `CategoryTheory.ShortComplex.X₃` `inr` `descShortComplex` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `inr_desc`
`inr_descShortComplex_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `inr` `CategoryTheory.ShortComplex.X₃` `descShortComplex` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_descShortComplex`
`inr_f_descShortComplex_f` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.ShortComplex.X₂` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.ShortComplex.X₃` `HomologicalComplex.Hom.f` `inr` `descShortComplex` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `inr_f_desc_f`
`inr_f_descShortComplex_f_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.ShortComplex.X₂` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.Hom.f` `inr` `CategoryTheory.ShortComplex.X₃` `descShortComplex` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_f_descShortComplex_f`
`quasiIso_descShortComplex` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms`	`QuasiIso` `CochainComplex.mappingCone` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `CategoryTheory.ShortComplex.X₃` `descShortComplex` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `quasiIsoAt_iff_isIso_homologyMap` `CategoryTheory.NatTrans.naturality` `CategoryTheory.NatTrans.naturality_assoc` `HomologicalComplex.homologyMap_comp` `inr_descShortComplex` `homologySequenceδ_triangleh` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono` `CategoryTheory.ComposableArrows.Exact.δlast` `CategoryTheory.Functor.homologySequenceComposableArrows₅_exact` `HomotopyCategory.instHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `HomotopyCategory.instAdditiveIntUpShiftFunctor` `HomotopyCategory.instIsHomologicalIntUpHomologyFunctor` `HomotopyCategory.mappingCone_triangleh_distinguished` `HomologicalComplex.HomologySequence.composableArrows₅_exact` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.Functor.instIsSplitMonoApp` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsIso.of_isIso_comp_left`

---

← Back to Index