HomologicalFunctor

📁 Source: Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Statistics

Metric	Count
Definitions `IsHomological`, `homologicalKernel`, `homologySequenceComposableArrows₅`, `homologySequenceδ`	4
Theorems `exact`, `mk'`, `of_iso`, `toPreservesZeroMorphisms`, `comp_homologySequenceδ`, `comp_homologySequenceδ_assoc`, `homologySequenceComposableArrows₅_exact`, `homologySequence_comp`, `homologySequence_comp_assoc`, `homologySequence_epi_shift_map_mor₁_iff`, `homologySequence_epi_shift_map_mor₂_iff`, `homologySequence_exact₁`, `homologySequence_exact₂`, `homologySequence_exact₃`, `homologySequence_mono_shift_map_mor₁_iff`, `homologySequence_mono_shift_map_mor₂_iff`, `homologySequenceδ_comp`, `homologySequenceδ_comp_assoc`, `homologySequenceδ_naturality`, `homologySequenceδ_naturality_assoc`, `instAdditiveOfIsHomological`, `instIsClosedUnderIsomorphismsHomologicalKernel`, `instIsHomologicalCompOfIsTriangulated`, `instIsTriangulatedHomologicalKernel`, `instPreservesLimitsOfShapeDiscreteWalkingPairOfIsHomological`, `isHomological_of_localization`, `map_distinguished_exact`, `mem_homologicalKernel_iff`, `mem_homologicalKernel_trW_iff`	29
Total	33

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`IsHomological` 📖	CompData	8 math math: `HomotopyCategory.instIsHomologicalIntUpHomologyFunctor`, `CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda`, `isHomological_of_localization`, `instIsHomologicalCompOfIsTriangulated`, `IsHomological.of_iso`, `CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda`, `DerivedCategory.instIsHomologicalHomologyFunctor`, `IsHomological.mk'`
`homologicalKernel` 📖	CompOp	4 math math: `instIsTriangulatedHomologicalKernel`, `mem_homologicalKernel_iff`, `instIsClosedUnderIsomorphismsHomologicalKernel`, `mem_homologicalKernel_trW_iff`
`homologySequenceComposableArrows₅` 📖	CompOp	1 math math: `homologySequenceComposableArrows₅_exact`
`homologySequenceδ` 📖	CompOp	17 math math: `CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply`, `CochainComplex.mappingCone.homologySequenceδ_triangleh`, `homologySequenceδ_naturality`, `CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply`, `CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc`, `homologySequenceδ_comp_assoc`, `homologySequence_mono_shift_map_mor₁_iff`, `CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply`, `comp_homologySequenceδ`, `homologySequence_exact₃`, `homologySequence_exact₁`, `CochainComplex.homologySequenceδ_quotient_mapTriangle_obj`, `homologySequenceδ_naturality_assoc`, `homologySequenceδ_comp`, `comp_homologySequenceδ_assoc`, `CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply`, `homologySequence_epi_shift_map_mor₂_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_homologySequenceδ` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologySequenceδ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`shiftMap_comp'` `CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃` `shiftMap_zero` `IsHomological.toPreservesZeroMorphisms` `preservesZeroMorphisms_of_additive`
`comp_homologySequenceδ_assoc` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Pretriangulated.Triangle.obj₁` `homologySequenceδ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_homologySequenceδ`
`homologySequenceComposableArrows₅_exact` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ComposableArrows.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `homologySequenceComposableArrows₅`	—	`CategoryTheory.ComposableArrows.exact_of_δ₀` `CategoryTheory.ShortComplex.Exact.exact_toComposableArrows` `homologySequence_comp` `homologySequence_exact₂` `comp_homologySequenceδ` `homologySequence_exact₃` `homologySequenceδ_comp` `homologySequence_exact₁`
`homologySequence_comp` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.mor₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`map_comp` `CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂` `map_zero` `instPreservesZeroMorphismsShift` `IsHomological.toPreservesZeroMorphisms` `preservesZeroMorphisms_of_additive`
`homologySequence_comp_assoc` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologySequence_comp`
`homologySequence_epi_shift_map_mor₁_iff` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.Epi` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.ShortComplex.Exact.epi_f_iff` `homologySequence_comp` `homologySequence_exact₂`
`homologySequence_epi_shift_map_mor₂_iff` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.Epi` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologySequenceδ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.ShortComplex.Exact.epi_f_iff` `comp_homologySequenceδ` `homologySequence_exact₃`
`homologySequence_exact₁` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `homologySequenceδ` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `homologySequenceδ_comp`	—	`CategoryTheory.ShortComplex.exact_of_iso` `homologySequence_comp` `CategoryTheory.Pretriangulated.inv_rot_of_distTriang` `homologySequenceδ_comp` `add_neg_cancel` `neg_add_cancel` `CategoryTheory.Preadditive.neg_comp` `shiftIso_hom_app_comp_shiftMap_of_add_eq_zero` `map_neg` `instAdditiveShift` `instAdditiveOfIsHomological` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `homologySequence_exact₂`
`homologySequence_exact₂` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologySequence_comp`	—	`CategoryTheory.ShortComplex.exact_of_iso` `CategoryTheory.Pretriangulated.Triangle.shift_distinguished` `IsHomological.toPreservesZeroMorphisms` `homologySequence_comp` `map_units_smul` `intLinear` `instAdditiveOfIsHomological` `CategoryTheory.Linear.comp_units_smul` `CategoryTheory.Linear.units_smul_comp` `isoShift_hom_naturality` `smul_smul` `Int.units_mul_self` `one_smul` `map_distinguished_exact`
`homologySequence_exact₃` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologySequenceδ` `comp_homologySequenceδ`	—	`CategoryTheory.ShortComplex.exact_of_iso` `homologySequence_comp` `CategoryTheory.Pretriangulated.rot_of_distTriang` `comp_homologySequenceδ` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `homologySequence_exact₂`
`homologySequence_mono_shift_map_mor₁_iff` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.Mono` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `homologySequenceδ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.ShortComplex.Exact.mono_g_iff` `homologySequenceδ_comp` `homologySequence_exact₁`
`homologySequence_mono_shift_map_mor₂_iff` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.Mono` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.ShortComplex.Exact.mono_g_iff` `homologySequence_comp` `homologySequence_exact₂`
`homologySequenceδ_comp` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `homologySequenceδ` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`shiftMap_comp` `CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁` `shiftMap_zero` `IsHomological.toPreservesZeroMorphisms` `preservesZeroMorphisms_of_additive`
`homologySequenceδ_comp_assoc` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `homologySequenceδ` `CategoryTheory.Pretriangulated.Triangle.obj₂` `map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologySequenceδ_comp`
`homologySequenceδ_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `map` `CategoryTheory.Pretriangulated.TriangleMorphism.hom₃` `homologySequenceδ` `CategoryTheory.Pretriangulated.TriangleMorphism.hom₁`	—	`shiftMap_comp'` `CategoryTheory.Pretriangulated.TriangleMorphism.comm₃` `shiftMap_comp`
`homologySequenceδ_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `shift` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle.obj₃` `map` `CategoryTheory.Pretriangulated.TriangleMorphism.hom₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `homologySequenceδ` `CategoryTheory.Pretriangulated.TriangleMorphism.hom₁`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologySequenceδ_naturality`
`instAdditiveOfIsHomological` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Abelian.toPreadditive`	—	`additive_of_preserves_binary_products` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Pretriangulated.instHasFiniteProducts` `Finite.of_fintype` `instPreservesLimitsOfShapeDiscreteWalkingPairOfIsHomological` `IsHomological.toPreservesZeroMorphisms`
`instIsClosedUnderIsomorphismsHomologicalKernel` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `homologicalKernel`	—	`CategoryTheory.Limits.IsZero.of_iso`
`instIsHomologicalCompOfIsTriangulated` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsHomological` `comp`	—	`preservesZeroMorphisms_comp` `IsTriangulated.instPreservesZeroMorphisms` `IsHomological.toPreservesZeroMorphisms` `map_distinguished_exact` `map_distinguished`
`instIsTriangulatedHomologicalKernel` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.ObjectProperty.IsTriangulated` `homologicalKernel`	—	`CategoryTheory.Limits.IsZero.of_iso` `CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk'` `instIsClosedUnderIsomorphismsHomologicalKernel` `CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros` `CategoryTheory.Pretriangulated.Triangle.shift_distinguished` `IsHomological.toPreservesZeroMorphisms` `map_distinguished_exact` `CategoryTheory.Limits.IsZero.eq_of_src` `CategoryTheory.Limits.IsZero.eq_of_tgt` `CategoryTheory.Limits.isZero_zero` `map_isZero` `preservesZeroMorphisms_comp` `preservesZeroMorphisms_of_additive`
`instPreservesLimitsOfShapeDiscreteWalkingPairOfIsHomological` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Limits.PreservesLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory`	—	`CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CategoryTheory.Pretriangulated.instHasBinaryBiproducts` `CategoryTheory.Preadditive.mono_iff_cancel_zero` `CategoryTheory.Limits.biprod.inl_snd` `IsHomological.toPreservesZeroMorphisms` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.instIsSplitMonoMap` `CategoryTheory.Limits.biprod.inl_mono` `map_distinguished_exact` `CategoryTheory.Pretriangulated.binaryBiproductTriangle_distinguished` `CategoryTheory.ShortComplex.Exact.lift'` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `CategoryTheory.Category.assoc` `biprodComparison_snd` `CategoryTheory.Limits.zero_comp` `CategoryTheory.eq_whisker` `biprodComparison_fst` `map_comp` `CategoryTheory.Limits.biprod.inl_fst` `map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison` `CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct` `CategoryTheory.Limits.preservesLimit_of_iso_diagram`
`isHomological_of_localization` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsHomological`	—	`preservesZeroMorphisms_of_map_zero_object` `CategoryTheory.Abelian.hasZeroObject` `IsTriangulated.instPreservesZeroMorphisms` `IsHomological.toPreservesZeroMorphisms` `IsHomological.of_iso` `IsHomological.mk'` `CategoryTheory.Pretriangulated.isomorphic_distinguished` `distTriang_iff` `map_distinguished_exact`
`map_distinguished_exact` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.map` `CategoryTheory.Pretriangulated.shortComplexOfDistTriangle` `IsHomological.toPreservesZeroMorphisms`	—	`IsHomological.exact`
`mem_homologicalKernel_iff` 📖	mathematical	—	`homologicalKernel` `CategoryTheory.Limits.IsZero` `obj` `shift` `Int.instAddMonoid`	—	`CategoryTheory.Iso.isZero_iff`
`mem_homologicalKernel_trW_iff` 📖	mathematical	`Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.ObjectProperty.trW` `homologicalKernel` `CategoryTheory.IsIso` `obj` `shift` `map`	—	`CategoryTheory.Pretriangulated.distinguished_cocone_triangle` `CategoryTheory.ObjectProperty.trW_iff_of_distinguished` `instIsClosedUnderIsomorphismsHomologicalKernel` `comp_homologySequenceδ` `CategoryTheory.ShortComplex.Exact.isZero_X₂_iff` `homologySequence_exact₃` `homologySequence_mono_shift_map_mor₁_iff` `homologySequence_epi_shift_map_mor₁_iff` `sub_add_cancel` `CategoryTheory.isIso_of_mono_of_epi` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso`

CategoryTheory.Functor.IsHomological

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.map` `CategoryTheory.Pretriangulated.shortComplexOfDistTriangle` `toPreservesZeroMorphisms`	—	—
`mk'` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.map` `CategoryTheory.Pretriangulated.shortComplexOfDistTriangle` `CategoryTheory.Pretriangulated.isomorphic_distinguished` `CategoryTheory.Iso.symm` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory`	`CategoryTheory.Functor.IsHomological`	—	`CategoryTheory.Pretriangulated.isomorphic_distinguished` `CategoryTheory.ShortComplex.exact_iff_of_iso`
`of_iso` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.IsHomological`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_iso` `toPreservesZeroMorphisms` `CategoryTheory.ShortComplex.exact_of_iso` `CategoryTheory.Functor.map_distinguished_exact`
`toPreservesZeroMorphisms` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	—

---

← Back to Index