Commit 2024-04-18 09:26 94860b32

View on Github →

feat(CategoryTheory): triangulated subcategories (#11740) This PR defines the type Triangulated.Subcategory C when C is a pretriangulated category. It also introduces a type class CategoryTheory.ClosedUnderIsomorphisms for a predicate on objects in a category C.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ClosedUnderIsomorphisms.lean

added def CategoryTheory.isoClosure

added theorem CategoryTheory.isoClosure_eq_self

added theorem CategoryTheory.isoClosure_le_iff

added theorem CategoryTheory.le_isoClosure

added theorem CategoryTheory.mem_iff_of_isIso

added theorem CategoryTheory.mem_iff_of_iso

added theorem CategoryTheory.mem_isoClosure

added theorem CategoryTheory.mem_isoClosure_iff

added theorem CategoryTheory.mem_of_isIso

added theorem CategoryTheory.mem_of_iso

added theorem CategoryTheory.monotone_isoClosure

Created Mathlib/CategoryTheory/Triangulated/Subcategory.lean

added theorem CategoryTheory.Triangulated.Subcategory.ext₂

added def CategoryTheory.Triangulated.Subcategory.isoClosure

added def CategoryTheory.Triangulated.Subcategory.mk'

added structure CategoryTheory.Triangulated.Subcategory