Additive

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

Statistics

Metric	Count
Definitions mapHomologicalComplex, mapHomologicalComplex, mapHomologicalComplexIdIso, mapHomologicalComplex, mapHomologicalComplex, fAddMonoidHom, hasIntScalar, hasNatScalar, instAddCommGroupHom, instAddHom, instNegHom, instPreadditive, instSubHom, instZeroHom_1, singleMapHomologicalComplex	15
Theorems mapHomologicalComplex_counitIso, mapHomologicalComplex_functor, mapHomologicalComplex_inverse, mapHomologicalComplex_unitIso, mapHomologicalComplexIdIso_hom_app_f, mapHomologicalComplexIdIso_inv_app_f, mapHomologicalComplex_map_f, mapHomologicalComplex_obj_X, mapHomologicalComplex_obj_d, mapHomologicalComplex_reflects_iso, map_homogical_complex_additive, mapHomologicalComplex_hom_app_f, mapHomologicalComplex_inv_app_f, mapHomologicalComplex_app_f, mapHomologicalComplex_comp, mapHomologicalComplex_id, mapHomologicalComplex_naturality, mapHomologicalComplex_naturality_assoc, instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex, map_chain_complex_of, fAddMonoidHom_apply, add_f_apply, eval_additive, instAdditiveSingle, neg_f_apply, nsmul_f_apply, singleMapHomologicalComplex_hom_app_ne, singleMapHomologicalComplex_hom_app_self, singleMapHomologicalComplex_inv_app_ne, singleMapHomologicalComplex_inv_app_self, sub_f_apply, zero_f_apply, zsmul_f_apply	33
Total	48

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex 📖	mathematical	—	Functor.PreservesZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms Functor.mapHomologicalComplex	—	HomologicalComplex.hom_ext Functor.map_zero

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
mapHomologicalComplex 📖	CompOp	4 math math: mapHomologicalComplex_unitIso, mapHomologicalComplex_functor, mapHomologicalComplex_counitIso, mapHomologicalComplex_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomologicalComplex_counitIso 📖	mathematical	—	counitIso HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.mapHomologicalComplex inverse functor CategoryTheory.Functor.id CategoryTheory.NatIso.mapHomologicalComplex CategoryTheory.Functor.mapHomologicalComplexIdIso	—	—
mapHomologicalComplex_functor 📖	mathematical	—	functor HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex CategoryTheory.Functor.mapHomologicalComplex	—	—
mapHomologicalComplex_inverse 📖	mathematical	—	inverse HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex CategoryTheory.Functor.mapHomologicalComplex	—	—
mapHomologicalComplex_unitIso 📖	mathematical	—	unitIso HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.comp functor inverse CategoryTheory.Iso.symm CategoryTheory.Functor.mapHomologicalComplexIdIso CategoryTheory.NatIso.mapHomologicalComplex	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapHomologicalComplex 📖	CompOp	107 math math: HomologicalComplex.singleMapHomologicalComplex_hom_app_ne, CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f, mapHomologicalComplexIdIso_hom_app_f, HomologicalComplex.singleMapHomologicalComplex_hom_app_self, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, mapHomologicalComplex_linear, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, mapHomotopyEquiv_inv, mapHomologicalComplex_obj_d, mapHomologicalComplex_map_f, mapHomotopyEquiv_homotopyHomInvId, HomologicalComplex.map_isStrictlySupported, CochainComplex.HomComplex.Cochain.map_v, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, map_homogical_complex_additive, CategoryTheory.NatTrans.mapHomologicalComplex_app_f, CochainComplex.HomComplex.Cochain.map_zero, CategoryTheory.NatTrans.mapHomologicalComplex_id, CategoryTheory.NatTrans.mapHomotopyCategory_app, mapProjectiveResolution_π, CategoryTheory.instIsIsoToRightDerivedZero', CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, mapHomologicalComplex_commShiftIso_eq, CategoryTheory.Equivalence.mapHomologicalComplex_unitIso, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc, Homotopy.map_nullHomotopicMap', mapProjectiveResolution_complex, Rep.standardComplex.εToSingle₀_comp_eq, HomologicalComplex.quasiIso_iff_evaluation, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.NatTrans.mapHomologicalComplex_comp, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, HomologicalComplex.singleMapHomologicalComplex_inv_app_self, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, mapHomologicalComplex_obj_X, CochainComplex.HomComplex.Cochain.map_add, mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, mapHomologicalComplex_reflects_iso, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, Homotopy.map_nullHomotopicMap, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, CochainComplex.mappingCone.map_inr, mapCochainComplexShiftIso_inv_app_f, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, mapHomotopy_hom, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, mapHomologicalComplexIdIso_inv_app_f, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, CochainComplex.HomComplex.Cochain.map_comp, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, CochainComplex.HomComplex.Cochain.map_sub, mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor, CategoryTheory.Equivalence.mapHomologicalComplex_functor, CategoryTheory.NatTrans.mapHomologicalComplex_naturality, mapHomologicalComplex_commShiftIso_inv_app_f, mapHomotopyEquiv_homotopyInvHomId, AlgebraicTopology.map_alternatingFaceMapComplex, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, HomologicalComplex.singleMapHomologicalComplex_inv_app_ne, CategoryTheory.Equivalence.mapHomologicalComplex_counitIso, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, leftDerived_map_eq, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, HomologicalComplex.quasiIsoAt_iff_evaluation, CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc, mapHomotopyCategory_map, rightDerived_map_eq, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, mapHomotopyCategory_obj, mapHomologicalComplex_commShiftIso_hom_app_f, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, CochainComplex.HomComplex.δ_map, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, CochainComplex.HomComplex.Cochain.map_ofHom, mapCochainComplexShiftIso_hom_app_f, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, HomologicalComplex.quasiIsoAt_map_of_preservesHomology, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, mapHomotopyEquiv_hom, CategoryTheory.Equivalence.mapHomologicalComplex_inverse, mapDerivedCategoryFactorsh_hom_app, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CochainComplex.HomComplex.Cochain.map_neg, ChainComplex.map_chain_complex_of, CategoryTheory.instIsIsoFromLeftDerivedZero', HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, CochainComplex.mappingCone.map_δ, HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology
mapHomologicalComplexIdIso 📖	CompOp	4 math math: mapHomologicalComplexIdIso_hom_app_f, CategoryTheory.Equivalence.mapHomologicalComplex_unitIso, mapHomologicalComplexIdIso_inv_app_f, CategoryTheory.Equivalence.mapHomologicalComplex_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomologicalComplexIdIso_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f obj HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category preservesZeroMorphisms_of_full Full.id mapHomologicalComplexIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X	—	preservesZeroMorphisms_of_full Full.id
mapHomologicalComplexIdIso_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f obj HomologicalComplex HomologicalComplex.instCategory id mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category preservesZeroMorphisms_of_full Full.id mapHomologicalComplexIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X	—	preservesZeroMorphisms_of_full Full.id
mapHomologicalComplex_map_f 📖	mathematical	—	HomologicalComplex.Hom.f obj HomologicalComplex.X map HomologicalComplex.d HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex	—	—
mapHomologicalComplex_obj_X 📖	mathematical	—	HomologicalComplex.X obj HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex	—	—
mapHomologicalComplex_obj_d 📖	mathematical	—	HomologicalComplex.d obj HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex map HomologicalComplex.X	—	—
mapHomologicalComplex_reflects_iso 📖	mathematical	—	ReflectsIsomorphisms HomologicalComplex HomologicalComplex.instCategory mapHomologicalComplex	—	HomologicalComplex.Hom.isIso_of_components CategoryTheory.isIso_of_reflects_iso CategoryTheory.Iso.isIso_hom
map_homogical_complex_additive 📖	mathematical	—	Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex.instPreadditive mapHomologicalComplex preservesZeroMorphisms_of_additive	—	preservesZeroMorphisms_of_additive HomologicalComplex.hom_ext map_add

CategoryTheory.NatIso

Definitions

Name	Category	Theorems
mapHomologicalComplex 📖	CompOp	4 math math: mapHomologicalComplex_inv_app_f, CategoryTheory.Equivalence.mapHomologicalComplex_unitIso, mapHomologicalComplex_hom_app_f, CategoryTheory.Equivalence.mapHomologicalComplex_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomologicalComplex_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapHomologicalComplex HomologicalComplex.X	—	—
mapHomologicalComplex_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapHomologicalComplex HomologicalComplex.X	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
mapHomologicalComplex 📖	CompOp	10 math math: mapHomologicalComplex_app_f, mapHomologicalComplex_id, mapHomotopyCategory_app, mapHomologicalComplex_comp, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, mapHomologicalComplex_naturality, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, mapHomologicalComplex_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, CategoryTheory.InjectiveResolution.rightDerived_app_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomologicalComplex_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex app mapHomologicalComplex HomologicalComplex.X	—	—
mapHomologicalComplex_comp 📖	mathematical	—	mapHomologicalComplex CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex	—	—
mapHomologicalComplex_id 📖	mathematical	—	mapHomologicalComplex CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex	—	—
mapHomologicalComplex_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.map app mapHomologicalComplex	—	naturality
mapHomologicalComplex_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.map app mapHomologicalComplex	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapHomologicalComplex_naturality

ChainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_chain_complex_of 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Functor.obj HomologicalComplex ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex of CategoryTheory.Functor.map	—	HomologicalComplex.ext AddRightCancelSemigroup.toIsRightCancelAdd of_d CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

HomologicalComplex

Definitions

Name	Category	Theorems
hasIntScalar 📖	CompOp	3 math math: HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, zsmul_f_apply, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc
hasNatScalar 📖	CompOp	1 math math: nsmul_f_apply
instAddCommGroupHom 📖	CompOp	1 math math: Hom.fAddMonoidHom_apply
instAddHom 📖	CompOp	26 math math: CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, add_f_apply, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, CategoryTheory.ProjectiveResolution.extMk_hom, homologyMap_add, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, AlgebraicTopology.DoldKan.P_succ, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, Homotopy.add_hom, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, extendMap_add, AlgebraicTopology.DoldKan.P_add_Q, CategoryTheory.InjectiveResolution.extMk_hom, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, CochainComplex.HomComplex.Cocycle.equivHom_apply, CochainComplex.HomComplex.Cochain.ofHom_add, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, CochainComplex.HomComplex.CohomologyClass.toHom_mk, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, AlgebraicTopology.DoldKan.PInfty_add_QInfty
instNegHom 📖	CompOp	9 math math: homologyMap_neg, CochainComplex.HomComplex.Cochain.ofHom_neg, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, neg_f_apply, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃
instPreadditive 📖	CompOp	29 math math: CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, CategoryTheory.Functor.mapHomologicalComplex_linear, CochainComplex.instLinearIntFunctorSingleFunctors, CategoryTheory.Functor.map_homogical_complex_additive, HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, DerivedCategory.instLinearCochainComplexIntQ, CochainComplex.instAdditiveIntFunctorSingleFunctors, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, instAdditiveHomologyFunctor, CochainComplex.instLinearIntShiftFunctor, CochainComplex.instAdditiveIntShiftFunctor, ComplexShape.Embedding.instAdditiveHomologicalComplexRestrictionFunctor, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, ComplexShape.Embedding.instAdditiveHomologicalComplexExtendFunctor, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, CochainComplex.mappingCone.triangleRotateShortComplex_g, DerivedCategory.instAdditiveCochainComplexIntQ, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, HomotopyCategory.instAdditiveHomologicalComplexQuotient, instAdditiveSingle, opFunctor_additive, eval_additive, CochainComplex.mappingCone.triangleRotateShortComplex_f, unopFunctor_additive, HomotopyCategory.instLinearHomologicalComplexQuotient, CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor
instSubHom 📖	CompOp	7 math math: cylinder.πCompι₀Homotopy.nullHomotopicMap_eq, sub_f_apply, CochainComplex.HomComplex.Cochain.ofHom_sub, homologyMap_sub, cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, AlgebraicTopology.DoldKan.Q_succ, cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f
instZeroHom_1 📖	CompOp	28 math math: homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, CochainComplex.IsKInjective.nonempty_homotopy_zero, HomotopyCategory.isZero_quotient_obj_iff, CochainComplex.IsKProjective.homotopyZero_def, HomotopyCategory.quotient_map_eq_zero_iff, CochainComplex.mappingCone.inr_triangleδ, homotopyCofiber.inrCompHomotopy_hom, homotopyCofiber.descSigma_ext_iff, homotopyCofiber.inrCompHomotopy_hom_desc_hom, groupCohomology.cochainsMap_zero, CochainComplex.IsKInjective.homotopyZero_def, homotopyCofiber.inlX_desc_f_assoc, CochainComplex.mappingCone.inr_triangleδ_assoc, homotopyCofiber.eq_desc, CochainComplex.IsKProjective.nonempty_homotopy_zero, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, homotopyCofiber.inrCompHomotopy_hom_eq_zero, zero_f_apply, homotopyCofiber.desc_f, groupHomology.chainsMap_zero, CochainComplex.HomComplex.Cochain.ofHom_zero, Homotopy.nullHomotopy_hom, homotopyCofiber.inlX_desc_f, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, AlgebraicTopology.DoldKan.Q_zero, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, Homotopy.nullHomotopy'_hom
singleMapHomologicalComplex 📖	CompOp	6 math math: singleMapHomologicalComplex_hom_app_ne, singleMapHomologicalComplex_hom_app_self, CategoryTheory.Functor.mapProjectiveResolution_π, Rep.standardComplex.εToSingle₀_comp_eq, singleMapHomologicalComplex_inv_app_self, singleMapHomologicalComplex_inv_app_ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
eval_additive 📖	mathematical	—	CategoryTheory.Functor.Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive eval	—	—
instAdditiveSingle 📖	mathematical	—	CategoryTheory.Functor.Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive single	—	from_single_hom_ext CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_add
neg_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom X NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
nsmul_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory hasNatScalar X AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
singleMapHomologicalComplex_hom_app_ne 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.comp single CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category singleMapHomologicalComplex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.NatIso.ofComponents.congr_simp
singleMapHomologicalComplex_hom_app_self 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.comp single CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category singleMapHomologicalComplex CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Functor.map singleObjXSelf CategoryTheory.Iso.inv	—	CategoryTheory.NatIso.ofComponents.congr_simp CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans
singleMapHomologicalComplex_inv_app_ne 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.comp single CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category singleMapHomologicalComplex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.NatIso.ofComponents.congr_simp
singleMapHomologicalComplex_inv_app_self 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.comp single CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category singleMapHomologicalComplex CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom singleObjXSelf CategoryTheory.Functor.map	—	CategoryTheory.NatIso.ofComponents.congr_simp CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans
sub_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom X SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
zero_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom_1 X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
zsmul_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory hasIntScalar X SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—

HomologicalComplex.Hom

Definitions

Name	Category	Theorems
fAddMonoidHom 📖	CompOp	1 math math: fAddMonoidHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.X AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup HomologicalComplex.instAddCommGroupHom CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike fAddMonoidHom f	—	—

---

← Back to Index