topological groups and uniformity

Stream: maths

[Moritz Doll]

What is the reason that docs#topological_group.to_uniform_space is not an instance? I am trying to prove some things about uniform boundedness/Cauchy sequences in topological vector spaces and it is extremely annoying to specify all the uniformity classes by hand.

[Kevin Buzzard]

Surely the issue will be that topological group -> uniform space -> topological space will be different to topological group -> topological space in general (I mean the two topologies will be equal but not definitionally equal, which will mess up type class inference). Is there a way around this though?

[Kevin Buzzard]

docs#uniform_space

[Kevin Buzzard]

Yeah, uniform space extends topological space so I don't immediately see why one can't make the triangle commute. Is the issue simply that the authors didn't want to assume in the non abelian case that you wanted the left or right uniformity? What happens if you make the def a local instance? Does anything break in your file? Here the group is abelian so I can't see any issues (but then again it is getting late here...)

[Moritz Doll]

ah I think you are not supposed to use [topological_space E] [topological_group E], but [uniform_space E] [uniform_group E], then everything works just fine. The documentation in topology.algebra.group and topology.algebra.uniform_group is not really mentioning it though.

[Kevin Buzzard]

docs#uniform_group

[Kevin Buzzard]

Oh nice. My students also had this sort of problem -- "how do you make a Banach space?". There are all these typeclasses but perhaps less documentation about how to use them, and it's got a lot more complicated since back in the day when it was just [topological_space]

[Patrick Massot]

Yes, the answer is almost surely that you want to use [uniform_space E] [uniform_group E].

[Moritz Doll]

Is there any reason to use [topological_space E] [topological_group E] at all? Even in the case that you don't need the uniform structure?

[Patrick Massot]

Not really. I also know I should make a big refactor at some point to also allow using the uniform structure on non-commutative groups, but I've been postponing this forever since nobody ever needed it.

[Moritz Doll]

For my purposes everything is fine, it is just a bit unintuitive. Before Lean I have never heard of uniformity and topological_add_group looks like the thing one needs for topological vector spaces. I will write some documentation for this today.

[Anatole Dedecker]

I have a related question. I will soon define the strong topology/uniform structure on E →L F, using the general setup in #13073. In the linear case, one can define the topology directly from the topology on F without referencing the uniform structure. Is this worth doing in Lean, or do we assume that any topological vector space has a uniform_space instance anyway ? Would it have better definitional properties ?

[Moritz Doll]

I am not really qualified to answer that, but I would use the uniform structure. As Heather pointed out the uniform structure might not be defeq to the one coming from the topological group, so if you need uniformities you might run into annoying issues if you don't use uniform_space.