topology on units

Stream: maths

[Yury G. Kudryashov]

We have docs#units.topological_space and docs#topological_space_units/docs#induced_units. Which of these two instances is better for which applications? Currently, the first one is an instance while the other one isn't. Should both of them be non-instances? Am I right that they're equal in a division_monoid such that has_inv.inv is continuous at any unit?

[Yury G. Kudryashov]

@Patrick Massot @Scott Morrison @Heather Macbeth @Sebastien Gouezel :up:

[Heather Macbeth]

There is an argument of this style at docs#units.open_embedding_coe, showing that in a complete normed ring, the inverse function is continuous at units, and as a consequence that the coercion from units of R (with the current topological_space instance) into R is an open embedding.

[Heather Macbeth]

I'm not sure that the other topology, docs#topological_ring.topological_space_units, has any uses. My impression had been that the docs#units.topological_space is the useful one, that in some cases the docs#topological_ring.topological_space_units topology agrees with it and in other cases that topology is nonsense.

[Heather Macbeth]

Happy to learn that I'm wrong here!

[Adam Topaz]

Isn't the correct topology always the one induced by embedding the units in M x M via u |--> (u,u^{-1}) where the product has the usual product topology? IIRC this gives the right answer for ideles in number theory.

[Adam Topaz]

I guess this is exactly what Heather said too ;)

[Kevin Buzzard]

It's a little tough to come up with examples where the topologies don't coincide (for example they coincide for $GL_n(\R)$ and $GL_n(\mathbb{C})$, the units in $n\times n$ matrices), but as Adam says they don't coincide for $GL_n(\mathbb{A})$ where $\mathbb{A}$ is the adeles of a global field, and automorphic forms are continuous functions on $GL_n(\mathbb{A})$ with the correct topology (the one Adam explicitly writes above). The problem with the subspace topology is that it does not always make the units into a topological group because inversion might not be continuous (this is what happens with $GL_n(\mathbb{A})$).

[Yury G. Kudryashov]

Let's wait for @Patrick Massot and @Scott Morrison who are listed as the authors of the file that adds docs#topological_space_units. Should we drop this definition&TC?

[Yury G. Kudryashov]

A related question: should we replace has_continuous_inv₀ with has_continuous_inv_units : ∀ x, is_unit x → continuous_at has_inv.inv x?

[Yury G. Kudryashov]

(not sure)

[Patrick Massot]

To be honest I don't remember the details. This was during the perfectoid spaces project. I think the key target was docs#topological_division_ring.units_top_group

[Patrick Massot]

From the context of the perfectoid spaces project, it is clear this was intended to be used around docs#uniform_space.completion.hat_inv_extends (completion of topological fields).

[Patrick Massot]

I think this is all I have to say: if you think this def is harmful or confusing or pointless and you can remove it without breaking uniform_field.lean then I'm ok.

[Kevin Buzzard]

The adeles are very very far from being a field -- they have many zero divisors. I don't know if it's true that if K is a topological field (or maybe a uniform field) then the two topologies coincide. I do remember from discussions with Patrick at that time that the theory of topological fields and in particular the theory of completion of uniform fields is far more subtle than I had imagined. Completions of uniform fields have played a key role in recent work of Maria Ines in p-adic Hodge theory

[Yury G. Kudryashov]

Opened #18536

[Eric Wieser]

Just to check; the stuff being removed was not harmful, but the claim is that it was pointless?

[Johan Commelin]

It might be mathematically harmful :wink:

[Kevin Buzzard]

My understand of the issue is that for certain topological rings $K$, Patrick defined a topology on $K^\times$ to be the subspace topology (because this was 2018), and then (for the rings in question) proved that this made $K^\times$ into a topological group. Yury's change is, for these rings, to define the topology on $K^\times$ to be the usual topology (coming from the diagonal embedding), thus removing the diamond, and then proving that it's equal to the subspace topology (thus meaning that we don't lose any mathematical content). Yury/Patrick please let me know if I've misunderstood.

[Eric Wieser]

Kevin Buzzard said:

My understand of the issue is that for certain topological rings $K$, Patrick defined a topology on $K^\times$ to be the subspace topology (because this was 2018), and then (for the rings in question) proved that this made $K^\times$ into a topological group.

This topology was a def, but was not an instance

Yury's change is, for these rings, to define the topology on $K^\times$ to be the usual topology (coming from the diagonal embedding)

This is already docs#units.topological_space in master

thus removing the diamond

so there was no diamond

[Yury G. Kudryashov]

This def was never used outside of 1 file.

[Yury G. Kudryashov]

The other file that Patrick mentioned used docs#units.topological_space anyway.

[Yury G. Kudryashov]

I think that having unused definitions is harmful because new users can open topology.algebra.field, read it, decide that this is the way to deal with topology on units _ in mathlib, then be surprised why no theorems from outside of this file work for this topology.

[Eric Wieser]

That can also be fixed with documentation though.