SpectralObject

📁 Source: Mathlib/CategoryTheory/Triangulated/SpectralObject.lean

Statistics

Metric	Count
Definitions mapTriangulatedSpectralObject, SpectralObject, hom, instCategory, mapTriangulatedFunctor, precomp, triangle, δ, δ', ω₁, ω₂	11
Theorems comm, comm_assoc, ext, ext_iff, comp_hom, comp_hom_assoc, distinguished', hom_ext, hom_ext_iff, id_hom, mapTriangulatedFunctor_δ, mapTriangulatedFunctor_δ', mapTriangulatedFunctor_ω₁, triangle_distinguished, triangle_mor₁, triangle_mor₂, triangle_mor₃, triangle_obj₁, triangle_obj₂, triangle_obj₃, ω₂_map_hom₁, ω₂_map_hom₂, ω₂_map_hom₃, ω₂_obj_distinguished, ω₂_obj_mor₁, ω₂_obj_mor₂, ω₂_obj_mor₃, ω₂_obj_obj₁, ω₂_obj_obj₂, ω₂_obj_obj₃	30
Total	41

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapTriangulatedSpectralObject 📖	CompOp	—

CategoryTheory.Triangulated

Definitions

Name	Category	Theorems
SpectralObject 📖	CompData	3 math math: SpectralObject.id_hom, SpectralObject.comp_hom, SpectralObject.comp_hom_assoc

CategoryTheory.Triangulated.SpectralObject

Definitions

Name	Category	Theorems
instCategory 📖	CompOp	3 math math: id_hom, comp_hom, comp_hom_assoc
mapTriangulatedFunctor 📖	CompOp	3 math math: mapTriangulatedFunctor_ω₁, mapTriangulatedFunctor_δ, mapTriangulatedFunctor_δ'
precomp 📖	CompOp	—
triangle 📖	CompOp	7 math math: triangle_mor₃, triangle_obj₂, triangle_mor₂, triangle_mor₁, triangle_obj₃, triangle_obj₁, triangle_distinguished
δ 📖	CompOp	4 math math: Hom.comm, triangle_mor₃, Hom.comm_assoc, mapTriangulatedFunctor_δ
δ' 📖	CompOp	7 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, ω₂_obj_mor₃, ω₂_map_hom₁, distinguished', mapTriangulatedFunctor_δ', ω₂_map_hom₂, ω₂_map_hom₃
ω₁ 📖	CompOp	24 math math: Hom.comm, ω₂_obj_mor₃, ω₂_map_hom₁, triangle_obj₂, mapTriangulatedFunctor_ω₁, triangle_mor₂, Hom.comm_assoc, ω₂_obj_mor₂, id_hom, distinguished', triangle_mor₁, mapTriangulatedFunctor_δ, comp_hom, mapTriangulatedFunctor_δ', HomotopyCategory.spectralObjectMappingCone_ω₁, ω₂_map_hom₂, triangle_obj₃, comp_hom_assoc, ω₂_obj_obj₂, triangle_obj₁, ω₂_obj_mor₁, ω₂_map_hom₃, ω₂_obj_obj₁, ω₂_obj_obj₃
ω₂ 📖	CompOp	10 math math: ω₂_obj_distinguished, ω₂_obj_mor₃, ω₂_map_hom₁, ω₂_obj_mor₂, ω₂_map_hom₂, ω₂_obj_obj₂, ω₂_obj_mor₁, ω₂_map_hom₃, ω₂_obj_obj₁, ω₂_obj_obj₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Triangulated.SpectralObject CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁	—	—
comp_hom_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Category.toCategoryStruct ω₁ Hom.hom CategoryTheory.Triangulated.SpectralObject instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
distinguished' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.functorArrows CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mapFunctorArrows CategoryTheory.Functor.comp δ'	—	—
hom_ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Hom.hom	—	hom_ext
id_hom 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Triangulated.SpectralObject CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁	—	—
mapTriangulatedFunctor_δ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	δ mapTriangulatedFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.CommShift.commShiftIso	—	—
mapTriangulatedFunctor_δ' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	δ' mapTriangulatedFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.ComposableArrows.functorArrows ω₁ CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.Functor.CommShift.commShiftIso	—	—
mapTriangulatedFunctor_ω₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	ω₁ mapTriangulatedFunctor CategoryTheory.Functor.comp CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—
triangle_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles triangle	—	ω₂_obj_distinguished
triangle_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ triangle CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ComposableArrows.twoδ₂Toδ₁	—	—
triangle_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ triangle CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	—
triangle_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ triangle δ	—	—
triangle_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ triangle CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.mk₁	—	—
triangle_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ triangle CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
triangle_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ triangle CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder ω₁ CategoryTheory.ComposableArrows.mk₁	—	—
ω₂_map_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.ComposableArrows.functorArrows ω₁ CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskerRight CategoryTheory.ComposableArrows.mapFunctorArrows δ' CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE CategoryTheory.ComposableArrows.homMk₁	—	—
ω₂_map_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.ComposableArrows.functorArrows ω₁ CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskerRight CategoryTheory.ComposableArrows.mapFunctorArrows δ' CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE CategoryTheory.ComposableArrows.homMk₁	—	—
ω₂_map_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.ComposableArrows.functorArrows ω₁ CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskerRight CategoryTheory.ComposableArrows.mapFunctorArrows δ' CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE CategoryTheory.ComposableArrows.homMk₁	—	—
ω₂_obj_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.triangleCategory ω₂	—	distinguished'
ω₂_obj_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ CategoryTheory.Functor.map ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ComposableArrows.obj' CategoryTheory.CategoryStruct.comp CategoryTheory.ComposableArrows.map' CategoryTheory.Functor.map_id	—	CategoryTheory.Functor.map_id CategoryTheory.ComposableArrows.homMk₁.congr_simp
ω₂_obj_mor₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ CategoryTheory.Functor.map ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ComposableArrows.obj' CategoryTheory.CategoryStruct.comp CategoryTheory.ComposableArrows.map' CategoryTheory.Functor.map_id	—	CategoryTheory.Functor.map_id CategoryTheory.ComposableArrows.homMk₁.congr_simp
ω₂_obj_mor₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.ComposableArrows.functorArrows ω₁ δ'	—	—
ω₂_obj_obj₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.homOfLE	—	—
ω₂_obj_obj₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.homOfLE	—	—
ω₂_obj_obj₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory ω₂ ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.homOfLE	—	—

CategoryTheory.Triangulated.SpectralObject.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: comm, comm_assoc, CategoryTheory.Triangulated.SpectralObject.id_hom, CategoryTheory.Triangulated.SpectralObject.comp_hom, ext_iff, CategoryTheory.Triangulated.SpectralObject.comp_hom_assoc, CategoryTheory.Triangulated.SpectralObject.hom_ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Triangulated.SpectralObject.ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Triangulated.SpectralObject.δ CategoryTheory.Functor.map CategoryTheory.NatTrans.app hom	—	—
comm_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Triangulated.SpectralObject.ω₁ CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Triangulated.SpectralObject.δ CategoryTheory.Functor.map CategoryTheory.NatTrans.app hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
ext 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid hom	—	—	—
ext_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	hom	—	ext

---

← Back to Index