# Documentation

Mathlib.GroupTheory.GroupAction.DomAct.Basic

# 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

def DomAddAct (M : Type u_1) :
Type u_1

If M additively acts on α, then DomAddAct M acts on α → β as well as some bundled maps from α. This is a type synonym for AddOpposite M, so this corresponds to a right action of M.

Instances For
def DomMulAct (M : Type u_1) :
Type u_1

If M multiplicatively acts on α, then DomMulAct M acts on α → β as well as some bundled maps from α. This is a type synonym for MulOpposite M, so this corresponds to a right action of M.

Instances For

If M multiplicatively acts on α, then DomMulAct M acts on α → β as well as some bundled maps from α. This is a type synonym for MulOpposite M, so this corresponds to a right action of M.

Instances For

If M additively acts on α, then DomAddAct M acts on α → β as well as some bundled maps from α. This is a type synonym for AddOpposite M, so this corresponds to a right action of M.

Instances For
def DomAddAct.mk {M : Type u_1} :

Equivalence between M and Mᵈᵐᵃ.

Instances For
def DomMulAct.mk {M : Type u_1} :

Equivalence between M and Mᵈᵐᵃ.

Instances For

### Copy instances from Mᵐᵒᵖ#

instance DomMulAct.instOneDomMulAct {M : Type u_1} [] :
instance DomMulAct.instMulDomMulAct {M : Type u_1} [] :
instance DomMulAct.instInvDomMulAct {M : Type u_1} [] :
@[simp]
theorem DomAddAct.mk_zero {M : Type u_1} [Zero M] :
@[simp]
theorem DomMulAct.mk_one {M : Type u_1} [One M] :
DomMulAct.mk 1 = 1
@[simp]
theorem DomAddAct.symm_mk_zero {M : Type u_1} [Zero M] :
@[simp]
theorem DomMulAct.symm_mk_one {M : Type u_1} [One M] :
DomMulAct.mk.symm 1 = 1
@[simp]
@[simp]
theorem DomMulAct.mk_mul {M : Type u_1} [Mul M] (a : M) (b : M) :
DomMulAct.mk (a * b) = DomMulAct.mk b * DomMulAct.mk a
@[simp]
@[simp]
theorem DomMulAct.symm_mk_mul {M : Type u_1} [Mul M] (a : Mᵈᵐᵃ) (b : Mᵈᵐᵃ) :
DomMulAct.mk.symm (a * b) = DomMulAct.mk.symm b * DomMulAct.mk.symm a
@[simp]
theorem DomAddAct.mk_neg {M : Type u_1} [Neg M] (a : M) :
@[simp]
theorem DomMulAct.mk_inv {M : Type u_1} [Inv M] (a : M) :
DomMulAct.mk a⁻¹ = (DomMulAct.mk a)⁻¹
@[simp]
theorem DomAddAct.symm_mk_neg {M : Type u_1} [Neg M] (a : Mᵈᵃᵃ) :
@[simp]
theorem DomMulAct.symm_mk_inv {M : Type u_1} [Inv M] (a : Mᵈᵐᵃ) :
DomMulAct.mk.symm a⁻¹ = (DomMulAct.mk.symm a)⁻¹
@[simp]
theorem DomAddAct.mk_nsmul {M : Type u_1} [] (a : M) (n : ) :
@[simp]
theorem DomMulAct.mk_pow {M : Type u_1} [] (a : M) (n : ) :
DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
@[simp]
theorem DomAddAct.symm_mk_nsmul {M : Type u_1} [] (a : Mᵈᵃᵃ) (n : ) :
@[simp]
theorem DomMulAct.symm_mk_pow {M : Type u_1} [] (a : Mᵈᵐᵃ) (n : ) :
DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
@[simp]
theorem DomAddAct.mk_zsmul {M : Type u_1} [] (a : M) (n : ) :
@[simp]
theorem DomMulAct.mk_zpow {M : Type u_1} [] (a : M) (n : ) :
DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
@[simp]
theorem DomAddAct.symm_mk_zsmul {M : Type u_1} [] (a : Mᵈᵃᵃ) (n : ) :
@[simp]
theorem DomMulAct.symm_mk_zpow {M : Type u_1} [] (a : Mᵈᵐᵃ) (n : ) :
DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
instance DomMulAct.instSMulDomMulActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] :
SMul Mᵈᵐᵃ (αβ)
theorem DomAddAct.vadd_apply {β : Type u_1} {M : Type u_2} {α : Type u_3} [VAdd M α] (c : Mᵈᵃᵃ) (f : αβ) (a : α) :
(Mᵈᵃᵃ +ᵥ (αβ)) (αβ) instHVAdd c f a = f (DomAddAct.mk.symm c +ᵥ a)
theorem DomMulAct.smul_apply {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] (c : Mᵈᵐᵃ) (f : αβ) (a : α) :
(Mᵈᵐᵃ (αβ)) (αβ) instHSMul c f a = f (DomMulAct.mk.symm c a)
instance DomMulAct.instSMulCommClassDomMulActForAllInstSMulDomMulActForAllInstSMul {β : Type u_1} {M : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N β] :
SMulCommClass Mᵈᵐᵃ N (αβ)
instance DomMulAct.instSMulCommClassDomMulActForAllInstSMulInstSMulDomMulActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N β] :
SMulCommClass N Mᵈᵐᵃ (αβ)
instance DomMulAct.instFaithfulSMulDomMulActForAllInstSMulDomMulActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] [] [] :
FaithfulSMul Mᵈᵐᵃ (αβ)
instance DomMulAct.instSMulZeroClassDomMulActForAllInstZero {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] [Zero β] :
instance DomMulAct.instDistribSMulDomMulActForAllAddZeroClass {M : Type u_2} {α : Type u_3} {A : Type u_4} [SMul M α] [] :
0 +ᵥ f = f
∀ (x x_1 : Mᵈᵃᵃ) (f : αβ), x + x_1 +ᵥ f = x +ᵥ (x_1 +ᵥ f)
instance DomMulAct.instMulActionDomMulActForAllInstMonoidDomMulActMonoid {β : Type u_1} {M : Type u_2} {α : Type u_3} [] [] :
MulAction Mᵈᵐᵃ (αβ)
instance DomMulAct.instSMulDomMulActMonoidHomToMulOneClass {M : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] :
theorem DomMulAct.smul_monoidHom_apply {M : Type u_2} {A : Type u_4} {B : Type u_3} [] [] [] [] (c : Mᵈᵐᵃ) (f : A →* B) (a : A) :
↑(c f) a = f (DomMulAct.mk.symm c a)
@[simp]
theorem DomMulAct.mk_smul_monoidHom_apply {M : Type u_4} {A : Type u_3} {B : Type u_2} [] [] [] [] (c : M) (f : A →* B) (a : A) :
↑(DomMulAct.mk c f) a = f (c a)
instance DomMulAct.instSMulDomMulActAddMonoidHomToAddZeroClass {A : Type u_2} {M : Type u_3} {B : Type u_4} [] [] [] :
theorem DomMulAct.smul_addMonoidHom_apply {A : Type u_4} {M : Type u_2} {B : Type u_3} [] [] [] (c : Mᵈᵐᵃ) (f : A →+ B) (a : A) :
↑(c f) a = f (DomMulAct.mk.symm c a)
@[simp]
theorem DomMulAct.mk_smul_addMonoidHom_apply {A : Type u_3} {M : Type u_4} {B : Type u_2} [] [] [] (c : M) (f : A →+ B) (a : A) :
↑(DomMulAct.mk c f) a = f (c a)