Commit 2024-05-15 11:20 880c4cb8

View on Github →

feat(CategoryTheory/Triangulated): t-structures (#12619) This PR defines t-structures on (pre)triangulated categories.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Shift/Predicate.lean

added def CategoryTheory.PredicateShift

added theorem CategoryTheory.predicateShift_iff

added theorem CategoryTheory.predicateShift_predicateShift

added theorem CategoryTheory.predicateShift_zero

Created Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean

added theorem CategoryTheory.Triangulated.TStructure.GE_antitone

added theorem CategoryTheory.Triangulated.TStructure.LE_monotone

added theorem CategoryTheory.Triangulated.TStructure.exists_triangle

added theorem CategoryTheory.Triangulated.TStructure.mem_of_isGE

added theorem CategoryTheory.Triangulated.TStructure.mem_of_isLE

added theorem CategoryTheory.Triangulated.TStructure.predicateShift_GE

added theorem CategoryTheory.Triangulated.TStructure.predicateShift_LE

added structure CategoryTheory.Triangulated.TStructure

Modified docs/references.bib