Uniform spaces, uniform add groups, and topological rings

Stream: maths

[Antoine Chambert-Loir]

I am a bit confused with the typeclasses relative to the objects in the title.

• My impression is that a topological ring gives rise to a uniform add group, but mathlib doesn't seem to agree, for things don't work well in the absence an explicit [UniformAddGroup R]

• What is the proper way to enter typeclasses relative to such objects: all three of them?

[Kevin Buzzard]

My guess is that topological add group to uniform add group gives some kind of typeclass loop so it might be there as a def but not an instance (in lean 3 these loops were deadly)

[Patrick Massot]

Yes you need all three of them.

[Antoine Chambert-Loir]

Thanks.

[Antoine Chambert-Loir]

docs#UniformGroup is a nice typeclass that corresponds to the case where both, left and right, uniformities on the group coincide, which is the case, eg, when the group is commutative. In general, there is docs#TopologicalGroup.toUniformSpace to define the right uniformity, but how should one proceed if one needed to work with the left one?

[Antoine Chambert-Loir]

If I understand things correctly, the right uniformity is characterized by the fact that the right translations are uniformly continuous, the left uniformity by the fact that the left translations are uniformly continuous, and the docs#UniformGroup case is the stronger assumption that the multiplication is uniformly continuous (wrt to both variables at the same time). (I wonder whether it is implied by the conjunction of the first two?)

[Anatole Dedecker]

Antoine Chambert-Loir said:

docs#UniformGroup is a nice typeclass that corresponds to the case where both, left and right, uniformities on the group coincide, which is the case, eg, when the group is commutative. In general, there is docs#TopologicalGroup.toUniformSpace to define the right uniformity, but how should one proceed if one needed to work with the left one?

We do not have it yet. I've had some loose plans about it for a while, but nothing concrete yet. Do you need something in particular?

[Anatole Dedecker]

Kevin Buzzard said:

My guess is that topological add group to uniform add group gives some kind of typeclass loop so it might be there as a def but not an instance (in lean 3 these loops were deadly)

Here it's not only a loop problem, it's a defeq problem. There is extra data in UniformSpace, so if we had an instance TopologicalRing -> UniformSpace we'd end up with non-defeq uniformities.

[Anatole Dedecker]

Antoine Chambert-Loir said:

If I understand things correctly, the right uniformity is characterized by the fact that the right translations are uniformly continuous, the left uniformity by the fact that the left translations are uniformly continuous

I'm never sure about the side, but the key point is that the right uniformity in mathlib is the right uniformity according to Bourbaki (a lot of books reverse the conventions)

[Antoine Chambert-Loir]

That's cool. I have no plan in particular, I'm just trying to evaluate power series, using density of polynomials. mathlib and the computer on one lap, Bourbaki on the other one, and I try to ask myself at each page what does what correspond to?