DifferentialObject

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

Statistics

Metric	Count
Definitions objEqToHom, dgoEquivHomologicalComplex, dgoEquivHomologicalComplexCounitIso, dgoEquivHomologicalComplexUnitIso, dgoToHomologicalComplex, homologicalComplexToDGO	6
Theorems d_squared_apply, d_squared_apply_assoc, eqToHom_f', eqToHom_f'_assoc, objEqToHom_d, objEqToHom_d_assoc, objEqToHom_refl, d_eqToHom, d_eqToHom_assoc, dgoEquivHomologicalComplexCounitIso_hom_app_f, dgoEquivHomologicalComplexCounitIso_inv_app_f, dgoEquivHomologicalComplexUnitIso_hom_app_f, dgoEquivHomologicalComplexUnitIso_inv_app_f, dgoEquivHomologicalComplex_counitIso, dgoEquivHomologicalComplex_functor, dgoEquivHomologicalComplex_inverse, dgoEquivHomologicalComplex_unitIso, dgoToHomologicalComplex_map_f, dgoToHomologicalComplex_obj_X, dgoToHomologicalComplex_obj_d, homologicalComplexToDGO_map_f, homologicalComplexToDGO_obj_d, homologicalComplexToDGO_obj_obj	23
Total	29

CategoryTheory.DifferentialObject

Definitions

Name	Category	Theorems
objEqToHom 📖	CompOp	7 math math: HomologicalComplex.dgoToHomologicalComplex_obj_d, objEqToHom_d, eqToHom_f', objEqToHom_refl, HomologicalComplex.dgoToHomologicalComplex_map_f, eqToHom_f'_assoc, objEqToHom_d_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_squared_apply 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	d_squared
d_squared_apply_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_squared_apply
eqToHom_f' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift objEqToHom Hom.f	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
eqToHom_f'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift objEqToHom Hom.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_f'
objEqToHom_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne objEqToHom d	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
objEqToHom_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift objEqToHom CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' objEqToHom_d
objEqToHom_refl 📖	mathematical	—	objEqToHom refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift	—	refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv

HomologicalComplex

Definitions

Name	Category	Theorems
dgoEquivHomologicalComplex 📖	CompOp	4 math math: dgoEquivHomologicalComplex_unitIso, dgoEquivHomologicalComplex_functor, dgoEquivHomologicalComplex_counitIso, dgoEquivHomologicalComplex_inverse
dgoEquivHomologicalComplexCounitIso 📖	CompOp	3 math math: dgoEquivHomologicalComplex_counitIso, dgoEquivHomologicalComplexCounitIso_hom_app_f, dgoEquivHomologicalComplexCounitIso_inv_app_f
dgoEquivHomologicalComplexUnitIso 📖	CompOp	3 math math: dgoEquivHomologicalComplex_unitIso, dgoEquivHomologicalComplexUnitIso_hom_app_f, dgoEquivHomologicalComplexUnitIso_inv_app_f
dgoToHomologicalComplex 📖	CompOp	8 math math: dgoToHomologicalComplex_obj_d, dgoEquivHomologicalComplexUnitIso_hom_app_f, dgoEquivHomologicalComplex_functor, dgoToHomologicalComplex_obj_X, dgoToHomologicalComplex_map_f, dgoEquivHomologicalComplexCounitIso_hom_app_f, dgoEquivHomologicalComplexUnitIso_inv_app_f, dgoEquivHomologicalComplexCounitIso_inv_app_f
homologicalComplexToDGO 📖	CompOp	8 math math: dgoEquivHomologicalComplexUnitIso_hom_app_f, homologicalComplexToDGO_map_f, dgoEquivHomologicalComplexCounitIso_hom_app_f, homologicalComplexToDGO_obj_d, homologicalComplexToDGO_obj_obj, dgoEquivHomologicalComplex_inverse, dgoEquivHomologicalComplexUnitIso_inv_app_f, dgoEquivHomologicalComplexCounitIso_inv_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_eqToHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup d CategoryTheory.eqToHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
d_eqToHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup d CategoryTheory.eqToHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_eqToHom
dgoEquivHomologicalComplexCounitIso_hom_app_f 📖	mathematical	—	Hom.f ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.comp CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.DifferentialObject.categoryOfDifferentialObjects homologicalComplexToDGO dgoToHomologicalComplex CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup CategoryTheory.Functor.category dgoEquivHomologicalComplexCounitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplexCounitIso_inv_app_f 📖	mathematical	—	Hom.f ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.DifferentialObject.categoryOfDifferentialObjects homologicalComplexToDGO dgoToHomologicalComplex CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup CategoryTheory.Functor.category dgoEquivHomologicalComplexCounitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplexUnitIso_hom_app_f 📖	mathematical	—	CategoryTheory.DifferentialObject.Hom.f AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects CategoryTheory.Functor.id CategoryTheory.Functor.comp HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instCategory dgoToHomologicalComplex homologicalComplexToDGO CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup dgoEquivHomologicalComplexUnitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplexUnitIso_inv_app_f 📖	mathematical	—	CategoryTheory.DifferentialObject.Hom.f AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects CategoryTheory.Functor.comp HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instCategory dgoToHomologicalComplex homologicalComplexToDGO CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup dgoEquivHomologicalComplexUnitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplex_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup CategoryTheory.DifferentialObject.categoryOfDifferentialObjects instCategory dgoEquivHomologicalComplex dgoEquivHomologicalComplexCounitIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplex_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup CategoryTheory.DifferentialObject.categoryOfDifferentialObjects instCategory dgoEquivHomologicalComplex dgoToHomologicalComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplex_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup CategoryTheory.DifferentialObject.categoryOfDifferentialObjects instCategory dgoEquivHomologicalComplex homologicalComplexToDGO	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoEquivHomologicalComplex_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup CategoryTheory.DifferentialObject.categoryOfDifferentialObjects instCategory dgoEquivHomologicalComplex dgoEquivHomologicalComplexUnitIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoToHomologicalComplex_map_f 📖	mathematical	—	Hom.f ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.DifferentialObject.obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne CategoryTheory.DifferentialObject.d CategoryTheory.DifferentialObject.objEqToHom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.map CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup instCategory dgoToHomologicalComplex CategoryTheory.DifferentialObject.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoToHomologicalComplex_obj_X 📖	mathematical	—	X ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.DifferentialObject.categoryOfDifferentialObjects HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup instCategory dgoToHomologicalComplex CategoryTheory.DifferentialObject.obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
dgoToHomologicalComplex_obj_d 📖	mathematical	—	d ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj CategoryTheory.DifferentialObject AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.DifferentialObject.categoryOfDifferentialObjects HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup instCategory dgoToHomologicalComplex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj CategoryTheory.CategoryStruct.comp CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne CategoryTheory.DifferentialObject.d CategoryTheory.DifferentialObject.objEqToHom CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
homologicalComplexToDGO_map_f 📖	mathematical	—	CategoryTheory.DifferentialObject.Hom.f AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift X ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid d CategoryTheory.Functor.map HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup instCategory CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects homologicalComplexToDGO Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
homologicalComplexToDGO_obj_d 📖	mathematical	—	CategoryTheory.DifferentialObject.d AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup instCategory CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects homologicalComplexToDGO d	—	AddRightCancelSemigroup.toIsRightCancelAdd
homologicalComplexToDGO_obj_obj 📖	mathematical	—	CategoryTheory.DifferentialObject.obj AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.GradedObjectWithShift CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.hasZeroMorphisms CategoryTheory.GradedObject.hasShift CategoryTheory.Functor.obj HomologicalComplex ComplexShape.up' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddCommGroup.toAddGroup instCategory CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects homologicalComplexToDGO X	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index