# 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.

Equations
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.

Equations
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.

Equations
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.

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

Equivalence between M and Mᵈᵐᵃ.

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

Equivalence between M and Mᵈᵐᵃ.

Equations
• DomMulAct.mk = MulOpposite.opEquiv
Instances For

### Copy instances from Mᵐᵒᵖ#

Equations
Equations
Equations
Equations
Equations
Equations
• DomMulAct.instSemigroupOfMulOpposite = inst
Equations
Equations
Equations
Equations
• DomMulAct.instCommMonoidOfMulOpposite = inst
Equations
Equations
• DomMulAct.instInvolutiveInvOfMulOpposite = inst
Equations
Equations
• DomMulAct.instDivInvOneMonoidOfMulOpposite = inst
Equations
Equations
instance DomMulAct.instMonoidOfMulOpposite {M : Type u_1} [] :
Equations
• DomMulAct.instMonoidOfMulOpposite = inst
Equations
• DomMulAct.instInvOneClassOfMulOpposite = inst
Equations
Equations
Equations
• DomMulAct.instRightCancelMonoidOfMulOpposite = inst
Equations
Equations
• DomMulAct.instMulOneClassOfMulOpposite = inst
Equations
• DomMulAct.instNonAssocSemiringOfMulOpposite = inst
Equations
Equations
instance DomMulAct.instGroupOfMulOpposite {M : Type u_1} [] :
Equations
• DomMulAct.instGroupOfMulOpposite = inst
Equations
Equations
• DomMulAct.instCommGroupOfMulOpposite = inst
Equations
• DomMulAct.instSemiringOfMulOpposite = inst
Equations
Equations
Equations
• DomMulAct.instCancelMonoidOfMulOpposite = inst
Equations
instance DomMulAct.instMulOfMulOpposite {M : Type u_1} [] :
Equations
• DomMulAct.instMulOfMulOpposite = inst
Equations
• DomMulAct.instDivisionMonoidOfMulOpposite = inst
Equations
• DomMulAct.instLeftCancelMonoidOfMulOpposite = inst
Equations
• DomMulAct.instLeftCancelSemigroupOfMulOpposite = inst
Equations
• DomMulAct.instDivisionCommMonoidOfMulOpposite = inst
Equations
Equations
• DomMulAct.instCommSemigroupOfMulOpposite = inst
Equations
• DomMulAct.instCommRingOfMulOpposite = inst
Equations
Equations
Equations
instance DomMulAct.instRingOfMulOpposite {M : Type u_1} [] :
Equations
• DomMulAct.instRingOfMulOpposite = inst
instance DomMulAct.instOneOfMulOpposite {M : Type u_1} [] :
Equations
• DomMulAct.instOneOfMulOpposite = inst
Equations
• DomMulAct.instRightCancelSemigroupOfMulOpposite = inst
Equations
Equations
Equations
• DomMulAct.instDivInvMonoidOfMulOpposite = inst
instance DomMulAct.instInvOfMulOpposite {M : Type u_1} [] :
Equations
• DomMulAct.instInvOfMulOpposite = inst
Equations
• DomMulAct.instCancelCommMonoidOfMulOpposite = inst
Equations
Equations
• DomMulAct.instNonUnitalSemiringOfMulOpposite = inst
Equations
• DomMulAct.instNonAssocSemiringOfMulOpposite_1 = inst
Equations
• = inst
Equations
• = inst
Equations
• = inst
Equations
• = inst
Equations
• = inst
instance DomMulAct.instIsCancelMulOfMulOpposite {M : Type u_1} [] [] :
Equations
• = inst
@[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 DomAddAct.instVAddForall {M : Type u_1} {β : Type u_2} {α : Type u_3} [VAdd M α] :
Equations
• DomAddAct.instVAddForall = { vadd := fun (c : Mᵈᵃᵃ) (f : αβ) (a : α) => f (DomAddAct.mk.symm c +ᵥ a) }
instance DomMulAct.instSMulForall {M : Type u_1} {β : Type u_2} {α : Type u_3} [SMul M α] :
SMul Mᵈᵐᵃ (αβ)
Equations
• DomMulAct.instSMulForall = { smul := fun (c : Mᵈᵐᵃ) (f : αβ) (a : α) => f (DomMulAct.mk.symm c a) }
theorem DomAddAct.vadd_apply {M : Type u_1} {β : Type u_2} {α : Type u_3} [VAdd M α] (c : Mᵈᵃᵃ) (f : αβ) (a : α) :
(c +ᵥ f) a = f (DomAddAct.mk.symm c +ᵥ a)
theorem DomMulAct.smul_apply {M : Type u_1} {β : Type u_2} {α : Type u_3} [SMul M α] (c : Mᵈᵐᵃ) (f : αβ) (a : α) :
(c f) a = f (DomMulAct.mk.symm c a)
instance DomAddAct.instVAddCommClassForall {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [VAdd M α] [VAdd N β] :
Equations
• =
instance DomMulAct.instSMulCommClassForall {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N β] :
SMulCommClass Mᵈᵐᵃ N (αβ)
Equations
• =
instance DomAddAct.instVAddCommClassForall_1 {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [VAdd M α] [VAdd N β] :
Equations
• =
instance DomMulAct.instSMulCommClassForall_1 {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N β] :
SMulCommClass N Mᵈᵐᵃ (αβ)
Equations
• =
instance DomAddAct.instVAddCommClassForall_2 {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [VAdd M α] [VAdd N α] [] :
Equations
• =
instance DomMulAct.instSMulCommClassForall_2 {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N α] [] :
Equations
• =
instance DomAddAct.instFaithfulVAddForallOfNontrivial {M : Type u_1} {β : Type u_2} {α : Type u_3} [VAdd M α] [] [] :
Equations
• =
instance DomMulAct.instFaithfulSMulForallOfNontrivial {M : Type u_1} {β : Type u_2} {α : Type u_3} [SMul M α] [] [] :
FaithfulSMul Mᵈᵐᵃ (αβ)
Equations
• =
instance DomMulAct.instSMulZeroClassForallOfSMul {M : Type u_1} {β : Type u_2} {α : Type u_3} [SMul M α] [Zero β] :
Equations
• DomMulAct.instSMulZeroClassForallOfSMul =
instance DomMulAct.instDistribSMulForallOfSMul {M : Type u_1} {α : Type u_3} {A : Type u_5} [SMul M α] [] :
Equations
• DomMulAct.instDistribSMulForallOfSMul =
instance DomAddAct.instAddActionForall {M : Type u_1} {β : Type u_2} {α : Type u_3} [] [] :
Equations
theorem DomAddAct.instAddActionForall.proof_2 {M : Type u_1} {β : Type u_3} {α : Type u_2} [] [] :
∀ (x x_1 : Mᵈᵃᵃ) (f : αβ), x + x_1 +ᵥ f = x +ᵥ (x_1 +ᵥ f)
theorem DomAddAct.instAddActionForall.proof_1 {M : Type u_3} {β : Type u_2} {α : Type u_1} [] [] (f : αβ) :
0 +ᵥ f = f
instance DomMulAct.instMulActionForall {M : Type u_1} {β : Type u_2} {α : Type u_3} [] [] :
MulAction Mᵈᵐᵃ (αβ)
Equations
• DomMulAct.instMulActionForall =
instance DomMulAct.instDistribMulActionForallOfMulAction {M : Type u_1} {α : Type u_3} {A : Type u_5} [] [] [] :
Equations
• DomMulAct.instDistribMulActionForallOfMulAction =
instance DomMulAct.instMulDistribMulActionForallOfMulAction {M : Type u_1} {α : Type u_3} {A : Type u_5} [] [] [] :
Equations
• DomMulAct.instMulDistribMulActionForallOfMulAction =
instance DomMulAct.instSMulMonoidHom {M : Type u_5} {A : Type u_7} {B : Type u_8} [] [] [] [] :
Equations
instance DomMulAct.instSMulCommClassMonoidHom {M : Type u_5} {M' : Type u_6} {A : Type u_7} {B : Type u_8} [] [] [] [] [Monoid M'] [] [SMulCommClass M M' A] :
Equations
• =
theorem DomMulAct.smul_monoidHom_apply {M : Type u_5} {A : Type u_7} {B : Type u_8} [] [] [] [] (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_5} {A : Type u_7} {B : Type u_8} [] [] [] [] (c : M) (f : A →* B) (a : A) :
(DomMulAct.mk c f) a = f (c a)
instance DomMulAct.instMulActionMonoidHom {M : Type u_5} {A : Type u_7} {B : Type u_8} [] [] [] [] :
Equations
instance DomMulAct.instSMulAddMonoidHom {A : Type u_5} {B : Type u_6} {M : Type u_7} [] [] [] :
Equations
instance DomMulAct.instSMulCommClassAddMonoidHom {A : Type u_5} {B : Type u_6} {M : Type u_7} {M' : Type u_8} [] [] [] [DistribSMul M' A] [SMulCommClass M M' A] :
Equations
• =
instance DomMulAct.instSMulCommClassAddMonoidHom_1 {A : Type u_5} {B : Type u_6} {M : Type u_7} {M' : Type u_8} [] [] [] [DistribSMul M' B] :
Equations
• =
theorem DomMulAct.smul_addMonoidHom_apply {A : Type u_5} {B : Type u_6} {M : Type u_7} [] [] [] (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_5} {B : Type u_6} {M : Type u_7} [] [] [] (c : M) (f : A →+ B) (a : A) :
(DomMulAct.mk c f) a = f (c a)
theorem DomMulAct.coe_smul_addMonoidHom {A : Type u_5} {B : Type u_6} {M : Type u_7} [] [] [] (c : Mᵈᵐᵃ) (f : A →+ B) :
(c f) = c f
instance DomMulAct.instMulActionAddMonoidHomOfDistribMulAction {A : Type u_5} {M : Type u_6} {B : Type u_7} [] [] [] [] :
Equations
instance DomMulAct.instDistribMulActionAddMonoidHom {A : Type u_5} {M : Type u_6} {B : Type u_7} [] [] [] [] :
Equations