RightActions

Stream: mathlib4

[Lara Toledano]

I think it would be quite convenient if we had a lemma

open scoped Pointwise RightActions
lemma Set.smul_singleton_eq_op_smul [Mul M] {s : Set M} {a : M} :
s • {a} = s <• a := calc
  s • {a} = (MulOpposite.op a • ·)'' s := by simp
  _       = s <• a := rfl

Is someone already working on this? Do you find it unnecessary? Should I just go ahead and PR?

[Bhavik Mehta]

I think the left-hand-side of the new lemma should be s * {a}, but I agree we should have that. Note that we have the Finset version (docs#Finset.mul_singleton) of what you want but the corresponding Set version is (in my eyes) quite a lot less convenient (docs#Set.mul_singleton)

[Lara Toledano]

Writing s * {a} does seem better.

I was not aware of (docs#Finset.mul_singleton), thank you for the insight.

If we want the lemmas {a} * s = a • s and s * {a} = s <• a for sets, then I wonder if they might replace the current Set.mul_singleton and Set.singleton_mul. These are tagged with simp so I cannot say I understand what effect that would have...

[Bhavik Mehta]

I believe the current simp setup for docs#Set.mul_singleton is quite awkward in practice, you could try making a PR which adds your lemma and marks it simp and un-simps the existing ones. I think the statements of docs#Set.mul_singleton and singleton_mul should still be in mathlib, just not as simp lemmas

[Yaël Dillies]

I have a PR in the works that does this, fyi

[Lara Toledano]

I would also like to use

variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
open scoped Topology RightActions Pointwise
lemma smul_nhds  (x y : G) : x • 𝓝 y = 𝓝 (x * y) := calc
    x • 𝓝 y = (𝓝 y).map (Homeomorph.mulLeft x) := rfl
    _ = 𝓝 (x * y) := by simp

lemma op_smul_nhds (x y : G) : (𝓝 x) <• y = 𝓝 (x * y) := calc
    (𝓝 x) <• y = (𝓝 x).map (Homeomorph.mulRight y) := rfl
    _ = 𝓝 (x * y) := by simp

as well as the specializations

example  (x : G) : x⁻¹ • 𝓝 x = 𝓝 1 := by rw [smul_nhds]; simp
example  (x : G) : (𝓝 x) <• x⁻¹ = 𝓝 1 := by rw [op_smul_nhds]; simp

Are you working on that too?

[Eric Wieser]

Those are not the right generalizations, I think you just want

open scoped Topology RightActions Pointwise
lemma nhds_smul [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α]
    (x : G) (y : α) : 𝓝 (x • y) = x • 𝓝 y :=
  (isOpenMap_smul x).map_nhds_eq (continuous_id.const_smul _ |>.continuousAt) |>.symm

[Lara Toledano]

That is indeed a better generalization of the smul lemma, but what about op_smul? Before we can generalize (𝓝 x) <• y = 𝓝 (x * y) from [Group G]to [MulAction G α] I feel like we would need way more lemmas about the topological properties of fun x : G => x • y given y : α.
On that subject you might be interested in #maths > topological groups and uniformity @ 💬 and #mathlib4 > defining `MulAction.ball`

[Bhavik Mehta]

Yaël Dillies said:

I have a PR in the works that does this, fyi

Out of interest, did you end up changing the statement of mul_singleton or just changing the simp-set?

[Eric Wieser]

but what about op_smul?

It's the same lemma :)

[Yaël Dillies]

Bhavik Mehta said:

Out of interest, did you end up changing the statement of mul_singleton or just changing the simp-set?

The statement, with RHS a \smul s

[Eric Wieser]

#34795 adds the above

[Bhavik Mehta]

Yaël Dillies said:

Bhavik Mehta said:

Out of interest, did you end up changing the statement of mul_singleton or just changing the simp-set?

The statement, with RHS a \smul s

and the idea is that if someone wants the image version, they can do that further rewrite? That sounds reasonable to me!

[Eric Wieser]

Another set of lemmas we might want is:

lemma nhdsWithin_smul {s} (c : G) (x : α) : 𝓝[c • s] (c • x) = c • 𝓝[s] x := by
  rw [nhdsWithin, nhdsWithin, nhds_smul, ← Filter.map_smul, ← Filter.map_smul]
  rw [Filter.map_inf, Filter.map_principal]
  congr
  sorry

where the ugly proof is because we're missing some API elsewhere

[Lara Toledano]

Eric Wieser said:

but what about op_smul?

It's the same lemma :)

I can see how

Eric Wieser said:

open scoped Topology RightActions Pointwise
lemma nhds_smul [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α]
    (x : G) (y : α) : 𝓝 (x • y) = x • 𝓝 y :=
  (isOpenMap_smul x).map_nhds_eq (continuous_id.const_smul _ |>.continuousAt) |>.symm

also gives us [IsTopologicalGroup G] (x y : G) : (𝓝 x) <• y = 𝓝 (x*y)

What seems much more difficult to me is to generalize this to [MulAction G α] (x : G) (y : α) : (𝓝 x).map (fun g => g • y) = 𝓝 (x • y). The Effros Theorem states some sufficient conditions on the map • and the topological structures on Gand α, but this is really not trivial.

[Lara Toledano]

To be fair, this last question has little to do with RightActions or MulOpposite :sweat_smile:

[Lara Toledano]

Do you consider the specialization of nhds_smul to x⁻¹ • 𝓝 x = 𝓝 1 rather convenient or unnecessary?