refactor(CategoryTheory): colimits of representable presheaves

[joelriou]

The file Mathlib/CategoryTheory/Limits/Presheaf.lean has already been refactored a few times. This PR is an effort in order to cleanup this file which contains various results about presheaves of types which should be organized better. All the definitions in Limits/Presheaf.lean have been moved or deprecated.
The fact that a presheaf of types is a colimit of representable presheaves is now in the file Functor/KanExtension/DenseAtYoneda.lean. The results are stated using cocones indexed by (the opposite) of a category of elements, but they are also stated as the density of the Yoneda embedding Functor.IsDense. We prove the results first for the most general version of the Yoneda embedding which is shrinkYoneda, and we deduce similar results for uliftYoneda and yoneda. (Some dual versions are also obtained in the file Functor/KanExtension/DenseAtCoyoneda.lean).
Results about left Kan extensions along the Yoneda embedding are obtained in the file Functor/KanExtension/RestrictedYoneda.lean, and an application is obtained in the file Functor/KanExtension/RestrictedYoneda.lean: if F is a functor between locally w-small categories, we have the isomorphism F ⋙ shrinkYoneda.{w} ≅ shrinkYoneda.{w} ⋙ F.op.lan, which makes F.op.lan a left Kan extension of F ⋙ shrinkYoneda.{w} along the Yoneda embedding.
(Doing so required splitting the file Dense.lean. New files DenseIff.lean and StrongGenerator.lean contains respectively a characterization of dense functors in terms of the restricted Yoneda functors, and the fact that the image of a dense functor is strong generator.)

---

• depends on: feat(CategoryTheory/Limits): commutation of limits and colimits #43977

[github-actions]

PR summary ec1177aa9f

Import changes exceeding 2%

%	File
+16.52%	Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits	1017	1185	+168 (+16.52%)
Mathlib.CategoryTheory.Functor.KanExtension.Dense	903	769	-134 (-14.84%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Functor.KanExtension.Dense	-134
3 files Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.Monoidal.Closed.Types	2
17 files Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.Presentable.CardinalPure Mathlib.CategoryTheory.Presentable.Comma Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.Presheaf Mathlib.CategoryTheory.Presentable.SharplyLT.Basic Mathlib.CategoryTheory.Presentable.SharplyLT.Lemmas Mathlib.CategoryTheory.Presentable.SolutionSetCondition Mathlib.CategoryTheory.Presentable.StrongGenerator Mathlib.CategoryTheory.Presentable.Type Mathlib.CategoryTheory.Presentable.Uniformization	3
9 files Mathlib.AlgebraicTopology.SimplicialSet.Subdivision Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.AlgebraicTopology.SingularSet Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy	4
341 files Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.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.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf.Submodule Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Category.Ring.Under.Property Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Birational.Birational Mathlib.AlgebraicGeometry.Birational.Composition Mathlib.AlgebraicGeometry.Birational.Dominant Mathlib.AlgebraicGeometry.Birational.RationalMap Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Connected Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Affine Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde 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.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.FlatRank 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.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber 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.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.OrderOfVanishing Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.Affine Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.AlgebraicTopology.ModelCategory.Over Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.InnerFibration Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.Quasicategory.TwoTruncatedQuasicategory Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms Mathlib.AlgebraicTopology.SimplicialSet.Skeleton 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.PresheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.SheafOfModules 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.HasExt 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.Adhesive.Over Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Filtered.CostructuredArrow Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Filtered.FinallySmall Mathlib.CategoryTheory.Filtered.Flat Mathlib.CategoryTheory.Functor.Flat Mathlib.CategoryTheory.Functor.TypeValuedFlat Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Limits.ConstructLimitMap Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit 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.FunctorCategory Mathlib.CategoryTheory.Limits.Preserves.Presheaf Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete Mathlib.CategoryTheory.Monoidal.Limits.Colimits Mathlib.CategoryTheory.MorphismProperty.CommaSites Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.ColimitPresentation Mathlib.CategoryTheory.Presentable.Directed Mathlib.CategoryTheory.Presentable.EssentiallyLarge Mathlib.CategoryTheory.Presentable.Finite Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.IsDiscrete Mathlib.CategoryTheory.Presentable.Limits Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.PreservesCardinalPresentable Mathlib.CategoryTheory.Presentable.Retracts Mathlib.CategoryTheory.Sites.Abelian 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.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.CoversTop.Over Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.Descent.IsStack Mathlib.CategoryTheory.Sites.Descent.Precoverage Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.InducedTopology Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocalProperties Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.RegularEpi Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.SubcanonicalOver Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration Mathlib.CategoryTheory.Topos.Sheaf Mathlib.Condensed.AB Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Instances Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Sequence Mathlib.Condensed.Light.Small Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid 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.Order.Interval.Set.Final Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Sets.BaseChangeNhds Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.EtaleSpace Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.Module Mathlib.Topology.Sheaves.Over 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	5
16 files Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.EtalePoint Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.IsMonoidalW Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.Monoidal Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.Topology.Sheaves.Points	6
3 files Mathlib.CategoryTheory.Limits.Presheaf Mathlib.CategoryTheory.Sites.LocalSite Mathlib.CategoryTheory.Sites.Point.Presheaf	7
Mathlib.CategoryTheory.Limits.Types.PreservesLimit Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits	168
Mathlib.CategoryTheory.RestrictedYoneda (new file)	569
Mathlib.CategoryTheory.Functor.KanExtension.DenseIff (new file)	771
Mathlib.CategoryTheory.Functor.KanExtension.DenseAtYoneda (new file)	784
Mathlib.CategoryTheory.Functor.KanExtension.DenseAtCoyoneda (new file)	785
Mathlib.CategoryTheory.Functor.KanExtension.RestrictedYoneda (new file)	786
Mathlib.CategoryTheory.Functor.KanExtension.Yoneda (new file)	789
Mathlib.CategoryTheory.Functor.KanExtension.StrongGenerator (new file)	892

---

Declarations diff (regex)

+ IsDense.of_fullyFaithful_restrictedShrinkYoneda
+ IsDense.of_fullyFaithful_restrictedYoneda
+ Presheaf.final_toCostructuredArrow_comp_pre
+ colim.coconeCompFlip
+ colim.coconeFlip
+ colim.isColimitCoconeCompFlip
+ colim.isColimitCoconeFlip
+ colimitLimToLimitColim
+ colimitLimToLimitColim_eq_colimit_desc
+ colimitLimToLimitColim_eq_limit_lift
+ compShrinkYonedaIsoShrinkYonedaCompLan
+ compShrinkYonedaIsoShrinkYonedaCompLan_inv_app_app_eq_id
+ comp_restrictedShrinkYonedaHomEquiv_symm_apply
+ comp_shrinkYonedaMap_comp_eq_uliftYonedaMap
+ comp_shrinkYonedaMap_comp_eq_yonedaMap
+ comp_whiskerLeft_compShrinkYonedaIsoShrinkYonedaCompLan_hom_app
+ comp_whiskerLeft_compShrinkYonedaIsoShrinkYonedaCompLan_inv_app
+ congrElements
+ costructuredArrowShrinkCoyonedaEquivalence
+ costructuredArrow_yoneda_equivalence_naturality
+ denseAtCoyoneda
+ denseAtShrinkCoyoneda
+ denseAtShrinkYoneda
+ hasPointwiseLeftKanExtension_shrinkYoneda_of_uliftYoneda
+ initialShrinkCoyonedaObj
+ initialShrinkYonedaObj
+ instance (F : C ⥤ D) (X : C) : (uliftYoneda.{max w v₁}.obj (F.obj X)).IsLeftKanExtension
+ instance (F : K ⥤ J) [HasColimitsOfShape K' C] :
+ instance (L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ D) [PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂} L]
+ instance (L : (Cᵒᵖ ⥤ Type w) ⥤ D) [PreservesColimitsOfSize.{v₁, max w u₁} L]
+ instance (X : C) (Y : F.op.LeftExtension (shrinkYoneda.{w}.obj X)) :
+ instance (X : C) :
+ instance :
+ instance : (L.lan (H := H)).IsLeftAdjoint := (L.lanAdjunction H).isLeftAdjoint
+ instance : (coyoneda (C := C)).IsDense
+ instance : F.op.lan.IsLeftKanExtension (compShrinkYonedaIsoShrinkYonedaCompLan.{w} F).hom
+ instance : F.op.lan.IsLeftKanExtension (compULiftYonedaIsoULiftYonedaCompLan.{w} F).hom := by
+ instance : IsIso α
+ instance [F.IsDense] : (restrictedYoneda F).Faithful
+ instance [F.IsDense] : (restrictedYoneda F).Full
+ instance [F.IsDense] [LocallySmall.{w} D] : (restrictedShrinkYoneda.{w} F).Faithful
+ instance [F.IsDense] [LocallySmall.{w} D] : (restrictedShrinkYoneda.{w} F).Full
+ instance [HasColimitsOfShape K' C] :
+ instance [HasColimitsOfShape K' C] [HasExactColimitsOfShape K' C] [HasFiniteLimits C] :
+ instance [HasColimitsOfShape K' C] [HasLimitsOfShape K C]
+ instance [HasFiniteColimits C] :
+ instance [LocallySmall.{w} C] : (shrinkCoyoneda.{w} (C := C)).IsDense
+ instance [LocallySmall.{w} C] : (shrinkYoneda.{w} (C := C)).IsDense
+ instance {D : Type*} [Category.{v₁} D] (F : C ⥤ D) (X : C) :
+ instance {F' : D ⥤ H} (α : F₁ ⟶ L ⋙ F') [F'.IsLeftKanExtension α]
+ instance {F' : D ⥤ H} (α : L ⋙ F' ⟶ F₁) [F'.IsRightKanExtension α]
+ instance {F'' : D ⥤ H} {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (f : F' ⟶ F'') [IsIso f]
+ instance {F'' : D ⥤ H} {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (f : F'' ⟶ F') [IsIso f]
+ instance {L L' : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (f : L ⟶ L') [IsIso f]
+ instance {L L' : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (f : L' ⟶ L) [IsIso f]
+ instance {ι : Type*} (P : ι → ObjectProperty C) [∀ i, (P i).IsClosedUnderColimitsOfShape J] :
+ instance {ι : Type*} (P : ι → ObjectProperty C) [∀ i, (P i).IsClosedUnderLimitsOfShape J] :
+ isColimitShrinkCoyonedaCocone
+ isColimitShrinkCoyonedaCoconeObj
+ isColimitShrinkYonedaCocone
+ isColimitShrinkYonedaCoconeObj
+ isColimitUliftYonedaCocone
+ isColimitUliftYonedaCoconeObj
+ isColimitYonedaCocone
+ isColimitYonedaCoconeObj
+ isDense_iff_fullyFaithful_restrictedShrinkYoneda
+ isDense_iff_fullyFaithful_restrictedYoneda
+ isInitialShrinkCoyonedaObj
+ isInitialShrinkYonedaObj
+ isIso_colimitLimToLimitColim_iff_preservesColimit
+ isIso_colimitLimToLimitColim_iff_preservesLimit
+ isLeftKanExtension_along_shrinkYoneda_iff
+ isLeftKanExtension_along_shrinkYoneda_of_preservesColimits
+ isLeftKanExtension_along_uliftYoneda_of_preservesColimits
+ isPointwiseLeftKanExtensionAlongShrinkYoneda
+ isPointwiseLeftKanExtensionLanOp
+ lim.cone
+ lim.isLimitCone
+ mapElementsOpCompToCostructuredArrow
+ preservesColimit_flip_lim_iff_preservesLimit_colim
+ preservesColimit_lim_iff_preservesLimit_colim
+ preservesColimitsOfShape_lim_iff_preservesLimitsOfShape_colim
+ presheafHom'
+ restrictedShrinkYoneda
+ restrictedShrinkYonedaAdjunction
+ restrictedShrinkYonedaAdjunction_homEquiv
+ restrictedShrinkYonedaAdjunction_unit_app_app
+ restrictedShrinkYonedaHomEquiv
+ restrictedShrinkYonedaHomEquivAux
+ restrictedShrinkYonedaHomEquiv_app_apply
+ restrictedShrinkYonedaHomEquiv_naturality_left
+ restrictedShrinkYonedaHomEquiv_naturality_right
+ restrictedShrinkYonedaHomEquiv_symm_naturality_left
+ restrictedShrinkYonedaHomEquiv_symm_naturality_right
+ restrictedULiftYonedaAdjunction
+ restrictedULiftYonedaAdjunction_homEquiv_app
+ restrictedULiftYonedaAdjunction_unit_app_app
+ restrictedULiftYonedaIso
+ restrictedYoneda
+ restrictedYonedaIso
+ shrinkCoyonedaCocone
+ shrinkCoyonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm_comp
+ shrinkYonedaCocone
+ shrinkYonedaEquiv_apply
+ shrinkYonedaEquiv_symm_app
+ shrinkYonedaEquiv_symm_comp
+ shrinkYonedaMap
+ shrinkYonedaMap_app_shrinkYonedaObjObjEquiv_symm
+ shrinkYoneda_map_app_shrinkCoyonedaCocone_ι_app_app
+ uliftYonedaCocone
+ uliftYonedaEquiv_symm_naturality_left
+ uliftYonedaIsoShrinkYoneda_hom_app_app
+ uliftYonedaIsoShrinkYoneda_hom_app_comp_shrinkYoneda_symm
+ uliftYonedaIsoShrinkYoneda_inv_app_app
+ uliftYonedaIsoShrinkYoneda_inv_app_comp_uliftYonedaEquiv_symm
+ yonedaCocone
+ ι_colimitToLimit_π
++ ι
- final_toCostructuredArrow_comp_pre
- instance (L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ ℰ) [PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂} L]
- instance (X : C) (Y : F.op.LeftExtension (uliftYoneda.{max w v₂}.obj X)) :
- instance (X : C) (Y : F.op.LeftExtension (yoneda.obj X)) :
- instance (X : C) : (uliftYoneda.{max w v₁}.obj (F.obj X)).IsLeftKanExtension
- instance (X : C) : (yoneda.obj (F.obj X)).IsLeftKanExtension (yonedaMap F X)
- instance (X : C) : HasInitial (shrinkYoneda.{w}.flip.obj (op X)).Elements
- instance (Φ : StructuredArrow (F ⋙ uliftYoneda.{max w v₁})
- instance : F.op.lan.IsLeftKanExtension (compULiftYonedaIsoULiftYonedaCompLan.{w} F).hom
- instance : IsIso (uliftYoneda.{max w v₂}.leftKanExtensionUnit A)
- instance [L.IsLeftKanExtension α] : IsIso α

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

Decrease in strong tech debt: (relative, absolute) = (8.87, 0.01)

Current number	Change	Type (strong)
4104	-22	backward.defeqAttrib.useBackward
4284	-8	backward.isDefEq.respectTransparency
2294	-2	backward.isDefEq.respectTransparency.types

Increase in weak tech debt: (relative, absolute) = (7.00, 0.00)

Current number	Change	Type (weak)
5076	7	exposed public sections

Current commit ec1177aa9f
Reference commit 1a547d8a48

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[mathlib-merge-conflicts]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Limits): commutation of limits and colimits #43977
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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