HomComplexSingle

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

Statistics

Metric	Count
Definitions fromSingleEquiv, fromSingleMk, toSingleEquiv, toSingleMk, fromSingleMk, toSingleMk	6
Theorems fromSingleEquiv_fromSingleMk, fromSingleMk_add, fromSingleMk_neg, fromSingleMk_postcomp, fromSingleMk_precomp, fromSingleMk_sub, fromSingleMk_surjective, fromSingleMk_v, fromSingleMk_v_eq_zero, fromSingleMk_zero, toSingleEquiv_toSingleMk, toSingleMk_add, toSingleMk_neg, toSingleMk_postcomp, toSingleMk_precomp, toSingleMk_sub, toSingleMk_surjective, toSingleMk_v, toSingleMk_v_eq_zero, toSingleMk_zero, δ_fromSingleMk, δ_toSingleMk, fromSingleMk_add, fromSingleMk_coe, fromSingleMk_mem_coboundaries_iff, fromSingleMk_neg, fromSingleMk_postcomp, fromSingleMk_precomp, fromSingleMk_sub, fromSingleMk_surjective, fromSingleMk_zero, toSingleMk_add, toSingleMk_coe, toSingleMk_mem_coboundaries_iff, toSingleMk_neg, toSingleMk_postcomp, toSingleMk_precomp, toSingleMk_sub, toSingleMk_surjective, toSingleMk_zero	40
Total	46

CochainComplex.HomComplex.Cochain

Definitions

Name	Category	Theorems
fromSingleEquiv 📖	CompOp	1 math math: fromSingleEquiv_fromSingleMk
fromSingleMk 📖	CompOp	12 math math: fromSingleMk_neg, fromSingleEquiv_fromSingleMk, δ_fromSingleMk, fromSingleMk_postcomp, fromSingleMk_v, fromSingleMk_add, fromSingleMk_zero, CochainComplex.HomComplex.Cocycle.fromSingleMk_coe, fromSingleMk_surjective, fromSingleMk_precomp, fromSingleMk_sub, fromSingleMk_v_eq_zero
toSingleEquiv 📖	CompOp	1 math math: toSingleEquiv_toSingleMk
toSingleMk 📖	CompOp	12 math math: toSingleMk_neg, toSingleMk_v, toSingleMk_add, toSingleMk_v_eq_zero, CochainComplex.HomComplex.Cocycle.toSingleMk_coe, toSingleMk_surjective, δ_toSingleMk, toSingleMk_zero, toSingleMk_postcomp, toSingleEquiv_toSingleMk, toSingleMk_sub, toSingleMk_precomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSingleEquiv_fromSingleMk 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Preadditive.homGroup EquivLike.toFunLike AddEquiv.instEquivLike fromSingleEquiv fromSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd fromSingleMk_v CategoryTheory.Iso.inv_hom_id_assoc
fromSingleMk_add 📖	mathematical	—	fromSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_add
fromSingleMk_neg 📖	mathematical	—	fromSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_neg
fromSingleMk_postcomp 📖	mathematical	—	fromSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.Hom.f comp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective add_zero fromSingleMk_v CategoryTheory.Iso.inv_hom_id_assoc comp_zero_cochain_v ofHom_v CategoryTheory.Category.assoc
fromSingleMk_precomp 📖	mathematical	—	fromSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing comp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor ofHom CategoryTheory.Functor.map zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective zero_add fromSingleMk_v CategoryTheory.Iso.inv_hom_id_assoc add_zero zero_cochain_comp_v ofHom_v HomologicalComplex.single_map_f_self CategoryTheory.Category.assoc
fromSingleMk_sub 📖	mathematical	—	fromSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_sub
fromSingleMk_surjective 📖	mathematical	—	fromSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.surjective
fromSingleMk_v 📖	mathematical	—	v CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor fromSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.single CategoryTheory.Iso.hom HomologicalComplex.singleObjXSelf	—	AddRightCancelSemigroup.toIsRightCancelAdd single_v
fromSingleMk_v_eq_zero 📖	mathematical	—	v CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor fromSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd single_v_eq_zero
fromSingleMk_zero 📖	mathematical	—	fromSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Limits.HasZeroMorphisms.zero CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.comp_zero single_zero
toSingleEquiv_toSingleMk 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Preadditive.homGroup EquivLike.toFunLike AddEquiv.instEquivLike toSingleEquiv toSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd toSingleMk_v CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
toSingleMk_add 📖	mathematical	—	toSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_add
toSingleMk_neg 📖	mathematical	—	toSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_neg
toSingleMk_postcomp 📖	mathematical	—	toSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing comp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor ofHom CategoryTheory.Functor.map add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective add_zero toSingleMk_v CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id comp_zero_cochain_v ofHom_v HomologicalComplex.single_map_f_self CategoryTheory.Iso.inv_hom_id_assoc
toSingleMk_precomp 📖	mathematical	—	toSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.Hom.f comp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor ofHom zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective zero_add toSingleMk_v CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id add_zero zero_cochain_comp_v ofHom_v
toSingleMk_sub 📖	mathematical	—	toSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_sub
toSingleMk_surjective 📖	mathematical	—	toSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.surjective
toSingleMk_v 📖	mathematical	—	v CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor toSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.single CategoryTheory.Iso.inv HomologicalComplex.singleObjXSelf	—	AddRightCancelSemigroup.toIsRightCancelAdd single_v
toSingleMk_v_eq_zero 📖	mathematical	—	v CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor toSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd single_v_eq_zero
toSingleMk_zero 📖	mathematical	—	toSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Limits.HasZeroMorphisms.zero CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.zero_comp single_zero
δ_fromSingleMk 📖	mathematical	—	CochainComplex.HomComplex.δ CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor fromSingleMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd δ_single CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp single_zero smul_zero add_zero CochainComplex.HomComplex.δ_shape HomologicalComplex.shape CategoryTheory.Limits.comp_zero
δ_toSingleMk 📖	mathematical	—	CochainComplex.HomComplex.δ CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor toSingleMk Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd δ_single CategoryTheory.Limits.comp_zero single_zero zero_add CategoryTheory.Category.assoc CochainComplex.HomComplex.δ_shape HomologicalComplex.shape CategoryTheory.Limits.zero_comp toSingleMk_zero smul_zero

CochainComplex.HomComplex.Cocycle

Definitions

Name	Category	Theorems
fromSingleMk 📖	CompOp	11 math math: fromSingleMk_add, fromSingleMk_surjective, fromSingleMk_coe, fromSingleMk_neg, fromSingleMk_zero, CategoryTheory.InjectiveResolution.extMk_hom, fromSingleMk_sub, fromSingleMk_precomp, fromSingleMk_mem_coboundaries_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, fromSingleMk_postcomp
toSingleMk 📖	CompOp	11 math math: toSingleMk_surjective, toSingleMk_add, toSingleMk_mem_coboundaries_iff, CategoryTheory.ProjectiveResolution.extMk_hom, toSingleMk_zero, toSingleMk_coe, toSingleMk_sub, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, toSingleMk_neg, toSingleMk_postcomp, toSingleMk_precomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSingleMk_add 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	fromSingleMk AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.fromSingleMk_add
fromSingleMk_coe 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fromSingleMk CochainComplex.HomComplex.Cochain.fromSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd
fromSingleMk_mem_coboundaries_iff 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCocycle SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.coboundaries fromSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.mem_coboundaries_iff sub_add_cancel CochainComplex.HomComplex.Cochain.fromSingleMk_surjective AddEquiv.injective CochainComplex.HomComplex.Cochain.δ_fromSingleMk fromSingleMk_coe
fromSingleMk_neg 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	fromSingleMk NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.fromSingleMk_neg
fromSingleMk_postcomp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	fromSingleMk HomologicalComplex.Hom.f postcomp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd ext AddEquiv.injective add_zero CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp
fromSingleMk_precomp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	fromSingleMk precomp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd ext AddEquiv.injective zero_add CochainComplex.HomComplex.Cochain.fromSingleMk_precomp
fromSingleMk_sub 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	fromSingleMk SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.fromSingleMk_sub
fromSingleMk_surjective 📖	mathematical	—	fromSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.fromSingleMk_surjective δ_eq_zero CochainComplex.HomComplex.Cochain.congr_v CochainComplex.HomComplex.Cochain.δ_fromSingleMk CochainComplex.HomComplex.Cochain.fromSingleMk_v CategoryTheory.Iso.isIso_hom ext
fromSingleMk_zero 📖	mathematical	—	fromSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Limits.HasZeroMorphisms.zero CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.fromSingleMk_zero
toSingleMk_add 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	toSingleMk AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.toSingleMk_add
toSingleMk_coe 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle toSingleMk CochainComplex.HomComplex.Cochain.toSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd
toSingleMk_mem_coboundaries_iff 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCocycle SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.coboundaries toSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.mem_coboundaries_iff sub_add_cancel CochainComplex.HomComplex.Cochain.toSingleMk_surjective AddEquiv.injective CategoryTheory.Linear.comp_units_smul map_zsmul_unit AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass CochainComplex.HomComplex.Cochain.δ_toSingleMk toSingleMk_coe CochainComplex.HomComplex.δ_units_smul smul_smul Int.units_mul_self one_smul
toSingleMk_neg 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	toSingleMk NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.toSingleMk_neg
toSingleMk_postcomp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	toSingleMk postcomp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd ext AddEquiv.injective add_zero CochainComplex.HomComplex.Cochain.toSingleMk_postcomp
toSingleMk_precomp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	toSingleMk HomologicalComplex.Hom.f precomp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd ext AddEquiv.injective zero_add CochainComplex.HomComplex.Cochain.toSingleMk_precomp
toSingleMk_sub 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	toSingleMk SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.toSingleMk_sub
toSingleMk_surjective 📖	mathematical	—	toSingleMk	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.toSingleMk_surjective δ_eq_zero CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cochain.toSingleMk_v CochainComplex.HomComplex.Cochain.congr_v one_smul Int.units_mul_self smul_smul CochainComplex.HomComplex.Cochain.δ_toSingleMk CochainComplex.HomComplex.δ_units_smul coe_units_smul ext
toSingleMk_zero 📖	mathematical	—	toSingleMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Limits.HasZeroMorphisms.zero CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.toSingleMk_zero

---

← Back to Index