Two

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

Statistics

Metric	Count
Definitions twoδ₁Toδ₀, twoδ₁Toδ₀', twoδ₂Toδ₁, twoδ₂Toδ₁'	4
Theorems instIsIsoOfNatNatTwoδ₁Toδ₀, instIsIsoOfNatNatTwoδ₂Toδ₁, twoδ₁Toδ₀_app_one, twoδ₁Toδ₀_app_zero, twoδ₂Toδ₁_app_one, twoδ₂Toδ₁_app_zero	6
Total	10

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
twoδ₁Toδ₀ 📖	CompOp	24 math math: CategoryTheory.Abelian.SpectralObject.zero₂_assoc, twoδ₁Toδ₀_app_zero, CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc, CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.zero₃, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_g, CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_g, CategoryTheory.Abelian.SpectralObject.sc₂_g, CategoryTheory.Abelian.SpectralObject.zero₂, CategoryTheory.Triangulated.SpectralObject.triangle_mor₂, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc, twoδ₁Toδ₀_app_one, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_g, instIsIsoOfNatNatTwoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc, CategoryTheory.Abelian.SpectralObject.zero₃_assoc, CategoryTheory.Abelian.SpectralObject.sc₃_f, CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc
twoδ₁Toδ₀' 📖	CompOp	6 math math: CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀', CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃, CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀', CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀'
twoδ₂Toδ₁ 📖	CompOp	21 math math: CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc, CategoryTheory.Abelian.SpectralObject.zero₂_assoc, twoδ₂Toδ₁_app_zero, CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_f, CategoryTheory.Abelian.SpectralObject.zero₂, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc, CategoryTheory.Abelian.SpectralObject.zero₁, CategoryTheory.Triangulated.SpectralObject.triangle_mor₁, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc, twoδ₂Toδ₁_app_one, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_f, CategoryTheory.Abelian.SpectralObject.sc₂_f, instIsIsoOfNatNatTwoδ₂Toδ₁, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_f, CategoryTheory.Abelian.SpectralObject.zero₁_assoc, CategoryTheory.Abelian.SpectralObject.sc₁_g
twoδ₂Toδ₁' 📖	CompOp	3 math math: CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoOfNatNatTwoδ₁Toδ₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ twoδ₁Toδ₀	—	isIso_iff₁ CategoryTheory.IsIso.id
instIsIsoOfNatNatTwoδ₂Toδ₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ twoδ₂Toδ₁	—	isIso_iff₁ CategoryTheory.IsIso.id
twoδ₁Toδ₀_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ twoδ₁Toδ₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
twoδ₁Toδ₀_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ twoδ₁Toδ₀	—	—
twoδ₂Toδ₁_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ twoδ₂Toδ₁	—	—
twoδ₂Toδ₁_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ twoδ₂Toδ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—

---

← Back to Index