Documentation

Mathlib.Algebra.GroupWithZero.Action.Basic

Definitions of group actions #

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes SMul and its additive version VAdd:

The hierarchy is extended further by Module, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,

Notation #

Implementation details #

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

Tags #

group action

theorem MulAction.bijective₀ {G₀ : Type u_2} {α : Type u_8} [GroupWithZero G₀] [MulAction G₀ α] {a : G₀} (ha : a 0) :
Function.Bijective fun (x : α) => a x
theorem MulAction.injective₀ {G₀ : Type u_2} {α : Type u_8} [GroupWithZero G₀] [MulAction G₀ α] {a : G₀} (ha : a 0) :
Function.Injective fun (x : α) => a x
theorem MulAction.surjective₀ {G₀ : Type u_2} {α : Type u_8} [GroupWithZero G₀] [MulAction G₀ α] {a : G₀} (ha : a 0) :
Function.Surjective fun (x : α) => a x
@[simp]
theorem DistribMulAction.toAddEquiv_symm_apply {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) :
∀ (a : A), (DistribMulAction.toAddEquiv A x).symm a = x⁻¹ a
@[simp]
theorem DistribMulAction.toAddEquiv_apply {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) :
∀ (a : A), (DistribMulAction.toAddEquiv A x) a = x a
def DistribMulAction.toAddEquiv {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) :
A ≃+ A

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of MulAction.toPerm.

Equations
Instances For
    def DistribMulAction.toAddAut (G : Type u_1) (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] :

    Each element of the group defines an additive monoid isomorphism.

    This is a stronger version of MulAction.toPermHom.

    Equations
    Instances For
      @[simp]
      theorem smulMonoidWithZeroHom_apply {M₀ : Type u_5} {N₀ : Type u_6} [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] :
      ∀ (a : M₀ × N₀), smulMonoidWithZeroHom a = (↑smulMonoidHom).toFun a
      def smulMonoidWithZeroHom {M₀ : Type u_5} {N₀ : Type u_6} [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] :
      M₀ × N₀ →*₀ N₀

      Scalar multiplication as a monoid homomorphism with zero.

      Equations
      • smulMonoidWithZeroHom = { toFun := (↑smulMonoidHom).toFun, map_zero' := , map_one' := , map_mul' := }
      Instances For
        @[simp]
        theorem MulDistribMulAction.toMulEquiv_symm_apply {G : Type u_1} (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) :
        ∀ (a : M), (MulDistribMulAction.toMulEquiv M x).symm a = x⁻¹ a
        @[simp]
        theorem MulDistribMulAction.toMulEquiv_apply {G : Type u_1} (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) :
        ∀ (a : M), (MulDistribMulAction.toMulEquiv M x) a = x a
        def MulDistribMulAction.toMulEquiv {G : Type u_1} (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) :
        M ≃* M

        Each element of the group defines a multiplicative monoid isomorphism.

        This is a stronger version of MulAction.toPerm.

        Equations
        Instances For

          Each element of the group defines a multiplicative monoid isomorphism.

          This is a stronger version of MulAction.toPermHom.

          Equations
          Instances For

            The tautological action by MulAut M on M.

            This generalizes Function.End.applyMulAction.

            Equations

            The tautological action by AddAut A on A.

            This generalizes Function.End.applyMulAction.

            Equations
            def arrowMulDistribMulAction {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] :

            When M is a monoid, ArrowAction is additionally a MulDistribMulAction.

            Equations
            Instances For
              @[simp]
              theorem mulAutArrow_apply_apply {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) :
              ∀ (a : AM) (a_1 : A), (mulAutArrow x) a a_1 = (x a) a_1
              @[simp]
              theorem mulAutArrow_apply_symm_apply {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) :
              ∀ (a : AM) (a_1 : A), (MulEquiv.symm (mulAutArrow x)) a a_1 = (x⁻¹ a) a_1
              def mulAutArrow {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] :
              G →* MulAut (AM)

              Given groups G H with G acting on A, G acts by multiplicative automorphisms on A → H.

              Equations
              Instances For
                theorem IsUnit.smul_sub_iff_sub_inv_smul {G : Type u_1} {R : Type u_7} [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R] [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R) :
                IsUnit (r 1 - a) IsUnit (1 - r⁻¹ a)