[Merged by Bors] - feat(CategoryTheory): Relation between the Grothendieck construction and AsSmall

[javra]

---

[github-actions]

PR summary 7efc4bcbec

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Grothendieck	385	387	+2 (+0.52%)

Import changes for all files

Files	Import difference
240 files Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.CategoryTheory.Sites.Pullback Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.CategoryTheory.Sites.SheafHom Mathlib.Condensed.Limits Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.Topology.Sheaves.Sheaf Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Condensed.TopComparison Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.Algebra.Category.Grp.AB5 Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.CategoryTheory.Monad.Monadicity Mathlib.Condensed.Light.Explicit Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.Topology.Category.LightProfinite.Extend Mathlib.CategoryTheory.Filtered.Final Mathlib.Topology.Sheaves.CommRingCat Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.CategoryTheory.Sites.EpiMono Mathlib.AlgebraicTopology.CechNerve Mathlib.CategoryTheory.Abelian.GrothendieckAxioms Mathlib.Condensed.Explicit Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Condensed.Discrete.Characterization Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Topology.Sheaves.Forget Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Condensed.Light.CartesianClosed Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.CategoryTheory.Monad.Equalizer Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.CategoryTheory.Limits.Presheaf Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Topology.Sheaves.LocalPredicate Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.AlgebraicGeometry.Over Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Discrete.LocallyConstant Mathlib.CategoryTheory.Limits.Preserves.Presheaf Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.CategoryTheory.Monad.Comonadicity Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.Condensed.Solid Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.Condensed.Discrete.Module Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.AlgebraicTopology.SingularSet Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.CategoryTheory.Limits.Shapes.Grothendieck Mathlib.AlgebraicGeometry.Cover.Over Mathlib.Condensed.Light.Epi Mathlib.CategoryTheory.GuitartExact.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.CategoryTheory.Filtered.Grothendieck Mathlib.Geometry.RingedSpace.Basic Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.AffineSpace Mathlib.Condensed.TopCatAdjunction Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.CategoryTheory.Closed.FunctorCategory.Complete Mathlib.CategoryTheory.Limits.IsConnected Mathlib.CategoryTheory.Functor.KanExtension.Adjunction Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Final.ParallelPair Mathlib.Topology.Sheaves.Limits Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Limits.Shapes.Countable Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Topology.Sheaves.LocallySurjective Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicGeometry.AffineScheme Mathlib.CategoryTheory.Limits.Shapes.Reflexive Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.GuitartExact.VerticalComposition Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.CategoryTheory.Closed.Types Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.Geometry.RingedSpace.Stalks Mathlib.Condensed.Light.Limits Mathlib.CategoryTheory.Adjunction.Lifting.Left Mathlib.Condensed.Discrete.Colimit Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.Topology.Category.Profinite.Extend Mathlib.Condensed.CartesianClosed Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Algebra.Homology.LocalCohomology Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.CategoryTheory.Comma.Final Mathlib.AlgebraicGeometry.Scheme Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Condensed.Light.Basic Mathlib.AlgebraicGeometry.Gluing Mathlib.Topology.Sheaves.Functors Mathlib.CategoryTheory.Sites.Over Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.AlgebraicGeometry.Cover.Open Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.CategoryTheory.Adjunction.Lifting.Right Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.Condensed.Epi Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.Topology.Sheaves.PUnit Mathlib.CategoryTheory.Monad.Coequalizer Mathlib.AlgebraicTopology.MooreComplex Mathlib.Condensed.Light.Functors Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.Topology.Sheaves.Presheaf Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Restrict Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.Condensed.Equivalence Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Topology.Sheaves.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.CategoryTheory.Functor.Flat Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Topology.Sheaves.Stalks Mathlib.CategoryTheory.Limits.Final Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.CategoryTheory.Limits.Sifted Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit Mathlib.CategoryTheory.Sites.CoverLifting	1
Mathlib.CategoryTheory.Grothendieck Mathlib.CategoryTheory.Comma.StructuredArrow.Functor	2
Mathlib.CategoryTheory.Category.Cat.AsSmall (new file)	328

---

Declarations diff

+ asSmallFunctor
+ compAsSmallFunctorEquivalence
+ compAsSmallFunctorEquivalenceFunctor
+ compAsSmallFunctorEquivalenceInverse
+ down_comp
+ eqToHom_down
+ mapWhiskerRightAsSmallFunctor

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style