Spectral maps #
This file defines spectral maps. A map is spectral when it's continuous and the preimage of a compact open set is compact open.
Main declarations #
IsSpectralMap
: Predicate for a map to be spectral.SpectralMap
: Bundled spectral maps.SpectralMapClass
: Typeclass for a type to be a type of spectral maps.
TODO #
Once we have SpectralSpace
, IsSpectralMap
should move to topology.spectral.basic
.
A function between topological spaces is spectral if it is continuous and the preimage of every compact open set is compact open.
A function between topological spaces is spectral if it is continuous and the preimage of every compact open set is compact open.
Instances For
- toFun : α → β
function between topological spaces
- spectral' : IsSpectralMap s.toFun
proof that
toFun
is a spectral map
The type of spectral maps from α
to β
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_spectral : ∀ (f : F), IsSpectralMap ↑f
statement that
F
is a type of spectral maps
SpectralMapClass F α β
states that F
is a type of spectral maps.
You should extend this class when you extend SpectralMap
.
Instances
Spectral maps #
Reinterpret a SpectralMap
as a ContinuousMap
.
Instances For
Copy of a SpectralMap
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
id
as a SpectralMap
.
Instances For
Composition of SpectralMap
s as a SpectralMap
.