HomologicalBicomplex

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

Statistics

Metric	Count
Definitions HomologicalComplex₂, XXIsoOfEq, flip, flipEquivalence, flipEquivalenceCounitIso, flipEquivalenceUnitIso, flipFunctor, homMk, ofGradedObject, toGradedObject, toGradedObjectFunctor, toGradedObjectMap	12
Theorems XXIsoOfEq_rfl, comm_f, comm_f_assoc, d_comm, d_comm_assoc, d_f_comp_d_f, d_f_comp_d_f_assoc, flipEquivalenceCounitIso_hom_app_f_f, flipEquivalenceCounitIso_inv_app_f_f, flipEquivalenceUnitIso_hom_app_f_f, flipEquivalenceUnitIso_inv_app_f_f, flipEquivalence_counitIso, flipEquivalence_functor, flipEquivalence_inverse, flipEquivalence_unitIso, flipFunctor_map_f_f, flipFunctor_obj, flip_X_X, flip_X_d, flip_d_f, flip_flip, homMk_f_f, instFaithfulGradedObjectProdToGradedObjectFunctor, ofGradedObject_X_X, ofGradedObject_X_d, ofGradedObject_d_f, ofGradedObject_toGradedObject, shape_f, toGradedObjectFunctor_map, toGradedObjectFunctor_obj, toGradedObjectMap_apply	31
Total	43

HomologicalComplex₂

Definitions

Name	Category	Theorems
XXIsoOfEq 📖	CompOp	5 math math: XXIsoOfEq_hom_ιTotal_assoc, XXIsoOfEq_rfl, XXIsoOfEq_inv_ιTotal_assoc, XXIsoOfEq_inv_ιTotal, XXIsoOfEq_hom_ιTotal
flip 📖	CompOp	22 math math: totalFlipIso_hom_f_D₁, ιTotal_totalFlipIso_f_inv_assoc, flip_flip, totalFlipIsoX_hom_D₂_assoc, flipFunctor_obj, flip_X_X, instHasTotalFlip, ιTotal_totalFlipIso_f_hom_assoc, totalFlipIso_hom_f_D₂, totalFlipIso_hom_f_D₁_assoc, totalFlipIsoX_hom_D₁, instHasTotalFlip_1, flip_totalFlipIso, ιTotal_totalFlipIso_f_hom, flip_X_d, totalFlipIsoX_hom_D₂, flip_d_f, flip_hasTotal_iff, flipFunctor_map_f_f, totalFlipIsoX_hom_D₁_assoc, totalFlipIso_hom_f_D₂_assoc, ιTotal_totalFlipIso_f_inv
flipEquivalence 📖	CompOp	4 math math: flipEquivalence_unitIso, flipEquivalence_counitIso, flipEquivalence_functor, flipEquivalence_inverse
flipEquivalenceCounitIso 📖	CompOp	3 math math: flipEquivalence_counitIso, flipEquivalenceCounitIso_inv_app_f_f, flipEquivalenceCounitIso_hom_app_f_f
flipEquivalenceUnitIso 📖	CompOp	3 math math: flipEquivalence_unitIso, flipEquivalenceUnitIso_hom_app_f_f, flipEquivalenceUnitIso_inv_app_f_f
flipFunctor 📖	CompOp	8 math math: flipEquivalenceUnitIso_hom_app_f_f, flipFunctor_obj, flipEquivalenceUnitIso_inv_app_f_f, flipEquivalence_functor, flipEquivalence_inverse, flipEquivalenceCounitIso_inv_app_f_f, flipEquivalenceCounitIso_hom_app_f_f, flipFunctor_map_f_f
homMk 📖	CompOp	1 math math: homMk_f_f
ofGradedObject 📖	CompOp	6 math math: CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, ofGradedObject_toGradedObject, ofGradedObject_X_d, ofGradedObject_X_X, ofGradedObject_d_f, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f
toGradedObject 📖	CompOp	56 math math: totalAux.ιMapObj_D₁, totalFlipIso_hom_f_D₁, ofGradedObject_toGradedObject, totalAux.d₂_eq, D₂_totalShift₁XIso_hom_assoc, D₂_totalShift₂XIso_hom_assoc, d₁_eq_zero', D₁_D₁_assoc, total.mapAux.mapMap_D₁_assoc, D₁_D₁, D₂_D₁_assoc, toGradedObjectFunctor_obj, D₂_D₂, ι_D₁_assoc, d₂_eq_zero, ι_D₂, total.mapAux.d₁_mapMap, totalAux.ιMapObj_D₂_assoc, D₁_shape, totalFlipIsoX_hom_D₂_assoc, ι_D₂_assoc, totalAux.d₂_eq', totalAux.d₁_eq, D₁_totalShift₂XIso_hom_assoc, total.mapAux.d₂_mapMap_assoc, d₁_eq_zero, D₁_totalShift₁XIso_hom_assoc, total.mapAux.mapMap_D₁, d₂_eq_zero', total.mapAux.mapMap_D₂, totalAux.ιMapObj_D₂, D₂_shape, total.mapAux.mapMap_D₂_assoc, totalFlipIso_hom_f_D₂, D₁_totalShift₁XIso_hom, D₂_totalShift₁XIso_hom, totalFlipIso_hom_f_D₁_assoc, totalFlipIsoX_hom_D₁, D₂_D₂_assoc, D₂_D₁, D₁_D₂_assoc, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, total.mapAux.d₂_mapMap, ι_D₁, total_d, total.mapAux.d₁_mapMap_assoc, totalFlipIsoX_hom_D₂, D₁_totalShift₂XIso_hom, D₂_totalShift₂XIso_hom, totalAux.ιMapObj_D₁_assoc, totalAux.d₁_eq', D₁_D₂, totalFlipIsoX_hom_D₁_assoc, total.forget_map, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, totalFlipIso_hom_f_D₂_assoc
toGradedObjectFunctor 📖	CompOp	3 math math: toGradedObjectFunctor_obj, toGradedObjectFunctor_map, instFaithfulGradedObjectProdToGradedObjectFunctor
toGradedObjectMap 📖	CompOp	11 math math: total.mapAux.mapMap_D₁_assoc, total.mapAux.d₁_mapMap, total.mapAux.d₂_mapMap_assoc, total.mapAux.mapMap_D₁, total.mapAux.mapMap_D₂, total.mapAux.mapMap_D₂_assoc, total.mapAux.d₂_mapMap, toGradedObjectFunctor_map, total.mapAux.d₁_mapMap_assoc, toGradedObjectMap_apply, total.forget_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
XXIsoOfEq_rfl 📖	mathematical	—	XXIsoOfEq CategoryTheory.Iso.refl HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms	—	—
comm_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d	—	HomologicalComplex.congr_hom HomologicalComplex.Hom.comm
comm_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm_f
d_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d	—	HomologicalComplex.Hom.comm
d_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comm
d_f_comp_d_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.comp_f HomologicalComplex.d_comp_d HomologicalComplex.zero_f
d_f_comp_d_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_f_comp_d_f
flipEquivalenceCounitIso_hom_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Functor.comp flipFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category flipEquivalenceCounitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipEquivalenceCounitIso_inv_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Functor.id CategoryTheory.Functor.comp flipFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category flipEquivalenceCounitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipEquivalenceUnitIso_hom_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Functor.id CategoryTheory.Functor.comp flipFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category flipEquivalenceUnitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipEquivalenceUnitIso_inv_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Functor.comp flipFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category flipEquivalenceUnitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms flipEquivalence flipEquivalenceCounitIso	—	—
flipEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms flipEquivalence flipFunctor	—	—
flipEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms flipEquivalence flipFunctor	—	—
flipEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms flipEquivalence flipEquivalenceUnitIso	—	—
flipFunctor_map_f_f 📖	mathematical	—	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms flip CategoryTheory.Functor.map HomologicalComplex₂ flipFunctor	—	—
flipFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms flipFunctor flip	—	—
flip_X_X 📖	mathematical	—	HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms flip	—	—
flip_X_d 📖	mathematical	—	HomologicalComplex.d HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms flip HomologicalComplex.Hom.f	—	—
flip_d_f 📖	mathematical	—	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.d shape_f flip	—	shape_f
flip_flip 📖	mathematical	—	flip	—	—
homMk_f_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct toGradedObject HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.Hom.f HomologicalComplex.d	homMk	—	—
instFaithfulGradedObjectProdToGradedObjectFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects toGradedObjectFunctor	—	HomologicalComplex.hom_ext
ofGradedObject_X_X 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp	HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ofGradedObject	—	—
ofGradedObject_X_d 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp	HomologicalComplex.d HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ofGradedObject	—	—
ofGradedObject_d_f 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp	HomologicalComplex.Hom.f HomologicalComplex.d HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ofGradedObject	—	—
ofGradedObject_toGradedObject 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp	toGradedObject ofGradedObject	—	—
shape_f 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.shape HomologicalComplex.zero_f
toGradedObjectFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects toGradedObjectFunctor toGradedObjectMap	—	—
toGradedObjectFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects toGradedObjectFunctor toGradedObject	—	—
toGradedObjectMap_apply 📖	mathematical	—	toGradedObjectMap HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms	—	—

(root)

Definitions

Name	Category	Theorems
HomologicalComplex₂ 📖	CompOp	64 math math: CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, HomologicalComplex₂.shiftFunctor₂XXIso_refl, HomologicalComplex₂.total.mapIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, HomologicalComplex₂.flipEquivalence_unitIso, HomologicalComplex₂.toGradedObjectFunctor_obj, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d, HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X, HomologicalComplex₂.totalFunctor_obj, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, HomologicalComplex₂.flipFunctor_obj, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex₂.shiftFunctor₁XXIso_refl, CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.total.mapIso_inv, HomologicalComplex₂.flipEquivalence_counitIso, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, HomologicalComplex₂.total.map_comp, HomologicalComplex₂.flipEquivalence_functor, HomologicalComplex₂.flipEquivalence_inverse, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, HomologicalComplex₂.total.map_comp_assoc, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomologicalComplex₂.totalShift₂Iso_hom_naturality, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f, HomologicalComplex₂.toGradedObjectFunctor_map, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁, HomologicalComplex₂.totalShift₁Iso_hom_naturality, HomologicalComplex₂.D₁_totalShift₂XIso_hom, HomologicalComplex₂.D₂_totalShift₂XIso_hom, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f, HomologicalComplex₂.flipFunctor_map_f_f, HomologicalComplex₂.total.map_id, HomologicalComplex₂.totalFunctor_map, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f

---

← Back to Index