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
              • DomMulAct.instCommRingDomMulAct = inst
              Equations
              • DomMulAct.instMonoidDomMulAct = inst
              Equations
              • DomAddAct.instSubNegAddMonoidDomAddAct = inst
              Equations
              • DomAddAct.instAddCommGroupDomAddAct = inst
              Equations
              • DomMulAct.instNonAssocSemiringDomMulAct_1 = inst
              Equations
              • DomMulAct.instSemigroupDomMulAct = inst
              Equations
              • DomAddAct.instInvolutiveNegDomAddAct = inst
              Equations
              • DomMulAct.instMulOneClassDomMulAct = inst
              Equations
              • DomMulAct.instMulDomMulAct = inst
              Equations
              • DomAddAct.instZeroDomAddAct = inst
              Equations
              • DomAddAct.instSubNegZeroAddMonoidDomAddAct = inst
              Equations
              • DomAddAct.instAddSemigroupDomAddAct = inst
              Equations
              • DomAddAct.instAddCancelMonoidDomAddAct = inst
              Equations
              • DomAddAct.instAddLeftCancelMonoidDomAddAct = inst
              Equations
              • DomMulAct.instCommSemigroupDomMulAct = inst
              Equations
              • DomMulAct.instDivInvMonoidDomMulAct = inst
              Equations
              • DomMulAct.instCancelMonoidDomMulAct = inst
              Equations
              • DomAddAct.instCommRingDomAddAct = inst
              Equations
              • DomMulAct.instCancelCommMonoidDomMulAct = inst
              Equations
              • DomMulAct.instInvolutiveInvDomMulAct = inst
              Equations
              • DomAddAct.instNegZeroClassDomAddAct = inst
              Equations
              • DomMulAct.instSemiringDomMulAct = inst
              Equations
              • DomAddAct.instAddCommMonoidDomAddAct = inst
              Equations
              • DomAddAct.instDivisionAddCommMonoidDomAddAct = inst
              Equations
              • DomMulAct.instDivisionMonoidDomMulAct = inst
              Equations
              • DomMulAct.instLeftCancelSemigroupDomMulAct = inst
              Equations
              • DomMulAct.instNonUnitalSemiringDomMulAct = inst
              Equations
              • DomAddAct.instAddMonoidDomAddAct = inst
              Equations
              • DomAddAct.instAddGroupDomAddAct = inst
              Equations
              • DomMulAct.instLeftCancelMonoidDomMulAct = inst
              Equations
              • DomAddAct.instSemiringDomAddAct = inst
              Equations
              • DomMulAct.instDivisionCommMonoidDomMulAct = inst
              Equations
              • DomAddAct.instNonUnitalSemiringDomAddAct = inst
              Equations
              • DomAddAct.instAddCommSemigroupDomAddAct = inst
              Equations
              • DomMulAct.instRingDomMulAct = inst
              Equations
              • DomMulAct.instCommGroupDomMulAct = inst
              Equations
              • DomAddAct.instAddLeftCancelSemigroupDomAddAct = inst
              Equations
              • DomMulAct.instDivInvOneMonoidDomMulAct = inst
              Equations
              • DomAddAct.instNonAssocSemiringDomAddAct = inst
              Equations
              • DomMulAct.instRightCancelSemigroupDomMulAct = inst
              Equations
              • DomAddAct.instNegDomAddAct = inst
              Equations
              • DomMulAct.instNonAssocSemiringDomMulAct = inst
              Equations
              • DomMulAct.instRightCancelMonoidDomMulAct = inst
              Equations
              • DomAddAct.instNonAssocSemiringDomAddAct_1 = inst
              Equations
              • DomAddAct.instAddRightCancelSemigroupDomAddAct = inst
              Equations
              • DomMulAct.instCommMonoidDomMulAct = inst
              Equations
              • DomAddAct.instRingDomAddAct = inst
              Equations
              • DomAddAct.instAddCancelCommMonoidDomAddAct = inst
              Equations
              • DomMulAct.instInvDomMulAct = inst
              Equations
              • DomAddAct.instDivisionAddMonoidDomAddAct = inst
              Equations
              • DomMulAct.instInvOneClassDomMulAct = inst
              Equations
              • DomMulAct.instGroupDomMulAct = inst
              Equations
              • DomAddAct.instAddDomAddAct = inst
              Equations
              • DomAddAct.instAddZeroClassDomAddAct = inst
              Equations
              • DomAddAct.instAddRightCancelMonoidDomAddAct = inst
              Equations
              • DomMulAct.instOneDomMulAct = 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.instVAddDomAddActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} [VAdd M α] :
              VAdd Mᵈᵃᵃ (αβ)
              Equations
              • DomAddAct.instVAddDomAddActForAll = { vadd := fun (c : Mᵈᵃᵃ) (f : αβ) (a : α) => f (DomAddAct.mk.symm c +ᵥ a) }
              instance DomMulAct.instSMulDomMulActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] :
              SMul Mᵈᵐᵃ (αβ)
              Equations
              • DomMulAct.instSMulDomMulActForAll = { smul := fun (c : Mᵈᵐᵃ) (f : αβ) (a : α) => f (DomMulAct.mk.symm c a) }
              theorem DomAddAct.vadd_apply {β : Type u_1} {M : 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 {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] (c : Mᵈᵐᵃ) (f : αβ) (a : α) :
              (c f) a = f (DomMulAct.mk.symm c a)
              instance DomAddAct.instVAddCommClassDomAddActForAllInstVAddDomAddActForAllInstVAdd {β : Type u_1} {M : Type u_2} {α : Type u_3} {N : Type u_4} [VAdd M α] [VAdd N β] :
              VAddCommClass Mᵈᵃᵃ N (αβ)
              Equations
              • =
              instance DomMulAct.instSMulCommClassDomMulActForAllInstSMulDomMulActForAllInstSMul {β : Type u_1} {M : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N β] :
              SMulCommClass Mᵈᵐᵃ N (αβ)
              Equations
              • =
              instance DomAddAct.instVAddCommClassDomAddActForAllInstVAddInstVAddDomAddActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} {N : Type u_4} [VAdd M α] [VAdd N β] :
              VAddCommClass N Mᵈᵃᵃ (αβ)
              Equations
              • =
              instance DomMulAct.instSMulCommClassDomMulActForAllInstSMulInstSMulDomMulActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} {N : Type u_4} [SMul M α] [SMul N β] :
              SMulCommClass N Mᵈᵐᵃ (αβ)
              Equations
              • =
              Equations
              • =
              Equations
              • =
              instance DomAddAct.instFaithfulVAddDomAddActForAllInstVAddDomAddActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} [VAdd M α] [FaithfulVAdd M α] [Nontrivial β] :
              FaithfulVAdd Mᵈᵃᵃ (αβ)
              Equations
              • =
              instance DomMulAct.instFaithfulSMulDomMulActForAllInstSMulDomMulActForAll {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] [FaithfulSMul M α] [Nontrivial β] :
              FaithfulSMul Mᵈᵐᵃ (αβ)
              Equations
              • =
              instance DomMulAct.instSMulZeroClassDomMulActForAllInstZero {β : Type u_1} {M : Type u_2} {α : Type u_3} [SMul M α] [Zero β] :
              Equations
              instance DomMulAct.instDistribSMulDomMulActForAllAddZeroClass {M : Type u_2} {α : Type u_3} {A : Type u_4} [SMul M α] [AddZeroClass A] :
              Equations
              Equations
              • DomAddAct.instAddActionDomAddActForAllInstAddMonoidDomAddActAddMonoid = AddAction.mk
              theorem DomAddAct.instAddActionDomAddActForAllInstAddMonoidDomAddActAddMonoid.proof_1 {β : Type u_2} {M : Type u_3} {α : Type u_1} [AddMonoid M] [AddAction M α] (f : αβ) :
              0 +ᵥ f = f
              theorem DomAddAct.instAddActionDomAddActForAllInstAddMonoidDomAddActAddMonoid.proof_2 {β : Type u_3} {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] :
              ∀ (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} [Monoid M] [MulAction M α] :
              MulAction Mᵈᵐᵃ (αβ)
              Equations
              • DomMulAct.instMulActionDomMulActForAllInstMonoidDomMulActMonoid = MulAction.mk
              Equations
              • DomMulAct.instDistribMulActionDomMulActForAllInstMonoidDomMulActMonoidAddMonoid = DistribMulAction.mk
              Equations
              theorem DomMulAct.smul_monoidHom_apply {M : Type u_2} {A : Type u_4} {B : Type u_3} [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_4} {A : Type u_3} {B : Type u_2} [Monoid M] [Monoid A] [MulDistribMulAction M A] [MulOneClass B] (c : M) (f : A →* B) (a : A) :
              (DomMulAct.mk c f) a = f (c a)
              Equations
              Equations
              theorem DomMulAct.smul_addMonoidHom_apply {A : Type u_4} {M : Type u_2} {B : Type u_3} [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_3} {M : Type u_4} {B : Type u_2} [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_4} {M : Type u_2} {B : Type u_3} [AddMonoid A] [DistribSMul M A] [AddZeroClass B] (c : Mᵈᵐᵃ) (f : A →+ B) :
              (c f) = c f
              Equations