feat(Topology/Category): the standard Grothendieck topology on TopCat

[chrisflav]

We define the Grothendieck topology generated by families of jointly surjective open embeddings on TopCat and show it is subcanonical. This will be used to show that for a topological space T, the presheaf U ↦ C(U, T) on Scheme is a Zariski-sheaf.

Co-authored by: Edward van de Meent edwardvdmeent@gmail.com

From Proetale.

---

[github-actions]

PR summary 8115783e28

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Sites.JointlySurjective	602	604	+2 (+0.33%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Sites.JointlySurjective	2
Mathlib.Topology.Category.TopCat.GrothendieckTopology (new file)	923

---

Declarations diff

+ IsStableUnderBaseChange.of_forall_exists_isPullback
+ IsStableUnderCobaseChange.of_forall_exists_isPullback
+ Small.inf
+ Topology.IsClosedEmbedding.uliftMap
+ Topology.IsEmbedding.uliftMap
+ Topology.IsOpenEmbedding.uliftMap
+ exists_mem_zeroHypercover_range
+ grothendieckTopology
+ instance : Precoverage.Small.{u} jointlySurjectivePrecoverage.{u}
+ instance : Precoverage.Small.{u} precoverage.{u}
+ instance : isOpenEmbedding.IsMultiplicative
+ instance : isOpenEmbedding.IsStableUnderBaseChange
+ instance : isOpenEmbedding.RespectsIso
+ instance {D : Type*} [Category* D] {F : C ⥤ D} (J : Precoverage D) [Small.{w} J] :
+ isOpenEmbedding
+ isOpenEmbedding_f_zeroHypercover
+ isOpenEmbedding_iff
+ precoverage
+ subcanonical_grothendieckTopology
+ toHomeomorph_symm_apply

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

[chrisflav]

Thanks for the reviews @joelriou, @peabrainiac!