Four

📁 Source: Mathlib/CategoryTheory/ComposableArrows/Four.lean

Statistics

Metric	Count
Definitions fourδ₁Toδ₀, fourδ₁Toδ₀', fourδ₂Toδ₁, fourδ₂Toδ₁', fourδ₃Toδ₂, fourδ₃Toδ₂', fourδ₄Toδ₃, fourδ₄Toδ₃'	8
Theorems fourδ₁Toδ₀_app_one, fourδ₁Toδ₀_app_three, fourδ₁Toδ₀_app_two, fourδ₁Toδ₀_app_zero, fourδ₂Toδ₁_app_one, fourδ₂Toδ₁_app_three, fourδ₂Toδ₁_app_two, fourδ₂Toδ₁_app_zero, fourδ₃Toδ₂_app_one, fourδ₃Toδ₂_app_three, fourδ₃Toδ₂_app_two, fourδ₃Toδ₂_app_zero, fourδ₄Toδ₃_app_one, fourδ₄Toδ₃_app_three, fourδ₄Toδ₃_app_two, fourδ₄Toδ₃_app_zero	16
Total	24

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
fourδ₁Toδ₀ 📖	CompOp	16 math math: fourδ₁Toδ₀_app_zero, CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_inv, CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d, CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d_assoc, CategoryTheory.Abelian.SpectralObject.dHomologyData_left_i, CategoryTheory.Abelian.SpectralObject.dHomologyData_right_ι, fourδ₁Toδ₀_app_two, CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero, CategoryTheory.Abelian.SpectralObject.dKernelSequence_f, CategoryTheory.Abelian.SpectralObject.instMonoMapFourδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_hom, CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc, fourδ₁Toδ₀_app_one, fourδ₁Toδ₀_app_three, CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃, CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀
fourδ₁Toδ₀' 📖	CompOp	—
fourδ₂Toδ₁ 📖	CompOp	4 math math: fourδ₂Toδ₁_app_three, fourδ₂Toδ₁_app_zero, fourδ₂Toδ₁_app_one, fourδ₂Toδ₁_app_two
fourδ₂Toδ₁' 📖	CompOp	—
fourδ₃Toδ₂ 📖	CompOp	4 math math: fourδ₃Toδ₂_app_one, fourδ₃Toδ₂_app_two, fourδ₃Toδ₂_app_three, fourδ₃Toδ₂_app_zero
fourδ₃Toδ₂' 📖	CompOp	—
fourδ₄Toδ₃ 📖	CompOp	16 math math: CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero, CategoryTheory.Abelian.SpectralObject.instEpiMapFourδ₄Toδ₃, CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_inv, fourδ₄Toδ₃_app_two, fourδ₄Toδ₃_app_one, CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃, CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃_assoc, CategoryTheory.Abelian.SpectralObject.dHomologyData_right_p, CategoryTheory.Abelian.SpectralObject.dHomologyData_left_π, CategoryTheory.Abelian.SpectralObject.dHomologyData_iso_hom, CategoryTheory.Abelian.SpectralObject.dCokernelSequence_g, CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc, fourδ₄Toδ₃_app_zero, CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃, fourδ₄Toδ₃_app_three, CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃
fourδ₄Toδ₃' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourδ₁Toδ₀_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₁Toδ₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₁Toδ₀_app_three 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₁Toδ₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₁Toδ₀_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₁Toδ₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₁Toδ₀_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₁Toδ₀	—	—
fourδ₂Toδ₁_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₂Toδ₁	—	—
fourδ₂Toδ₁_app_three 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₂Toδ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₂Toδ₁_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₂Toδ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₂Toδ₁_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₂Toδ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₃Toδ₂_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₃Toδ₂ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₃Toδ₂_app_three 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₃Toδ₂ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₃Toδ₂_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₃Toδ₂	—	—
fourδ₃Toδ₂_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₃Toδ₂ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₄Toδ₃_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₄Toδ₃ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₄Toδ₃_app_three 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₄Toδ₃	—	—
fourδ₄Toδ₃_app_two 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₄Toδ₃ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
fourδ₄Toδ₃_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₃ fourδ₄Toδ₃ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—

---

← Back to Index