topology on finsupp

Stream: general

[Reid Barton]

Yaël Dillies said:

Okay so I have branch#std_simplex_finsupp (currently a mess, feel free to help!) to change docs#std_simplex to a set of finsupps, hence relaxing the fintype assumption.

I took a brief look at this branch and as far as I can tell, mathlib doesn't actually have the topology on ι →₀ ℝ defined yet--is that right?

[Reid Barton]

I just want to comment that this std_simplex ι does arise in algebraic topology and the correct topology on it is not the subspace topology from ι → ℝ. It is the subspace topology from ι →₀ ℝ where the latter is topologized as the union of the subspaces of functions with support contained in s for each finite subset s.

[Reid Barton]

And std_simplex ℝ ι is only compact when ι is finite.

[Eric Rodriguez]

is this the box/product topology stuff?

[Reid Barton]

Might be actually, I never thought about it that way.

[Johan Commelin]

It's not the product topology, that's exactly your point, right? If you put the product topology on ι → ℝ, and then take the subspace topology for std_simplex ℝ ι you get something compact. But if you take this "colimit" topology on ι →₀ ℝ, and then take the subspace topology, you get something different?
Or am I misunderstanding one/both of you?

[Yaël Dillies]

Reid Barton said:

I took a brief look at this branch and as far as I can tell, mathlib doesn't actually have the topology on ι →₀ ℝ defined yet--is that right?

Yup, that's what I meant by "hitting a wall of bricks".

[Yaël Dillies]

Well, of missing bricks!

[Yaël Dillies]

I have no ideas what those different topologies are on about, so I'll just ask the obvious questions.

• Does the topology you're talking about coincide with the subspace topology when ι is a fintype?
• Does the topology matter somewhere else?
• Is it relevant for the topological results we already have about std_simplex?

[Johan Commelin]

Yaël Dillies said:

• Does the topology you're talking about coincide with the subspace topology when ι is a fintype?

Up to propeq, yes, but not defeq.

[Yaël Dillies]

And how hard is it to define that topology?

[Johan Commelin]

I don't think it is too hard. Otoh, I've never used infinite-dimensional simplices myself. So it would be good to hear from Reid about the other two questions.

[Reid Barton]

Johan Commelin said:

It's not the product topology, that's exactly your point, right? If you put the product topology on ι → ℝ, and then take the subspace topology for std_simplex ℝ ι you get something compact. But if you take this "colimit" topology on ι →₀ ℝ, and then take the subspace topology, you get something different?
Or am I misunderstanding one/both of you?

Yes that's right. But the box topology is another topology on the product of topological spaces, finer than the product topology, and if you restrict that to finsupp or std_simplex, it seems like it does give the correct "colimit" topology. But I'm not sure if that is really a useful fact.

[Reid Barton]

Yaël Dillies said:

• Does the topology matter somewhere else?
• Is it relevant for the topological results we already have about std_simplex?

I don't think I understand either of these questions, can you be more specific?

[Yaël Dillies]

They are now caduque as Johan said the correct topology on ι →₀ ℝ is an extension of the topology on ι → ℝ for fintype ι.

[Yaël Dillies]

I meant "Does it matter if the lemmas now apply to a different topology?". And they actually will apply to the same topology.

[Reid Barton]

I see.

[Reid Barton]

Yaël Dillies said:

And how hard is it to define that topology?

There are a few equivalent ways, but if you want to make it definitionally a subspace of finsupp, then you could do it like this. For any s : finset ι there is a function (s -> X) -> (ι →₀ X) which "extends by zero", and the topology on finsupp is the join of the docs#topological_space.coinduced of all the product topologies on the s -> Xs.

[Reid Barton]

Or you can also do the same type of construction directly on std_simplex and not all of finsupp

[Yaël Dillies]

Well, std_simplex should be a set, not a topological space.

[Yaël Dillies]

Does it matter that the maps are going ↥s → X? Or is it preferable to avoid this coe_to_sort?

[Yaël Dillies]

Yaël Dillies said:

Well, std_simplex should be a set, not a topological space.

Or at least I think so? How do you use it in algebraic geometry?

[Shing Tak Lam]

Yaël Dillies said:

Well, std_simplex should be a set, not a topological space.

What do you mean by this? A set gives you a subtype which has the subspace topology.

[Yaël Dillies]

Yes. I mean that we shouldn't endow the set itself with the topology, but leave the subspace topology instance do its job.

[Yaël Dillies]

Sorry, this was highly unclear.

[Johan Commelin]

Yaël Dillies said:

Yaël Dillies said:

Well, std_simplex should be a set, not a topological space.

Or at least I think so? How do you use it in algebraic geometry?

AG doesn't use simplices at all. In algebraic topology they are used a lot (as topological space), but in 99% of the use cases, the ι will be finite.

[Yaël Dillies]

Argh sorry I always write AG when I mean AT.

[Reid Barton]

The (potentially) infinite case comes up in conjunction with partitions of unity. A partition of unity on X with index set I determines a map from X into the I-simplex (equipped with this CW/colimit-type topology). If you have a map from X into a CW complex, then you have a pretty good handle on the homotopy type (as opposed to weak homotopy type) of X.

[Reid Barton]

The fact that a partition of unity is locally finite is enough to get a map into the I-simplex with its CW topology. To get a map into the one with the topology that comes from the product topology, you would just need a point-finite partition of unity.

[Reid Barton]

So for example, suppose you have a cover of X by open subsets (indexed by a set I) such that every finite intersection of the open subsets is contractible or empty, and the cover is numerable (admits a partition of unity). Inside the I-simplex, you can consider the union of those simplices whose vertices correspond to a family of members of the cover with nonempty intersection. The partition of unity determines a map from X to this subcomplex, and it will be a homotopy equivalence.

[Reid Barton]

That said, I agree that the case of finite ι (or just fin (n+1)) is way more important overall.