[Merged by Bors] - feat(CategoryTheory): abstract argument for the stability under transfinite compositions by joelriou · Pull Request #26030 · leanprover-community/mathlib4

joelriou · 2025-06-17T13:41:51Z

If a class of morphisms is multiplicative, respects isomorphisms and is stable under filtered colimits, then it is stable under transfinite compositions.
(This simplifies the proof in the case of monomorphisms in Grothendieck abelian categories, for isomorphisms, and in #23282, we shall apply this to monomorphisms in Type.)

This PR continues the work from #24777.

Original PR: #24777

…hape a class

…sfinite-composition-argument

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

….lean Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

…sfinite-composition-argument

…ctives.lean

…sfinite-composition-argument

joelriou · 2025-06-17T13:41:53Z

Comments from Original PR #24777

This section contains 2 comment(s) from the original PR, excluding bot comments.

@github-actions (2025-05-11 13:33 UTC):

PR summary 610816e983

Import changes exceeding 2%

%	File
+2.57%	`Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition	738	757	+19 (+2.57%)
Mathlib.CategoryTheory.MorphismProperty.Limits	650	652	+2 (+0.31%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms	1038	1037	-1 (-0.10%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives	1157	1156	-1 (-0.09%)

Import changes for all files

Files	Import difference
6 files `Mathlib.CategoryTheory.Abelian.FreydMitchell` `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`	-1
54 files `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `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.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `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.OpenImmersion` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.CategoryTheory.Limits.MorphismProperty`	1
24 files `Mathlib.Algebra.Homology.Square` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells` `Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.CategoryTheory.Abelian.Monomorphisms` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.MorphismProperty.Descent` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.CategoryTheory.MorphismProperty.RetractArgument` `Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem` `Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.CategoryTheory.Sites.MorphismProperty` `Mathlib.CategoryTheory.SmallObject.Construction` `Mathlib.Topology.Sheaves.MayerVietoris`	2
`Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.SmallObject.TransfiniteIteration`	19

Declarations diff

+ IsStableUnderFilteredColimits
+ IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape
+ colimitsOfShape.of_isColimit
+ instance (j : J) : IsIso (h.incl.app j) := (h.ici j).isIso
+ instance : IsStableUnderFilteredColimits.{w, w'} (isomorphisms C)
+ instance [HasFilteredColimitsOfSize.{v', u'} C] [AB5OfSize.{v', u'} C] :
+ instance {C : Type u} [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{w} C] :
+ instance {i j : J} (f : i ⟶ j) : IsIso (h.F.map f) := ((h.iic j).ici (⟨i, leOfHom f⟩)).isIso
+ mem
+ mem_map_bot_le
++ instance [W.IsMultiplicative] [W.RespectsIso]
- instance (j : J) : IsIso (h.incl.app j)
- instance : (isomorphisms C).IsStableUnderTransfiniteComposition
- instance : IsStableUnderTransfiniteComposition.{w} (monomorphisms C)
- instance {j : J} (g : ⊥ ⟶ j) : IsIso (h.F.map g) := by
- instance {j j' : J} (f : j ⟶ j') : IsIso (h.F.map f)
- map_bot_le
- mono
- mono_map

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

@callesonne (2025-06-01 14:59 UTC):
@erdOne do you want to have a look and/or maintainer merge? :)

github-actions · 2025-06-17T13:43:30Z

PR summary 3f11243a35

Import changes exceeding 2%

%	File
+2.49%	`Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition	763	782	+19 (+2.49%)
Mathlib.CategoryTheory.MorphismProperty.Limits	671	673	+2 (+0.30%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms	962	961	-1 (-0.10%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives	1088	1087	-1 (-0.09%)

Import changes for all files

Files	Import difference
6 files `Mathlib.CategoryTheory.Abelian.FreydMitchell` `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`	-1
56 files `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `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.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `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.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `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.OpenImmersion` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.CategoryTheory.Limits.MorphismProperty`	1
161 files `Mathlib.Algebra.Category.CommAlgCat.FiniteType` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Homology.Square` `Mathlib.AlgebraicTopology.ModelCategory.Basic` `Mathlib.AlgebraicTopology.ModelCategory.Cylinder` `Mathlib.AlgebraicTopology.ModelCategory.Instances` `Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant` `Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick` `Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy` `Mathlib.AlgebraicTopology.ModelCategory.PathObject` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells` `Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.CategoryTheory.Abelian.Monomorphisms` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.MorphismProperty.Descent` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.CategoryTheory.MorphismProperty.RetractArgument` `Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem` `Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.CategoryTheory.Sites.MorphismProperty` `Mathlib.CategoryTheory.SmallObject.Construction` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.Ideal` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.Instances` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Grassmannian` `Mathlib.RingTheory.Ideal.Int` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant.Basic` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.Localization.Free` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Regular.Depth` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Support` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Sheaves.MayerVietoris`	2
`Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.SmallObject.TransfiniteIteration`	19

Declarations diff

+ IsStableUnderFilteredColimits
+ IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape
+ colimitsOfShape.of_isColimit
+ instance (j : J) : IsIso (h.incl.app j) := h.mem_incl_app j
+ instance : IsStableUnderFilteredColimits.{w, w'} (isomorphisms C)
+ instance [HasFilteredColimitsOfSize.{v', u'} C] [AB5OfSize.{v', u'} C] :
+ instance {C : Type u} [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{w} C] :
+ instance {i j : J} (f : i ⟶ j) : IsIso (h.F.map f) := h.mem_map f
+ mem
+ mem_incl_app
+ mem_map
+ mem_map_bot_le
++ instance [W.IsMultiplicative] [W.RespectsIso]
- instance (j : J) : IsIso (h.incl.app j)
- instance : (isomorphisms C).IsStableUnderTransfiniteComposition
- instance : IsStableUnderTransfiniteComposition.{w} (monomorphisms C)
- instance {j : J} (g : ⊥ ⟶ j) : IsIso (h.F.map g) := by
- instance {j j' : J} (f : j ⟶ j') : IsIso (h.F.map f)
- map_bot_le
- mono
- mono_map

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

callesonne

LGTM (already from previous PR)

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

….lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

mathlib4-merge-conflict-bot · 2025-08-06T04:13:32Z

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

…er-transfinite-composition-argument

robin-carlier

Thanks!

maintainer delegate

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

github-actions · 2025-08-14T17:26:33Z

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

riccardobrasca · 2025-08-14T17:50:48Z

Thanks!

bors d+

mathlib-bors · 2025-08-14T17:50:51Z

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

…er-transfinite-composition-argument

….lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

joelriou · 2025-08-15T06:37:13Z

Thanks!

bors merge

…finite compositions (#26030) If a class of morphisms is multiplicative, respects isomorphisms and is stable under filtered colimits, then it is stable under transfinite compositions. (This simplifies the proof in the case of monomorphisms in Grothendieck abelian categories, for isomorphisms, and in #23282, we shall apply this to monomorphisms in `Type`.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-08-15T06:52:26Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

…finite compositions (leanprover-community#26030) If a class of morphisms is multiplicative, respects isomorphisms and is stable under filtered colimits, then it is stable under transfinite compositions. (This simplifies the proof in the case of monomorphisms in Grothendieck abelian categories, for isomorphisms, and in leanprover-community#23282, we shall apply this to monomorphisms in `Type`.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

joelriou and others added 17 commits May 11, 2025 13:39

chore(CategoryTheory): make MorphismProperty.IsStableUnderColimitsOfS…

065b96d

…hape a class

fix

dc84886

abstracted the stability by transfinite composition

70b64c3

fix

9837877

fix

c99276b

fix

fe01008

Merge remote-tracking branch 'origin' into jriou-is-stable-under-tran…

3bdff2e

…sfinite-composition-argument

Merge remote-tracking branch 'origin' into jriou-is-stable-under-tran…

01487e8

…sfinite-composition-argument

Merge remote-tracking branch 'origin' into jriou-is-stable-under-tran…

f303d73

…sfinite-composition-argument

colimitsOfShape.of_isColimit

5aa733d

Update Mathlib/CategoryTheory/MorphismProperty/Limits.lean

c76e83d

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

Update Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition…

a1af4d7

….lean Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

Update Mathlib/CategoryTheory/MorphismProperty/Limits.lean

83e2db7

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

fixing imports

26c7f75

Merge remote-tracking branch 'origin' into jriou-is-stable-under-tran…

9e57abb

…sfinite-composition-argument

Update Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInje…

610816e

…ctives.lean

Merge remote-tracking branch 'origin' into jriou-is-stable-under-tran…

1a7ff5a

…sfinite-composition-argument

joelriou mentioned this pull request Jun 17, 2025

feat(CategoryTheory): abstract argument for the stability under transfinite compositions #24777

Closed

1 task

github-actions bot added t-category-theory Category theory large-import Automatically added label for PRs with a significant increase in transitive imports labels Jun 17, 2025

callesonne self-requested a review June 18, 2025 12:15

callesonne approved these changes Jun 21, 2025

View reviewed changes

robin-carlier reviewed Jun 24, 2025

View reviewed changes

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean Outdated Show resolved Hide resolved

robin-carlier reviewed Jun 24, 2025

View reviewed changes

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean Outdated Show resolved Hide resolved

robin-carlier reviewed Jun 24, 2025

View reviewed changes

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean Outdated Show resolved Hide resolved

robin-carlier reviewed Jun 24, 2025

View reviewed changes

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean Outdated Show resolved Hide resolved

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 24, 2025

Update Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition…

b1282b9

….lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

joelriou and others added 2 commits June 24, 2025 15:16

Update Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition…

68f68ed

….lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

Update Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition…

ff9d8a9

….lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

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 Aug 6, 2025

joelriou added 2 commits August 6, 2025 12:11

suggestion by robin carlier

982d725

Merge remote-tracking branch 'origin/master' into jriou-is-stable-und…

8a3c0ae

…er-transfinite-composition-argument

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

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 Aug 6, 2025

joelriou mentioned this pull request Aug 11, 2025

feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions #23282

Closed

2 tasks

Merge remote-tracking branch 'origin/master' into jriou-is-stable-und…

37187b7

…er-transfinite-composition-argument

joelriou mentioned this pull request Aug 11, 2025

[Merged by Bors] - feat(CategoryTheory): monomorphisms in Type are stable under transfinite compositions #28219

Closed

1 task

robin-carlier reviewed Aug 14, 2025

View reviewed changes

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean Outdated Show resolved Hide resolved

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 14, 2025

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 14, 2025

joelriou and others added 2 commits August 15, 2025 11:45

Merge remote-tracking branch 'origin/master' into jriou-is-stable-und…

846ebeb

…er-transfinite-composition-argument

Update Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition…

9167216

….lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

ghost added the ready-to-merge This PR has been sent to bors. label Aug 15, 2025

mathlib-bors bot changed the title ~~feat(CategoryTheory): abstract argument for the stability under transfinite compositions~~ [Merged by Bors] - feat(CategoryTheory): abstract argument for the stability under transfinite compositions Aug 15, 2025

mathlib-bors bot closed this Aug 15, 2025

Conversation

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

Uh oh!

Uh oh!

joelriou commented Jun 17, 2025

Comments from Original PR #24777

PR summary 610816e983

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

PR summary 3f11243a35

Import changes for modified files

Declarations diff

Uh oh!

callesonne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Aug 6, 2025

Uh oh!

robin-carlier left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Aug 14, 2025

Uh oh!

riccardobrasca commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

joelriou commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

joelriou commented Jun 17, 2025 •

edited

Loading

github-actions bot commented Jun 17, 2025 •

edited

Loading