Homotopy

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

Statistics

Metric	Count
Definitions mapHomotopy, mapHomotopyEquiv, homotopyEquivalences, add, comp, compLeft, compLeftId, compRight, compRightId, equivSubZero, hom, mkCoinductive, mkCoinductiveAux₁, mkCoinductiveAux₂, mkInductive, mkInductiveAux₁, mkInductiveAux₂, nullHomotopicMap, nullHomotopicMap', nullHomotopy, nullHomotopy', ofEq, refl, smul, toShortComplex, trans, HomotopyEquiv, hom, homotopyHomInvId, homotopyInvHomId, instInhabited, inv, ofIso, refl, toHomologyIso, trans, dNext, fromNext, prevD, toPrev	40
Theorems mapHomotopyEquiv_hom, mapHomotopyEquiv_homotopyHomInvId, mapHomotopyEquiv_homotopyInvHomId, mapHomotopyEquiv_inv, mapHomotopy_hom, add_hom, comm, compLeftId_hom, compLeft_hom, compRightId_hom, compRight_hom, comp_hom, comp_nullHomotopicMap, comp_nullHomotopicMap', dNext_cochainComplex, dNext_succ_chainComplex, dNext_zero_chainComplex, ext, ext_iff, homologyMap_eq, map_nullHomotopicMap, map_nullHomotopicMap', mkCoinductiveAux₂_add_one, mkCoinductiveAux₂_zero, mkCoinductiveAux₃, mkInductiveAux₂_add_one, mkInductiveAux₂_zero, mkInductiveAux₃, nullHomotopicMap'_comp, nullHomotopicMap'_f, nullHomotopicMap'_f_eq_zero, nullHomotopicMap'_f_of_not_rel_left, nullHomotopicMap'_f_of_not_rel_right, nullHomotopicMap_comp, nullHomotopicMap_f, nullHomotopicMap_f_eq_zero, nullHomotopicMap_f_of_not_rel_left, nullHomotopicMap_f_of_not_rel_right, nullHomotopy'_hom, nullHomotopy_hom, ofEq_hom, prevD_chainComplex, prevD_succ_cochainComplex, prevD_zero_cochainComplex, refl_hom, smul_hom, symm_hom, trans_hom, zero, dNext_comp_left, dNext_comp_right, dNext_eq, dNext_eq_dFrom_fromNext, dNext_eq_zero, dNext_nat, prevD_comp_left, prevD_comp_right, prevD_eq, prevD_eq_toPrev_dTo, prevD_eq_zero, prevD_nat	61
Total	101

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapHomotopy 📖	CompOp	3 math math: mapHomotopyEquiv_homotopyHomInvId, mapHomotopy_hom, mapHomotopyEquiv_homotopyInvHomId
mapHomotopyEquiv 📖	CompOp	4 math math: mapHomotopyEquiv_inv, mapHomotopyEquiv_homotopyHomInvId, mapHomotopyEquiv_homotopyInvHomId, mapHomotopyEquiv_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomotopyEquiv_hom 📖	mathematical	—	HomotopyEquiv.hom obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory mapHomologicalComplex preservesZeroMorphisms_of_additive mapHomotopyEquiv map	—	preservesZeroMorphisms_of_additive
mapHomotopyEquiv_homotopyHomInvId 📖	mathematical	—	HomotopyEquiv.homotopyHomInvId obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory mapHomologicalComplex preservesZeroMorphisms_of_additive mapHomotopyEquiv Homotopy CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map HomotopyEquiv.hom HomotopyEquiv.inv CategoryTheory.CategoryStruct.id mapHomotopy	—	preservesZeroMorphisms_of_additive
mapHomotopyEquiv_homotopyInvHomId 📖	mathematical	—	HomotopyEquiv.homotopyInvHomId obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory mapHomologicalComplex preservesZeroMorphisms_of_additive mapHomotopyEquiv Homotopy CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map HomotopyEquiv.inv HomotopyEquiv.hom CategoryTheory.CategoryStruct.id mapHomotopy	—	preservesZeroMorphisms_of_additive
mapHomotopyEquiv_inv 📖	mathematical	—	HomotopyEquiv.inv obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory mapHomologicalComplex preservesZeroMorphisms_of_additive mapHomotopyEquiv map	—	preservesZeroMorphisms_of_additive
mapHomotopy_hom 📖	mathematical	—	Homotopy.hom obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory mapHomologicalComplex preservesZeroMorphisms_of_additive map mapHomotopy HomologicalComplex.X	—	preservesZeroMorphisms_of_additive

HomologicalComplex

Definitions

Name	Category	Theorems
homotopyEquivalences 📖	CompOp	6 math math: homotopyEquivalences_le_quasiIso, HomotopyCategory.quotient_inverts_homotopyEquivalences, HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, ComplexShape.quotient_isLocalization

Homotopy

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: add_hom
comp 📖	CompOp	1 math math: comp_hom
compLeft 📖	CompOp	1 math math: compLeft_hom
compLeftId 📖	CompOp	1 math math: compLeftId_hom
compRight 📖	CompOp	2 math math: HomologicalComplex.homotopyCofiber.eq_desc, compRight_hom
compRightId 📖	CompOp	1 math math: compRightId_hom
equivSubZero 📖	CompOp	—
hom 📖	CompOp	37 math math: HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, extend_hom_eq, CochainComplex.homotopyUnop_hom_eq, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom, HomologicalComplex.homotopyCofiber.descSigma_ext_iff, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom, zero, HomologicalComplex.homotopyCofiber.inlX_desc_f_assoc, CategoryTheory.Functor.mapHomotopy_hom, compRight_hom, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_eq_zero, CochainComplex.homotopyOp_hom_eq, ofEq_hom, ofExtend_hom, symm_hom, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, compLeftId_hom, add_hom, ext_iff, compRightId_hom, trans_hom, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, smul_hom, comm, comp_hom, HomologicalComplex.homotopyCofiber.desc_f, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, compLeft_hom, nullHomotopy_hom, HomologicalComplex.homotopyCofiber.inlX_desc_f, CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, refl_hom, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, nullHomotopy'_hom
mkCoinductive 📖	CompOp	—
mkCoinductiveAux₁ 📖	CompOp	1 math math: mkCoinductiveAux₂_add_one
mkCoinductiveAux₂ 📖	CompOp	3 math math: mkCoinductiveAux₂_add_one, mkCoinductiveAux₂_zero, mkCoinductiveAux₃
mkInductive 📖	CompOp	—
mkInductiveAux₁ 📖	CompOp	1 math math: mkInductiveAux₂_add_one
mkInductiveAux₂ 📖	CompOp	3 math math: mkInductiveAux₃, mkInductiveAux₂_zero, mkInductiveAux₂_add_one
nullHomotopicMap 📖	CompOp	8 math math: nullHomotopicMap_comp, nullHomotopicMap_f_eq_zero, nullHomotopicMap_f, map_nullHomotopicMap, nullHomotopicMap_f_of_not_rel_right, comp_nullHomotopicMap, nullHomotopicMap_f_of_not_rel_left, nullHomotopy_hom
nullHomotopicMap' 📖	CompOp	9 math math: nullHomotopicMap'_f_eq_zero, map_nullHomotopicMap', nullHomotopicMap'_comp, comp_nullHomotopicMap', nullHomotopicMap'_f_of_not_rel_left, nullHomotopicMap'_f, nullHomotopicMap'_f_of_not_rel_right, CochainComplex.HomComplex.δ_neg_one_cochain, nullHomotopy'_hom
nullHomotopy 📖	CompOp	1 math math: nullHomotopy_hom
nullHomotopy' 📖	CompOp	1 math math: nullHomotopy'_hom
ofEq 📖	CompOp	7 math math: AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, HomologicalComplex.homotopyCofiber.eq_desc, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq, ofEq_hom, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CochainComplex.mappingCone.map_eq_mapOfHomotopy, CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq
refl 📖	CompOp	2 math math: CochainComplex.HomComplex.Cochain.ofHomotopy_refl, refl_hom
smul 📖	CompOp	1 math math: smul_hom
toShortComplex 📖	CompOp	—
trans 📖	CompOp	3 math math: HomologicalComplex.homotopyCofiber.eq_desc, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, trans_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_hom 📖	mathematical	—	hom Quiver.Hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.instAddHom add HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
comm 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike dNext hom prevD	—	—
compLeftId_hom 📖	mathematical	—	hom CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory compLeftId HomologicalComplex.X HomologicalComplex.Hom.f CategoryTheory.CategoryStruct.id	—	add_zero
compLeft_hom 📖	mathematical	—	hom CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory compLeft HomologicalComplex.X HomologicalComplex.Hom.f	—	—
compRightId_hom 📖	mathematical	—	hom CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory compRightId HomologicalComplex.X CategoryTheory.CategoryStruct.id HomologicalComplex.Hom.f	—	add_zero
compRight_hom 📖	mathematical	—	hom CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory compRight HomologicalComplex.X HomologicalComplex.Hom.f	—	—
comp_hom 📖	mathematical	—	hom CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f	—	—
comp_nullHomotopicMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory nullHomotopicMap HomologicalComplex.X HomologicalComplex.Hom.f	—	HomologicalComplex.hom_ext CategoryTheory.Preadditive.comp_add HomologicalComplex.Hom.comm_assoc CategoryTheory.Category.assoc
comp_nullHomotopicMap' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory nullHomotopicMap' HomologicalComplex.X HomologicalComplex.Hom.f	—	nullHomotopicMap'.eq_1 comp_nullHomotopicMap CategoryTheory.Limits.comp_zero
dNext_cochainComplex 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.next
dNext_succ_chainComplex 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd ChainComplex.next_nat_succ
dNext_zero_chainComplex 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.shape ChainComplex.next_nat_zero CategoryTheory.Limits.zero_comp
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext
homologyMap_eq 📖	mathematical	—	HomologicalComplex.homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.ShortComplex.Homotopy.homologyMap_congr
map_nullHomotopicMap 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive nullHomotopicMap CategoryTheory.Functor.obj HomologicalComplex.X	—	HomologicalComplex.hom_ext CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_add CategoryTheory.Functor.map_comp
map_nullHomotopicMap' 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive nullHomotopicMap' CategoryTheory.Functor.obj HomologicalComplex.X	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive nullHomotopicMap'.eq_1 map_nullHomotopicMap CategoryTheory.Functor.map_zero
mkCoinductiveAux₂_add_one 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	mkCoinductiveAux₂ HomologicalComplex.xPrev HomologicalComplex.xNext HomologicalComplex.dTo HomologicalComplex.dFrom mkCoinductiveAux₁ CategoryTheory.Iso.inv HomologicalComplex.xPrevIso CategoryTheory.Iso.hom HomologicalComplex.xNextIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkCoinductiveAux₂_zero 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	mkCoinductiveAux₂ HomologicalComplex.xPrev HomologicalComplex.xNext HomologicalComplex.dTo HomologicalComplex.dFrom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Iso.hom HomologicalComplex.xNextIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkCoinductiveAux₃ 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	HomologicalComplex.xNext CategoryTheory.Iso.inv HomologicalComplex.xNextIso HomologicalComplex.xPrev HomologicalComplex.dTo HomologicalComplex.dFrom mkCoinductiveAux₂ CategoryTheory.Iso.hom HomologicalComplex.xPrevIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
mkInductiveAux₂_add_one 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	mkInductiveAux₂ HomologicalComplex.xNext HomologicalComplex.xPrev HomologicalComplex.dFrom HomologicalComplex.dTo CategoryTheory.Iso.hom HomologicalComplex.xNextIso mkInductiveAux₁ CategoryTheory.Iso.inv HomologicalComplex.xPrevIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkInductiveAux₂_zero 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	mkInductiveAux₂ HomologicalComplex.xNext HomologicalComplex.xPrev HomologicalComplex.dFrom HomologicalComplex.dTo CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Iso.inv HomologicalComplex.xPrevIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkInductiveAux₃ 📖	mathematical	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	HomologicalComplex.xPrev HomologicalComplex.xNext HomologicalComplex.dFrom HomologicalComplex.dTo mkInductiveAux₂ CategoryTheory.Iso.hom HomologicalComplex.xPrevIso CategoryTheory.Iso.inv HomologicalComplex.xNextIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc
nullHomotopicMap'_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory nullHomotopicMap' HomologicalComplex.X HomologicalComplex.Hom.f	—	nullHomotopicMap'.eq_1 nullHomotopicMap_comp CategoryTheory.Limits.zero_comp
nullHomotopicMap'_f 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	nullHomotopicMap_f
nullHomotopicMap'_f_eq_zero 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	nullHomotopicMap_f_eq_zero
nullHomotopicMap'_f_of_not_rel_left 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d	—	nullHomotopicMap_f_of_not_rel_left
nullHomotopicMap'_f_of_not_rel_right 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d	—	nullHomotopicMap_f_of_not_rel_right
nullHomotopicMap_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory nullHomotopicMap HomologicalComplex.X HomologicalComplex.Hom.f	—	HomologicalComplex.hom_ext CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc HomologicalComplex.Hom.comm
nullHomotopicMap_f 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	dNext_eq prevD_eq
nullHomotopicMap_f_eq_zero 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.shape CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero add_zero
nullHomotopicMap_f_of_not_rel_left 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d	—	prevD_eq dNext.eq_1 AddMonoidHom.mk'_apply HomologicalComplex.shape CategoryTheory.Limits.zero_comp zero_add
nullHomotopicMap_f_of_not_rel_right 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopicMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d	—	dNext_eq prevD.eq_1 AddMonoidHom.mk'_apply HomologicalComplex.shape CategoryTheory.Limits.comp_zero add_zero
nullHomotopy'_hom 📖	mathematical	—	hom nullHomotopicMap' Quiver.Hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.instZeroHom_1 nullHomotopy' HomologicalComplex.X ComplexShape.Rel CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
nullHomotopy_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	hom nullHomotopicMap HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instZeroHom_1 nullHomotopy	—	—
ofEq_hom 📖	mathematical	—	hom ofEq Pi.instZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
prevD_chainComplex 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd ChainComplex.prev
prevD_succ_cochainComplex 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.prev_nat_succ
prevD_zero_cochainComplex 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.shape CochainComplex.prev_nat_zero CategoryTheory.Limits.comp_zero
refl_hom 📖	mathematical	—	hom refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
smul_hom 📖	mathematical	—	hom Quiver.Hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.instSMulHom smul HomologicalComplex.X SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	—
symm_hom 📖	mathematical	—	hom symm Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
trans_hom 📖	mathematical	—	hom trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
zero 📖	mathematical	ComplexShape.Rel	hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—

HomotopyEquiv

Definitions

Name	Category	Theorems
hom 📖	CompOp	23 math math: CochainComplex.mappingConeCompTriangleh_comm₁_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, HomotopyCategory.isoOfHomotopyEquiv_hom, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, Rep.standardComplex.εToSingle₀_comp_eq, quasiIso_hom, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, quasiIsoAt_hom, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.Functor.mapHomotopyEquiv_hom, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc
homotopyHomInvId 📖	CompOp	2 math math: CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId
homotopyInvHomId 📖	CompOp	2 math math: CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId
instInhabited 📖	CompOp	—
inv 📖	CompOp	15 math math: CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, CategoryTheory.Functor.mapHomotopyEquiv_inv, CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, quasiIsoAt_inv, quasiIso_inv, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, HomotopyCategory.isoOfHomotopyEquiv_inv, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc
ofIso 📖	CompOp	—
refl 📖	CompOp	—
toHomologyIso 📖	CompOp	—
trans 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
HomotopyEquiv 📖	CompData	—
dNext 📖	CompOp	10 math math: Homotopy.dNext_zero_chainComplex, dNext_comp_left, Homotopy.dNext_succ_chainComplex, dNext_eq_dFrom_fromNext, Homotopy.comm, dNext_eq, Homotopy.dNext_cochainComplex, dNext_comp_right, dNext_nat, dNext_eq_zero
fromNext 📖	CompOp	1 math math: dNext_eq_dFrom_fromNext
prevD 📖	CompOp	10 math math: prevD_comp_left, Homotopy.prevD_succ_cochainComplex, prevD_eq_toPrev_dTo, Homotopy.prevD_chainComplex, prevD_nat, prevD_eq, prevD_eq_zero, Homotopy.prevD_zero_cochainComplex, Homotopy.comm, prevD_comp_right
toPrev 📖	CompOp	1 math math: prevD_eq_toPrev_dTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dNext_comp_left 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f	—	HomologicalComplex.Hom.comm_assoc
dNext_comp_right 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f	—	CategoryTheory.Category.assoc
dNext_eq 📖	mathematical	ComplexShape.Rel	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	ComplexShape.next_eq'
dNext_eq_dFrom_fromNext 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.xNext HomologicalComplex.dFrom fromNext	—	—
dNext_eq_zero 📖	mathematical	ComplexShape.Rel ComplexShape.next	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.shape CategoryTheory.Limits.zero_comp
dNext_nat 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike dNext CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.shape ChainComplex.next_nat_zero CategoryTheory.Limits.zero_comp ChainComplex.next_nat_succ add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
prevD_comp_left 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f	—	CategoryTheory.Category.assoc
prevD_comp_right 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f	—	CategoryTheory.Category.assoc HomologicalComplex.Hom.comm
prevD_eq 📖	mathematical	ComplexShape.Rel	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	ComplexShape.prev_eq'
prevD_eq_toPrev_dTo 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.xPrev toPrev HomologicalComplex.dTo	—	—
prevD_eq_zero 📖	mathematical	ComplexShape.Rel ComplexShape.prev	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.shape CategoryTheory.Limits.comp_zero
prevD_nat 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike prevD CategoryTheory.CategoryStruct.comp HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.shape CochainComplex.prev_nat_zero CategoryTheory.Limits.comp_zero CochainComplex.prev_nat_succ add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid

---

← Back to Index