Commit 2025-07-23 11:06 da5d6e78

View on Github →

refactor(CategoryTheory): redefine triangulated subcategories using ObjectProperty (#25931)

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

added def HomotopyCategory.subcategoryAcyclic

Modified Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean

Modified Mathlib/CategoryTheory/ObjectProperty/Shift.lean

added theorem CategoryTheory.ObjectProperty.le_shift

added theorem CategoryTheory.ObjectProperty.prop_shift_iff_of_isStableUnderShift

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

modified def CategoryTheory.Functor.homologicalKernel

deleted theorem CategoryTheory.Functor.mem_homologicalKernel_W_iff

modified theorem CategoryTheory.Functor.mem_homologicalKernel_iff

added theorem CategoryTheory.Functor.mem_homologicalKernel_trW_iff

Modified Mathlib/CategoryTheory/Triangulated/Subcategory.lean

added theorem CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.mk'

added theorem CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk'

added theorem CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.mk'

added theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁'

added theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁

added theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂'

added theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂

added theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃'

added theorem CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃

added theorem CategoryTheory.ObjectProperty.smul_mem_trW_iff

added theorem CategoryTheory.ObjectProperty.trW.mk'

added theorem CategoryTheory.ObjectProperty.trW.mk

added theorem CategoryTheory.ObjectProperty.trW.shift

added theorem CategoryTheory.ObjectProperty.trW.unshift

added def CategoryTheory.ObjectProperty.trW

added theorem CategoryTheory.ObjectProperty.trW_iff'

added theorem CategoryTheory.ObjectProperty.trW_iff

added theorem CategoryTheory.ObjectProperty.trW_iff_of_distinguished

added theorem CategoryTheory.ObjectProperty.trW_isoClosure

added theorem CategoryTheory.ObjectProperty.trW_of_isIso

deleted theorem CategoryTheory.Triangulated.Subcategory.W.mk'

deleted theorem CategoryTheory.Triangulated.Subcategory.W.mk

deleted theorem CategoryTheory.Triangulated.Subcategory.W.shift

deleted theorem CategoryTheory.Triangulated.Subcategory.W.unshift

deleted def CategoryTheory.Triangulated.Subcategory.W

deleted theorem CategoryTheory.Triangulated.Subcategory.W_iff'

deleted theorem CategoryTheory.Triangulated.Subcategory.W_iff

deleted theorem CategoryTheory.Triangulated.Subcategory.W_of_isIso

deleted theorem CategoryTheory.Triangulated.Subcategory.ext₁'

deleted theorem CategoryTheory.Triangulated.Subcategory.ext₁

deleted theorem CategoryTheory.Triangulated.Subcategory.ext₂

deleted theorem CategoryTheory.Triangulated.Subcategory.ext₃'

deleted theorem CategoryTheory.Triangulated.Subcategory.ext₃

deleted def CategoryTheory.Triangulated.Subcategory.isoClosure

deleted theorem CategoryTheory.Triangulated.Subcategory.isoClosure_W

deleted theorem CategoryTheory.Triangulated.Subcategory.mem_W_iff_of_distinguished

deleted def CategoryTheory.Triangulated.Subcategory.mk'

deleted theorem CategoryTheory.Triangulated.Subcategory.smul_mem_W_iff

deleted theorem CategoryTheory.Triangulated.Subcategory.zero

deleted structure CategoryTheory.Triangulated.Subcategory