refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881

joelriou · 2025-09-22T14:07:26Z

This PR renames ClosedUnderLimitsOfShape as ObjectProperty.IsClosedUnderLimitsOfShape, and make it a typeclass.

The stability condition of a property P by (co)limits of shape J is now expressed as P.colimitsOfShape J ≤ P. This facilitates the connection with the relatively new API ColimitPresentation #29382 (and the related ObjectProperty.ColimitOfShape).

By using a typeclass for the stability condition, it will be possible to add instances HasLimitsOfShape instances for fullsubcategories.

This also makes the design more parallel to what we have for the stability under (co)limits of MorphismProperty.

…-limits-of-shape

…its-of-shape

github-actions · 2025-09-22T14:08:38Z

PR summary 0d837987e5

Import changes exceeding 2%

%	File
+40.57%	`Mathlib.CategoryTheory.Limits.FullSubcategory`
+4.75%	`Mathlib.CategoryTheory.Monoidal.Cartesian.Basic`
+3.25%	`Mathlib.CategoryTheory.Subobject.MonoOver`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.FullSubcategory	456	641	+185 (+40.57%)
Mathlib.CategoryTheory.Monoidal.Cartesian.Basic	652	683	+31 (+4.75%)
Mathlib.CategoryTheory.Subobject.MonoOver	676	698	+22 (+3.25%)
Mathlib.CategoryTheory.Limits.Indization.Equalizers	745	751	+6 (+0.81%)
Mathlib.CategoryTheory.Limits.Indization.Category	778	784	+6 (+0.77%)
Mathlib.CategoryTheory.Limits.MorphismProperty	767	772	+5 (+0.65%)

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`	5
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`	6
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`	8
6 files `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal`	9
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback`	11
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`	12
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`	13
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`	14
`Mathlib.Algebra.Category.CommAlgCat.Monoidal` `Mathlib.Algebra.Category.CommBialgCat`	15
3 files `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory`	16
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`	18
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`	19
3 files `Mathlib.CategoryTheory.Monoidal.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Grp_` `Mathlib.CategoryTheory.Preadditive.CommGrp_`	20
`Mathlib.CategoryTheory.Closed.Ideal`	21
4 files `Mathlib.CategoryTheory.ChosenFiniteProducts.Over` `Mathlib.CategoryTheory.Monoidal.Cartesian.Over` `Mathlib.CategoryTheory.Subobject.MonoOver` `Mathlib.CategoryTheory.Subterminal`	22
`Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_`	28
`Mathlib.CategoryTheory.Category.Cat.CartesianClosed`	29
3 files `Mathlib.CategoryTheory.Closed.Cartesian` `Mathlib.CategoryTheory.Closed.Functor` `Mathlib.CategoryTheory.Closed.Zero`	30
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`	31
`Mathlib.CategoryTheory.Limits.FullSubcategory`	185

Declarations diff

+ ColimitOfShape.prop
+ IsClosedUnderColimitsOfShape
+ IsClosedUnderColimitsOfShape.mk'
+ IsClosedUnderLimitsOfShape
+ IsClosedUnderLimitsOfShape.mk'
+ LimitOfShape.prop
+ instance : (Over.isMono X).IsClosedUnderLimitsOfShape J
+ 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 [P.RespectsIso] [P.ContainsIdentities] :
+ instance {J : Type v} [HasLimitsOfShape (Discrete J) C] :
+ instance {J : Type v} [SmallCategory J] [IsFiltered J] :
+ isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair
+ prop_colimit
+ prop_limit
+ prop_of_isColimit
+ prop_of_isLimit
- 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).

…y-closed-under-limits-of-shape

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

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

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

…tation

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

…tation

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

mathlib4-dependent-issues-bot · 2025-10-13T08:51:53Z

This PR/issue depends on:

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

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

Mathlib/CategoryTheory/Limits/Indization/Category.lean

jcommelin · 2025-10-16T07:42:08Z

Could you please provide a bit more motivation? E.g. the diff is positive. It doesn't look like this makes many things shorter... (maybe in the future?)
And the large import?

Mathlib.CategoryTheory.Limits.FullSubcategory 	456 	641 	+185 (+40.57%)

seems quite substantial.

joelriou · 2025-10-16T17:06:09Z

I have added some arguments in the description above.

Apart from the setup of the basic API, the diff is mostly neutral (some lemmas are replaced by instances, which is overall a convenience for downstream applications). Part of the reason the imports of Limits.FullSubcategory are increased is that the code which was in this file was moved to the imported files ObjectProperty.(Co)limitsOfShape, and otherwise some basic API has been added.

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

joelriou added 12 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

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

f2e0f5c

…its-of-shape

wip

d328e58

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

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 22, 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 22, 2025

joelriou and others added 13 commits September 22, 2025 17:10

fixing the build

f7f1478

fix

2b7b1ce

fixing the build

d3c4a13

chore(CategoryTheory): split Limits.Presentation

57c6400

added comment

14ca7ef

fix

43c5d3b

updated Mathlib.lean

d8abdda

wip

4a16754

Merge branch 'split-limits-presentation' into refactor-object-propert…

ebfbf0b

…y-closed-under-limits-of-shape

Update Mathlib/CategoryTheory/Limits/Presentation.lean

98b8c68

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

Update Mathlib/CategoryTheory/Limits/Presentation.lean

733dbd9

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

Update Mathlib/CategoryTheory/Limits/Presentation.lean

3c9f5e8

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

Update Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean

cfa5139

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

joelriou mentioned this pull request Oct 5, 2025

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

Open

13 tasks

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

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 5, 2025

joelriou mentioned this pull request Oct 5, 2025

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

Open

13 tasks

joelriou added 3 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

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

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

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

7412fde

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

joelriou commented Oct 13, 2025

View reviewed changes

Mathlib/CategoryTheory/Limits/Indization/Category.lean Show resolved Hide resolved

Apply suggestion from @joelriou

6ec9b89

joelriou removed the WIP Work in progress label Oct 13, 2025

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 16, 2025

fix

6da7d95

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 16, 2025

joelriou added 2 commits October 16, 2025 19:47

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

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!

refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881

refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881

Uh oh!

joelriou commented Sep 22, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Sep 22, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

mathlib4-dependent-issues-bot commented Oct 13, 2025

Uh oh!

Uh oh!

jcommelin commented Oct 16, 2025

Uh oh!

joelriou commented Oct 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881

Are you sure you want to change the base?

refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881

Uh oh!

Conversation

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

Uh oh!

Uh oh!

github-actions bot commented Sep 22, 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-merge-conflict-bot commented Oct 5, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Oct 13, 2025

Uh oh!

Uh oh!

jcommelin commented Oct 16, 2025

Uh oh!

joelriou commented Oct 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

joelriou commented Sep 22, 2025 •

edited

Loading

github-actions bot commented Sep 22, 2025 •

edited

Loading