Three

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

Statistics

Metric	Count
Definitions threeδ₁Toδ₀, threeδ₁Toδ₀', threeδ₂Toδ₁, threeδ₂Toδ₁', threeδ₃Toδ₂, threeδ₃Toδ₂'	6
Theorems threeδ₁Toδ₀_app_one, threeδ₁Toδ₀_app_two, threeδ₁Toδ₀_app_zero, threeδ₂Toδ₁_app_one, threeδ₂Toδ₁_app_two, threeδ₂Toδ₁_app_zero, threeδ₃Toδ₂_app_one, threeδ₃Toδ₂_app_two, threeδ₃Toδ₂_app_zero	9
Total	15

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
threeδ₁Toδ₀ 📖	CompOp	8 math math: threeδ₁Toδ₀_app_zero, CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_exact, CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_assoc, threeδ₁Toδ₀_app_two, CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE, CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ, threeδ₁Toδ₀_app_one, CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE_assoc
threeδ₁Toδ₀' 📖	CompOp	—
threeδ₂Toδ₁ 📖	CompOp	6 math math: threeδ₂Toδ₁_app_zero, CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, threeδ₂Toδ₁_app_one, threeδ₂Toδ₁_app_two, CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_f, CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE
threeδ₂Toδ₁' 📖	CompOp	—
threeδ₃Toδ₂ 📖	CompOp	7 math math: CategoryTheory.Abelian.SpectralObject.πE_EToCycles, CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap, threeδ₃Toδ₂_app_one, CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap_exact, threeδ₃Toδ₂_app_two, CategoryTheory.Abelian.SpectralObject.πE_EToCycles_assoc, threeδ₃Toδ₂_app_zero
threeδ₃Toδ₂' 📖	CompOp	—

Theorems

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

---

← Back to Index