[Merged by Bors] - refactor(CategoryTheory/Sites): Allow non-fully-faithful dense subsites.

[erdOne]

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Site): Locally fully-faithful functors into sites. #15062
• depends on: [Merged by Bors] - feat(CategoryTheory/Sites): Sieves under equivalences. #15063

[github-actions]

PR summary c5093fe32d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Sites.DenseSubsite	703	890	+187 (+26.60%)
Mathlib.CategoryTheory.Sites.InducedTopology	704	891	+187 (+26.56%)
Mathlib.CategoryTheory.Sites.Discrete	727	892	+165 (+22.70%)
Mathlib.CategoryTheory.Sites.Coherent.SheafComparison	882	913	+31 (+3.51%)
Mathlib.CategoryTheory.Sites.Equivalence	893	894	+1 (+0.11%)

Import changes for all files

Files	Import difference
13 files Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.Topology.Sheaves.LocallySurjective Mathlib.CategoryTheory.Sites.Equivalence Mathlib.Condensed.Light.Module Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.Condensed.Light.Discrete Mathlib.Condensed.Epi	1
Mathlib.Condensed.TopCatAdjunction	5
Mathlib.Condensed.TopComparison Mathlib.Condensed.Explicit	6
Mathlib.AlgebraicGeometry.Modules.Presheaf	18
31 files Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Stalk Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed	19
15 files Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.AlgebraicGeometry.Spec Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.Basic Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Topology.Sheaves.Operations Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Sheafify Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Topology.Sheaves.Stalks	20
Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Topology.Sheaves.Functors	21
Mathlib.Condensed.Equivalence	28
Mathlib.CategoryTheory.Sites.Coherent.SheafComparison	31
4 files Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections	44
3 files Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.PUnit	47
Mathlib.CategoryTheory.Sites.Discrete	165
Mathlib.CategoryTheory.Sites.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite	187

---

Declarations diff

+ IsCoverDense.sheafEquivOfCoverPreservingCoverLifting
+ IsCoverDense.sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility
+ IsDenseSubsite
+ equalizer_mem
+ faithful_sheafPushforwardContinuous
+ full_sheafPushforwardContinuous
+ imageSieve_mem
+ inducedTopologyOfIsCoverDense
+ instance (priority := 900) [G.IsCoverDense K] : G.IsDenseSubsite (G.inducedTopology K) K
+ instance (priority := 900) [G.IsDenseSubsite J K] : G.IsCocontinuous J K
+ instance (priority := 900) [G.IsDenseSubsite J K] : G.IsContinuous J K
+ instance (priority := 900) [G.IsEquivalence] : IsCoverDense G J
+ instance (priority := 900) locallyCoverDense_of_isCoverDense [G.IsCoverDense K] :
+ instance : e.TransportsGrothendieckTopology J (e.inverse.inducedTopology J) := ⟨rfl⟩
+ instance : e.functor.IsDenseSubsite J (e.inverse.inducedTopology J) := by
+ instance : haveI := F.reflects_precoherent;
+ instance : haveI := F.reflects_preregular;
+ isCoverDense
+ isIso_ranCounit_app_of_isDenseSubsite
+ isLocallyFaithful
+ isLocallyFull
+ naturality
+ naturality_apply
+ sheafEquiv
+ sheafInducedTopologyEquivOfIsCoverDense
++- coverPreserving
- Functor.locallyCoverDense_of_isCoverDense
- Functor.sheafInducedTopologyEquivOfIsCoverDense
- instance : IsCoverDense e.functor (e.locallyCoverDense J).inducedTopology
- instance : IsCoverDense e.inverse J
- instance : e.TransportsGrothendieckTopology J (e.locallyCoverDense J).inducedTopology := ⟨rfl⟩
- locallyCoverDense
- sheafEquivOfCoverPreservingCoverLifting
-- coverLifting
-- instance [G.Full] [G.Faithful] [G.IsCoverDense K] :
---+ isContinuous

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>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Site): Locally fully-faithful functors into sites. #15062
• [Merged by Bors] - feat(CategoryTheory/Sites): Sieves under equivalences. #15063
  By Dependent Issues (🤖). Happy coding!

[erdOne]

Can this be replaced with the new IsDenseSubsite typeclass? @dagurtomas

[joelriou]

I would think that for an equivalence of categories, the TransportsGrothendieckTopology condition should be equivalent to the functorPushforward_mem_iff condition from IsDenseSubsite (while the first three should be automatic). However, the main goal of the TransportsGrothendieckTopology API is to show that the HasSheafify assumption can be transported by an equivalence of categories, and for this we cannot use the main result sheafEquiv of this new IsDenseSubsite API because of the existence of limits assumption. Then, it could be interesting to write an iff lemma for IsDenseSubsite in the case of an equivalence, and maybe change the definition of TransportsGrothendieckTopology, but I do not think that this needs to be done in this PR.

[erdOne]

Yes the results below needs to stay. I'm just saying that the type class itself could be replaced, and should it?
Not in this PR anyways.

[dagurtomas]

I agree that this is probably equivalent, but I haven't worked out the details.

#13486 has now been adapted and is ready for review.

[joelriou]

Suggested change

	ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
	ReflectsIsomorphisms.reflects (sheafToPresheaf J A)

[joelriou]

Here, I believe you could use NatTrans.isIso_iff_isIso_app.

[joelriou]

Thanks!

bors d+

[mathlib-bors]

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

Thanks for the review!
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style