Documentation

Mathlib.Algebra.Group.Action.End

Interaction between actions and endomorphisms/automorphisms #

This file provides two things:

Tags #

monoid action, group action

Tautological actions #

Tautological action by Function.End #

The tautological action by Function.End α on α.

This is generalized to bundled endomorphisms by:

Equations

    The tautological additive action by Additive (Function.End α) on α.

    Equations
      @[simp]
      theorem Function.End.smul_def {α : Type u_5} (f : Function.End α) (a : α) :
      f a = f a
      theorem Function.End.mul_def {α : Type u_5} (f g : Function.End α) :
      f * g = f g
      theorem Function.End.one_def {α : Type u_5} :
      1 = id

      Tautological action by Equiv.Perm #

      instance Equiv.Perm.applyMulAction (α : Type u_6) :
      MulAction (Perm α) α

      The tautological action by Equiv.Perm α on α.

      This generalizes Function.End.applyMulAction.

      Equations
        @[simp]
        theorem Equiv.Perm.smul_def {α : Type u_6} (f : Perm α) (a : α) :
        f a = f a

        Tautological action by MulAut #

        instance MulAut.applyMulAction {M : Type u_2} [Monoid M] :

        The tautological action by MulAut M on M.

        Equations

          The tautological action by MulAut M on M.

          This generalizes Function.End.applyMulAction.

          Equations
            @[simp]
            theorem MulAut.smul_def {M : Type u_2} [Monoid M] (f : MulAut M) (a : M) :
            f a = f a

            MulAut.applyDistribMulAction is faithful.

            Tautological action by AddAut #

            instance AddAut.applyMulAction {M : Type u_2} [AddMonoid M] :

            The tautological action by AddAut M on M.

            Equations
              @[simp]
              theorem AddAut.smul_def {M : Type u_2} [AddMonoid M] (f : AddAut M) (a : M) :
              f a = f a

              AddAut.applyDistribMulAction is faithful.

              Converting actions to and from homs to the monoid/group of endomorphisms/automorphisms #

              def MulAction.toEndHom {M : Type u_2} {α : Type u_5} [Monoid M] [MulAction M α] :

              The monoid hom representing a monoid action.

              When M is a group, see MulAction.toPermHom.

              Equations
                Instances For
                  @[reducible, inline]
                  abbrev MulAction.ofEndHom {M : Type u_2} {α : Type u_5} [Monoid M] (f : M →* Function.End α) :

                  The monoid action induced by a monoid hom to Function.End α

                  See note [reducible non-instances].

                  Equations
                    Instances For
                      def AddAction.toEndHom {M : Type u_2} {α : Type u_5} [AddMonoid M] [AddAction M α] :

                      The additive monoid hom representing an additive monoid action.

                      When M is a group, see AddAction.toPermHom.

                      Equations
                        Instances For
                          @[reducible, inline]
                          abbrev AddAction.ofEndHom {M : Type u_2} {α : Type u_5} [AddMonoid M] (f : M →+ Additive (Function.End α)) :

                          The additive action induced by a hom to Additive (Function.End α)

                          See note [reducible non-instances].

                          Equations
                            Instances For
                              def MulAction.toPermHom (G : Type u_1) (α : Type u_5) [Group G] [MulAction G α] :

                              Given an action of a group G on a set α, each g : G defines a permutation of α.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem MulAction.toPermHom_apply (G : Type u_1) (α : Type u_5) [Group G] [MulAction G α] (a : G) :
                                  (toPermHom G α) a = toPerm a
                                  def AddAction.toPermHom (G : Type u_1) (α : Type u_5) [AddGroup G] [AddAction G α] :

                                  Given an action of an additive group G on a set α, each g : G defines a permutation of α.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem AddAction.toPermHom_apply_symm_apply (G : Type u_1) (α : Type u_5) [AddGroup G] [AddAction G α] (a : G) (x : α) :
                                      @[simp]
                                      theorem AddAction.toPermHom_apply_apply (G : Type u_1) (α : Type u_5) [AddGroup G] [AddAction G α] (a : G) (x : α) :
                                      ((toPermHom G α) a) x = a +ᵥ x
                                      def MulDistribMulAction.toMulEquiv {G : Type u_1} (M : Type u_2) [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
                                          @[simp]
                                          theorem MulDistribMulAction.toMulEquiv_apply {G : Type u_1} (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) (a✝ : M) :
                                          (toMulEquiv M x) a✝ = x a✝
                                          @[simp]
                                          theorem MulDistribMulAction.toMulEquiv_symm_apply {G : Type u_1} (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) (a✝ : M) :
                                          (toMulEquiv M x).symm a✝ = x⁻¹ a✝

                                          Each element of the group defines a multiplicative monoid isomorphism.

                                          This is a stronger version of MulAction.toPermHom.

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem MulDistribMulAction.toMulAut_apply (G : Type u_1) (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) :
                                              (toMulAut G M) x = toMulEquiv M x
                                              def mulAutArrow {G : Type u_1} {M : Type u_2} {A : 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
                                                  @[simp]
                                                  theorem mulAutArrow_apply_apply {G : Type u_1} {M : Type u_2} {A : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) (a✝ : AM) (a✝¹ : A) :
                                                  (mulAutArrow x) a✝ a✝¹ = (x a✝) a✝¹
                                                  @[simp]
                                                  theorem mulAutArrow_apply_symm_apply {G : Type u_1} {M : Type u_2} {A : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) (a✝ : AM) (a✝¹ : A) :
                                                  (MulEquiv.symm (mulAutArrow x)) a✝ a✝¹ = (x⁻¹ a✝) a✝¹