Dense submonoids vs subgroups

Stream: maths

[Yury G. Kudryashov]

Consider the following property: ∀ S : Set G, Dense (AddSubgroup.closure S) → Dense (AddSubmonoid.closure S). This statement isn't true for Real or Int but it's true for AddCircle. Is there a proof that doesn't rely on very circle-specific arguments? E.g., is it true for any compact commutative group?

[Yaël Dillies]

Can you do something along the lines of

1. Assume X ∈ closure (Subgroup.closure S)
2. Find a sequence x n ∈ Subgroup.closure S converging to X
3. Write x n = y n / z n where y n, z n ∈ Submonoid.closure
4. By (sequential) compactness, WLOG y n and z n converge
5. Call Y and Z their limit. We have X = Y / Z
6. By (sequential) compactness, find a sequence k n such that Y ^ k n and Z ^ k n converge
7. Cancel out the limit of Z ^ k n (??)

[Yaël Dillies]

I think looking at the special case of S = {x} is instructive. We want to approximate x ^ -a by a sequence x ^ b n (a, b n ≥ 0). So find a (WLOG increasing) sequence k n such that x ^ k n converges. In particular, we have a (WLOG increasing) sequence k' n such that x ^ k' n converges to 1 (take eg k' n := k (n + 1) - k n). Then set b n := k' n - a (which is eventually positive) and you have x ^ b n converging to x ^ -a. Done

[Yaël Dillies]

For general S, I would think that the idea in my first message of splitting into the "positive" and "negative" parts will do the trick, as then all you need to do is to perform the argument in my second message element-wise. There might be some issue when S is infinite, I haven't checked

[Yaël Dillies]

I guess this generally shows [CommGroup G] [TopologicalSpace G] [CompactSpace G] (S : Set G) : closure (Subgroup.closure S) = closure (Submonoid.closure S)

[Kevin Buzzard]

This latter statement is surely not true for the circle if I'm parsing it correctly, just let S be any irrational rotation. Did you mean to take topological closures too?(yes)

[Yaël Dillies]

Sorry, yes, too many closures around

[Yury G. Kudryashov]

Thank you! I'll try to formalize this on Saturday.

[Kevin Buzzard]

So basically I think Yael is saying that everything follows from the claim that if x is an element of a compact commutative group then -x is in the top closure of the submonoid generated by x, which is the same as the claim that 0 is in the top closure of {x,2x,3x,...} which should follow from the claim that either the set is finite, or its top closure is strictly bigger. I'm a bit unclear about the relationship between compactness and sequential compactness in a topological group. Are they the same thing?

[Yaël Dillies]

Kevin Buzzard said:

I'm a bit unclear about the relationship between compactness and sequential compactness in a topological group. Are they the same thing?

I don't think so, no. ℝ → Circle (with the product topology) is a compact topological group which is not sequentially compact.

[Yaël Dillies]

This makes me think that there is a proof of Yury's conjecture using compactness and not sequential compactness: Both kinds of compactness only differ in uncountably-dimensional groups, but Subgroup.closure/Submonoid.closure only probe countably many dimensions at once.

[Antoine Chambert-Loir]

Your ambient group does not need to be commutative, but everything will happen in the compact subgroup generated by $x$.
Choose a neighborhood $W$ of $e$; we want to show that $W$ contains infinitely many points of the form $x ^ n$ ($n>0$).
If $x$ has finite order, this is clear.
Otherwise, this set $S$ is not compact (for example, the $x^m S$ is a decreasing sequence of compact sets with empty intersection). Choose a cluster point $\xi$ of $S$ such that $\xi\notin S$ — which exists because $S$ is not compact and your group is assumed to be compact. By assumption, every neighborhood $V$ of $\xi$ contains infinitely many such $x ^n$, say the $x ^ {n_k}$, for some strictly increasing sequence $(n_k)$.
Choose $V$ such that $V\cdot V^{-1}$ is contained in $W$. Then $x^{n_{q}-n_p}$ is contained in $W$ for all $q>p$. This concludes the proof.

[Antoine Chambert-Loir]

(Of course, this is the same argument as the one given by Yael and Kevin.)

[Yury G. Kudryashov]

So, the submonoid has to be commutative, not the whole group. I'll reread the arguments, try to figure out the optimal typeclass assumptions and formalize this during a flight this week-end.

[Sébastien Gouëzel]

No, the submonoid doesn't have to be commutative. If you denote the submonoid by S, then the argument above shows that S^{-1} is in the closure of S, because each s^{-1} is in the closure of {s^n}_{n > 0}. And that's enough to conclude that the subgroup generated by S is contained in the closure of S.

[Yaël Dillies]

That's a nice reformulation of my idea! And here you really only assume compactness.

[Yury G. Kudryashov]

I opened file#Topology/Algebra/Group/Compact to formalize this, but dropped [LocallyCompactGroup] assumption from the last instance instead, see #16521 (moved to #16551).

[Yury G. Kudryashov]

Thanks everyone! #16521 is ready for review, depends on #16572.