Documentation Verification Report

HomComplexCohomology

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

Statistics

Metric	Count
Definitions `CohomologyClass`, `descAddMonoidHom`, `homAddEquiv`, `mk`, `mkAddMonoidHom`, `toHom`, `coboundaries`, `homologyAddEquiv`, `instAddCommGroupCohomologyClass`, `leftHomologyData`, `leftHomologyData'`	11
Theorems `descAddMonoidHom_cohomologyClass`, `homAddEquiv_apply`, `mkAddMonoidHom_apply`, `mk_add`, `mk_eq_zero_iff`, `mk_neg`, `mk_sub`, `mk_surjective`, `mk_zero`, `toHom_bijective`, `toHom_mk`, `toHom_mk_eq_zero_iff`, `leftHomologyData'_H_coe`, `leftHomologyData'_K_coe`, `leftHomologyData'_i`, `leftHomologyData'_π`, `leftHomologyData_H_coe`, `leftHomologyData_K_coe`, `leftHomologyData_i_hom_apply`, `leftHomologyData_π_hom_apply`, `mem_coboundaries_iff`	21
Total	32

CochainComplex.HomComplex

Definitions

Name	Category	Theorems
`CohomologyClass` 📖	CompOp	46 math math: `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add`, `CohomologyClass.equivOfIsKInjective_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub`, `CohomologyClass.mk_surjective`, `CohomologyClass.mk_eq_zero_iff`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub`, `leftHomologyData_π_hom_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom`, `CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective`, `CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg`, `CohomologyClass.equivOfIsKInjective_symm_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero`, `CohomologyClass.mk_zero`, `CohomologyClass.toHom_bijective`, `CohomologyClass.mkAddMonoidHom_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg`, `leftHomologyData_H_coe`, `CohomologyClass.descAddMonoidHom_cohomologyClass`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk`, `CohomologyClass.equivOfIsKProjective_symm_apply`, `leftHomologyData'_H_coe`, `leftHomologyData'_π`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add`, `CohomologyClass.mk_add`, `CohomologyClass.toHom_mk_eq_zero_iff`, `CohomologyClass.mk_sub`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk`, `CohomologyClass.equivOfIsKProjective_apply`, `CohomologyClass.mk_neg`, `CohomologyClass.toHom_mk`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `CohomologyClass.homAddEquiv_apply`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg`
`coboundaries` 📖	CompOp	5 math math: `CohomologyClass.mk_eq_zero_iff`, `Cocycle.toSingleMk_mem_coboundaries_iff`, `mem_coboundaries_iff`, `CohomologyClass.toHom_mk_eq_zero_iff`, `Cocycle.fromSingleMk_mem_coboundaries_iff`
`homologyAddEquiv` 📖	CompOp	—
`instAddCommGroupCohomologyClass` 📖	CompOp	33 math math: `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub`, `CohomologyClass.mk_eq_zero_iff`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub`, `leftHomologyData_π_hom_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero`, `CohomologyClass.mk_zero`, `CohomologyClass.toHom_bijective`, `CohomologyClass.mkAddMonoidHom_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg`, `CohomologyClass.descAddMonoidHom_cohomologyClass`, `leftHomologyData'_π`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add`, `CohomologyClass.mk_add`, `CohomologyClass.toHom_mk_eq_zero_iff`, `CohomologyClass.mk_sub`, `CohomologyClass.mk_neg`, `CohomologyClass.toHom_mk`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `CohomologyClass.homAddEquiv_apply`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg`
`leftHomologyData` 📖	CompOp	4 math math: `leftHomologyData_K_coe`, `leftHomologyData_π_hom_apply`, `leftHomologyData_i_hom_apply`, `leftHomologyData_H_coe`
`leftHomologyData'` 📖	CompOp	4 math math: `leftHomologyData'_i`, `leftHomologyData'_K_coe`, `leftHomologyData'_H_coe`, `leftHomologyData'_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftHomologyData'_H_coe` 📖	mathematical	—	`AddCommGrpCat.carrier` `CategoryTheory.ShortComplex.LeftHomologyData.H` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc'` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData'` `CohomologyClass`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData'_K_coe` 📖	mathematical	—	`AddCommGrpCat.carrier` `CategoryTheory.ShortComplex.LeftHomologyData.K` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc'` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData'` `Cocycle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData'_i` 📖	mathematical	—	`CategoryTheory.ShortComplex.LeftHomologyData.i` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc'` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData'` `AddCommGrpCat.ofHom` `Cocycle` `Cochain` `instAddCommGroupCocycle` `instAddCommGroupCochain` `Cocycle.toCochainAddMonoidHom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData'_π` 📖	mathematical	—	`CategoryTheory.ShortComplex.LeftHomologyData.π` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc'` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData'` `AddCommGrpCat.ofHom` `Cocycle` `CohomologyClass` `instAddCommGroupCocycle` `instAddCommGroupCohomologyClass` `CohomologyClass.mkAddMonoidHom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData_H_coe` 📖	mathematical	—	`AddCommGrpCat.carrier` `CategoryTheory.ShortComplex.LeftHomologyData.H` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData` `CohomologyClass`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData_K_coe` 📖	mathematical	—	`AddCommGrpCat.carrier` `CategoryTheory.ShortComplex.LeftHomologyData.K` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData` `Cocycle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData_i_hom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Cocycle` `Cochain` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupCocycle` `instAddCommGroupCochain` `AddMonoidHom.instFunLike` `AddCommGrpCat.Hom.hom` `AddCommGrpCat.of` `CategoryTheory.ShortComplex.LeftHomologyData.i` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `cocycle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`leftHomologyData_π_hom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Cocycle` `CohomologyClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroupCocycle` `instAddCommGroupCohomologyClass` `AddMonoidHom.instFunLike` `AddCommGrpCat.Hom.hom` `AddCommGrpCat.of` `CategoryTheory.ShortComplex.LeftHomologyData.π` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddCommGrpCat.instPreadditive` `HomologicalComplex.sc` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.HomComplex` `leftHomologyData`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mem_coboundaries_iff` 📖	mathematical	—	`Cocycle` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupCocycle` `SetLike.instMembership` `AddSubgroup.instSetLike` `coboundaries` `δ` `Cochain` `instAddCommGroupCochain` `cocycle`	—	—

CochainComplex.HomComplex.CohomologyClass

Definitions

Name	Category	Theorems
`descAddMonoidHom` 📖	CompOp	1 math math: `descAddMonoidHom_cohomologyClass`
`homAddEquiv` 📖	CompOp	1 math math: `homAddEquiv_apply`
`mk` 📖	CompOp	—
`mkAddMonoidHom` 📖	CompOp	2 math math: `mkAddMonoidHom_apply`, `CochainComplex.HomComplex.leftHomologyData'_π`
`toHom` 📖	CompOp	4 math math: `toHom_bijective`, `toHom_mk_eq_zero_iff`, `toHom_mk`, `homAddEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`descAddMonoidHom_cohomologyClass` 📖	mathematical	`AddSubgroup` `CochainComplex.HomComplex.Cocycle` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCocycle` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `CochainComplex.HomComplex.coboundaries` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`DFunLike.coe` `AddMonoidHom` `CochainComplex.HomComplex.CohomologyClass` `AddZeroClass.toAddZero` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `AddMonoidHom.instFunLike` `descAddMonoidHom`	—	—
`homAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `CochainComplex.HomComplex.CohomologyClass` `Quiver.Hom` `HomotopyCategory` `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.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `CategoryTheory.Preadditive.homGroup` `HomotopyCategory.instPreadditive` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `homAddEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `toHom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mkAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `CochainComplex.HomComplex.Cocycle` `CochainComplex.HomComplex.CohomologyClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCocycle` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `AddMonoidHom.instFunLike` `mkAddMonoidHom`	—	—
`mk_add` 📖	mathematical	—	`CochainComplex.HomComplex.Cocycle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CochainComplex.HomComplex.instAddCommGroupCocycle` `CochainComplex.HomComplex.CohomologyClass` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass`	—	—
`mk_eq_zero_iff` 📖	mathematical	—	`CochainComplex.HomComplex.CohomologyClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `CochainComplex.HomComplex.Cocycle` `AddSubgroup` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCocycle` `SetLike.instMembership` `AddSubgroup.instSetLike` `CochainComplex.HomComplex.coboundaries`	—	`QuotientAddGroup.eq_zero_iff` `AddSubgroup.normal_of_comm`
`mk_neg` 📖	mathematical	—	`CochainComplex.HomComplex.Cocycle` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CochainComplex.HomComplex.instAddCommGroupCocycle` `CochainComplex.HomComplex.CohomologyClass` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass`	—	—
`mk_sub` 📖	mathematical	—	`CochainComplex.HomComplex.Cocycle` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCocycle` `CochainComplex.HomComplex.CohomologyClass` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass`	—	—
`mk_surjective` 📖	mathematical	—	`CochainComplex.HomComplex.Cocycle` `CochainComplex.HomComplex.CohomologyClass`	—	`Quotient.mk_surjective`
`mk_zero` 📖	mathematical	—	`CochainComplex.HomComplex.Cocycle` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CochainComplex.HomComplex.instAddCommGroupCocycle` `CochainComplex.HomComplex.CohomologyClass` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass`	—	—
`toHom_bijective` 📖	mathematical	—	`Function.Bijective` `CochainComplex.HomComplex.CohomologyClass` `Quiver.Hom` `HomotopyCategory` `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.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `CategoryTheory.Preadditive.homGroup` `HomotopyCategory.instPreadditive` `AddMonoidHom.instFunLike` `toHom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `mk_surjective` `sub_eq_zero` `mk_sub` `mk_eq_zero_iff` `toHom_mk_eq_zero_iff` `map_sub` `AddMonoidHom.instAddMonoidHomClass` `sub_self` `CategoryTheory.Functor.map_surjective` `HomotopyCategory.instFullHomologicalComplexQuotient` `AddEquiv.symm_apply_apply`
`toHom_mk` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `CochainComplex.HomComplex.CohomologyClass` `Quiver.Hom` `HomotopyCategory` `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.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `CategoryTheory.Preadditive.homGroup` `HomotopyCategory.instPreadditive` `AddMonoidHom.instFunLike` `toHom` `CategoryTheory.Functor.map` `CochainComplex` `AddEquiv` `CochainComplex.HomComplex.Cocycle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CochainComplex.HomComplex.instAddCommGroupCocycle` `HomologicalComplex.instAddHom` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `CochainComplex.HomComplex.Cocycle.equivHomShift`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`toHom_mk_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `CochainComplex.HomComplex.CohomologyClass` `Quiver.Hom` `HomotopyCategory` `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.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCohomologyClass` `CategoryTheory.Preadditive.homGroup` `HomotopyCategory.instPreadditive` `AddMonoidHom.instFunLike` `toHom` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CochainComplex.HomComplex.Cocycle` `AddSubgroup` `CochainComplex.HomComplex.instAddCommGroupCocycle` `SetLike.instMembership` `AddSubgroup.instSetLike` `CochainComplex.HomComplex.coboundaries`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomotopyCategory.quotient_map_eq_zero_iff` `sub_add_cancel` `CochainComplex.HomComplex.δ_units_smul` `zero_add` `CochainComplex.HomComplex.Cochain.δ_rightUnshift` `CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe` `CochainComplex.HomComplex.Cochain.ofHom_zero` `add_zero` `CochainComplex.HomComplex.Cochain.rightUnshift_rightShift` `smul_smul` `Int.units_mul_self` `one_smul` `mk_eq_zero_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`

---

← Back to Index