-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(topology/spectral/hom): Spectral maps #12228
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The fun_like
parts look good to me, but I know very little about spectral maps to confirm the definition itself. So let's ask another reviewer.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
variables [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {s : set β} | ||
|
||
/-- A function between topological spaces is spectral if it is continuous and the preimage of every | ||
compact open set is compact open. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
compact open set is compact open. -/ | |
compact open set is compact. -/ |
Define spectral maps in three ways: * `is_spectral_map`, the unbundled predicate * `spectral_map`, the bundled type * `spectral_map_class`, the hom class The design for `is_spectral_map` matches `continuous`. The design for `spectral_map` and `spectral_map_class` follows the hom refactor.
Pull request successfully merged into master. Build succeeded: |
Define spectral maps in three ways:
is_spectral_map
, the unbundled predicatespectral_map
, the bundled typespectral_map_class
, the hom classThe design for
is_spectral_map
matchescontinuous
. The design forspectral_map
andspectral_map_class
follows the hom refactor.The plan is to add spectral spaces in
topology.spectral.basic
andSpectral
, the category, intopology.category.Spectral
.