Documentation Verification Report

Heart

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

Statistics

Metric	Count
Definitions `Heart`, `ι`, `hasHeartFullSubcategory`, `heart`, `instIsClosedUnderIsomorphismsHeart`, `ιHeart`	6
Theorems `additive_ι`, `essImage_eq_heart`, `faithful_ι`, `full_ι`, `essImage_ιHeart`, `instAdditiveιHeart`, `instFaithfulιHeart`, `instFullιHeart`, `instIsGEObjιHeartOfNatInt`, `instIsLEObjιHeartOfNatInt`, `mem_heart_iff`, `ιHeart_obj_mem`	12
Total	18

CategoryTheory.Triangulated.TStructure

Definitions

Name	Category	Theorems
`Heart` 📖	CompData	—
`hasHeartFullSubcategory` 📖	CompOp	—
`heart` 📖	CompOp	4 math math: `essImage_ιHeart`, `ιHeart_obj_mem`, `mem_heart_iff`, `Heart.essImage_eq_heart`
`instIsClosedUnderIsomorphismsHeart` 📖	CompOp	—
`ιHeart` 📖	CompOp	7 math math: `essImage_ιHeart`, `instFullιHeart`, `instFaithfulιHeart`, `ιHeart_obj_mem`, `instAdditiveιHeart`, `instIsGEObjιHeartOfNatInt`, `instIsLEObjιHeartOfNatInt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essImage_ιHeart` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.essImage` `ιHeart` `heart`	—	`Heart.essImage_eq_heart`
`instAdditiveιHeart` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.Additive` `ιHeart`	—	`Heart.additive_ι`
`instFaithfulιHeart` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.Faithful` `ιHeart`	—	`Heart.faithful_ι`
`instFullιHeart` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.Full` `ιHeart`	—	`Heart.full_ι`
`instIsGEObjιHeartOfNatInt` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsGE` `CategoryTheory.Functor.obj` `ιHeart`	—	`ιHeart_obj_mem`
`instIsLEObjιHeartOfNatInt` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`IsLE` `CategoryTheory.Functor.obj` `ιHeart`	—	`ιHeart_obj_mem`
`mem_heart_iff` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`heart` `IsLE` `IsGE`	—	—
`ιHeart_obj_mem` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`heart` `CategoryTheory.Functor.obj` `ιHeart`	—	`essImage_ιHeart` `CategoryTheory.Functor.obj_mem_essImage`

CategoryTheory.Triangulated.TStructure.Heart

Definitions

Name	Category	Theorems
`ι` 📖	CompOp	4 math math: `additive_ι`, `full_ι`, `faithful_ι`, `essImage_eq_heart`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`additive_ι` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.Additive` `ι`	—	—
`essImage_eq_heart` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.essImage` `ι` `CategoryTheory.Triangulated.TStructure.heart`	—	—
`faithful_ι` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.Faithful` `ι`	—	—
`full_ι` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.Functor.Full` `ι`	—	—

---

← Back to Index