Type tags for right action on the domain of a function #

By default, M acts on α → β if it acts on β, and the action is given by (c • f) a = c • (f a).

In some cases, it is useful to consider another action: if M acts on α on the left, then it acts on α → β on the right so that (c • f) a = f (c • a). E.g., this action is used to reformulate the Mean Ergodic Theorem in terms of an operator on (L^2).

Main definitions #

DomMulAct M (notation: Mᵈᵐᵃ): type synonym for Mᵐᵒᵖ; if M multiplicatively acts on α, then Mᵈᵐᵃ acts on α → β for any type β;
DomAddAct M (notation: Mᵈᵃᵃ): the additive version.

We also define actions of Mᵈᵐᵃ on:

α → β provided that M acts on α;
A →* B provided that M acts on A by a MulDistribMulAction;
A →+ B provided that M acts on A by a DistribMulAction.

Implementation details #

Motivation #

Right action can be represented in mathlib as an action of the opposite group Mᵐᵒᵖ. However, this "domain shift" action cannot be an instance because this would create a "diamond" (a.k.a. ambiguous notation): if M is a monoid, then how does Mᵐᵒᵖ act on M → M? On the one hand, Mᵐᵒᵖ acts on M by c • a = a * c.unop, thus we have an action (c • f) a = f a * c.unop. On the other hand, M acts on itself by multiplication on the left, so with this new instance we would have (c • f) a = f (c.unop * a). Clearly, these are two different actions, so both of them cannot be instances in the library.

To overcome this difficulty, we introduce a type synonym DomMulAct M := Mᵐᵒᵖ (notation: Mᵈᵐᵃ). This new type carries the same algebraic structures as Mᵐᵒᵖ but acts on α → β by this new action. So, e.g., Mᵈᵐᵃ acts on (M → M) → M by DomMulAct.mk c • F f = F (fun a ↦ c • f a) while (Mᵈᵐᵃ)ᵈᵐᵃ (which is isomorphic to M) acts on (M → M) → M by DomMulAct.mk (DomMulAct.mk c) • F f = F (fun a ↦ f (c • a)).

Action on bundled homomorphisms #

If the action of M on A preserves some structure, then Mᵈᵐᵃ acts on bundled homomorphisms from A to any type B that preserve the same structure. Examples (some of them are not yet in the library) include:

a MulDistribMulAction generates an action on A →* B;
a DistribMulAction generates an action on A →+ B;
an action on α that commutes with action of some other monoid N generates an action on α →[N] β;
a DistribMulAction on an R-module that commutes with scalar multiplications by c : R generates an action on R-linear maps from this module;
a continuous action on X generates an action on C(X, Y);
a measurable action on X generates an action on { f : X → Y // Measurable f };
a quasi measure preserving action on X generates an action on X →ₘ[μ] Y;
a measure preserving action generates an isometric action on MeasureTheory.Lp _ _ _.

Left action vs right action #

It is common in the literature to consider the left action given by (c • f) a = f (c⁻¹ • a) instead of the action defined in this file. However, this left action is defined only if c belongs to a group, not to a monoid, so we decided to go with the right action.

The left action can be written in terms of DomMulAct as (DomMulAct.mk c)⁻¹ • f. As for higher level dynamics objects (orbits, invariant functions etc), they coincide for the left and for the right action, so lemmas can be formulated in terms of DomMulAct.

Keywords #

group action, function, domain