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 b6865bbcda

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Spectral.ConstructibleTopology	890	893	+3 (+0.34%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Spectral.ConstructibleTopology	3

---

Declarations diff

+ HasCompactFibers
+ IsOpenEmbedding.isSpectralMap_of_compactSpace
+ IsProperMap.hasCompactFibers
+ IsSpectralMap.hasCompactFibers
+ WithConstructibleTopology.continuous_equiv
+ WithConstructibleTopology.equiv
+ WithConstructibleTopology.map
+ WithConstructibleTopology.map_comp
+ WithConstructibleTopology.map_continuous
+ WithConstructibleTopology.map_id
+ instance [PrespectralSpace X] [T0Space X] [QuasiSober X] :
+ isOpen_ofConstructibleTopology_preimage_iff
+ 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.

---

No changes to strong technical debt.

No changes to weak technical debt.