feat(CategoryTheory): categories of presheaves are locally presentable #30247
Conversation
… object is a colimit of objects in S
…imits-closure-bounded
…entable-strong-generators
…refactor-object-property-closed-under-limits-of-shape
github-actions
bot
added
the
merge-conflict
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
…under-limits-of-shape' into object-property-limits-closure
…into object-property-colimits-closure
…' into object-property-colimits-closure-bounded
…-bounded' into locally-presentable-strong-generators
…ators' into locally-presentable-presheaf
github-actions
bot
added
large-import
PR summary 586e9c3862Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Limits.FullSubcategory | 456 | 652 | +196 (+42.98%) |
| Mathlib.CategoryTheory.Limits.Presentation | 891 | 635 | -256 (-28.73%) |
| Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape | 893 | 649 | -244 (-27.32%) |
| Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape | 893 | 651 | -242 (-27.10%) |
| Mathlib.CategoryTheory.ObjectProperty.Small | 389 | 459 | +70 (+17.99%) |
| Mathlib.CategoryTheory.SmallRepresentatives | 700 | 805 | +105 (+15.00%) |
| Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation | 893 | 958 | +65 (+7.28%) |
| Mathlib.CategoryTheory.Monoidal.Cartesian.Basic | 651 | 685 | +34 (+5.22%) |
| Mathlib.CategoryTheory.Subobject.MonoOver | 676 | 700 | +24 (+3.55%) |
| Mathlib.CategoryTheory.Presentable.Limits | 870 | 895 | +25 (+2.87%) |
| Mathlib.CategoryTheory.Generator.Basic | 757 | 778 | +21 (+2.77%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.Limits.Presentation |
-256 |
Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape |
-244 |
Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape |
-242 |
4 filesMathlib.CategoryTheory.Category.Cat.Adjunction Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.Presentable.Basic |
1 |
Mathlib.CategoryTheory.ConnectedComponents Mathlib.CategoryTheory.IsConnected |
2 |
56 filesMathlib.Algebra.Category.GrpWithZero Mathlib.Algebra.Category.MonCat.Basic Mathlib.Algebra.Category.MonCat.ForgetCorepresentable Mathlib.Algebra.Category.Semigrp.Basic Mathlib.CategoryTheory.Adjunction.Basic Mathlib.CategoryTheory.Adjunction.Opposites Mathlib.CategoryTheory.Adjunction.Parametrized Mathlib.CategoryTheory.Adjunction.Restrict Mathlib.CategoryTheory.Adjunction.Whiskering Mathlib.CategoryTheory.Bicategory.Adjunction.Adj Mathlib.CategoryTheory.Bicategory.Coherence Mathlib.CategoryTheory.Bicategory.Free Mathlib.CategoryTheory.Bicategory.Functor.Lax Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Functor.Oplax Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax Mathlib.CategoryTheory.Bicategory.Grothendieck Mathlib.CategoryTheory.Bicategory.Modification.Oplax Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor Mathlib.CategoryTheory.Category.Bipointed Mathlib.CategoryTheory.Category.Cat.AsSmall Mathlib.CategoryTheory.Category.Cat.Op Mathlib.CategoryTheory.Category.Cat Mathlib.CategoryTheory.Category.Pointed Mathlib.CategoryTheory.Category.TwoP Mathlib.CategoryTheory.CodiscreteCategory Mathlib.CategoryTheory.ConcreteCategory.Basic Mathlib.CategoryTheory.ConcreteCategory.BundledHom Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom Mathlib.CategoryTheory.Core Mathlib.CategoryTheory.Elementwise Mathlib.CategoryTheory.FiberedCategory.Grothendieck Mathlib.CategoryTheory.Functor.EpiMono Mathlib.CategoryTheory.Functor.Hom Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced Mathlib.CategoryTheory.IsomorphismClasses Mathlib.CategoryTheory.Join.Pseudofunctor Mathlib.CategoryTheory.LiftingProperties.Adjunction Mathlib.CategoryTheory.Limits.Cones Mathlib.CategoryTheory.Limits.IsLimit Mathlib.CategoryTheory.Limits.Types.ColimitType Mathlib.CategoryTheory.Monad.Algebra Mathlib.CategoryTheory.Monad.Kleisli Mathlib.CategoryTheory.Monad.Types Mathlib.CategoryTheory.Types.Basic Mathlib.CategoryTheory.UnivLE Mathlib.CategoryTheory.Yoneda Mathlib.Tactic.CategoryTheory.BicategoryCoherence Mathlib.Tactic.CategoryTheory.Elementwise Mathlib.Tactic.CategoryTheory.ToApp |
4 |
75 filesMathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.CategoryTheory.Balanced Mathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.EqToHom Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Strict.Basic Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.Category.ULift Mathlib.CategoryTheory.Center.Basic Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Conj Mathlib.CategoryTheory.DinatTrans Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.Endomorphism Mathlib.CategoryTheory.EpiMono Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.EssentialImage Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HasFibers Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Groupoid.Basic Mathlib.CategoryTheory.Groupoid.Discrete Mathlib.CategoryTheory.Groupoid.FreeGroupoid Mathlib.CategoryTheory.Groupoid.VertexGroup Mathlib.CategoryTheory.Groupoid Mathlib.CategoryTheory.Join.Basic Mathlib.CategoryTheory.Join.Opposites Mathlib.CategoryTheory.Join.Sum Mathlib.CategoryTheory.LiftingProperties.Basic Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform Mathlib.CategoryTheory.Limits.Shapes.StrongEpi Mathlib.CategoryTheory.Monad.Basic Mathlib.CategoryTheory.Monoidal.Action.Basic Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.ObjectProperty.Basic Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms Mathlib.CategoryTheory.ObjectProperty.FullSubcategory Mathlib.CategoryTheory.ObjectProperty.Retract Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.PathCategory.Basic Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Quotient Mathlib.CategoryTheory.Retract Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Sums.Products Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.Widget.StringDiagram |
5 |
78 filesMathlib.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.RationalMap Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Topology.CWComplex.Abstract.Basic |
8 |
65 filesMathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.LocalCohomology Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.Closed.Types Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafHom Mathlib.Condensed.AB Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Order.Interval.Set.Final Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend |
9 |
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 |
11 |
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback |
14 |
37 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.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 |
15 |
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 |
16 |
3 filesMathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems |
18 |
Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory |
19 |
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 |
21 |
20 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.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.CategoryTheory.Preadditive.CommGrp_ |
22 |
Mathlib.CategoryTheory.Closed.Ideal |
23 |
4 filesMathlib.CategoryTheory.ChosenFiniteProducts.Over Mathlib.CategoryTheory.Monoidal.Cartesian.Over Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.CategoryTheory.Subterminal |
24 |
Mathlib.CategoryTheory.Presentable.Limits |
25 |
Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ |
31 |
Mathlib.CategoryTheory.Category.Cat.CartesianClosed |
32 |
3 filesMathlib.CategoryTheory.Closed.Cartesian Mathlib.CategoryTheory.Closed.Functor Mathlib.CategoryTheory.Closed.Zero |
33 |
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 |
34 |
Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.LocallyPresentable |
65 |
Mathlib.CategoryTheory.ObjectProperty.Small |
70 |
Mathlib.CategoryTheory.SmallRepresentatives |
105 |
Mathlib.CategoryTheory.Limits.FullSubcategory |
196 |
Mathlib.CategoryTheory.ObjectProperty.Equivalence (new file) |
339 |
Mathlib.CategoryTheory.ObjectProperty.Opposite (new file) |
340 |
Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (new file) |
413 |
Mathlib.CategoryTheory.Limits.Canonical (new file) |
458 |
Mathlib.CategoryTheory.Generator.Type (new file) |
779 |
Mathlib.CategoryTheory.Generator.StrongGenerator (new file) |
780 |
Mathlib.CategoryTheory.Functor.Dense (new file) |
792 |
Mathlib.CategoryTheory.ObjectProperty.LimitsClosure (new file) |
889 |
Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (new file) Mathlib.CategoryTheory.Presentable.ColimitPresentation (new file) |
892 |
Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure (new file) |
895 |
Mathlib.CategoryTheory.Presentable.StrongGenerator (new file) |
977 |
Mathlib.CategoryTheory.Presentable.Type (new file) |
979 |
Mathlib.CategoryTheory.Presentable.Presheaf (new file) |
982 |
Declarations diff
+ CanonicalColimis.ofIsIso
+ CanonicalColimit
+ CanonicalColimit.hom_ext'
+ CanonicalColimit.ofEquivalence
+ CanonicalColimit.ofNatIso
+ ColimitOfShape.prop
+ CostructuredArrow.essentiallySmall
+ CostructuredArrow.locallySmall
+ CostructuredArrow.small
+ EssentiallySmall
+ EssentiallySmall.exists_small
+ EssentiallySmall.exists_small_le
+ EssentiallySmall.of_le
+ Functor.congr_isCanonicalColimit
+ Functor.isCanonicalColimit
+ Functor.isCanonicalColimit.canonicalColimit
+ HasCardinalFilteredGenerators.of_dense
+ HasCardinalFilteredGenerators.of_essentiallySmall_of_dense
+ HasCardinalFilteredGenerators.of_small_of_dense
+ HasColimitsOfShape.of_essentiallySmall
+ HasColimitsOfShape.of_small
+ IsCardinalPresentable.exists_hom_of_isColimit
+ IsClosedUnderColimitsOfShape
+ IsClosedUnderColimitsOfShape.mk'
+ IsClosedUnderColimitsOfShape.of_equivalence
+ IsClosedUnderLimitsOfShape
+ IsClosedUnderLimitsOfShape.mk'
+ IsClosedUnderLimitsOfShape.of_equivalence
+ IsDense
+ IsDense.comp_left_iff_of_isEquivalence
+ IsDense.iff_of_iso
+ IsDense.of_fullyFaithful_restrictedULiftYoneda
+ IsDense.of_iso
+ IsLocallyPresentable.essentiallySmall_isCardinalPresentable
+ IsSeparating.mk_of_exists_colimitPresentation
+ IsSeparating.mono_iff
+ IsStrongGenerator
+ IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentable
+ IsStrongGenerator.isDense_colimitsCardinalClosure_ι
+ IsStrongGenerator.mk_of_exists_colimitPresentation
+ LimitOfShape.prop
+ ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable
+ ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι
+ ObjectProperty.isFiltered_costructuredArrow_colimitsCardinalClosure_ι
+ SmallCategoryCardinalLT
+ Types.isSeparator_punit
+ arrowEquiv
+ canonicalCocone
+ canonicalColimitOfIsDense
+ categoryFamily
+ colimitsCardinalClosure
+ colimitsCardinalClosure_le
+ colimitsClosure
+ colimitsClosure_eq_unop_limitsClosure
+ colimitsClosure_isoClosure
+ colimitsClosure_le
+ colimitsClosure_monotone
+ colimitsOfShape_congr
+ colimitsOfShape_eq_unop_limitsOfShape
+ colimitsOfShape_le_of_final
+ colimitsOfShape_op
+ coproductOfSet
+ coproductOfSet.hasCoproduct
+ coproductOfSet.obj
+ epi_coproductOfSetπ
+ essSurj_ιOfLE_iff
+ essentiallySmall_op_iff
+ essentiallySmall_unop_iff
+ exists_equivalence
+ exists_of_mono_not_isIso
+ exists_of_subobject_ne_top
+ extremalEpi_coproductOfSetπ
+ fullSubcategory'
+ hasCardinalLT
+ iff_exists_isStrongGenerator
+ instance (C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] [LocallySmall.{w'} C] :
+ instance (G : C' ⥤ C) [F.IsDense] [G.IsEquivalence] :
+ instance (P : ObjectProperty C) [LocallySmall.{w} C]
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
+ instance (P : ObjectProperty Cᵒᵖ) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w} P] :
+ instance (P : ObjectProperty Cᵒᵖ) [P.IsClosedUnderIsomorphisms] :
+ instance (S : SmallCategoryCardinalLT κ) :
+ instance (a : α) : (P.colimitsClosure J).IsClosedUnderColimitsOfShape (J a)
+ instance (a : α) : (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a)
+ instance : (Over.isMono X).IsClosedUnderLimitsOfShape J
+ instance : (P.colimitsCardinalClosure κ).IsClosedUnderIsomorphisms := by
+ instance : (P.colimitsClosure J).IsClosedUnderIsomorphisms
+ instance : (P.limitsClosure J).IsClosedUnderIsomorphisms
+ instance : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms
+ instance : (ιOfLE P.le_isoClosure).IsEquivalence := by rw [isEquivalence_ιOfLE_iff]
+ instance : IsCardinalLocallyPresentable (Type u) κ := by
+ instance : IsCardinalPresentable PUnit.{u + 1} κ
+ instance : IsLocallyPresentable.{u} (Type u)
+ 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 [IsCardinalLocallyPresentable C κ] :
+ instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] :
+ 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.IsClosedUnderColimitsOfShape J] :
+ instance [P.IsClosedUnderColimitsOfShape Jᵒᵖ] :
+ instance [P.IsClosedUnderColimitsOfShape WalkingParallelPair] :
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [P.IsClosedUnderLimitsOfShape J] :
+ instance [P.IsClosedUnderLimitsOfShape Jᵒᵖ] :
+ instance [P.RespectsIso] [P.ContainsIdentities] :
+ instance [Q.IsClosedUnderColimitsOfShape J] :
+ instance [Q.IsClosedUnderColimitsOfShape Jᵒᵖ] :
+ instance [Q.IsClosedUnderLimitsOfShape J] :
+ instance [Q.IsClosedUnderLimitsOfShape Jᵒᵖ] :
+ instance [∀ a, (P a).IsClosedUnderIsomorphisms] :
+ instance {A : Type u'} [Category.{v'} A] (κ : Cardinal.{w}) [Fact κ.IsRegular]
+ instance {A : Type u'} [Category.{v'} A] [IsLocallyPresentable.{w} A] [HasPullbacks A]
+ instance {A : Type u'} [Category.{v'} A] [LocallySmall.{w} A] (C : Type w) [SmallCategory C] :
+ instance {C : Type u} [Category.{v} C] {A : Type u'} [Category.{v'} A]
+ 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] :
+ instance {ι : Type t} [Small.{w} ι] (X : ι → C) : ObjectProperty.Small.{w} (ofObj X)
+ isCardinalPresentable
+ isCardinalPresentable_iff
+ isCardinalPresentable_monotone
+ isClosedUnderColimitsOfShape_colimitsCardinalClosure
+ isClosedUnderColimitsOfShape_iff_of_equivalence
+ isClosedUnderColimitsOfShape_iff_op
+ isClosedUnderColimitsOfShape_iff_unop
+ isClosedUnderColimitsOfShape_isCardinalPresentable
+ isClosedUnderColimitsOfShape_op_iff_op
+ isClosedUnderColimitsOfShape_op_iff_unop
+ isClosedUnderIsomorphisms_iff_isoClosure_eq_self
+ isClosedUnderLimitsOfShape_iff_of_equivalence
+ isClosedUnderLimitsOfShape_iff_op
+ isClosedUnderLimitsOfShape_iff_unop
+ isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair
+ isClosedUnderLimitsOfShape_op_iff_op
+ isClosedUnderLimitsOfShape_op_iff_unop
+ isDense_iff_fullyFaithful_restrictedULiftYoneda
+ isEquivalence_ιOfLE_iff
+ isEssentiallySmall_limitsClosure
+ isIso_of_mono
+ isSeparating
+ isSeparating_iff_exists_epi
+ isStableUnderRetracts_colimitsCardinalClosure
+ isStrongGenerator_iff
+ isStrongGenerator_iff_exists_extremalEpi
+ isStrongGenerator_punit
+ isStrongGenerator_range_of_isDense
+ isoClosure_iSup
+ isoClosure_op
+ isoClosure_strictLimitsClosureIter_eq_limitsClosure
+ isoClosure_sup
+ isoClosure_unop
+ le_colimitsCardinalClosure
+ le_colimitsClosure
+ le_limitsClosure
+ le_strictLimitsClosureIter
+ le_strictLimitsClosureStep
+ limitsClosure
+ limitsClosure_isoClosure
+ limitsClosure_le
+ limitsClosure_monotone
+ limitsOfShape_congr
+ limitsOfShape_eq_unop_colimitsOfShape
+ limitsOfShape_le_of_initial
+ limitsOfShape_op
+ mk_of_exists_epi
+ mk_of_exists_extremalEpi
+ ofObj
+ ofObj_eq_setRange
+ ofObj_iff
+ ofObj_le_iff
+ of_le
+ op
+ op_iff
+ op_injective
+ op_injective_iff
+ op_le_op_iff
+ op_unop
+ prop_colimit
+ prop_iSup_iff
+ prop_inf_iff
+ prop_limit
+ prop_ofObj
+ prop_of_isColimit
+ prop_of_isLimit
+ prop_sup_iff
+ singleton
+ singleton_eq_setSingleton
+ singleton_iff
+ singleton_le_iff
+ small_op_iff
+ small_unop_iff
+ strictLimitsClosureIter
+ strictLimitsClosureIter_le_limitsClosure
+ strictLimitsClosureStep
+ strictLimitsClosureStep_monotone
+ strictLimitsClosureStep_strictLimitsClosureIter_eq_self
+ subobject_eq_top
+ unop
+ unop_iff
+ unop_injective
+ unop_injective_iff
+ unop_le_unop_iff
+ unop_op
+ ι
+ ι_π
+ π
++ instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
++ instance {α : Type*} (P : α → ObjectProperty C)
++ isStrongGenerator
++ reindex
+++ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
- ClosedUnderColimitsOfShape.essImage
- ClosedUnderLimitsOfShape.essImage
- closedUnderLimitsOfShape_isMono
- instCartesianMonoidalCategory
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
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).
…ators' into locally-presentable-presheaf
|
This pull request has conflicts, please merge |
mathlib4-merge-conflict-bot
added
the
merge-conflict
3 participants
If
Cis aw-small category andAis locallyκ-presentable, then the categoryCᵒᵖ ⥤ Type wis locallyκ-presentable; in particular, the category of presheaves of types on a small category is locally (finitely) presentable. (Currently, we formalise this under the additional assumption thatAhas pullbacks. This assumption shall be removed in the future as a locally presentable category is complete.)