Compactly generated spaces

Stream: maths

[Floris van Doorn]

My student @Hannah Scholz is working on CW-complexes and wants to define compactly generated spaces. In Mathlib we have a very similar notion docs#IsCompactlyGenerated for complete lattices that are compactly generated.
Am I correct that the current Mathlib notion does not allow us to define compactly generated spaces, since IsCompactlyGenerated (Opens X) would state that all opens are generated by compact open sets?

Does this mean we should generalize the concepts IsCompactlyGenerated and CompleteLattice.IsCompactElement to be "these elements are compact(ly generated) w.r.t. to this sublattice. If we do that, we can say that K : Set X is compact iff it is an compact element w.r.t. to the sublattice of open sets, and X is a compactly generated space iff all the opens are sups of compact elements.

Or should we just define a separate notion of compactly generated spaces?

[Yaël Dillies]

Floris van Doorn said:

Does this mean we should generalize the concepts IsCompactlyGenerated and CompleteLattice.IsCompactElement to be "these elements are compact(ly generated) w.r.t. to this sublattice

Yes, this seems like the most reasonable option

[Johan Commelin]

I am a bit worried that this will make existing use cases jump through unnecessary hoops.

[Yaël Dillies]

There are not that many existing use cases, right?

[Johan Commelin]

I didn't check. But I know it's used for the lattice of submodules in some places.

[Floris van Doorn]

Actually, is docs#IsCompactlyGenerated even related to the topological notion of compactly generated spaces / K-spaces? Every set is already a sup of compact sets in any topological space, by docs#isCompact_singleton

[Damiano Testa]

In this context, I always think of "compact" as meaning "compact and closure of an open set" (or sometimes as "open set that has compact closure"). This is more related to pre-compact, than compact, I think.

[Yaël Dillies]

Floris van Doorn said:

Actually, is docs#IsCompactlyGenerated even related to the topological notion of compactly generated spaces / K-spaces? Every set is already a sup of compact sets in any topological space, by docs#isCompact_singleton

Reading the wikipedia page about compactly generated spaces, it seems like it's completely different actually

[Yaël Dillies]

I must say "compactly generated" is a weird name for the topological notion. I would rather have expected something like "compactly specified"

[David Michael Roberts]

I would point out that one shouldn't assume Hausdorffness, so that one can separately have CGWH (i.e. with weak Hausdorffness) or CGH spaces. So the topology is generated by a maps from a family compact Hausdorff spaces, not from a collection of compact subsets.

[Adam Topaz]

@Floris van Doorn you may want to see #14514

[Yury G. Kudryashov]

@Anatole Dedecker was going to investigate which of the three definitions we should formalize first.

[Yury G. Kudryashov]

Some can be easily formalized using docs#RestrictGenTopology, the one in #14514 is a different one.

[Yury G. Kudryashov]

@Steven Clontz What do you think about this? If we want to start with one of the definitions and add other definitions later as needed, which one should we first?

[Adam Topaz]

Maybe I should add that the PR I mention above depends on this one which defines compactly generated spaces: #14508
All this (great!) work was done by @Dagur Asgeirsson .

[Dagur Asgeirsson]

The definition in #14508 is really designed to make the proof in #14514 that it's a full subcategory of condensed sets easy. I'm not sure it should be the "official definition", at least one should develop some API to characterize open/closed sets etc.

I should also mention that the analogous result for light condensed sets and sequential spaces (defined using the existing mathlib notion) went really smoothly using the existing API. See #14618

[Steven Clontz]

In the literature, authors frequently define k-space uncritically, and I think it may actually have been Wikipedia editors that first carefully sussed out the three different notions, which pi-Base adopted: CG3 implies CG2 implies CG1. There are corresponding separation axioms known as k-Hausdorff that I have a preprint teasing out: $T_2$ implies k1H implies (two other weak Hausdorff properties from the literature, which imply) k2H implies (another weak Hausdorff property implies) $T_1$. (k3H is something you can define, but doesn't even imply $T_0$ so it's not a great "separation axiom").

Under $T_2$ all the CGs are equivalent (hence the uncareful treatment in the literature). The square of the one-point compactification of the rationals is weak Hausdorff but and CG1, but not CG3. But under the weak Hausdorff property, or even just k2H, CG2 and CG3 are equivalent.

[Steven Clontz]

I should puzzle out whether k1H or KC (compacts are closed) is sufficient to get all CGs to be equivalent, rather than needing all of $T_2$. (EDIT: hm, well, it's pretty immediate that k1H is sufficient for all CGs to be equivalent - it literally means that all compacts are Hausdorff.)

[Steven Clontz]

my gut instinct is that CG2 is the place to start, with a theorem that it is implied by CG3. I think CG1 is mostly just used when Hausdorff is taken for granted anyway.

[Dagur Asgeirsson]

#14508 is ready for review. I'd be happy to change the name to something like UCompactlyGenerated, since there is some emphasis on size here (e.g. the category which embeds fully faithfully in condensed sets is that of u-compactly generated topological spaces of size u+1 (i.e. those X : TopCat.{u+1} such that continuity can be tested by precomposing with maps from S : CompHaus.{u})).

There are also some TODOs in the file, the last one being the most important (that all first countable spaces are u-compactly generated for every u) since it shows that there is a large class of examples. I will work on that soon, but it might require developing some API for transporting topologies via ULift, which I think we don't have much of in mathlib?

[Dagur Asgeirsson]

The fully faithful embedding of compactly generated spaces in condensed sets (#14514) and sequential spaces in light condensed sets (#14618) are now independent and both ready for review

[Floris van Doorn]

Dagur Asgeirsson said:

might require developing some API for transporting topologies via ULift

I'm wondering whether it is actually easier to use α × PUnit instead of ULift α, since the API for products and terminal objects is better developed (although I have noticed with a student that Lean sometimes needs universe-annotations for the former)

[Dagur Asgeirsson]

I hadn’t thought of that, sounds like a good idea

[Etienne Marion]

Hi! I would be happy to take part in developing an API for compactly generated spaces, on the topological side (rather than the categorical one). I managed to "prove" SequentialSpace => CompactlyGeneratedSpace, but I have a problem.
I followed the proof given here (Proposition 1.6). It uses the one-point compactification of Nat, so I proved a few lemmas about that (I found almost nothing about it in Mathlib), but at the end, ENat has type Type so my theorem only works for X : Type, rather thant X : Type*. I don't really know how to manipulate universes and I've never done category theory in Lean, so I have no idea if this is a serious issue or can be easily fixed, or maybe there's a much better proof than mine. My code is messy atm but you can find it here : #15066.

[Yaël Dillies]

The solution is usually to use docs#ULift

[Etienne Marion]

Thanks, I managed it!

[Etienne Marion]

Ok I think it's in good shape but I still have some troubles with universes. I proved Sequential => CompactlyGenerated without any hypotheses on universes, and I proved WeaklyLocallyCompact + T2 => CompactlyGenerated, but this times with restriction on universes.
Then to check that it works I wanted to use it for docs#WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage and docs#SequentialSpace.isProperMap_iff_isCompact_preimage, which were work-around waiting for compactly generated spaces to be defined.
The first one works fine, but I have an error about the universes for the second one which I don't understand. The error disappear if I set everything to the same universe in Sequential => CompactlyGenerated, but this bothers me because it makes the statement less general. The attempt is #15066. Does anyone have a suggestion?

[Kevin Buzzard]

Looking at this PR, I'm confused by the definition of CompactlyGeneratedSpace:

class CompactlyGeneratedSpace (X : Type w) [t : TopologicalSpace X] : Prop where
  /-- The topology of `X` is finer than the compactly generated topology. -/
  le_compactlyGenerated : t ≤ compactlyGenerated.{u} X

We have X of type w, but allow compact Hausdorff spaces from universe u. Is there ever any situation where you want w != u? (Maybe this is explained above, I didn't read the whole thread carefully -- in fact looking at #14508 this seems to have been deliberate). I am assuming that the usual mathematical concept is w = u, and you will get weird answers for at least one of the situations u < w or u > w. For example I would imagine that if u < w and X is compact, the topology would maybe not in general be compactly generated for that choice of u?

The error is saying "Lean cannot guess universe u_6 from what you're telling it" so you can just fix it by adding universe w and then telling Lean to use it explicitly:

theorem SequentialSpace.isProperMap_iff_isCompact_preimage [T2Space Y] [SequentialSpace Y] :
    IsProperMap f ↔ Continuous f ∧ ∀ ⦃K⦄, IsCompact K → IsCompact (f ⁻¹' K) :=
  _root_.isProperMap_iff_isCompact_preimage.{_, _, w}

Whether or not this is a good idea is not something I'm clear on.

[Dagur Asgeirsson]

This is deliberate and it's designed to always use at least the parameter u explicitly. It's because u-compactly generated topological spaces of size w := u+1 embed fully faithfully in condensed sets (see #14514).

I agree that this might be confusing so I would be happy with renaming this UCompactlyGeneratedSpace or something like that and make an abbrev CompactlyGeneratedSpace which is UCompactlyGeneratedSpace.{u, u}

[Dagur Asgeirsson]

The note

Note: this definition should be used with an explicit universe parameter `u` for the size of the
compact Hausdorff spaces mapping to `X`.

in the docstring of TopologicalSpace.compactlygenerated also applies to CompactlyGeneratedSpace and should be added to the docstring there. I don't have any time today, so please feel free to PR this

[Etienne Marion]

Well I don't think having to specify a universe to use a theorem is something we want (when doing topology I mean). Now I don't know enough about universes, but can putting everything in the same universe cause some trouble when dealing with topology only (like instances or theorems which do not apply because of universes issues?) If not I'll just put everything with the same universe.

[Etienne Marion]

Dagur Asgeirsson said:

please feel free to PR this

#15132

[Etienne Marion]

Dagur Asgeirsson said:

I would be happy with renaming this UCompactlyGeneratedSpace or something like that and make an abbrev CompactlyGeneratedSpace which is UCompactlyGeneratedSpace.{u, u}

If I understand correctly, this is what we would need for topological purposes.

[Etienne Marion]

@Dagur Asgeirsson If you’re ok with it, I can do the renaming.

[Dagur Asgeirsson]

Yes, that's fine. It would also make sense to make the definition independent of the category CompHaus. I just wrote whatever API gave me the quickest proof of the result that compactly generated spaces embed fully faithfully in condensed sets, and it's maybe not completely in line with the "mathlib philosophy"

[Etienne Marion]

I encountered a new issue. I created a new file Mathlib.Topology.Compactness.CompactlyGeneratedSpace, which imports Mathlib.Topology.Category.CompactlyGenerated. However I need compactly generated spaces for another file (Mathlib.Topology.Maps.Proper.Basic), and here I encounter an import issue, because this file has a line assert_not_exists StoneCech, while Mathlib.Topology.StoneCech is imported by Mathlib.Topology.Category.CompHaus.Basic which is imported by Mathlib.Topology.Category.CompactlyGenerated.

What is the way to solve this? I can't remove the assert_not_exists StoneCech, because it is also in different files imported by Mathlib.Topology.Maps.Proper.Basic and I don't think I should edit all of them. Do I have to redefine compactly generated space from scratch instead of using an abbrev? The code is here: #15066.

[Yaël Dillies]

I added that assert_not_exists StoneCech recently. You should try removing the Topology.StoneCech → Topology.Category.CompHaus.Basic import, probably by splitting the latter file

[Yaël Dillies]

Also, why do you need to import Topology.Compactness.CompactlyGeneratedSpace in Topology.Maps.Proper.Basic?

[Etienne Marion]

Ok I'll try this.

Yaël Dillies said:

why do you need to import Topology.Compactness.CompactlyGeneratedSpace in Topology.Maps.Proper.Basic?

If f : X \to Y is continuous and Y is compactly generated and T2, then to prove that f is proper it is enough to show that preimages of compact sets are compact.

[Yaël Dillies]

Sounds like this could go in a new file Topology.Maps.Proper.CompactlyGenerated

[Etienne Marion]

I can do that. Should I still split Topology.Category.CompHaus.Basic?

[Yaël Dillies]

Feel free to

[Etienne Marion]

The renaming is done in #15201 and compactly generated spaces are defined in #15203.