feat(CategoryTheory): the κ-accessible category of κ-directed posets #31018
Conversation
… object is a colimit of objects in S
…nerator-of-colimit
…-cardinal-filtered-generators
…into refactor-are-cardinal-filtered-generators
…perty-closed-under-limits-of-shape
Co-authored-by: Christian Merten <christian@merten.dev>
…under-limits-of-shape' into object-property-limits-closure
…nerator-of-colimit
…-cardinal-filtered-generators
…into refactor-are-cardinal-filtered-generators
…order-cardinal-accessible
…enerators' into partial-order-cardinal-accessible
github-actions
bot
added
the
large-import
PR summary 337f3a7ec8Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation | 892 | 960 | +68 (+7.62%) |
| Mathlib.CategoryTheory.Presentable.LocallyPresentable | 893 | 961 | +68 (+7.61%) |
| Mathlib.CategoryTheory.ObjectProperty.Small | 399 | 417 | +18 (+4.51%) |
| Mathlib.CategoryTheory.Comma.StructuredArrow.Small | 461 | 474 | +13 (+2.82%) |
| Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape | 643 | 653 | +10 (+1.56%) |
Import changes for all files
| Files | Import difference |
|---|---|
385 filesMathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.ChosenFiniteProducts Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.AlternatingConst 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.ConcreteCategory 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.GrothendieckAbelian 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.LocalCohomology Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.Single Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Module.PID 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.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.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected 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.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.Abelian.Indization 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.Action.Monoidal Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Bicategory.CatEnriched Mathlib.CategoryTheory.Category.Cat.CartesianClosed Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.ChosenFiniteProducts.Cat Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice Mathlib.CategoryTheory.ChosenFiniteProducts.Over Mathlib.CategoryTheory.ChosenFiniteProducts Mathlib.CategoryTheory.Closed.Cartesian Mathlib.CategoryTheory.Closed.Enrichment Mathlib.CategoryTheory.Closed.FunctorCategory.Basic Mathlib.CategoryTheory.Closed.FunctorToTypes Mathlib.CategoryTheory.Closed.Functor Mathlib.CategoryTheory.Closed.Ideal Mathlib.CategoryTheory.Closed.Types Mathlib.CategoryTheory.Closed.Zero Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Enriched.Basic Mathlib.CategoryTheory.Enriched.EnrichedCat Mathlib.CategoryTheory.Enriched.FunctorCategory Mathlib.CategoryTheory.Enriched.HomCongr Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal Mathlib.CategoryTheory.Enriched.Opposite Mathlib.CategoryTheory.Enriched.Ordinary.Basic Mathlib.CategoryTheory.ExtremalEpi Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Functor.FunctorHom Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Limits.Constructions.Over.Basic 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.MorphismProperty Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition Mathlib.CategoryTheory.Monoidal.Cartesian.Basic Mathlib.CategoryTheory.Monoidal.Cartesian.Cat Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Over Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Functor.Types Mathlib.CategoryTheory.Monoidal.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration 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.MonoOver Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Subobject.Presheaf Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Subpresheaf.Subobject Mathlib.CategoryTheory.Subterminal Mathlib.CategoryTheory.Topos.Classifier 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.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.Order.Interval.Set.Final Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FiniteIndex 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 Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Regular.Category Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling |
1 |
11 filesMathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf |
2 |
3 filesMathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape |
10 |
Mathlib.CategoryTheory.Comma.StructuredArrow.Small |
13 |
Mathlib.CategoryTheory.ObjectProperty.Small |
18 |
Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.LocallyPresentable |
68 |
Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (new file) |
402 |
Mathlib.Order.Category.PartOrdEmb (new file) |
643 |
Mathlib.CategoryTheory.Generator.StrongGenerator (new file) |
784 |
Mathlib.CategoryTheory.Functor.KanExtension.Dense (new file) |
796 |
Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (new file) |
891 |
Mathlib.CategoryTheory.Presentable.Directed (new file) |
958 |
Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset (new file) |
1019 |
Declarations diff
+ CardinalFilteredPoset
+ CardinalFilteredPoset.ι
+ CategoryTheory.MorphismProperty.toSet_iSup
+ CategoryTheory.MorphismProperty.toSet_max
+ CoconePt
+ CoconePt.desc
+ CoconePt.fac_apply
+ ColimitOfShape.isCardinalPresentable
+ Diagram
+ Diagram.iSup
+ Diagram.max
+ Diagram.single
+ DiagramWithUniqueTerminal
+ DiagramWithUniqueTerminal.ext
+ DiagramWithUniqueTerminal.single
+ EssentiallySmall
+ EssentiallySmall.exists_small
+ EssentiallySmall.exists_small_le
+ EssentiallySmall.of_le
+ HasCardinalFilteredColimits.mk'
+ HasCardinalFilteredGenerator
+ HasCardinalFilteredGenerator.exists_small_generator
+ Hom
+ Hom.Simps.hom
+ Hom.hom
+ Hom.injective
+ Hom.le_iff_le
+ IsCardinalFilteredGenerator
+ IsCoseparating.mk_of_exists_limitsOfShape
+ IsCoseparating.mk_of_exists_mono
+ IsCoseparating.mono_productTo
+ IsDense
+ IsDense.of_fullyFaithful_restrictedULiftYoneda
+ IsFiltered.exists_directed
+ IsFiltered.isDirected
+ IsRegular.lift
+ IsSeparating.epi_coproductFrom
+ IsSeparating.mk_of_exists_colimitsOfShape
+ IsSeparating.mk_of_exists_epi
+ IsStrongGenerator
+ IsStrongGenerator.mk_of_exists_colimitsOfShape
+ IsTerminal
+ Iso.mk
+ ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator
+ PartOrdEmb
+ arrowEquiv
+ aux
+ cocone
+ coe_comp
+ coe_id
+ coe_of
+ comp_apply
+ coproductFrom
+ coproductFromFamily
+ denseAt
+ dual
+ dualEquiv
+ equiv
+ exists_cardinal_directed
+ exists_of_mono_not_isIso
+ exists_of_subobject_ne_top
+ ext
+ extremalEpi_coproductFrom
+ final_functor
+ forget_map
+ functor
+ functorMap
+ functorMap_comp
+ functorMap_id
+ hasCardinalLT_iUnion
+ hasCardinalLT_lift_iff
+ hasCardinalLT_of_finite
+ hasCardinalLT_prod
+ hasCardinalLT_prod'
+ hasCardinalLT_sigma
+ hasCardinalLT_sigma'
+ hasCardinalLT_subtype_iSup
+ hasCardinalLT_subtype_max
+ hasCardinalLT_subtype_objectPropertyOfObj
+ hasCardinalLT_toSet_morphismPropertyOfHoms
+ hasCardinalLT_ulift_iff
+ hasCardinalLT_union
+ hasForgetToPartOrd
+ hom_comp
+ hom_ext
+ hom_id
+ hom_inv_apply
+ hom_ofHom
+ id_apply
+ instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+ instance (a : α) : (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a)
+ instance (j : J) : Finite (Subtype (Diagram.single (κ := κ) j).P)
+ instance : (P.limitsClosure J).IsClosedUnderIsomorphisms
+ instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms
+ instance : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms
+ instance : Category PartOrdEmb.{u}
+ instance : CoeSort PartOrdEmb (Type _)
+ instance : ConcreteCategory PartOrdEmb (· ↪o ·)
+ instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ
+ instance : HasColimit F
+ instance : HasColimitsOfShape J PartOrdEmb.{u}
+ instance : HasFilteredColimitsOfSize.{u, u} PartOrdEmb.{u}
+ instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ
+ instance : PartialOrder (CoconePt hc)
+ instance : PartialOrder (DiagramWithUniqueTerminal J κ)
+ instance : PreservesColimit F (forget _)
+ instance : PreservesColimitsOfShape J (forget PartOrdEmb.{u})
+ instance : PreservesFilteredColimitsOfSize.{u, u} (forget PartOrdEmb.{u})
+ instance : Subsingleton (D.IsTerminal e)
+ instance [F.Initial] [G.Initial] : (F.prod G).Initial
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Faithful
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Full
+ instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+ instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [LocallySmall.{w} J] :
+ instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [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 {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] :
+ inv_hom_apply
+ isCardinalFiltered_aux
+ isCardinalFiltered_iff
+ isCardinalFiltered_pi
+ isCardinalFiltered_prod
+ isCardinalFiltered_pt
+ isCardinalPresentable
+ isCardinalPresentable_iff
+ isCardinalPresentable_monotone
+ isClosedUnderIsomorphisms_iff_isoClosure_eq_self
+ isColimitCocone
+ isDense_iff_fullyFaithful_restrictedULiftYoneda
+ isDense_iff_nonempty_isPointwiseLeftKanExtension
+ isEssentiallySmall_limitsClosure
+ isIso_of_mono
+ isRegular_lift_iff
+ isSeparating
+ isStrongGenerator
+ isStrongGenerator_iff
+ isStrongGenerator_iff_exists_extremalEpi
+ isStrongGenerator_of_isDense
+ isoClosure
+ isoClosure_iSup
+ isoClosure_iff
+ isoClosure_strictLimitsClosureIter_eq_limitsClosure
+ isoClosure_sup
+ jointly_surjective_of_isColimit₂
+ le_limitsClosure
+ le_strictLimitsClosureIter
+ le_strictLimitsClosureStep
+ lift_self
+ limitsClosure
+ limitsClosure_isoClosure
+ limitsClosure_le
+ limitsClosure_monotone
+ mem_toSet_iff
+ mk_of_exists_extremalEpi
+ mk_surjective
+ of
+ ofExistsUnique
+ ofHom
+ ofHom_apply
+ ofHom_comp
+ ofHom_hom
+ ofHom_id
+ of_le_isoClosure
+ orderIsoOfIso
+ partOrdEmb_dual_comp_forget_to_pardOrd
+ prod
+ productTo
+ productToFamily
+ prop
+ prop_iSup_iff
+ prop_inf_iff
+ prop_sup_iff
+ strictLimitsClosureIter
+ strictLimitsClosureIter_le_limitsClosure
+ strictLimitsClosureStep
+ strictLimitsClosureStep_monotone
+ strictLimitsClosureStep_strictLimitsClosureIter_eq_self
+ subobject_eq_top
+ ιCoproductFrom
+ πProductTo
++ instance {α : Type*} (P : α → ObjectProperty C)
++ isCardinalFiltered
- J
- colimitPresentation
- exists_colimitPresentation_diag_obj_iso
- instance (j : h.J X) :
- instance (j : h.J X) : IsPresentable.{w} ((h.colimitPresentation X).diag.obj j)
- instance : IsCardinalFiltered (h.J X) κ
- instance : SmallCategory (h.J X)
- isPresentable
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).
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
WIP
PardOrdEmbhas filtered colimits #30696κ-filtered categories #30781