feat(Topology/Spectral/ConstructibleTopology): properties of spectral maps

[FMLJohn]

---

• depends on: feat(Topology): A spectral map between quasi-separated, prespectral sober spaces has compact fibers #39663

In this pull request, I have proved some basic properties of spectral maps related to constructible topologies.

Main Results

1. IsSpectralMap.constructibleTopology_eq_induced_of_isEmbedding: Given two prespectral topological spaces X and Y and a spectral embedding f : X → Y, the constructible topology on X is the same as the topology induced by the constructible topology on Y via f.
2. WithConstructibleTopology.isSpectralMap_iff_continuous_and_map_continuous: Given topological spaces X and Y and a map f : X → Y, if X is compact, quasi-sober, quasi-separated and prespectral, then f is spectral if and only if it is continuous with respect to both the original topologies and the constructible topologies on X and Y.

Note that these results hold in particular when both X and Y are spectral.

This PR depends on #39663. I have updated the material from #39663 so that it compiles with the latest version of Mathlib. I have also generalised the declaration WithConstructibleTopology.map to the more general notion WithTopology.map.

[github-actions]

PR summary 142db82377

Import changes exceeding 2%

%	File
+5.98%	Mathlib.Topology.WithTopology

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.WithTopology	485	514	+29 (+5.98%)
Mathlib.Topology.Spectral.ConstructibleTopology	905	908	+3 (+0.33%)

Import changes for all files

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

---

Declarations diff (regex)

+ HasCompactFibers
+ IsOpenEmbedding.isSpectralMap_of_compactSpace
+ IsProperMap.hasCompactFibers
+ IsSpectralMap.constructibleTopology_eq_induced_of_isEmbedding
+ IsSpectralMap.hasCompactFibers
+ Topology.IsEmbedding.exists_of_isOpen_isCompact
+ WithConstructibleTopology.continuous_constructibleTopology_id
+ WithConstructibleTopology.continuous_equiv
+ WithConstructibleTopology.equiv
+ WithConstructibleTopology.isCompact_preimage_of_map_continuous
+ WithConstructibleTopology.isSpectralMap_iff_continuous_and_map_continuous
+ WithConstructibleTopology.isSpectralMap_of_continuous_of_map_continuous
+ WithConstructibleTopology.map
+ WithConstructibleTopology.map_comp
+ WithConstructibleTopology.map_continuous
+ WithConstructibleTopology.map_continuous_iff
+ WithConstructibleTopology.map_eq_map
+ WithConstructibleTopology.map_id
+ compactSpace_constructibleTopology
+ constructibleTopology_le
+ isCompact_of_le_of_isCompact
+ 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 142db82).

• +28 new declarations
• −0 removed declarations

+HasCompactFibers
+IsProperMap.hasCompactFibers
+IsSpectralMap.constructibleTopology_eq_induced_of_isEmbedding
+IsSpectralMap.hasCompactFibers
+Topology.IsEmbedding.exists_of_isOpen_isCompact
+Topology.IsOpenEmbedding.isSpectralMap_of_compactSpace
+WithConstructibleTopology.continuous_constructibleTopology_id
+WithConstructibleTopology.continuous_equiv
+WithConstructibleTopology.equiv
+WithConstructibleTopology.isCompact_preimage_of_map_continuous
+WithConstructibleTopology.isSpectralMap_iff_continuous_and_map_continuous
+WithConstructibleTopology.isSpectralMap_of_continuous_of_map_continuous
+WithConstructibleTopology.map
+WithConstructibleTopology.map_comp
+WithConstructibleTopology.map_continuous
+WithConstructibleTopology.map_continuous_iff
+WithConstructibleTopology.map_eq_map
+WithConstructibleTopology.map_id
+WithTopology.map
+WithTopology.map_continuous_iff
+WithTopology.ofTopology_comp_map_comp_toTopology
+compactSpace_constructibleTopology
+constructibleTopology_le
+isCompact_of_le_of_isCompact
+isOpen_ofConstructibleTopology_preimage_iff
+t2Space_constructibleTopology
+t2Space_withConstructibleTopology
+toConstructibleTopology

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 142db82377
Reference commit 6ca518ac72

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

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Topology): A spectral map between quasi-separated, prespectral sober spaces has compact fibers #39663
  By Dependent Issues (🤖). Happy coding!