defining `MulAction.ball`

Stream: mathlib4

[Lara Toledano]

In #32745 I try to create the file Topology.Algebra.MulActionConst in analogy to Topology.Algebra.ConstMulAction. The motivation is to establish definitions needed to formulate and proove the Effros Theorem, see #mathlib4 > Effros Theorem .

I wish to define

open scoped Pointwise
namespace MulAction
/--
The set `{g • x | g ∈ U}`. Intended to be used for `U ∈ 𝓝 1`. Named in analogy to
`UniformSpace.ball`.
-/
abbrev ball [SMul G X] (x : X) (U : Set G) : Set X := U • {x}

@Yury G. Kudryashov commented

This definition has nothing to do with topology, and should go to a file somewhere in Algebra/. I would discuss it on Zulip.

Consider the map

def r [SMul G X] (s : Set G) : Set (X × X) := {x | x.2 ∈ s • {x.1} }

Given IsTopologicalGroup G and MulAction G X, then we can call UniformSpace.Core.mkOfBasis on r '' (𝓝 1) to define a uniform structure on X. This is the motivation for the analogy between UniformSpace.ball and U • {x}. As UniformSpace.ball is defined in Topology.UniformSpace.Defs and not in Data.Rel, I thought the new file Topology.Algebra.MulActionConst would be a good place to define MulAction.ball, as opposed to somewhere in Algebra\.

Does anyone have a suggestion as to a better home for this definition?

[Snir Broshi]

Maybe Mathlib.Algebra.Group.Pointwise.Set.Scalar, next to docs#Set.smul_singleton ?

[Snir Broshi]

Also if it's going to be in Algebra I think there should be leftBall and rightBall ({x} • U).
Though "ball" sounds weird here, what metric is this a ball in?

[Lara Toledano]

For the name "ball": U • {x}is a ball in the uniform structure I described above, which may not be generated by any one metric but certainly is generated by a family of pseudometrics.

[Lara Toledano]

I am not sure what you imagine as the rightBall : given SMul G X, x : X and U : Set G, there is no definition for the expression {x} • U. I you are thinking of SMul G X, x : G and U : Set X, then the notation x • U is already scoped in Pointwise, so that a specific definition would at most serve symmetry.

[Snir Broshi]

I was thinking of the symmetry between docs#Set.smul_singleton and docs#Set.singleton_smul.
While the opposite version is the same as x • U without the singleton braces, the definition you suggest also doesn't shorten the notation: ball x U vs U • {x}. I don't understand why U • {x} deserves a named definition but {x} • U = x • U doesn't.

[Lara Toledano]

I agree that U • {x} does not necessarily deserve a named definition. I proposed it mainly because I needed a naming convention for the following lemmas

lemma ball_iUnion [SMul G X] (x : X) {ι : Type*} (U : ι → Set G) :
    (⋃ i, U i) • {x} = ⋃ i, (U i) • {x} := sorry

lemma ball_iUnion₂ [SMul G X] (x : X) {ι : Type*} {κ : ι → Sort*} (U : (i : ι) → κ i → Set G) :
    (⋃ i, ⋃ j, U i j) • {x} = ⋃ i, ⋃ j, (U i j) • {x} := sorry

lemma ball_mul [Monoid G] [MulAction G X] (x : X) (U V : Set G) :
    ((U * V) • {x} : Set X) = U • (V • {x}) := sorry

lemma ball_smul [Monoid G] [MulAction G X] (x : X) (g : G) (U : Set G) :
    (g • U) • ({x} : Set X) = g • (U • {x}) := sorry

lemma ball_inter [SMul G X] (x : X) (U V : Set G) :
    (U ∩ V) • ({x} : Set X) ⊆ U • {x} ∩ V • {x} := sorry

lemma ball_op_smul [Monoid G] [MulAction G X] (x : X) (g : G) (U : Set G) :
    (U <• g) • ({x} : Set X) = U • {g • x} := sorry

So I guess the true topic of this discussion is not the home for the definition of MulAction.ball, but rather the home and names for these lemmas. The convention that U • {x} should be called "ball" in lemma names could live in a module docstring.

[Lara Toledano]

As for the lack of symmetry, I would argue that it is built into the concept of scalar multiplication.

[Yury G. Kudryashov]

At least some of these lemmas are true for any set in place of {x}.

[Lara Toledano]

That is true, apart from

lemma ball_op_smul [Monoid G] [MulAction G X] (x : X) (g : G) (U : Set G) :
    (U <• g) • ({x} : Set X) = U • {g • x} := sorry

all of the above are true for any set in place of {x}.
I wanted to name these as a convenience issue because the proof of the Effros Theorem will use them so heavily.

[Eric Wieser]

That one is true as (U <• g) • S = U • g • S though

[Lara Toledano]

Let me motivate my wish for some API around s • {x} given [MulAction G X] (s : Set G) (x : X) more clearly.

A IsTopologicalGroup G instance not only defines a compatible uniform structure on G with a basis indexed by 𝓝 1, it also defines a uniform structure on X with a basis indexed by 𝓝 1, in which {s • {x} | s ∈ 𝓝 1} is a basis for 𝓝 x.

The main statement of the Effros Theorem is that, under the right assumptions, including continuity of fun g : G ↦ g • x for each x : X, the map g ↦ g • x is open. This is equivalent to s • {x} being a neighborhood of x for each s ∈ 𝓝 1 and x : X, which is equivalent to the given topology on X being finer than the topology of the uniform structure defined on X by the given IsTopologicalGroup G and MulAction G X instances.

In other words, this uniform structure induces the coarsest topology on Xsuch that g ↦ g • x is open.

[Lara Toledano]

Naming the map x : X ↦ s : Set G ↦ (s • {x} : Set X) would also have the benefit of avoiding situations where the type of {x} is unclear.