Action on functions

Stream: maths

[Yury G. Kudryashov]

If G acts on X, then it acts on X → Y (or C(X, Y), or X →₁[μ] E) on the right. I guess, having this action as an instance for unbundled functions will create a diamond somewhere (not sure). Do we have this action for some bundled maps? Do we have a name convention for lemmas about this action?

[Yury G. Kudryashov]

Context: I need the action on Lp (and continuity of this action) to prove that shift by an element with dense subgroup.closure is ergodic.

[Yury G. Kudryashov]

Of course, I can state the required lemmas in terms of (pending review) Lp.compMeasurePreserving if we don't want this as an instance.

[Yury G. Kudryashov]

(or put the instance in a scope)

[Eric Wieser]

We don't have this family of instances because we've chosen the convention that actions act on the codomain not the domain; and we can't have both without horrible diamonds everywhere

[Sebastien Gouezel]

I agree with Eric that, for f : G → G, we should keep the convention that a • f should still be the function mapping x to a * f x. It's maybe worth introducing a notation for the right action, though. It could be through a type synonym for G, say right_acting G which acts on the right by default. Then a.right • f would be the function mapping x to f (a⁻¹ * x).

[Eric Wieser]

The problem is that for compound types, there's actually a tree of choices regarding whether to act on the left or right. The current convention is to turn left at every fork, and we can use mul_opposite.op to turn right at the very last fork. I think we can probably get away with a synonym that means "turn right at every fork". All the intermediate choices seem very hard to label sanely, and are therefore best to just use via functions

[Eric Wieser]

For an example of what I mean, consider how G could act on ι → G → α; and then consider how the desired behavior is different if ι = G.

[Yaël Dillies]

Sorry, Eric, in my mental picture a type synonym can be inserted at any fork to change the way we're turning. Am I misunderstanding?

[Yaël Dillies]

Eg, taking your example, turn_left ι (turn_right G α).

[Eric Wieser]

I think that approach fails unless we remove the turn_left default

[Eric Wieser]

Because otherwise smul (turn_right G) (G → G) can still be resolved via pi.has_scalar and smul (turn_right G) G

[Eric Wieser]

Which in this analogy is a left turn!

[Yaël Dillies]

Oh that's not what I had in mind at all. To me, turn_right α β is a type synonym of α → β and your "turning right" action is smul G (turn_right G G).

[Yaël Dillies]

or, to avoid code duplication across types of bundled maps, turn_right F is a type synonym of F for some fun_like F, in which case the action is smul G (turn_right (G → G)) or smul G (turn_right (G →* G))

[Eric Wieser]

If you put the synonym on the right of the • then you lose the ability to talk about compatibility of actions

[Eric Wieser]

And now you have to write of_right (g • to_right f) instead of something simpler like right_act g • f

[Yaël Dillies]

I don't think that's such a high price to pay

[Eric Wieser]

Isn't all this a much higher price than my_act g f?

[Yaël Dillies]

well, as you said, your my_act doesn't work when having multiple forks.

[Eric Wieser]

For f' : ι → G → α you can write fun i => my_act g (f' i)

[Eric Wieser]

It's not clear that there's as much value in inheriting actions for the case Yury is asking for as there is for the existing element wise actions

[Eric Wieser]

And if you're not inheriting then you don't really need typeclasses and a regular definition will do

[Sebastien Gouezel]

I wasn't thinking of the most general situation, only of the situation that happens all the times in regular maths.

[Yury G. Kudryashov]

The specific action I need is

variable {X E : Type _}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  {p : ℝ≥0∞}

section MeasurableSMul

variable {M : Type _}
  [Monoid M] [MeasurableSpace M] [MulAction M X] [MeasurableSMul M X] [SMulInvariantMeasure M X μ]

@[to_additive]
instance : SMul Mᵐᵒᵖ (Lp E p μ) where
  smul c f := Lp.compMeasurePreserving (c.unop • · : X → X) (measurePreserving_smul _ μ) f

I guess, it creates a diamond for additive right actions of real numbers on the usual $L^1(\mathbb R)$ space.

[Yury G. Kudryashov]

What should I do: leave it as a def? Introduce a type synonym DomAct?

[Eric Wieser]

Can you add the rfl lemma above about (mul_opposite.op m • f) x = _ for clarity?

[Yury G. Kudryashov]

theorem coeFn_domAct (c : Mᵐᵒᵖ) (f : Lp E p μ) : c • f =ᵐ[μ] (f <| c.unop • ·) :=
  Lp.coeFn_compMeasurePreserving _ _

[Yury G. Kudryashov]

$L^p$ is a quotient space and coercion is given by Quotient.out, so no rfl...

[Yury G. Kudryashov]

So, should I add @[to_additive] def DomMulAct G := PreOpposite G, duplicate parts of the API, then add some MulAction instances?

[Kevin Buzzard]

We'll certainly one day want the left action of G on $L^2(X)$ given a right action of G on X, because this is how automorphic representations are defined.

[Eric Wieser]

What's the expected action of x : DomMulAct G on f : (G → G) → G?

• (x • f) i = f (fun j => x.unop • i j)
• (x • f) i = f (fun j => i (x.unop • j))?

[Yury G. Kudryashov]

It will look for MulAction G (G → G), find Pi.mulAction, and use it. So, the answer is (1). If you want (2), then you can use DomMulAct (DomMulAct G) (all of this is not tested).

[Yury G. Kudryashov]

Note that the second option is a left action while DomMulAct G is MulOpposite G, so an action of DomMulAct G is a right action.

[Yury G. Kudryashov]

#5368

[Yury G. Kudryashov]

BTW, I'm going to leave some good-first-project gaps in the DomMulAct API (example: action on C(X, Y); a function is invariant iff it is constant on the orbits), so if someone has an undergraduate who learns Lean 4 and needs exercised that can be turned into PRs, then please contact me.