refactor(CategoryTheory): introduce ObjectProperty

[joelriou]

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.

---

[github-actions]

PR summary f4b7c2bd4b

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.ClosedUnderIsomorphisms	279	0	-279 (-100.00%)
Mathlib.CategoryTheory.Shift.Predicate	472	0	-472 (-100.00%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Shift.Predicate	-472
Mathlib.CategoryTheory.ClosedUnderIsomorphisms	-279
181 files Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks	1
Mathlib.CategoryTheory.ObjectProperty.Basic (new file)	266
Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (new file)	280
Mathlib.CategoryTheory.ObjectProperty.Shift (new file)	473

---

Declarations diff

+ IsClosedUnderIsomorphisms
+ ObjectProperty
+ ge_antitone
+ ge_of_isGE
+ instance (a : A) [P.IsClosedUnderIsomorphisms] :
+ instance : (mk' P zero shift ext₂).P.IsClosedUnderIsomorphisms
+ instance : (subcategoryAcyclic C).P.IsClosedUnderIsomorphisms := by
+ instance : IsClosedUnderIsomorphisms (isoClosure P)
+ instance : ObjectProperty.IsClosedUnderIsomorphisms (IsIndObject (C := C))
+ instance : S.isoClosure.P.IsClosedUnderIsomorphisms := by
+ instance [F.IsHomological] : F.homologicalKernel.P.IsClosedUnderIsomorphisms := by
+ le_monotone
+ le_of_isLE
+ prop_iff_of_isIso
+ prop_iff_of_iso
+ prop_isoClosure
+ prop_isoClosure_iff
+ prop_of_isIso
+ prop_of_iso
+ prop_shift_iff
+ shift
+ shift_ge
+ shift_le
+ shift_shift
+ shift_zero
- instance : ClosedUnderIsomorphisms (IsIndObject (C := C))
- instance : ClosedUnderIsomorphisms (isoClosure P)
- instance : ClosedUnderIsomorphisms (mk' P zero shift ext₂).P
- instance : ClosedUnderIsomorphisms (subcategoryAcyclic C).P := by
- instance : ClosedUnderIsomorphisms S.isoClosure.P := by
- instance [F.IsHomological] : ClosedUnderIsomorphisms F.homologicalKernel.P := by
- predicateShift_closedUnderIsomorphisms

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[TwoFX]

Hmm, there is a question about naming here, or more specifically about capitalization. Things of type C → Prop should start with a capital letter according to the naming convention, while things of type Set C start with a small letter. Morphism properties start with small letters, which I think is a good convention, so I think object properties should start with a small letter as well. In this case, a good new name for PredicateShift might be ObjectProperty.shift. What do you think?

If you agree but want to keep the diff small, feel to mark this as a TODO for future cleanup.

Similar questions apply to Triangulated.Subcategory.P and TStructure.LE/TStructure.GE , and also IsIndObject (which I will make into an object property once this PR is merged).

[joelriou]

Here, I also prefer the small letter convention, which I shall implement for PredicateShift (as ObjectProperty.shift) and TStructure.le/ge. (For triangulated subcategories, a slightly more significant refactor is necessary; which I shall do later on. And for ind-objects, I am happy to let you do it.)