Commit 2025-02-26 09:05 f598df38

View on Github →

refactor(CategoryTheory): introduce ObjectProperty (#22286) An abbreviation ObjectProperty C for predicates on objects of a category C is introduced in the file CategoryTheory.ObjectProperty.Basic. The file CategoryTheory.ClosedUnderIsomorphisms is moved to ObjectProperty.ClosedUnderIsomorphisms.

Estimated changes

Modified Mathlib.lean

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

Deleted Mathlib/CategoryTheory/ClosedUnderIsomorphisms.lean

deleted def CategoryTheory.isoClosure

deleted theorem CategoryTheory.isoClosure_eq_self

deleted theorem CategoryTheory.isoClosure_le_iff

deleted theorem CategoryTheory.le_isoClosure

deleted theorem CategoryTheory.mem_iff_of_isIso

deleted theorem CategoryTheory.mem_iff_of_iso

deleted theorem CategoryTheory.mem_isoClosure

deleted theorem CategoryTheory.mem_isoClosure_iff

deleted theorem CategoryTheory.mem_of_isIso

deleted theorem CategoryTheory.mem_of_iso

deleted theorem CategoryTheory.monotone_isoClosure

Modified Mathlib/CategoryTheory/Limits/FullSubcategory.lean

modified theorem CategoryTheory.Limits.closedUnderColimitsOfShape_of_colimit

modified theorem CategoryTheory.Limits.closedUnderLimitsOfShape_of_limit

Modified Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

Modified Mathlib/CategoryTheory/Localization/Bousfield.lean

modified theorem CategoryTheory.Localization.LeftBousfield.W_isoClosure

Created Mathlib/CategoryTheory/ObjectProperty/Basic.lean

Created Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean

added def CategoryTheory.ObjectProperty.isoClosure

added theorem CategoryTheory.ObjectProperty.isoClosure_eq_self

added theorem CategoryTheory.ObjectProperty.isoClosure_le_iff

added theorem CategoryTheory.ObjectProperty.le_isoClosure

added theorem CategoryTheory.ObjectProperty.monotone_isoClosure

added theorem CategoryTheory.ObjectProperty.prop_iff_of_isIso

added theorem CategoryTheory.ObjectProperty.prop_iff_of_iso

added theorem CategoryTheory.ObjectProperty.prop_isoClosure

added theorem CategoryTheory.ObjectProperty.prop_isoClosure_iff

added theorem CategoryTheory.ObjectProperty.prop_of_isIso

added theorem CategoryTheory.ObjectProperty.prop_of_iso

Created Mathlib/CategoryTheory/ObjectProperty/Shift.lean

added theorem CategoryTheory.ObjectProperty.prop_shift_iff

added def CategoryTheory.ObjectProperty.shift

added theorem CategoryTheory.ObjectProperty.shift_shift

added theorem CategoryTheory.ObjectProperty.shift_zero

Deleted Mathlib/CategoryTheory/Shift/Predicate.lean

deleted def CategoryTheory.PredicateShift

deleted theorem CategoryTheory.predicateShift_iff

deleted theorem CategoryTheory.predicateShift_predicateShift

deleted theorem CategoryTheory.predicateShift_zero

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Modified Mathlib/CategoryTheory/Triangulated/Subcategory.lean

modified theorem CategoryTheory.Triangulated.Subcategory.ext₁

modified theorem CategoryTheory.Triangulated.Subcategory.ext₂

modified theorem CategoryTheory.Triangulated.Subcategory.ext₃

modified theorem CategoryTheory.Triangulated.Subcategory.zero

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

deleted theorem CategoryTheory.Triangulated.TStructure.GE_antitone

deleted theorem CategoryTheory.Triangulated.TStructure.LE_monotone

added theorem CategoryTheory.Triangulated.TStructure.ge_antitone

added theorem CategoryTheory.Triangulated.TStructure.ge_of_isGE

added theorem CategoryTheory.Triangulated.TStructure.le_monotone

added theorem CategoryTheory.Triangulated.TStructure.le_of_isLE

deleted theorem CategoryTheory.Triangulated.TStructure.mem_of_isGE

deleted theorem CategoryTheory.Triangulated.TStructure.mem_of_isLE

deleted theorem CategoryTheory.Triangulated.TStructure.predicateShift_GE

deleted theorem CategoryTheory.Triangulated.TStructure.predicateShift_LE

added theorem CategoryTheory.Triangulated.TStructure.shift_ge

added theorem CategoryTheory.Triangulated.TStructure.shift_le