Documentation Verification Report

SpectralObject

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

Statistics

Metric	Count
Definitions `SpectralObject`, `SpectralObject`, `spectralObject`, `spectralObjectFunctor`, `triangleω₁δ`, `triangleω₁δObjIso`, `ω₁`, `ω₁δ`	8
Theorems `spectralObjectFunctor_map_hom`, `spectralObjectFunctor_obj`, `spectralObject_δ`, `spectralObject_ω₁`, `triangleω₁δ_distinguished`, `triangleω₁δ_map_hom₁`, `triangleω₁δ_map_hom₂`, `triangleω₁δ_map_hom₃`, `triangleω₁δ_obj_mor₁`, `triangleω₁δ_obj_mor₂`, `triangleω₁δ_obj_mor₃`, `triangleω₁δ_obj_obj₁`, `triangleω₁δ_obj_obj₂`, `triangleω₁δ_obj_obj₃`, `ω₁_map`, `ω₁_obj`, `ω₁δ_app`, `ω₁δ_naturality`, `ω₁δ_naturality_assoc`	19
Total	27

CategoryTheory.Abelian

Definitions

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

CategoryTheory.Triangulated

Definitions

Name	Category	Theorems
`SpectralObject` 📖	CompData	5 math math: `TStructure.spectralObjectFunctor_map_hom`, `SpectralObject.id_hom`, `TStructure.spectralObjectFunctor_obj`, `SpectralObject.comp_hom`, `SpectralObject.comp_hom_assoc`

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
`spectralObject` 📖	CompOp	4 math math: `spectralObject_ω₁`, `spectralObjectFunctor_map_hom`, `spectralObjectFunctor_obj`, `spectralObject_δ`
`spectralObjectFunctor` 📖	CompOp	2 math math: `spectralObjectFunctor_map_hom`, `spectralObjectFunctor_obj`
`triangleω₁δ` 📖	CompOp	10 math math: `triangleω₁δ_obj_mor₁`, `triangleω₁δ_obj_obj₂`, `triangleω₁δ_map_hom₁`, `triangleω₁δ_map_hom₂`, `triangleω₁δ_distinguished`, `triangleω₁δ_map_hom₃`, `triangleω₁δ_obj_obj₁`, `triangleω₁δ_obj_mor₃`, `triangleω₁δ_obj_mor₂`, `triangleω₁δ_obj_obj₃`
`triangleω₁δObjIso` 📖	CompOp	—
`ω₁` 📖	CompOp	11 math math: `triangleω₁δ_map_hom₁`, `ω₁δ_naturality_assoc`, `triangleω₁δ_map_hom₂`, `spectralObject_ω₁`, `ω₁_map`, `triangleω₁δ_map_hom₃`, `spectralObjectFunctor_map_hom`, `ω₁_obj`, `ω₁δ_app`, `ω₁δ_naturality`, `spectralObject_δ`
`ω₁δ` 📖	CompOp	7 math math: `triangleω₁δ_map_hom₁`, `ω₁δ_naturality_assoc`, `triangleω₁δ_map_hom₂`, `triangleω₁δ_map_hom₃`, `ω₁δ_app`, `ω₁δ_naturality`, `spectralObject_δ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spectralObjectFunctor_map_hom` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Triangulated.SpectralObject.Hom.hom` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `spectralObject` `CategoryTheory.Functor.map` `CategoryTheory.Triangulated.SpectralObject` `CategoryTheory.Triangulated.SpectralObject.instCategory` `spectralObjectFunctor` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.Functor.obj` `CategoryTheory.evaluation`	—	—
`spectralObjectFunctor_obj` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.obj` `CategoryTheory.Triangulated.SpectralObject` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Triangulated.SpectralObject.instCategory` `spectralObjectFunctor` `spectralObject`	—	—
`spectralObject_δ` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Triangulated.SpectralObject.δ` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `spectralObject` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.leOfHom` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `ω₁δ`	—	—
`spectralObject_ω₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Triangulated.SpectralObject.ω₁` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `spectralObject` `CategoryTheory.Functor.comp` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.Functor.obj` `CategoryTheory.evaluation`	—	—
`triangleω₁δ_distinguished` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ`	—	`CategoryTheory.Pretriangulated.isomorphic_distinguished` `LE.le.trans` `eTriangleLTGE_distinguished`
`triangleω₁δ_map_hom₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₁` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `CategoryTheory.ComposableArrows.twoδ₂Toδ₁'` `CategoryTheory.ComposableArrows.twoδ₁Toδ₀'` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `ω₁δ` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `eTruncGE` `eTruncLT`	—	—
`triangleω₁δ_map_hom₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₂` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `CategoryTheory.ComposableArrows.twoδ₂Toδ₁'` `CategoryTheory.ComposableArrows.twoδ₁Toδ₀'` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `ω₁δ` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `eTruncGE` `eTruncLT`	—	—
`triangleω₁δ_map_hom₃` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.TriangleMorphism.hom₃` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `CategoryTheory.ComposableArrows.twoδ₂Toδ₁'` `CategoryTheory.ComposableArrows.twoδ₁Toδ₀'` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `ω₁δ` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `eTruncGE` `eTruncLT`	—	—
`triangleω₁δ_obj_mor₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `CategoryTheory.Functor.map` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `eTruncGE` `eTruncLT` `CategoryTheory.NatTrans.app` `CategoryTheory.homOfLE`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`triangleω₁δ_obj_mor₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `CategoryTheory.NatTrans.app` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `eTruncGE` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `eTruncLT`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`triangleω₁δ_obj_mor₃` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `eTruncGE` `eTruncLT` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `eTruncGEπ` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringRight` `eTruncGEδLT` `CategoryTheory.Iso.hom` `eTruncLTGEIsoGELT` `eTruncLTι`	—	`ω₁δ_app`
`triangleω₁δ_obj_obj₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `eTruncGE` `eTruncLT`	—	—
`triangleω₁δ_obj_obj₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `eTruncGE` `eTruncLT`	—	—
`triangleω₁δ_obj_obj₃` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.obj` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `triangleω₁δ` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `eTruncGE` `eTruncLT`	—	—
`ω₁_map` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.map` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.NatTrans.hcomp` `CategoryTheory.Functor.obj` `eTruncLT` `eTruncGE` `CategoryTheory.NatTrans.app`	—	—
`ω₁_obj` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.Functor.comp` `eTruncLT` `eTruncGE`	—	—
`ω₁δ_app` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `CategoryTheory.Functor.category` `Fin.instPartialOrder` `CategoryTheory.Functor` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `ω₁δ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `eTruncGE` `eTruncLT` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `eTruncGEπ` `CategoryTheory.Functor.whiskeringRight` `eTruncGEδLT` `CategoryTheory.Iso.hom` `eTruncLTGEIsoGELT` `eTruncLTι`	—	`eTruncGEToGEGE_app` `eTruncLTLTToLT_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp`
`ω₁δ_naturality` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Fin.instPartialOrder` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Functor.map` `CategoryTheory.ComposableArrows.homMk₁` `CategoryTheory.NatTrans.app` `CategoryTheory.ComposableArrows.mk₂` `ω₁δ` `CategoryTheory.Functor.whiskerRight`	—	`CategoryTheory.NatTrans.ext'` `ω₁δ_app` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_app_assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.map_comp` `eTruncLTGEIsoGELT_naturality_app` `Mathlib.Tactic.Reassoc.eq_whisker'` `eTruncLTGEIsoGELT_hom_naturality` `eTruncLT_map_app_eTruncLTι_app` `eTruncGEπ_naturality` `eTruncLT_map_app_eTruncLTι_app_assoc` `eTruncGEπ_app_eTruncGE_map_app`
`ω₁δ_naturality_assoc` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `EInt` `Preorder.toLE` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.ComposableArrows` `EInt` `Preorder.smallCategory` `WithBot.instPreorder` `WithTop` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Fin.instPartialOrder` `ω₁` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.homOfLE` `CategoryTheory.Functor.map` `CategoryTheory.ComposableArrows.homMk₁` `CategoryTheory.NatTrans.app` `CategoryTheory.ComposableArrows.mk₂` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `ω₁δ` `CategoryTheory.Functor.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ω₁δ_naturality`

---

← Back to Index