Torus: quotient or pi?

Stream: maths

[Yury G. Kudryashov]

I'm going to formalize some facts about measures on the n-dimensional torus. There are at least 2 ways to represent it:

• ι → UnitAddCircle;
• the quotient of (ι → Real) by the integer sublattice.

What do you think should be the normal form? Of course, I'm going to prove that they are homeomorph (awaiting review of #16549 and #16551). Also, should I allow

• ι → AddCircle r with some r, not necessarily 1?
• (i : ι) → AddCircle (r i) with variable r?

The latter would be difficult, because I'm going to talk about the action of $GL_n(\mathbb Z)$ on this torus.

[Sébastien Gouëzel]

Is it important for you to have the product structure? I mean, there are tori which are not products (take the quotient of $\mathbb{R}^n$ by a lattice without vectors on the coordinate axis). Would your framework still work there?

[Yaël Dillies]

As Sébastien points out, I would add a third option to your list:

• the quotient of ι → Real by a sublattice

[Sébastien Gouëzel]

If you need a concrete torus to talk about irrational translations, rotation numbers, and so on, I'd probaby go for ι → UnitAddCircle, by the way.

[Sébastien Gouëzel]

Yaël Dillies said:

As Sébastien points out, I would add a third option to your list:

• the quotient of ι → Real by a sublattice

Even the quotient of a finite-dimensional real topological vector space by a sublattice!

[Oliver Nash]

With apologies for repeating myself I suggest it might be worth developing your theory not about a concrete type but instead about any type with the right properties.

In other words, I think that tori are important enough that we should characterise them (e.g., in a typeclass) and prove theorems about types which satisfy the characterisation.

I said this before here and here so I promise not to say it a fourth time unless I commit to do this work myself!

[Kevin Buzzard]

I am unclear about what the universal property is here. "Isomorphic to a product of circles" works but presumably this is what Oliver wants to avoid? Was there an answer for how to characterise them purely topologically? Their Ponyrjagin duals are precisely the finite free discrete groups, but again this involves a model of a circle. Presumably you want to rule out infinite products of circles? (Such things play a crucial role in the Clausen-Scholze work on condensed sets)

[Oliver Nash]

How about compact, connected, Abelian topological group with no small subgroups?

[Yaël Dillies]

... no small connected subgroups?

[Patrick Massot]

No small subgroup means there is a neighborhood of identity that contains no non-trivial subgroup.

[Patrick Massot]

This avoids horrors such as $\Z_p$.

[Kevin Buzzard]

"connected" is also a pretty good way of ruling out Z_p. But what about my infinite products? They have no small subgroups.

[Yury G. Kudryashov]

I'm going to talk about some very specific self-maps of the torus like the action of $GL_n(\mathbb Z)$ or fun x => a + x, where $a$ is a vector such that coordinates of $a$ and $1$ are linearly independent over $\mathbb Q$. Some of these results can be stated for the quotient by any sublattice (I guess, I should read docs#ZLattice API), sometimes a nice coordinate description of the answer matters.

[Oliver Nash]

Kevin Buzzard said:

"connected" is also a pretty good way of ruling out Z_p. But what about my infinite products? They have no small subgroups.

OK then I also add finite automorphism group!

[Sébastien Gouëzel]

The standard torus has infinite automorphism group (GL_2(Z) acts on it...)

[Oliver Nash]

OK well this is what I get for again allowing myself to comment while I’m doing my day job. I may reply properly this evening.

[Yury G. Kudryashov]

E.g., I recently added docs#ergodic_add_left_of_denseRange_zsmul but I want to have a nice answer to "when the integer multiples of a point on the torus are dense?" There is an answer for the quotient by any lattice but I want to add the nice coordinate description for the integer lattice too.

[Kevin Buzzard]

Finitely-generated automorphism group will work if it's true that the only compact connected abelian topological groups with no small subgroups are (possibly infinite) products of tori.

If connected rules out Z_p then do we need no small subgroups?

Oh, what about solenoids? Give Q the discrete topology and its pontrjagin dual is some crazy thing. You take the projective limit of circles mapping to themselves via z mapsto z^{n!} for increasing n.

[Yury G. Kudryashov]

Note: all facts I want to specialize to tori are true for any compact topological group with second-countable topology. I only need the torus structure to give nice coordinate descriptions of general properties.

[Kevin Buzzard]

I's very frustrating. $\mathbb{Z}$ is the initial ring and $S^1$ is just its dual so surely there is something really cute here. Rings have a 1 and a multiplication though, and Pontrjagin duality ignores them . The 1 translates into "I have a canonical map to the circle", which is not something we want because we're trying to move away from circles. I don't quite know what multiplication means -- multiplication is bilinear not linear, so doesn't correspond to a morphism in the category of abelian topological groups.

[Kevin Buzzard]

Maybe "admits a topological manifold structure with model space some n-dimensional real vector space"? :-/

[Yury G. Kudryashov]

What exactly are you trying to generalize?

[Yury G. Kudryashov]

So far, it looks like an offtopic to me.

[Kevin Buzzard]

The question is whether we can just write down some list of topological properties which are equivalent to "I am a torus", because then you could prove theorems about that instead.

[Patrick Massot]

What about simply saying it’s compact and the image of a vector space by a topological group surjective morphism?

[Adam Topaz]

Doesn't pontryagin duality itself uniquely characterize the circle group? Once you have a universal property for the circle group, you can get one for tori in a number of ways.

[Adam Topaz]

If you use duality as the universal property, then it can be generalized in a number of other ways as well, e.g. to a universal property for $\mathbb{G}_m$ in the algebraic case, to $\mathbb{Q}_p/\mathbb{Z}_p(1)$ in p-adic contexts (sorry Patrick), etc.

[Yury G. Kudryashov]

Kevin Buzzard said:

The question is whether we can just write down some list of topological properties which are equivalent to "I am a torus", because then you could prove theorems about that instead.

Please read my message above. The general theorem is true for any compact topological group with second-countable topology. But I want to have coordinate descriptions for properties like "multiples of an element are dense in the group".

[Yury G. Kudryashov]

And other properties I want to formalize (e.g., "almost every element has a dense orbit") can be generalizable to something else.

[Yury G. Kudryashov]

So, I don't understand the point of discussing "how to generalize the notion of a torus" until we agree on "what theorem/construction do we want to generalize?"

[Scott Carnahan]

I don't understand why an infinite product of circles would have no small subgroups. Infinite products have "big" open sets.

[Antoine Chambert-Loir]

The solution to Hilbert 5th problem says that a topological group is a Lie group iff it is locally compact and has no small subgroups. If you want it to be a torus, you just need to add compact, connected and commutative. I don't know how easily Hilbert 5th could be formalized to have this in Lean.

[Yury G. Kudryashov]

Sébastien Gouëzel said:

Yaël Dillies said:

As Sébastien points out, I would add a third option to your list:

• the quotient of ι → Real by a sublattice

Even the quotient of a finite-dimensional real topological vector space by a sublattice!

I may decide to turn docs#IsZLattice into a bundled structure ZLattice to formalize some results in terms of this.