Commit 2024-06-04 08:15 fe15e6bd

View on Github →

feat(CategoryTheory): the class of morphisms whose cone belongs to a triangulated subcategory (#11789) Given S : Triangulated.Subcategory C, we introduce S.W : MorphismProperty C. A morphism belongs to S.W iff its cone satisfies the predicate S.P. We show that S.W has both a calculus of left and right fractions.

Estimated changes

Modified Mathlib/CategoryTheory/Triangulated/Subcategory.lean

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

added theorem CategoryTheory.Triangulated.Subcategory.W.mk

added theorem CategoryTheory.Triangulated.Subcategory.W.shift

added theorem CategoryTheory.Triangulated.Subcategory.W.unshift

added def CategoryTheory.Triangulated.Subcategory.W

added theorem CategoryTheory.Triangulated.Subcategory.W_iff'

added theorem CategoryTheory.Triangulated.Subcategory.W_iff

added theorem CategoryTheory.Triangulated.Subcategory.W_of_isIso

added theorem CategoryTheory.Triangulated.Subcategory.ext₁'

added theorem CategoryTheory.Triangulated.Subcategory.ext₁

added theorem CategoryTheory.Triangulated.Subcategory.ext₃'

added theorem CategoryTheory.Triangulated.Subcategory.ext₃

added theorem CategoryTheory.Triangulated.Subcategory.isoClosure_W

added theorem CategoryTheory.Triangulated.Subcategory.mem_W_iff_of_distinguished

added theorem CategoryTheory.Triangulated.Subcategory.respectsIso_W

added theorem CategoryTheory.Triangulated.Subcategory.smul_mem_W_iff

added theorem CategoryTheory.Triangulated.Subcategory.zero