feat(CategoryTheory): localization of locally presentable categories #30554
Conversation
… object is a colimit of objects in S
…perty-closed-under-limits-of-shape
…under-limits-of-shape' into orthogonal-reflection-3
…e' into orthogonal-reflection-3
…r κ-filtered colimits
…thogonal-reflection-3
…hogonal-reflection-6
github-actions
bot
added
the
large-import
PR summary 45dfe1bcb6Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Limits.FullSubcategory | 456 | 651 | +195 (+42.76%) |
| Mathlib.CategoryTheory.ObjectProperty.Retract | 368 | 460 | +92 (+25.00%) |
| Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation | 890 | 959 | +69 (+7.75%) |
| Mathlib.CategoryTheory.Presentable.LocallyPresentable | 891 | 960 | +69 (+7.74%) |
| Mathlib.CategoryTheory.Monoidal.Cartesian.Basic | 652 | 684 | +32 (+4.91%) |
| Mathlib.CategoryTheory.ObjectProperty.Small | 397 | 415 | +18 (+4.53%) |
| Mathlib.CategoryTheory.Subobject.MonoOver | 677 | 699 | +22 (+3.25%) |
| Mathlib.CategoryTheory.Generator.Basic | 758 | 777 | +19 (+2.51%) |
| Mathlib.CategoryTheory.Generator.Presheaf | 759 | 778 | +19 (+2.50%) |
| Mathlib.CategoryTheory.Generator.HomologicalComplex | 777 | 796 | +19 (+2.45%) |
| Mathlib.CategoryTheory.Comma.StructuredArrow.Small | 483 | 472 | -11 (-2.28%) |
| Mathlib.CategoryTheory.Generator.Preadditive | 849 | 868 | +19 (+2.24%) |
| Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems | 773 | 786 | +13 (+1.68%) |
| Mathlib.CategoryTheory.Generator.Sheaf | 791 | 804 | +13 (+1.64%) |
| Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator | 1350 | 1362 | +12 (+0.89%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.Comma.StructuredArrow.Small |
-11 |
87 filesMathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Equivalence Mathlib.Condensed.Light.Small Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks |
1 |
Mathlib.CategoryTheory.Preadditive.Projective.Internal |
3 |
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms |
4 |
9 filesMathlib.Algebra.Homology.GrothendieckAbelian Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic 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.Subobject |
5 |
16 filesMathlib.Algebra.Category.ModuleCat.AB Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf 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.NumberTheory.LSeries.PrimesInAP Mathlib.Topology.CWComplex.Abstract.Basic |
6 |
99 filesMathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Homology.LocalCohomology 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.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types 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.Over Mathlib.CategoryTheory.Sites.SheafHom Mathlib.Condensed.AB Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Light.AB Mathlib.Order.Interval.Set.Final Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend |
7 |
19 filesMathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Explicit 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 |
8 |
24 filesMathlib.Algebra.Homology.AlternatingConst Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialSet.Monoidal 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 |
Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape |
10 |
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback |
12 |
38 filesMathlib.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.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems 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 Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality 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 |
20 filesMathlib.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 |
16 |
Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory |
17 |
Mathlib.CategoryTheory.ObjectProperty.Small |
18 |
120 filesMathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.Grp.Subobject 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.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences 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.Ext Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.ExtremalEpi 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.Tor Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Subobject.ArtinianObject 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.NoetherianObject Mathlib.CategoryTheory.Subobject.Presheaf Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Subpresheaf.Subobject Mathlib.CategoryTheory.Topos.Classifier |
19 |
21 filesMathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.CategoryTheory.Bicategory.CatEnriched Mathlib.CategoryTheory.Closed.Enrichment Mathlib.CategoryTheory.Closed.FunctorCategory.Basic Mathlib.CategoryTheory.Closed.FunctorToTypes 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.Functor.FunctorHom Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Functor.Types Mathlib.CategoryTheory.Monoidal.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.CategoryTheory.Preadditive.CommGrp_ |
20 |
Mathlib.CategoryTheory.Closed.Ideal |
21 |
4 filesMathlib.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_ |
29 |
Mathlib.CategoryTheory.Category.Cat.CartesianClosed |
30 |
3 filesMathlib.CategoryTheory.Closed.Cartesian Mathlib.CategoryTheory.Closed.Functor Mathlib.CategoryTheory.Closed.Zero |
31 |
11 filesMathlib.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.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.LocallyPresentable |
69 |
Mathlib.CategoryTheory.ObjectProperty.Retract |
92 |
Mathlib.CategoryTheory.Limits.FullSubcategory |
195 |
Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (new file) |
400 |
Mathlib.CategoryTheory.ObjectProperty.Orthogonal (new file) |
431 |
Mathlib.CategoryTheory.Functor.KanExtension.DenseAt (new file) |
466 |
Mathlib.CategoryTheory.Adjunction.ReflectiveLimits (new file) |
481 |
Mathlib.CategoryTheory.Generator.StrongGenerator (new file) |
779 |
Mathlib.CategoryTheory.Functor.KanExtension.Dense (new file) |
791 |
Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (new file) |
860 |
Mathlib.CategoryTheory.Presentable.Retracts (new file) |
870 |
Mathlib.CategoryTheory.Presentable.Adjunction (new file) |
962 |
Mathlib.CategoryTheory.Presentable.OrthogonalReflection (new file) |
1064 |
Declarations diff
+ ColimitOfShape.isCardinalPresentable
+ ColimitOfShape.prop
+ CostructuredArrow.isSeparating_proj_preimage
+ DenseAt
+ DenseAt.ofIso
+ DenseAt.ofNatIso
+ DenseAt.postcompEquivalence
+ DenseAt.precompEquivalence
+ D₁
+ D₁.hasCoproductsOfShape
+ D₁.l
+ D₁.obj₁
+ D₁.obj₂
+ D₁.t
+ D₁.ιLeft
+ D₁.ιLeft_comp_l
+ D₁.ιLeft_comp_t
+ D₁.ιRight
+ D₁.ι_comp_t
+ D₂
+ D₂.condition
+ D₂.hasColimitsOfShape
+ D₂.multispanIndex
+ D₂.multispanShape
+ EssentiallySmall
+ EssentiallySmall.exists_small
+ EssentiallySmall.exists_small_le
+ EssentiallySmall.of_le
+ HasCardinalFilteredGenerator
+ HasCardinalFilteredGenerator.exists_small_generator
+ IsCardinalFilteredGenerator
+ IsCardinalPresentable.exists_eq_of_isColimit
+ IsCardinalPresentable.exists_eq_of_isColimit'
+ IsCardinalPresentable.exists_hom_of_isColimit
+ IsClosedUnderColimitsOfShape
+ IsClosedUnderColimitsOfShape.mk'
+ IsClosedUnderLimitsOfShape
+ IsClosedUnderLimitsOfShape.mk'
+ IsCodetecting.of_le
+ IsCoseparating.mk_of_exists_limitsOfShape
+ IsCoseparating.mk_of_exists_mono
+ IsCoseparating.mono_productTo
+ IsCoseparating.of_equivalence
+ IsCoseparating.of_le
+ IsDense
+ IsDense.of_fullyFaithful_restrictedULiftYoneda
+ IsDetecting.of_le
+ IsSeparating.epi_coproductFrom
+ IsSeparating.mk_of_exists_colimitsOfShape
+ IsSeparating.mk_of_exists_epi
+ IsSeparating.of_equivalence
+ IsSeparating.of_le
+ IsStrongGenerator
+ IsStrongGenerator.mk_of_exists_colimitsOfShape
+ LimitOfShape.prop
+ MorphismProperty.isCardinalAccessible_ι_rightOrthogonal
+ MorphismProperty.isClosedUnderColimitsOfShape_rightOrthogonal
+ MorphismProperty.le_leftBousfieldW_rightOrthogonal
+ ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator
+ ObjectProperty.IsSeparating.isSeparator_coproduct
+ ObjectProperty.le_rightOrthogonal_W
+ Retract.isCardinalPresentable
+ StructuredArrow.isCoseparating_proj_preimage
+ compUliftCoyonedaIso
+ congr_isDenseAt
+ coproductFrom
+ coproductFromFamily
+ corepresentableBy
+ denseAt
+ essentiallySmall_isPresentable
+ exists_of_mono_not_isIso
+ exists_of_subobject_ne_top
+ extremalEpi_coproductFrom
+ fromStep
+ fullSubcategory'
+ galoisConnection
+ hasCardinalFilteredGenerator
+ hasColimitsOfShape
+ hasLimitsOfShape
+ instance (C : Type u) [Category.{v} C]
+ instance (D : Type w) [SmallCategory.{w} D] : EssentiallySmall.{w} D
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] (F : C ⥤ D) :
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] (F : C ⥤ D) :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+ instance (a : J.R) (b : J.L) : IsEmpty (right a ⟶ left b) := ⟨by rintro ⟨⟩⟩
+ instance (a : WalkingMultispan J) : Unique (a ⟶ a)
+ instance (a b : J.L) : Subsingleton (left a ⟶ left b) := by
+ instance (a b : J.R) : Subsingleton (right a ⟶ right b) := by
+ instance (κ : Cardinal.{w}) [Fact κ.IsRegular] :
+ instance : (Over.isMono X).IsClosedUnderLimitsOfShape J
+ instance : (W P).IsStableUnderTransfiniteCompositionOfShape J
+ instance : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms
+ instance : E.isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms
+ instance : E.isPointwiseRightKanExtensionAt.IsClosedUnderIsomorphisms
+ instance : F.isDenseAt.IsClosedUnderIsomorphisms := by
+ instance : IsCardinalAccessible (𝟭 C) κ
+ instance : LocallySmall.{t} (WalkingMultispan J)
+ instance : MorphismProperty.IsStableUnderTransfiniteComposition.{w} (W P)
+ instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+ instance : Small.{w} (D₂ (W := W) (Z := Z)) := by
+ instance : Small.{w} (D₂.multispanShape W Z).L := by dsimp; infer_instance
+ instance : W.rightOrthogonal.IsClosedUnderIsomorphisms
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Faithful
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Full
+ 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 [IsCardinalPresentable X κ] :
+ instance [MorphismProperty.IsSmall.{w} W] [LocallySmall.{w} C] :
+ instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] :
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [P.RespectsIso] [P.ContainsIdentities] :
+ instance [PreservesColimitsOfSize.{w, w} F] : F.IsCardinalAccessible κ
+ instance [Small.{t} J.L] [Small.{t} J.R] : Small.{t} (WalkingMultispan J)
+ instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (CostructuredArrow S T)
+ instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (StructuredArrow S T)
+ instance [∀ a, (P a).IsClosedUnderIsomorphisms] :
+ instance {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E)
+ 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] :
+ isCardinalAccessible
+ isCardinalFilteredGenerator
+ isCardinalLocallyPresentable
+ isCardinalPresentable
+ isCardinalPresentable_iff
+ isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj
+ isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj
+ isCardinalPresentable_monotone
+ isClosedUnderIsomorphisms_iff_isoClosure_eq_self
+ isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair
+ isCodetecting_bot_of_isGroupoid
+ isCoseparating_bot_of_isThin
+ isCoseparating_inverseImage_proj
+ isCoseparator_iff_of_isLimit_fan
+ isCoseparator_of_isLimit_fan
+ isDenseAt
+ isDenseAt_eq_isPointwiseLeftKanExtensionAt
+ isDense_iff_fullyFaithful_restrictedULiftYoneda
+ isDense_iff_nonempty_isPointwiseLeftKanExtension
+ isDetecting_bot_of_isGroupoid
+ isGroupoid_of_isCodetecting_bot
+ isGroupoid_of_isDetecting_bot
+ isIso_of_mono
+ isIso_toSucc_iff
+ isLocallyPresentable_rightOrthogonal
+ isPointwiseLeftKanExtensionAt
+ isPointwiseRightKanExtensionAt
+ isPresentable_eq_retractClosure
+ isPresentable_leftAdjoint_obj
+ isRightAdjoint_ι
+ isRightAdjoint_ι_rightOrthogonal
+ isSeparating_bot_of_isThin
+ isSeparating_inverseImage_proj
+ isSeparator_iff_of_isColimit_cofan
+ isStrongGenerator
+ isStrongGenerator_iff
+ isStrongGenerator_iff_exists_extremalEpi
+ isStrongGenerator_of_isDense
+ isThin_of_isCoseparating_bot
+ isThin_of_isSeparating_bot
+ isoClosure
+ isoClosure_iSup
+ isoClosure_iff
+ isoClosure_sup
+ iteration
+ iterationObjSuccIso
+ iteration_map_succ
+ iteration_map_succ_injectivity
+ iteration_map_succ_surjectivity
+ le_W_iff
+ leftBousfieldW_rightOrthogonal_reflection
+ leftBousfieldW_rightOrthogonal_toSucc
+ mk_of_exists_extremalEpi
+ ofExists
+ of_le_isoClosure
+ productTo
+ productToFamily
+ prop_colimit
+ prop_iSup_iff
+ prop_inf_iff
+ prop_limit
+ prop_of_isColimit
+ prop_of_isLimit
+ prop_sup_iff
+ reflection
+ reflectionObj
+ retractClosure_isoClosure
+ rightOrthogonal
+ rightOrthogonal_iff
+ rightOrthogonal_reflectionObj
+ step
+ subobject_eq_top
+ succ
+ succStruct
+ toStep
+ toSucc
+ toSucc_injectivity
+ toSucc_surjectivity
+ transfiniteCompositionOfShapeReflection
+ uliftCoyoneda
+ ιCoproductFrom
+ πProductTo
++ hom_ext'
++ instance {α : Type*} (P : α → ObjectProperty C)
++ small_inverseImage_proj_of_locallySmall
++ w
++- IsCodetecting.isCoseparating
++- IsCodetecting.isIso_iff_of_epi
++- IsCoseparating.isCodetecting
++- IsDetecting.isIso_iff_of_mono
++- IsDetecting.isSeparating
++- IsSeparating.isDetecting
++- isCodetecting_iff_isCoseparating
++- isCodetecting_unop_iff
++- isCoseparating_unop_iff
++- isDetecting_unop_iff
++- isSeparating_unop_iff
++-- small_proj_preimage_of_locallySmall
+-+ IsCodetecting
+-+ IsCoseparating
+-+ IsDetecting
+-+ IsSeparating
+-+ isCodetecting_op_iff
+-+ isCoseparating_iff_mono
+-+ isCoseparating_op_iff
+-+ isDetecting_iff_isSeparating
+-+ isDetecting_op_iff
+-+ isSeparating_iff_epi
+-+ isSeparating_op_iff
- ClosedUnderColimitsOfShape.essImage
- ClosedUnderLimitsOfShape.essImage
- J
- closedUnderLimitsOfShape_isMono
- colimitPresentation
- exists_colimitPresentation_diag_obj_iso
- instCartesianMonoidalCategory
- instance (j : h.J X) :
- instance (j : h.J X) : IsPresentable.{w} ((h.colimitPresentation X).diag.obj j)
- instance : IsCardinalFiltered (h.J X) κ
- instance : Small.{u} (freeYoneda R) := by
- instance : SmallCategory (h.J X)
- isCoseparating_proj_preimage
- isPresentable
- isSeparating_proj_preimage
-++--++ isSeparating
--++ isSeparator
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
joelriou
changed the title
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
3 participants
Let
W : MorphismProperty Cbe aw-small property of morphisms in a locallyκ-presentable categoryC(withκ : Cardinal.{w}a regular cardinal), such that the domains and codomains of morphisms satisfyingWareκ-presentable.Then, the fullsubcategory
W.rightOrthogonalis also locallyκ-presentable (it is also stable underκ-filtered colimits, and the inclusion functor as a left adjoint).κ-filtered colimits #30507