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.

[Lara Toledano]

I am working with a non-commutative group. I am butting against the issue
Kevin Buzzard said:

topological group -> uniform space -> topological space will be different to topological group -> topological space

Here is a minimal example.

import Mathlib

namespace foo
variable [Group G] [iT: TopologicalSpace G] [IsTopologicalGroup G]

scoped instance iU : UniformSpace G := IsTopologicalGroup.toUniformSpace G
scoped instance iUT : TopologicalSpace G := iU.toTopologicalSpace

example : iT = iUT := rfl -- works fine
end foo

example [Group G] [iT : TopologicalSpace G] [IsTopologicalGroup G] : False := by
  have iU := IsTopologicalGroup.toUniformSpace G
  have iUT := iU.toTopologicalSpace
  have : iT = iUT := rfl -- Type mismatch
  sorry

I do not understand why the example in the foo namespace works and not the one outside of the namespace. I also do not understand why the equality does not hold definitionally since IsTopologicalGroup.toUniformSpace seems to be defined using the TopologicalSpace instance on the group.

[Yaël Dillies]

You should not use have for data if you care about the definition within a proof. Instead you should use let

[Lara Toledano]

@Yaël Dillies thank you for the tip

import Mathlib

namespace foo
variable [Group G] [iT: TopologicalSpace G] [IsTopologicalGroup G]

scoped instance iU : UniformSpace G := IsTopologicalGroup.toUniformSpace G
scoped instance iUT : TopologicalSpace G := iU.toTopologicalSpace

example : iT = iUT := rfl -- works fine
end foo

example [Group G] [iT : TopologicalSpace G] [IsTopologicalGroup G] : False := by
  let iU := IsTopologicalGroup.toUniformSpace G
  let iUT := iU.toTopologicalSpace
  have : iT = iUT := rfl -- now working too
  sorry

[Oliver Nash]

@Lara Toledano You may be well aware of this but I might mention that this corner of the library is under active development, and that we merged #30029 just yesterday.

[Oliver Nash]

Additionally (and again you may be well aware of all this) when formalising you will need to be mindful that the following are all different statements:

1. Let $G$ be a topological group, now take the right (say) uniformity and ...
2. Let $G$ be a uniform group for which the left and right uniformities coincide, and moreover suppose that this is the group's uniformity
3. Let $G$ be a uniform group with the left uniformity
4. Let $G$ be a uniform group with the right uniformity

[Oliver Nash]

After #30029 we can state each of these in Lean as follows:

-- Let `G` be a topological group
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

#check uniformity G -- Correctly fails: we have not given `G` a canonical uniform space structure
#check (IsTopologicalGroup.toUniformSpace (G := G)).uniformity -- The right uniformity

[Oliver Nash]

-- Let `G` be a uniform group for which the left and right uniformities coincide, and moreover
-- suppose that this is the group's uniformity.
variable {G : Type*} [Group G] [UniformSpace G] [IsUniformGroup G]

#synth IsLeftUniformGroup G -- The uniform structure is the left uniformity
#synth IsRightUniformGroup G -- The uniform structure is the right uniformity

[Oliver Nash]

-- Let `G` be a uniform group with the left uniformity
variable {G : Type*} [Group G] [UniformSpace G] [IsLeftUniformGroup G]

[Oliver Nash]

-- Let `G` be a uniform group with the right uniformity
variable {G : Type*} [Group G] [UniformSpace G] [IsRightUniformGroup G]

-- Indeed this is what is given by docs#IsTopologicalGroup.toUniformSpace
example : (IsTopologicalGroup.toUniformSpace (G := G)).uniformity = uniformity G := by
  simp_rw [IsRightUniformGroup.uniformity_eq, ← div_eq_mul_inv, ← uniformity_eq_comap_nhds_one' G]
  rfl

[Anatole Dedecker]

The only thing missing really is that we can't do "endow this topological group with its left uniform structure" right now. The first step on that road would be #30009, renaming IsTopologicalGroup.toUniformSpace to IsTopologicalGroup.rightUniformSpace. This might be slightly controversial for everyone working with commutative groups, but I tend to think that a comment saying "just use the right one when in doubt" would be enough?

[Yaël Dillies]

Hmm, but in other(/most?) parts of mathlib we instead say "use the left one when in doubt". How is a user supposed to discover which side they should fall onto when in doubt?

[Anatole Dedecker]

This could be written in the docstrings of the declarations, is that not enough? Btw, the reason right makes more sense here is simply that x - y = x + (-y) and not -y + x.

[Anatole Dedecker]

A slightly meaner option would be to argue that the litterature is not consistent about which one is the left or the right uniformity, so we can pick the one we want x) But I'd rather stay with Bourbaki's convention by default.

[Lara Toledano]

(deleted)