feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854

joelriou · 2025-09-21T12:39:41Z

In this PR, given a property P of objects in a category C and family of categories J : α → Type _, we introduce the closure P.limitsClosure J of P under limits of shapes J a for all a : α, and under certain smallness circumstances, we show that its essentially small.

depends on: [Merged by Bors] - feat(CategoryTheory): limits of objects satisfying a property #29851
depends on: refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881
depends on: [Merged by Bors] - chore(CategoryTheory): split Limits.Presentation #29903
depends on: [Merged by Bors] - feat(CategoryTheory): limit presentations #29849
depends on: [Merged by Bors] - feat(CategoryTheory): colimits of objects satisfying a property #29843

…-limits-of-shape

github-actions · 2025-09-21T12:40:49Z

PR summary 0d837987e5

Import changes exceeding 2%

%	File
+42.76%	`Mathlib.CategoryTheory.Limits.FullSubcategory`
+4.91%	`Mathlib.CategoryTheory.Monoidal.Cartesian.Basic`
+4.53%	`Mathlib.CategoryTheory.ObjectProperty.Small`
+3.40%	`Mathlib.CategoryTheory.Subobject.MonoOver`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.FullSubcategory	456	651	+195 (+42.76%)
Mathlib.CategoryTheory.Monoidal.Cartesian.Basic	652	684	+32 (+4.91%)
Mathlib.CategoryTheory.ObjectProperty.Small	397	415	+18 (+4.53%)
Mathlib.CategoryTheory.Subobject.MonoOver	676	699	+23 (+3.40%)
Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape	639	649	+10 (+1.56%)
Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape	639	649	+10 (+1.56%)
Mathlib.CategoryTheory.Limits.Indization.Equalizers	745	752	+7 (+0.94%)
Mathlib.CategoryTheory.Limits.Indization.Category	778	785	+7 (+0.90%)
Mathlib.CategoryTheory.Limits.MorphismProperty	767	773	+6 (+0.78%)

Import changes for all files

Files	Import difference
78 files `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `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.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `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.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.AlgebraicTopology.RelativeCellComplex.Basic` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject` `Mathlib.CategoryTheory.Limits.Constructions.Over.Basic` `Mathlib.CategoryTheory.Limits.MorphismProperty` `Mathlib.CategoryTheory.MorphismProperty.FunctorCategory` `Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting` `Mathlib.CategoryTheory.SmallObject.TransfiniteIteration` `Mathlib.Topology.CWComplex.Abstract.Basic`	6
65 files `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Homology.GrothendieckAbelian` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic` `Mathlib.CategoryTheory.Abelian.Indization` `Mathlib.CategoryTheory.Category.Cat.Colimit` `Mathlib.CategoryTheory.Closed.Types` `Mathlib.CategoryTheory.Comma.Final` `Mathlib.CategoryTheory.Distributive.Cartesian` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal` `Mathlib.CategoryTheory.Filtered.Final` `Mathlib.CategoryTheory.Generator.Indization` `Mathlib.CategoryTheory.Limits.Constructions.Over.Connected` `Mathlib.CategoryTheory.Limits.FinallySmall` `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.Preserves.Shapes.Preorder` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous` `Mathlib.CategoryTheory.Limits.Sifted` `Mathlib.CategoryTheory.Preadditive.Indization` `Mathlib.CategoryTheory.Sites.Monoidal` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.Condensed.AB` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.Epi` `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.Limits` `Mathlib.Condensed.Module` `Mathlib.Condensed.Solid` `Mathlib.Order.Interval.Set.Final` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.Profinite.Extend`	7
18 files `Mathlib.RepresentationTheory.GroupCohomology.Basic` `Mathlib.RepresentationTheory.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.GroupCohomology.Resolution` `Mathlib.RepresentationTheory.Homological.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro` `Mathlib.RepresentationTheory.Homological.GroupHomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro` `Mathlib.RepresentationTheory.Homological.Resolution`	9
8 files `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape` `Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape`	10
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback`	12
31 files `Mathlib.Algebra.Category.Grp.CartesianMonoidal` `Mathlib.Algebra.Category.Grp.ChosenFiniteProducts` `Mathlib.Algebra.Category.Grp.LeftExactFunctor` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.Module.PID` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.FieldTheory.Galois.NormalBasis` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.Coinduced` `Mathlib.RepresentationTheory.Coinvariants` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.FiniteIndex` `Mathlib.RepresentationTheory.Induced` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Rep` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.Regular.Category` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `Mathlib.Topology.Category.Profinite.Nobeling.Successor` `Mathlib.Topology.Category.Profinite.Nobeling`	13
7 files `Mathlib.CategoryTheory.Action.Monoidal` `Mathlib.CategoryTheory.Generator.Sheaf` `Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_` `Mathlib.CategoryTheory.Sites.CartesianClosed` `Mathlib.CategoryTheory.Sites.CartesianMonoidal` `Mathlib.CategoryTheory.Sites.ChosenFiniteProducts`	14
20 files `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.AlgebraicTopology.MooreComplex`	15
`Mathlib.Algebra.Category.CommAlgCat.Monoidal` `Mathlib.Algebra.Category.CommBialgCat`	16
3 files `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory`	17
`Mathlib.CategoryTheory.ObjectProperty.Small`	18
13 files `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.CategoryTheory.Abelian.Injective.Basic` `Mathlib.CategoryTheory.Abelian.Injective.Dimension` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Dimension` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Noetherian` `Mathlib.CategoryTheory.Subobject.ArtinianObject` `Mathlib.CategoryTheory.Subobject.NoetherianObject`	19
125 files `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.Augment` `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Algebra.Homology.DerivedCategory.Fractions` `Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.DerivedCategory.Linear` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.DerivedCategory.TStructure` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Algebra.Homology.Double` `Mathlib.Algebra.Homology.Embedding.AreComplementary` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Algebra.Homology.Embedding.CochainComplex` `Mathlib.Algebra.Homology.Embedding.Connect` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Algebra.Homology.Embedding.Extend` `Mathlib.Algebra.Homology.Embedding.HomEquiv` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.Algebra.Homology.Embedding.RestrictionHomology` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.Embedding.StupidTrunc` `Mathlib.Algebra.Homology.Embedding.TruncGEHomology` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Homology.Embedding.TruncLEHomology` `Mathlib.Algebra.Homology.Embedding.TruncLE` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Homology.Functor` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.Algebra.Homology.Linear` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Algebra.Homology.Single` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.CategoryTheory.Abelian.Injective.Resolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Projective.Resolution` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Bicategory.CatEnriched` `Mathlib.CategoryTheory.Closed.Enrichment` `Mathlib.CategoryTheory.Closed.FunctorCategory.Basic` `Mathlib.CategoryTheory.Closed.FunctorToTypes` `Mathlib.CategoryTheory.Dialectica.Basic` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.Enriched.Basic` `Mathlib.CategoryTheory.Enriched.EnrichedCat` `Mathlib.CategoryTheory.Enriched.FunctorCategory` `Mathlib.CategoryTheory.Enriched.HomCongr` `Mathlib.CategoryTheory.Enriched.Opposite` `Mathlib.CategoryTheory.Enriched.Ordinary.Basic` `Mathlib.CategoryTheory.ExtremalEpi` `Mathlib.CategoryTheory.Functor.FunctorHom` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Generator.HomologicalComplex` `Mathlib.CategoryTheory.Generator.Preadditive` `Mathlib.CategoryTheory.Generator.Presheaf` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_` `Mathlib.CategoryTheory.Monoidal.Functor.Types` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Monoidal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Types.Coyoneda` `Mathlib.CategoryTheory.Preadditive.Injective.Resolution` `Mathlib.CategoryTheory.Preadditive.Projective.Resolution` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.Simple` `Mathlib.CategoryTheory.Subobject.Basic` `Mathlib.CategoryTheory.Subobject.Comma` `Mathlib.CategoryTheory.Subobject.FactorThru` `Mathlib.CategoryTheory.Subobject.HasCardinalLT` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.CategoryTheory.Subobject.Limits` `Mathlib.CategoryTheory.Subobject.Presheaf` `Mathlib.CategoryTheory.Subobject.Types` `Mathlib.CategoryTheory.Subobject.WellPowered` `Mathlib.CategoryTheory.Subpresheaf.Subobject` `Mathlib.CategoryTheory.Topos.Classifier`	20
3 files `Mathlib.CategoryTheory.Monoidal.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Grp_` `Mathlib.CategoryTheory.Preadditive.CommGrp_`	21
`Mathlib.CategoryTheory.Closed.Ideal`	22
4 files `Mathlib.CategoryTheory.ChosenFiniteProducts.Over` `Mathlib.CategoryTheory.Monoidal.Cartesian.Over` `Mathlib.CategoryTheory.Subobject.MonoOver` `Mathlib.CategoryTheory.Subterminal`	23
`Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_`	29
`Mathlib.CategoryTheory.Category.Cat.CartesianClosed`	30
3 files `Mathlib.CategoryTheory.Closed.Cartesian` `Mathlib.CategoryTheory.Closed.Functor` `Mathlib.CategoryTheory.Closed.Zero`	31
11 files `Mathlib.CategoryTheory.ChosenFiniteProducts.Cat` `Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice` `Mathlib.CategoryTheory.ChosenFiniteProducts` `Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian` `Mathlib.CategoryTheory.Monoidal.Cartesian.Basic` `Mathlib.CategoryTheory.Monoidal.Cartesian.Cat` `Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_` `Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic` `Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric`	32
`Mathlib.CategoryTheory.Limits.FullSubcategory`	195
`Mathlib.CategoryTheory.ObjectProperty.CompleteLattice` (new file)	400
`Mathlib.CategoryTheory.ObjectProperty.LimitsClosure` (new file)	889

Declarations diff

+ ColimitOfShape.prop
+ EssentiallySmall
+ EssentiallySmall.exists_small
+ EssentiallySmall.exists_small_le
+ EssentiallySmall.of_le
+ IsClosedUnderColimitsOfShape
+ IsClosedUnderColimitsOfShape.mk'
+ IsClosedUnderLimitsOfShape
+ IsClosedUnderLimitsOfShape.mk'
+ LimitOfShape.prop
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+ instance (a : α) : (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a)
+ instance : (Over.isMono X).IsClosedUnderLimitsOfShape J
+ instance : (P.limitsClosure J).IsClosedUnderIsomorphisms
+ instance [HasColimitsOfShape J C] [PreservesColimitsOfShape J F] [F.Full] [F.Faithful] :
+ instance [HasLimitsOfShape J C] [PreservesLimitsOfShape J F] [F.Full] [F.Faithful] :
+ instance [HasPullbacks T] [P.IsStableUnderComposition]
+ instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+ instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [LocallySmall.{w} J] :
+ instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [P.RespectsIso] [P.ContainsIdentities] :
+ instance [∀ a, (P a).IsClosedUnderIsomorphisms] :
+ instance {J : Type v} [HasLimitsOfShape (Discrete J) C] :
+ instance {J : Type v} [SmallCategory J] [IsFiltered J] :
+ instance {P Q : ObjectProperty C}
+ instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} P] :
+ instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} P] [ObjectProperty.Small.{w} Q] :
+ instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] :
+ isClosedUnderIsomorphisms_iff_isoClosure_eq_self
+ isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair
+ isEssentiallySmall_limitsClosure
+ isoClosure_iSup
+ isoClosure_strictLimitsClosureIter_eq_limitsClosure
+ isoClosure_sup
+ le_limitsClosure
+ le_strictLimitsClosureIter
+ le_strictLimitsClosureStep
+ limitsClosure
+ limitsClosure_isoClosure
+ limitsClosure_le
+ limitsClosure_monotone
+ prop_colimit
+ prop_iSup_iff
+ prop_inf_iff
+ prop_limit
+ prop_of_isColimit
+ prop_of_isLimit
+ prop_sup_iff
+ strictLimitsClosureIter
+ strictLimitsClosureIter_le_limitsClosure
+ strictLimitsClosureStep
+ strictLimitsClosureStep_monotone
+ strictLimitsClosureStep_strictLimitsClosureIter_eq_self
++ instance {α : Type*} (P : α → ObjectProperty C)
- ClosedUnderColimitsOfShape.essImage
- ClosedUnderLimitsOfShape.essImage
- closedUnderLimitsOfShape_isMono
- instCartesianMonoidalCategory

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).

mathlib4-dependent-issues-bot · 2025-09-21T12:43:54Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory): limits of objects satisfying a property #29851~~
refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881
~~[Merged by Bors] - chore(CategoryTheory): split Limits.Presentation #29903~~
~~[Merged by Bors] - feat(CategoryTheory): limit presentations #29849~~
~~[Merged by Bors] - feat(CategoryTheory): colimits of objects satisfying a property #29843~~
By Dependent Issues (🤖). Happy coding!

…its-of-shape

…its-closure

mathlib4-merge-conflict-bot · 2025-10-05T15:42:29Z

This pull request has conflicts, please merge master and resolve them.

…tation

…refactor-object-property-closed-under-limits-of-shape

…under-limits-of-shape' into object-property-limits-closure

mathlib4-merge-conflict-bot · 2025-10-08T10:53:29Z

This pull request has conflicts, please merge master and resolve them.

…tation

…refactor-object-property-closed-under-limits-of-shape

…under-limits-of-shape' into object-property-limits-closure

…its-closure

…perty-closed-under-limits-of-shape

…under-limits-of-shape' into object-property-limits-closure

joelriou added 11 commits September 20, 2025 23:20

feat(CategoryTheory): colimits of objects satisfying a property

0757d2d

fix

d6676bd

typo

a57afac

fix

31376ce

better syntax

fd70884

typo

73661c2

fixing imports

41d6537

feat(CategoryTheory): limit presentations

89f7db3

Merge branch 'object-property-colimits-of-shape' into object-property…

34da8ad

…-limits-of-shape

wip

627eb98

feat(CategoryTheory/ObjectProperty): closure under limits

35c1354

joelriou added WIP Work in progress t-category-theory Category theory labels Sep 21, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 21, 2025

typo

581970c

github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 21, 2025

joelriou added 4 commits September 21, 2025 16:17

wip

6b20d72

wip

b5c6c94

Merge remote-tracking branch 'origin/master' into object-property-lim…

f2e0f5c

…its-of-shape

Merge remote-tracking branch 'origin/master' into object-property-lim…

d940d3b

…its-closure

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 22, 2025

joelriou added 7 commits September 22, 2025 06:56

wip

54e8d01

wip

796f4b0

wip

d912563

wip

71eea38

generalising universes

01df6fa

wip

d328e58

fixing the build

f7f1478

This was referenced Oct 3, 2025

feat(CategoryTheory): closure under bounded colimits #30168

Open

feat(CategoryTheory): locally presentable categories and strong generators #30241

Open

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 5, 2025

joelriou added 2 commits October 5, 2025 18:02

Merge remote-tracking branch 'origin/master' into split-limits-presen…

5aea955

…tation

Merge remote-tracking branch 'origin/split-limits-presentation' into …

fba5a70

…refactor-object-property-closed-under-limits-of-shape

joelriou mentioned this pull request Oct 5, 2025

feat(CategoryTheory): categories of presheaves are locally presentable #30247

Open

13 tasks

Merge remote-tracking branch 'origin/refactor-object-property-closed-…

45cb05f

…under-limits-of-shape' into object-property-limits-closure

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 6, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 8, 2025

joelriou added 4 commits October 8, 2025 19:51

Merge remote-tracking branch 'origin/master' into split-limits-presen…

e585c37

…tation

Merge remote-tracking branch 'origin/master' into split-limits-presen…

854a78b

…tation

Merge remote-tracking branch 'origin/split-limits-presentation' into …

552c1ab

…refactor-object-property-closed-under-limits-of-shape

Merge remote-tracking branch 'origin/refactor-object-property-closed-…

8dd48c2

…under-limits-of-shape' into object-property-limits-closure

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 11, 2025

This was referenced Oct 12, 2025

refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459

Open

feat(CategoryTheory): κ-presentable objects in a κ-accessible category is an essentially small category #30464

Open

joelriou and others added 3 commits October 13, 2025 15:30

Merge remote-tracking branch 'origin/master' into object-property-lim…

52e7c0e

…its-closure

Merge remote-tracking branch 'origin/master' into refactor-object-pro…

7412fde

…perty-closed-under-limits-of-shape

Apply suggestion from @joelriou

6ec9b89

joelriou added 4 commits October 16, 2025 19:04

fix

6da7d95

Merge remote-tracking branch 'origin/master' into refactor-object-pro…

5ed0d36

…perty-closed-under-limits-of-shape

Merge remote-tracking branch 'origin/master' into refactor-object-pro…

a8d9e19

…perty-closed-under-limits-of-shape

Merge remote-tracking branch 'origin/refactor-object-property-closed-…

a5eca07

…under-limits-of-shape' into object-property-limits-closure

joelriou mentioned this pull request Oct 20, 2025

feat(CategoryTheory/Presentable): transport via an equivalence #30731

Open

10 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854

feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854

joelriou commented Sep 21, 2025 •

edited by alreadydone

Loading

Uh oh!

github-actions bot commented Sep 21, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Sep 21, 2025 •

edited

Loading

Uh oh!

mathlib4-merge-conflict-bot commented Oct 5, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854

Are you sure you want to change the base?

feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854

Conversation

joelriou commented Sep 21, 2025 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0d837987e5

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Sep 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Oct 5, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

joelriou commented Sep 21, 2025 •

edited by alreadydone

Loading

github-actions bot commented Sep 21, 2025 •

edited

Loading

mathlib4-dependent-issues-bot commented Sep 21, 2025 •

edited

Loading