DifferentialObject

📁 Source: Mathlib/CategoryTheory/DifferentialObject.lean

Statistics

Metric	Count
Definitions DifferentialObject, comp, f, id, HomSubtype, categoryOfDifferentialObjects, concreteCategoryOfDifferentialObjects, d, forget, hasZeroMorphisms, instFunLikeHomSubtypeObj, instHasForget₂HomSubtypeObj, instHasShift, instZeroHom, isoApp, mkIso, obj, shiftFunctor, shiftFunctorAdd, shiftZero, mapDifferentialObject	21
Theorems comm, comm_assoc, comp_f, ext, ext_iff, id_f, comp_f, d_squared, d_squared_assoc, eqToHom_f, ext, ext_iff, forget_faithful, hasZeroObject, id_f, isoApp_hom, isoApp_inv, isoApp_refl, isoApp_symm, isoApp_trans, mkIso_hom_f, mkIso_inv_f, shiftFunctorAdd_hom_app_f, shiftFunctorAdd_inv_app_f, shiftFunctor_map_f, shiftFunctor_obj_d, shiftFunctor_obj_obj, shiftZero_hom_app_f, shiftZero_inv_app_f, zero_f, mapDifferentialObject_map_f, mapDifferentialObject_obj_d, mapDifferentialObject_obj_obj	33
Total	54

CategoryTheory

Definitions

Name	Category	Theorems
DifferentialObject 📖	CompData	37 math math: DifferentialObject.shiftFunctor_obj_d, DifferentialObject.shiftFunctor_obj_obj, DifferentialObject.shiftZero_hom_app_f, HomologicalComplex.dgoToHomologicalComplex_obj_d, DifferentialObject.eqToHom_f, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, DifferentialObject.hasZeroObject, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, DifferentialObject.mkIso_hom_f, DifferentialObject.forget_faithful, HomologicalComplex.dgoEquivHomologicalComplex_functor, DifferentialObject.comp_f, DifferentialObject.isoApp_refl, HomologicalComplex.dgoToHomologicalComplex_obj_X, DifferentialObject.shiftZero_inv_app_f, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, DifferentialObject.shiftFunctorAdd_hom_app_f, DifferentialObject.id_f, HomologicalComplex.homologicalComplexToDGO_map_f, DifferentialObject.shiftFunctor_map_f, HomologicalComplex.dgoToHomologicalComplex_map_f, DifferentialObject.shiftFunctorAdd_inv_app_f, Functor.mapDifferentialObject_obj_d, DifferentialObject.isoApp_trans, DifferentialObject.isoApp_hom, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, DifferentialObject.isoApp_symm, DifferentialObject.isoApp_inv, DifferentialObject.mkIso_inv_f, Functor.mapDifferentialObject_obj_obj, HomologicalComplex.homologicalComplexToDGO_obj_d, HomologicalComplex.homologicalComplexToDGO_obj_obj, HomologicalComplex.dgoEquivHomologicalComplex_inverse, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, Functor.mapDifferentialObject_map_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, DifferentialObject.zero_f

CategoryTheory.DifferentialObject

Definitions

Name	Category	Theorems
HomSubtype 📖	CompOp	—
categoryOfDifferentialObjects 📖	CompOp	37 math math: shiftFunctor_obj_d, shiftFunctor_obj_obj, shiftZero_hom_app_f, HomologicalComplex.dgoToHomologicalComplex_obj_d, eqToHom_f, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, hasZeroObject, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, mkIso_hom_f, forget_faithful, HomologicalComplex.dgoEquivHomologicalComplex_functor, comp_f, isoApp_refl, HomologicalComplex.dgoToHomologicalComplex_obj_X, shiftZero_inv_app_f, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, shiftFunctorAdd_hom_app_f, id_f, HomologicalComplex.homologicalComplexToDGO_map_f, shiftFunctor_map_f, HomologicalComplex.dgoToHomologicalComplex_map_f, shiftFunctorAdd_inv_app_f, CategoryTheory.Functor.mapDifferentialObject_obj_d, isoApp_trans, isoApp_hom, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, isoApp_symm, isoApp_inv, mkIso_inv_f, CategoryTheory.Functor.mapDifferentialObject_obj_obj, HomologicalComplex.homologicalComplexToDGO_obj_d, HomologicalComplex.homologicalComplexToDGO_obj_obj, HomologicalComplex.dgoEquivHomologicalComplex_inverse, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, CategoryTheory.Functor.mapDifferentialObject_map_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, zero_f
concreteCategoryOfDifferentialObjects 📖	CompOp	—
d 📖	CompOp	15 math math: shiftFunctor_obj_d, d_squared_apply, HomologicalComplex.dgoToHomologicalComplex_obj_d, d_squared, Hom.comm_assoc, objEqToHom_d, shiftFunctor_map_f, HomologicalComplex.dgoToHomologicalComplex_map_f, CategoryTheory.Functor.mapDifferentialObject_obj_d, Hom.comm, HomologicalComplex.homologicalComplexToDGO_obj_d, d_squared_assoc, objEqToHom_d_assoc, d_squared_apply_assoc, CategoryTheory.Functor.mapDifferentialObject_map_f
forget 📖	CompOp	1 math math: forget_faithful
hasZeroMorphisms 📖	CompOp	—
instFunLikeHomSubtypeObj 📖	CompOp	—
instHasForget₂HomSubtypeObj 📖	CompOp	—
instHasShift 📖	CompOp	—
instZeroHom 📖	CompOp	1 math math: zero_f
isoApp 📖	CompOp	5 math math: isoApp_refl, isoApp_trans, isoApp_hom, isoApp_symm, isoApp_inv
mkIso 📖	CompOp	2 math math: mkIso_hom_f, mkIso_inv_f
obj 📖	CompOp	39 math math: shiftFunctor_obj_d, d_squared_apply, shiftFunctor_obj_obj, shiftZero_hom_app_f, HomologicalComplex.dgoToHomologicalComplex_obj_d, eqToHom_f, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, ext_iff, comp_f, d_squared, isoApp_refl, HomologicalComplex.dgoToHomologicalComplex_obj_X, Hom.comm_assoc, shiftZero_inv_app_f, shiftFunctorAdd_hom_app_f, id_f, Hom.id_f, objEqToHom_d, eqToHom_f', Hom.comp_f, shiftFunctor_map_f, objEqToHom_refl, HomologicalComplex.dgoToHomologicalComplex_map_f, shiftFunctorAdd_inv_app_f, CategoryTheory.Functor.mapDifferentialObject_obj_d, isoApp_trans, isoApp_hom, isoApp_symm, Hom.comm, isoApp_inv, eqToHom_f'_assoc, CategoryTheory.Functor.mapDifferentialObject_obj_obj, HomologicalComplex.homologicalComplexToDGO_obj_obj, d_squared_assoc, objEqToHom_d_assoc, d_squared_apply_assoc, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, CategoryTheory.Functor.mapDifferentialObject_map_f, zero_f
shiftFunctor 📖	CompOp	7 math math: shiftFunctor_obj_d, shiftFunctor_obj_obj, shiftZero_hom_app_f, shiftZero_inv_app_f, shiftFunctorAdd_hom_app_f, shiftFunctor_map_f, shiftFunctorAdd_inv_app_f
shiftFunctorAdd 📖	CompOp	2 math math: shiftFunctorAdd_hom_app_f, shiftFunctorAdd_inv_app_f
shiftZero 📖	CompOp	2 math math: shiftZero_hom_app_f, shiftZero_inv_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp CategoryTheory.DifferentialObject CategoryTheory.Category.toCategoryStruct categoryOfDifferentialObjects obj	—	—
d_squared 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
d_squared_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_squared
eqToHom_f 📖	mathematical	—	Hom.f CategoryTheory.eqToHom CategoryTheory.DifferentialObject CategoryTheory.Category.toCategoryStruct categoryOfDifferentialObjects obj	—	CategoryTheory.eqToHom_refl
ext 📖	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Hom.f	—	—	Hom.ext
ext_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Hom.f	—	ext
forget_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.DifferentialObject categoryOfDifferentialObjects forget	—	ext
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject CategoryTheory.DifferentialObject categoryOfDifferentialObjects	—	CategoryTheory.Functor.map_zero CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp ext CategoryTheory.Limits.HasZeroObject.from_zero_ext CategoryTheory.Limits.HasZeroObject.to_zero_ext
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.DifferentialObject CategoryTheory.Category.toCategoryStruct categoryOfDifferentialObjects obj	—	—
isoApp_hom 📖	mathematical	—	CategoryTheory.Iso.hom obj isoApp Hom.f CategoryTheory.DifferentialObject categoryOfDifferentialObjects	—	—
isoApp_inv 📖	mathematical	—	CategoryTheory.Iso.inv obj isoApp Hom.f CategoryTheory.DifferentialObject categoryOfDifferentialObjects	—	—
isoApp_refl 📖	mathematical	—	isoApp CategoryTheory.Iso.refl CategoryTheory.DifferentialObject categoryOfDifferentialObjects obj	—	—
isoApp_symm 📖	mathematical	—	isoApp CategoryTheory.Iso.symm CategoryTheory.DifferentialObject categoryOfDifferentialObjects obj	—	—
isoApp_trans 📖	mathematical	—	isoApp CategoryTheory.Iso.trans CategoryTheory.DifferentialObject categoryOfDifferentialObjects obj	—	—
mkIso_hom_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d CategoryTheory.Functor.map CategoryTheory.Iso.hom	Hom.f CategoryTheory.DifferentialObject categoryOfDifferentialObjects mkIso	—	—
mkIso_inv_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne d CategoryTheory.Functor.map CategoryTheory.Iso.hom	Hom.f CategoryTheory.Iso.inv CategoryTheory.DifferentialObject categoryOfDifferentialObjects mkIso	—	—
shiftFunctorAdd_hom_app_f 📖	mathematical	—	Hom.f AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.DifferentialObject categoryOfDifferentialObjects shiftFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.shiftFunctorAdd obj	—	—
shiftFunctorAdd_inv_app_f 📖	mathematical	—	Hom.f AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.DifferentialObject categoryOfDifferentialObjects CategoryTheory.Functor.comp shiftFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.shiftFunctorAdd obj	—	—
shiftFunctor_map_f 📖	mathematical	—	Hom.f AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddMonoidWithOne.toOne CategoryTheory.Functor.map d CategoryTheory.Iso.hom AddCommMonoid.toAddMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne CategoryTheory.shiftComm CategoryTheory.DifferentialObject categoryOfDifferentialObjects shiftFunctor	—	—
shiftFunctor_obj_d 📖	mathematical	—	d AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.DifferentialObject categoryOfDifferentialObjects shiftFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid obj AddMonoidWithOne.toOne CategoryTheory.Functor.map CategoryTheory.Iso.hom AddCommMonoid.toAddMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne CategoryTheory.shiftComm	—	—
shiftFunctor_obj_obj 📖	mathematical	—	obj AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.DifferentialObject categoryOfDifferentialObjects shiftFunctor CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid	—	—
shiftZero_hom_app_f 📖	mathematical	—	Hom.f AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.DifferentialObject categoryOfDifferentialObjects shiftFunctor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroupWithOne.toAddCommGroup CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftZero CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj	—	—
shiftZero_inv_app_f 📖	mathematical	—	Hom.f AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne CategoryTheory.Functor.obj CategoryTheory.DifferentialObject categoryOfDifferentialObjects CategoryTheory.Functor.id shiftFunctor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroupWithOne.toAddCommGroup CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftZero CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj	—	—
zero_f 📖	mathematical	—	Hom.f Quiver.Hom CategoryTheory.DifferentialObject CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryOfDifferentialObjects instZeroHom obj CategoryTheory.Limits.HasZeroMorphisms.zero	—	—

CategoryTheory.DifferentialObject.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: comp_f
f 📖	CompOp	26 math math: CategoryTheory.DifferentialObject.shiftZero_hom_app_f, CategoryTheory.DifferentialObject.eqToHom_f, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, CategoryTheory.DifferentialObject.ext_iff, CategoryTheory.DifferentialObject.mkIso_hom_f, CategoryTheory.DifferentialObject.comp_f, comm_assoc, CategoryTheory.DifferentialObject.shiftZero_inv_app_f, ext_iff, CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f, CategoryTheory.DifferentialObject.id_f, HomologicalComplex.homologicalComplexToDGO_map_f, id_f, CategoryTheory.DifferentialObject.eqToHom_f', comp_f, CategoryTheory.DifferentialObject.shiftFunctor_map_f, HomologicalComplex.dgoToHomologicalComplex_map_f, CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f, CategoryTheory.DifferentialObject.isoApp_hom, comm, CategoryTheory.DifferentialObject.isoApp_inv, CategoryTheory.DifferentialObject.mkIso_inv_f, CategoryTheory.DifferentialObject.eqToHom_f'_assoc, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, CategoryTheory.Functor.mapDifferentialObject_map_f, CategoryTheory.DifferentialObject.zero_f
id 📖	CompOp	1 math math: id_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne CategoryTheory.DifferentialObject.d CategoryTheory.Functor.map f	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne CategoryTheory.DifferentialObject.d CategoryTheory.Functor.map f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comp_f 📖	mathematical	—	f comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj	—	—
ext 📖	—	f	—	—	—
ext_iff 📖	mathematical	—	f	—	ext
id_f 📖	mathematical	—	f id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.DifferentialObject.obj	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapDifferentialObject 📖	CompOp	3 math math: mapDifferentialObject_obj_d, mapDifferentialObject_obj_obj, mapDifferentialObject_map_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapDifferentialObject_map_f 📖	mathematical	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero obj	CategoryTheory.DifferentialObject.Hom.f CategoryTheory.DifferentialObject.obj CategoryTheory.CategoryStruct.comp CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne CategoryTheory.DifferentialObject.d CategoryTheory.NatTrans.app comp CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects mapDifferentialObject	—	—
mapDifferentialObject_obj_d 📖	mathematical	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero obj	CategoryTheory.DifferentialObject.d CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects mapDifferentialObject CategoryTheory.CategoryStruct.comp CategoryTheory.DifferentialObject.obj CategoryTheory.shiftFunctor AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne CategoryTheory.NatTrans.app comp	—	—
mapDifferentialObject_obj_obj 📖	mathematical	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero obj	CategoryTheory.DifferentialObject.obj CategoryTheory.DifferentialObject CategoryTheory.DifferentialObject.categoryOfDifferentialObjects mapDifferentialObject	—	—

---

← Back to Index