feat(Topology): A spectral map between quasi-separated, prespectral sober spaces has compact fibers

[Raph-DG]

In this PR, we develop some API around the constructible topology, culminating in the fact that a spectral map between quasi-separated, prespectral sober spaces has compact fibers. To see why this might be of interest, note that the analogous theorem in algebraic geometry (that a quasiseparated map between schemes has quasicompact fibers) does not require any global separatedness assumptions, and the proof of this is very algebraic. So we have the somewhat mysterious situation that it seems as though there are nontrvial topological restrictions on the kinds of spectral maps which can be the underlying maps of morphisms of schemes.

This PR was originally part of #26304, a PR on pushforwards of algebraic cycles. This is where the notion of compactness of fibers becomes relevant, as this guarantees each coefficient of the pushforward of a cycle is computed by a finite sum.

---

[github-actions]

PR summary f15f2c9696

Import changes exceeding 2%

%	File
+6.34%	Mathlib.Topology.WithTopology

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.WithTopology	473	503	+30 (+6.34%)
Mathlib.Topology.Spectral.ConstructibleTopology	895	898	+3 (+0.34%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Spectral.ConstructibleTopology	3
Mathlib.Topology.WithTopology	30

---

Declarations diff (regex)

+ HasCompactFibers
+ IsOpenEmbedding.isSpectralMap_of_compactSpace
+ IsProperMap.hasCompactFibers
+ IsSpectralMap.hasCompactFibers
+ WithConstructibleTopology.continuous_constructibleTopology_id
+ WithConstructibleTopology.continuous_equiv
+ WithConstructibleTopology.equiv
+ WithConstructibleTopology.map
+ WithConstructibleTopology.map_comp
+ WithConstructibleTopology.map_continuous
+ WithConstructibleTopology.map_continuous_iff
+ WithConstructibleTopology.map_id
+ compactSpace_constructibleTopology
+ isOpen_ofConstructibleTopology_preimage_iff
+ map
+ map_continuous_iff
+ ofTopology_comp_map_comp_toTopology
+ t2Space_constructibleTopology
+ t2Space_withConstructibleTopology
+ toConstructibleTopology

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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f15f2c9).

• +20 new declarations
• −0 removed declarations

+HasCompactFibers
+IsProperMap.hasCompactFibers
+IsSpectralMap.hasCompactFibers
+Topology.IsOpenEmbedding.isSpectralMap_of_compactSpace
+WithConstructibleTopology.continuous_constructibleTopology_id
+WithConstructibleTopology.continuous_equiv
+WithConstructibleTopology.equiv
+WithConstructibleTopology.map
+WithConstructibleTopology.map_comp
+WithConstructibleTopology.map_continuous
+WithConstructibleTopology.map_continuous_iff
+WithConstructibleTopology.map_id
+WithTopology.map
+WithTopology.map_continuous_iff
+WithTopology.ofTopology_comp_map_comp_toTopology
+compactSpace_constructibleTopology
+isOpen_ofConstructibleTopology_preimage_iff
+t2Space_constructibleTopology
+t2Space_withConstructibleTopology
+toConstructibleTopology

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f15f2c9696
Reference commit bd1b6969f7

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

It would be nice to wait for #39621, because it refactors WithConstructibleTopology and will hopefully make the proofs easier and less prone to def-eq abuse.

[chrisflav]

#39621 is now merged, could you please merge master and update this PR?

[Raph-DG]

#39621 is now merged, could you please merge master and update this PR?

Awesome, will do. Thanks for the heads up!

[j-loreaux]

not my area of expertise