feat(CategoryTheory/Sites): characterization of conservative families of points

[joelriou]

WIP (Only one implication is done)

---

• depends on: feat(CategoryTheory/Sites): conservative family of points #35141
• depends on: feat(CategoryTheory): functors jointly reflecting isomorphisms #35139

[github-actions]

PR summary 590c4e2da2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
182 files 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.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Artinian 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.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial 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.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.QuasiFinite 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.Normalization Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic 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.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf 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.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv 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.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafHom Mathlib.Condensed.AB 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.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.Small Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison 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.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective 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	1
Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly (new file)	599
Mathlib.CategoryTheory.Sites.Point.Conservative (new file)	1129

---

Declarations diff

+ IsConservativeFamilyOfPoints
+ JointlyFaithful
+ JointlyFaithful.of_jointly_reflects_isIso_of_mono
+ JointlyReflectEpimorphisms
+ JointlyReflectEpimorphisms.epi_iff
+ JointlyReflectIsomorphisms
+ JointlyReflectMonomorphisms
+ JointlyReflectMonomorphisms.mono_iff
+ ObjectProperty.IsConservativeFamilyOfPoints.mk'
+ coconeπOpCompShrinkYoneda
+ epi
+ instance [HasSheafify J A] [J.WEqualsLocallyBijective A] [(forget A).ReflectsIsomorphisms]
+ isColimitCoconeπOpCompShrinkYoneda
+ isIso_iff
+ jointlyReflectIsomorphisms
+ jointlyReflectsIsomorphisms
+ jointly_reflect_isLocallySurjective
+ jointly_reflect_ofArrows_mem
+ mono
+ ofArrows_mem_iff_isLocallySurjective
+ shrinkYonedaCompPresheafFiberIso
+ shrinkYonedaCompWhiskeringLeftObjπCompColimIso
+ shrinkYonedaObjObjEquiv_symm_comp
+ shrinkYoneda_map_app_coconeπOpCompShrinkYoneda_ι_app
+ shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm
+ shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm
++ jointlyFaithful
+++ jointlyReflectEpimorphisms
+++ jointlyReflectMonomorphisms

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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Sites): conservative family of points #35141
• feat(CategoryTheory): functors jointly reflecting isomorphisms #35139
  By Dependent Issues (🤖). Happy coding!