search

pi-base / viewer

Web UI for the π-Base
https://topology.pi-base.org
MIT License
9 stars 3 forks source link

Relationships between spaces #13

Open jamesdabbs opened 7 years ago

jamesdabbs commented 7 years ago

We eventually want to support full-on automated theorem prover integration, but would it be possible to model a handful of simple relationships between spaces ("is a (closed) subspace of", "is a product of")?

StevenClontz commented 7 years ago

On a related note, I'm also imagining a functor model, that does things like send X \mapsto C_p(X). Cp theory in particular has lots of nice results such as when X is T{3.5}, X is sigma-compact if and only if C_p(X) is Markov countably fan tight. So if S42 represents X and F13 represents applying C_p, we could have "spaces" like S42+F13 to represent C_p(X), and pi-base automatically converts the properties of X into the properties of C_p(X). In the case that C_p(X) is has been specifically studied in the literature and additional results not characterized by the functor itself are known, then a new space (and new uid) should be added to the database, and S42+F13 could redirect to it.