mathlib4 feat(CategoryTheory/Functor): refactoring Ran

This PR refactors the definition of the right Kan extension functor (Functor.ran : (C ⥤ E) ⥤ (D ⥤ E)) which sends a functor to its right Kan extension along a given functor F : C ⥤ D. It used to be defined under the existence of certain colimits. It is now part of the general Kan extension API.

The only significant change in this PR is about showing that the right Kan extension functor associated to a cocontinuous functors between sites sends sheaves to sheaves (this is in the file CategoryTheory.Sites.CoverLifting). As this functor is no longer based on the limits API, the proofs had to be changed. In the new proof, we proceed directly with sheaves with values in a category A rather than translating the sheaf property in terms of sheaves of types.

This PR is the dual counterpart of #10425 which refactored left Kan extensions.

As I had to make a slightly nontrivial change in the file Condensed.Solid (currently a leaf file in mathlib), it would be nice to a double-check that the new definitions are mathematically correct.

[x] depends on: #14261
[x] depends on: #14256
[x] depends on: #14258

Jun 30 '24 12:06 joelriou

PR summary fe91dff0d9

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.KanExtension	397	0	-397 (-100.00%)
Mathlib.CategoryTheory.Sites.CoverLifting	660	665	+5 (+0.76%)
Mathlib.CategoryTheory.Sites.DenseSubsite	685	687	+2 (+0.29%)
Mathlib.Condensed.Solid	1529	1528	-1 (-0.07%)

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Limits.KanExtension`	-397
58 files `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.Condensed.TopComparison` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Explicit` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.Topology.Sheaves.LocalPredicate` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.Condensed.Light.TopComparison` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.Condensed.Solid` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.CategoryTheory.Sites.Coherent.Equivalence` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Topology.Sheaves.LocallySurjective` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.Topology.Sheaves.Functors` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.Topology.Sheaves.Operations` `Mathlib.Condensed.Light.Module` `Mathlib.Topology.Sheaves.Skyscraper` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.Condensed.Equivalence` `Mathlib.CategoryTheory.Sites.Coherent.SheafComparison` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.Topology.Sheaves.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Topology.Sheaves.Stalks`	-1
9 files `Mathlib.Topology.Sheaves.SheafCondition.Sites` `Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing` `Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover` `Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts` `Mathlib.Topology.Sheaves.SheafOfFunctions` `Mathlib.CategoryTheory.Sites.Equivalence` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections` `Mathlib.Topology.Sheaves.PUnit`	1
4 files `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.CategoryTheory.Sites.InducedTopology` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.CategoryTheory.Sites.DenseSubsite`	2
`Mathlib.CategoryTheory.Sites.CoverLifting`	5

Declarations diff

+ Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso + IsSheaf.isLimitMultifork + comp_counit_app + comp_unit_app + fac + fac' + hom_ext + instance : (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R) := by + isLimitMultifork + lift + liftAux + liftAux_map + liftAux_map' + profiniteSolidCounit + profiniteSolidIsPointwiseRightKanExtension + pushforwardContinuousSheafificationCompatibility + pushforwardContinuousSheafificationCompatibility_hom_app_val + sheafAdjunctionCocontinuous + sheafAdjunctionCocontinuous_counit_app_val + sheafAdjunctionCocontinuous_homEquiv_apply_val + sheafAdjunctionCocontinuous_unit_app_val + sheafPushforwardContinuousCompSheafToPresheafIso + toSheafify_pullbackSheafificationCompatibility - Functor.pushforwardContinuousSheafificationCompatibility - Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val - Functor.sheafAdjunctionCocontinuous - Functor.toSheafify_pullbackSheafificationCompatibility - adjunction - cone - equiv - getSection - getSection_commute - getSection_isAmalgamation - getSection_is_unique - gluedLimitCone - gluedLimitCone_π_app - gluedSection - gluedSection_isAmalgamation - gluedSection_is_unique - helper - loc - pulledbackFamily - pulledbackFamily_apply - ran - reflective

You can run this locally as follows

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

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

Jun 30 '24 12:06 github-actions[bot]

!bench

Jul 01 '24 14:07 joelriou

Here are the benchmark results for commit 6605fdf416c00f0c10ffadb1886226300529b334. There were significant changes against commit 3ad5ad62a8cd2a2b15e5eab29faba5f294bcdc7d:

  Benchmark                                                 Metric         Change
  ===============================================================================
- ~Mathlib.CategoryTheory.Functor.KanExtension.Adjunction   instructions    85.5%
- ~Mathlib.CategoryTheory.Functor.KanExtension.Pointwise    instructions    88.7%
+ ~Mathlib.CategoryTheory.Limits.KanExtension               instructions   -35.9%

Jul 01 '24 15:07 leanprover-bot

Note: the variations in the benchmark are completely explained by additions/removals of content in these files.

Jul 04 '24 13:07 joelriou

This PR/issue depends on:

~~leanprover-community/mathlib4#14261~~
~~leanprover-community/mathlib4#14256~~
~~leanprover-community/mathlib4#14258~~ By Dependent Issues (🤖). Happy coding!