add kspace properties and theorems

[StevenClontz]

See #230

[prabau]

Shouldn't this be instead that a subset $U\subseteq X$ is open in $X$ if for every continuous map $f:K\to X$ with $K$ an arbitrary compact space, the inverse image $f^{-1}(U)$ is compact in $K$? And same thing for P141. Maybe we could mention "final topology" also?

[StevenClontz]

"image $f^{-1}(U)$ is open in K" I think, yes. I was being lazy when copy-pasting definitions and didn't think about this carefully.

I think these are equivalent when $f$ is an inclusion map from a subspace; it's less clear that these are equivalent when $f$ is not injective (and I suspect they aren't).

[prabau]

Where does Kelley space come from? As far as I know, the notion of compactly generated in Kelley's book of 1955 was "coherent with the collection of closed compact subspaces", which is different.

[StevenClontz]

Took this from https://ncatlab.org/nlab/show/compactly+generated+topological+space (also uses "kaonic space")

[prabau]

Checking the pdf linked from the nlab article, Kelley space is defined as Hausdorff space with P140. I don't think we should even mention this in pi-base.

[StevenClontz]

@prabau feel free to edit on this branch directly, or I'll return to this later this week.

[prabau]

I am wondering what the best terminology for these spaces is. "Generated" is ok, and so is maybe "determined" (as introduced by Gruenhage et al, https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-113/issue-2/Spaces-determined-by-point-countable-covers/pjm/1102709194.full). Not sure what my preference is, just writing it down to make it easier to decide.

Some possibilities for P142:

• Generated by compact Hausdorff subspaces
• Determined by compact Hausdorff subspaces

For P141:

• Generated by compact Hausdorff maps (maybe not so clear what a compact map is?)
• Generated by maps from compact Hausdorff spaces (clear, but too long?)
• Generated by maps from compact Hausdorff
• Determined by ...

For P140:

• Generated by compact subspaces
• ...

[StevenClontz]

Is "determined" correct for P141? It's defined in terms of the subspace topology within f[K], not the inverse image within K.

[prabau]

Is "determined" correct for P141? It's defined in terms of the subspace topology within f[K], not the inverse image within K.

Yeah, it does not really apply there.