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 #

We also define actions of Mᵈᵐᵃ on:

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:

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
          • DomAddAct.mk = AddOpposite.opEquiv
          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
              • DomAddAct.instAddOfAddOpposite = inst
              Equations
              • DomAddAct.instNonAssocSemiringOfAddOpposite = inst
              Equations
              • DomAddAct.instSubNegAddMonoidOfAddOpposite = inst
              Equations
              • DomAddAct.instAddCommGroupOfAddOpposite = inst
              Equations
              • DomAddAct.instAddCommSemigroupOfAddOpposite = inst
              Equations
              • DomMulAct.instLeftCancelMonoidOfMulOpposite = inst
              Equations
              • DomMulAct.instMulOneClassOfMulOpposite = inst
              Equations
              • DomAddAct.instNegOfAddOpposite = inst
              Equations
              • DomAddAct.instAddGroupOfAddOpposite = inst
              Equations
              • DomAddAct.instAddLeftCancelSemigroupOfAddOpposite = inst
              Equations
              • DomAddAct.instAddRightCancelMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instCancelMonoidOfMulOpposite = inst
              Equations
              • DomAddAct.instZeroOfAddOpposite = inst
              Equations
              • DomAddAct.instAddCommMonoidOfAddOpposite = inst
              Equations
              • DomAddAct.instAddCancelMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instNonUnitalSemiringOfMulOpposite = inst
              Equations
              • DomAddAct.instAddMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instNonAssocSemiringOfMulOpposite = inst
              Equations
              • DomMulAct.instCommRingOfMulOpposite = inst
              Equations
              • DomMulAct.instRightCancelMonoidOfMulOpposite = inst
              Equations
              • DomMulAct.instCancelCommMonoidOfMulOpposite = inst
              Equations
              • DomMulAct.instRightCancelSemigroupOfMulOpposite = inst
              Equations
              • DomMulAct.instDivInvOneMonoidOfMulOpposite = inst
              Equations
              • DomMulAct.instGroupOfMulOpposite = inst
              Equations
              • DomAddAct.instAddCancelCommMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instSemiringOfMulOpposite = inst
              Equations
              • DomMulAct.instDivisionMonoidOfMulOpposite = inst
              Equations
              • DomMulAct.instInvolutiveInvOfMulOpposite = inst
              Equations
              • DomMulAct.instMonoidOfMulOpposite = inst
              Equations
              • DomAddAct.instNegZeroClassOfAddOpposite = inst
              Equations
              • DomAddAct.instAddSemigroupOfAddOpposite = inst
              Equations
              • DomMulAct.instOneOfMulOpposite = inst
              Equations
              • DomAddAct.instAddZeroClassOfAddOpposite = inst
              Equations
              • DomMulAct.instInvOneClassOfMulOpposite = inst
              Equations
              • DomAddAct.instInvolutiveNegOfAddOpposite = inst
              Equations
              • DomMulAct.instNonAssocSemiringOfMulOpposite_1 = inst
              Equations
              • DomAddAct.instNonAssocSemiringOfAddOpposite_1 = inst
              Equations
              • DomAddAct.instSubNegZeroMonoidOfAddOpposite = inst
              Equations
              • DomAddAct.instDivisionAddCommMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instCommSemigroupOfMulOpposite = inst
              Equations
              • DomMulAct.instRingOfMulOpposite = inst
              Equations
              • DomMulAct.instLeftCancelSemigroupOfMulOpposite = inst
              Equations
              • DomAddAct.instRingOfAddOpposite = inst
              Equations
              • DomAddAct.instAddRightCancelSemigroupOfAddOpposite = inst
              Equations
              • DomMulAct.instInvOfMulOpposite = inst
              Equations
              • DomAddAct.instNonUnitalSemiringOfAddOpposite = inst
              Equations
              • DomAddAct.instSemiringOfAddOpposite = inst
              Equations
              • DomMulAct.instSemigroupOfMulOpposite = inst
              Equations
              • DomMulAct.instDivisionCommMonoidOfMulOpposite = inst
              Equations
              • DomAddAct.instCommRingOfAddOpposite = inst
              Equations
              • DomMulAct.instCommMonoidOfMulOpposite = inst
              Equations
              • DomMulAct.instDivInvMonoidOfMulOpposite = inst
              Equations
              • DomAddAct.instSubtractionMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instCommGroupOfMulOpposite = inst
              Equations
              • DomAddAct.instAddLeftCancelMonoidOfAddOpposite = inst
              Equations
              • DomMulAct.instMulOfMulOpposite = inst
              @[simp]
              theorem DomAddAct.mk_zero {M : Type u_1} [Zero M] :
              DomAddAct.mk 0 = 0
              @[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] :
              DomAddAct.mk.symm 0 = 0
              @[simp]
              theorem DomMulAct.symm_mk_one {M : Type u_1} [One M] :
              DomMulAct.mk.symm 1 = 1
              @[simp]
              theorem DomAddAct.mk_add {M : Type u_1} [Add M] (a : M) (b : M) :
              DomAddAct.mk (a + b) = DomAddAct.mk b + DomAddAct.mk a
              @[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]
              theorem DomAddAct.symm_mk_add {M : Type u_1} [Add M] (a : Mᵈᵃᵃ) (b : Mᵈᵃᵃ) :
              DomAddAct.mk.symm (a + b) = DomAddAct.mk.symm b + DomAddAct.mk.symm a
              @[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) :
              DomAddAct.mk (-a) = -DomAddAct.mk a
              @[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ᵈᵃᵃ) :
              DomAddAct.mk.symm (-a) = -DomAddAct.mk.symm a
              @[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} [AddMonoid M] (a : M) (n : ) :
              DomAddAct.mk (n a) = n DomAddAct.mk a
              @[simp]
              theorem DomMulAct.mk_pow {M : Type u_1} [Monoid M] (a : M) (n : ) :
              DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
              @[simp]
              theorem DomAddAct.symm_mk_nsmul {M : Type u_1} [AddMonoid M] (a : Mᵈᵃᵃ) (n : ) :
              DomAddAct.mk.symm (n a) = n DomAddAct.mk.symm a
              @[simp]
              theorem DomMulAct.symm_mk_pow {M : Type u_1} [Monoid M] (a : Mᵈᵐᵃ) (n : ) :
              DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
              @[simp]
              theorem DomAddAct.mk_zsmul {M : Type u_1} [SubNegMonoid M] (a : M) (n : ) :
              DomAddAct.mk (n a) = n DomAddAct.mk a
              @[simp]
              theorem DomMulAct.mk_zpow {M : Type u_1} [DivInvMonoid M] (a : M) (n : ) :
              DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
              @[simp]
              theorem DomAddAct.symm_mk_zsmul {M : Type u_1} [SubNegMonoid M] (a : Mᵈᵃᵃ) (n : ) :
              DomAddAct.mk.symm (n a) = n DomAddAct.mk.symm a
              @[simp]
              theorem DomMulAct.symm_mk_zpow {M : Type u_1} [DivInvMonoid M] (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 α] :
              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 β] :
              VAddCommClass Mᵈᵃᵃ 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 β] :
              VAddCommClass N Mᵈᵃᵃ (αβ)
              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 α] [VAddCommClass M N α] :
              Equations
              • =
              instance DomMulAct.instSMulCommClassForall_2 {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N α] [SMulCommClass M N α] :
              Equations
              • =
              instance DomAddAct.instFaithfulVAddForallOfNontrivial {M : Type u_1} {β : Type u_2} {α : Type u_3} [VAdd M α] [FaithfulVAdd M α] [Nontrivial β] :
              FaithfulVAdd Mᵈᵃᵃ (αβ)
              Equations
              • =
              instance DomMulAct.instFaithfulSMulForallOfNontrivial {M : Type u_1} {β : Type u_2} {α : Type u_3} [SMul M α] [FaithfulSMul M α] [Nontrivial β] :
              FaithfulSMul Mᵈᵐᵃ (αβ)
              Equations
              • =
              instance DomMulAct.instSMulZeroClassForallOfSMul {M : Type u_1} {β : Type u_2} {α : Type u_3} [SMul M α] [Zero β] :
              Equations
              instance DomMulAct.instDistribSMulForallOfSMul {M : Type u_1} {α : Type u_3} {A : Type u_5} [SMul M α] [AddZeroClass A] :
              Equations
              instance DomAddAct.instAddActionForall {M : Type u_1} {β : Type u_2} {α : Type u_3} [AddMonoid M] [AddAction M α] :
              AddAction Mᵈᵃᵃ (αβ)
              Equations
              instance DomMulAct.instMulActionForall {M : Type u_1} {β : Type u_2} {α : Type u_3} [Monoid M] [MulAction M α] :
              MulAction Mᵈᵐᵃ (αβ)
              Equations
              instance DomMulAct.instDistribMulActionForallOfMulAction {M : Type u_1} {α : Type u_3} {A : Type u_5} [Monoid M] [MulAction M α] [AddMonoid A] :
              Equations
              instance DomMulAct.instMulDistribMulActionForallOfMulAction {M : Type u_1} {α : Type u_3} {A : Type u_5} [Monoid M] [MulAction M α] [Monoid A] :
              Equations
              instance DomMulAct.instSMulMonoidHom {M : Type u_5} {A : Type u_7} {B : Type u_8} [Monoid M] [Monoid A] [MulDistribMulAction M A] [MulOneClass B] :
              Equations
              instance DomMulAct.instSMulCommClassMonoidHom {M : Type u_5} {M' : Type u_6} {A : Type u_7} {B : Type u_8} [Monoid M] [Monoid A] [MulDistribMulAction M A] [MulOneClass B] [Monoid M'] [MulDistribMulAction M' A] [SMulCommClass M M' A] :
              Equations
              • =
              theorem DomMulAct.smul_monoidHom_apply {M : Type u_5} {A : Type u_7} {B : Type u_8} [Monoid M] [Monoid A] [MulDistribMulAction M A] [MulOneClass B] (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} [Monoid M] [Monoid A] [MulDistribMulAction M A] [MulOneClass B] (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} [Monoid M] [Monoid A] [MulDistribMulAction M A] [MulOneClass B] :
              Equations
              instance DomMulAct.instSMulAddMonoidHom {A : Type u_5} {B : Type u_6} {M : Type u_7} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] :
              Equations
              instance DomMulAct.instSMulCommClassAddMonoidHom {A : Type u_5} {B : Type u_6} {M : Type u_7} {M' : Type u_8} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] [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} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] [DistribSMul M' B] :
              Equations
              • =
              theorem DomMulAct.smul_addMonoidHom_apply {A : Type u_5} {B : Type u_6} {M : Type u_7} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] (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} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] (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} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] (c : Mᵈᵐᵃ) (f : A →+ B) :
              (c f) = c f
              Equations
              Equations
              Equations