Documentation

Mathlib.GroupTheory.GroupAction.Group

Group actions applied to various types of group #

This file contains lemmas about SMul on GroupWithZero, and Group.

@[simp]
theorem neg_vadd_vadd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (c : α) (x : β) :
-c +ᵥ (c +ᵥ x) = x
@[simp]
theorem inv_smul_smul {α : Type u} {β : Type v} [Group α] [MulAction α β] (c : α) (x : β) :
c⁻¹ c x = x
@[simp]
theorem vadd_neg_vadd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (c : α) (x : β) :
c +ᵥ (-c +ᵥ x) = x
@[simp]
theorem smul_inv_smul {α : Type u} {β : Type v} [Group α] [MulAction α β] (c : α) (x : β) :
c c⁻¹ x = x
def AddAction.toPerm {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (a : α) :

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

Equations
  • AddAction.toPerm a = { toFun := fun (x : β) => a +ᵥ x, invFun := fun (x : β) => -a +ᵥ x, left_inv := , right_inv := }
Instances For
    @[simp]
    theorem MulAction.toPerm_apply {α : Type u} {β : Type v} [Group α] [MulAction α β] (a : α) (x : β) :
    @[simp]
    theorem MulAction.toPerm_symm_apply {α : Type u} {β : Type v} [Group α] [MulAction α β] (a : α) (x : β) :
    @[simp]
    theorem AddAction.toPerm_apply {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (a : α) (x : β) :
    @[simp]
    theorem AddAction.toPerm_symm_apply {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (a : α) (x : β) :
    def MulAction.toPerm {α : Type u} {β : Type v} [Group α] [MulAction α β] (a : α) :

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

    Equations
    Instances For
      theorem AddAction.toPerm_injective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] [FaithfulVAdd α β] :
      Function.Injective AddAction.toPerm

      AddAction.toPerm is injective on faithful actions.

      theorem MulAction.toPerm_injective {α : Type u} {β : Type v} [Group α] [MulAction α β] [FaithfulSMul α β] :
      Function.Injective MulAction.toPerm

      MulAction.toPerm is injective on faithful actions.

      @[simp]
      theorem MulAction.toPermHom_apply (α : Type u) (β : Type v) [Group α] [MulAction α β] (a : α) :
      def MulAction.toPermHom (α : Type u) (β : Type v) [Group α] [MulAction α β] :

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

      Equations
      Instances For
        @[simp]
        theorem AddAction.toPermHom_apply_apply (β : Type v) (α : Type u_1) [AddGroup α] [AddAction α β] (a : α) (x : β) :
        ((AddAction.toPermHom β α) a) x = a +ᵥ x
        @[simp]
        theorem AddAction.toPermHom_apply_symm_apply (β : Type v) (α : Type u_1) [AddGroup α] [AddAction α β] (a : α) (x : β) :
        (Equiv.symm ((AddAction.toPermHom β α) a)) x = (Multiplicative.ofAdd a)⁻¹ x
        def AddAction.toPermHom (β : Type v) (α : Type u_1) [AddGroup α] [AddAction α β] :

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

        Equations
        Instances For
          instance Equiv.Perm.applyMulAction (α : Type u_1) :

          The tautological action by Equiv.Perm α on α.

          This generalizes Function.End.applyMulAction.

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

          Equiv.Perm.applyMulAction is faithful.

          Equations
          • =
          theorem neg_vadd_eq_iff {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {a : α} {x : β} {y : β} :
          -a +ᵥ x = y x = a +ᵥ y
          theorem inv_smul_eq_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] {a : α} {x : β} {y : β} :
          a⁻¹ x = y x = a y
          theorem eq_neg_vadd_iff {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {a : α} {x : β} {y : β} :
          x = -a +ᵥ y a +ᵥ x = y
          theorem eq_inv_smul_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] {a : α} {x : β} {y : β} :
          x = a⁻¹ y a x = y
          theorem smul_inv {α : Type u} {β : Type v} [Group α] [MulAction α β] [Group β] [SMulCommClass α β β] [IsScalarTower α β β] (c : α) (x : β) :
          theorem smul_zpow {α : Type u} {β : Type v} [Group α] [MulAction α β] [Group β] [SMulCommClass α β β] [IsScalarTower α β β] (c : α) (x : β) (p : ) :
          (c x) ^ p = c ^ p x ^ p
          @[simp]
          theorem Commute.smul_right_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} (r : α) :
          Commute a (r b) Commute a b
          @[simp]
          theorem Commute.smul_left_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} (r : α) :
          Commute (r a) b Commute a b
          theorem AddAction.bijective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) :
          Function.Bijective fun (x : β) => g +ᵥ x
          theorem MulAction.bijective {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) :
          Function.Bijective fun (x : β) => g x
          theorem AddAction.injective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) :
          Function.Injective fun (x : β) => g +ᵥ x
          theorem MulAction.injective {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) :
          Function.Injective fun (x : β) => g x
          theorem AddAction.surjective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) :
          Function.Surjective fun (x : β) => g +ᵥ x
          theorem MulAction.surjective {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) :
          Function.Surjective fun (x : β) => g x
          theorem vadd_left_cancel {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} (h : g +ᵥ x = g +ᵥ y) :
          x = y
          theorem smul_left_cancel {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) {x : β} {y : β} (h : g x = g y) :
          x = y
          @[simp]
          theorem vadd_left_cancel_iff {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} :
          g +ᵥ x = g +ᵥ y x = y
          @[simp]
          theorem smul_left_cancel_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) {x : β} {y : β} :
          g x = g y x = y
          theorem vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} :
          g +ᵥ x = y x = -g +ᵥ y
          theorem smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) {x : β} {y : β} :
          g x = y x = g⁻¹ y
          @[simp]
          theorem invOf_smul_smul {α : Type u} {β : Type v} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] :
          c c x = x
          @[simp]
          theorem smul_invOf_smul {α : Type u} {β : Type v} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] :
          c c x = x
          theorem invOf_smul_eq_iff {α : Type u} {β : Type v} [Monoid α] [MulAction α β] {c : α} {x : β} {y : β} [Invertible c] :
          c x = y x = c y
          theorem smul_eq_iff_eq_invOf_smul {α : Type u} {β : Type v} [Monoid α] [MulAction α β] {c : α} {x : β} {y : β} [Invertible c] :
          c x = y x = c y

          Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.

          Equations
          • =
          @[simp]
          theorem inv_smul_smul₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {c : α} (hc : c 0) (x : β) :
          c⁻¹ c x = x
          @[simp]
          theorem smul_inv_smul₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {c : α} (hc : c 0) (x : β) :
          c c⁻¹ x = x
          theorem inv_smul_eq_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) {x : β} {y : β} :
          a⁻¹ x = y x = a y
          theorem eq_inv_smul_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) {x : β} {y : β} :
          x = a⁻¹ y a x = y
          @[simp]
          theorem Commute.smul_right_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} {c : α} (hc : c 0) :
          Commute a (c b) Commute a b
          @[simp]
          theorem Commute.smul_left_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} {c : α} (hc : c 0) :
          Commute (c a) b Commute a b
          @[simp]
          theorem Equiv.smulRight_symm_apply {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (b : β) :
          (Equiv.smulRight ha).symm b = a⁻¹ b
          @[simp]
          theorem Equiv.smulRight_apply {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (b : β) :
          (Equiv.smulRight ha) b = a b
          def Equiv.smulRight {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) :
          β β

          Right scalar multiplication as an order isomorphism.

          Equations
          Instances For
            theorem MulAction.bijective₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) :
            Function.Bijective fun (x : β) => a x
            theorem MulAction.injective₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) :
            Function.Injective fun (x : β) => a x
            theorem MulAction.surjective₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) :
            Function.Surjective fun (x : β) => a x
            @[simp]
            theorem DistribMulAction.toAddEquiv_apply {α : Type u} (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] (x : α) :
            ∀ (a : β), (DistribMulAction.toAddEquiv β x) a = x a
            @[simp]
            theorem DistribMulAction.toAddEquiv_symm_apply {α : Type u} (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] (x : α) :
            ∀ (a : β), (DistribMulAction.toAddEquiv β x).symm a = x⁻¹ a
            def DistribMulAction.toAddEquiv {α : Type u} (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] (x : α) :
            β ≃+ β

            Each element of the group defines an additive monoid isomorphism.

            This is a stronger version of MulAction.toPerm.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def DistribMulAction.toAddAut (α : Type u) (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] :
              α →* AddAut β

              Each element of the group defines an additive monoid isomorphism.

              This is a stronger version of MulAction.toPermHom.

              Equations
              Instances For
                def DistribMulAction.toAddEquiv₀ {α : Type u_1} (β : Type u_2) [GroupWithZero α] [AddMonoid β] [DistribMulAction α β] (x : α) (hx : x 0) :
                β ≃+ β

                Each non-zero element of a GroupWithZero defines an additive monoid isomorphism of an AddMonoid on which it acts distributively. This is a stronger version of DistribMulAction.toAddMonoidHom.

                Equations
                Instances For
                  theorem smul_eq_zero_iff_eq {α : Type u} {β : Type v} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} :
                  a x = 0 x = 0
                  theorem smul_ne_zero_iff_ne {α : Type u} {β : Type v} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} :
                  a x 0 x 0
                  @[simp]
                  theorem MulDistribMulAction.toMulEquiv_symm_apply {α : Type u} (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] (x : α) :
                  ∀ (a : β), (MulDistribMulAction.toMulEquiv β x).symm a = x⁻¹ a
                  @[simp]
                  theorem MulDistribMulAction.toMulEquiv_apply {α : Type u} (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] (x : α) :
                  ∀ (a : β), (MulDistribMulAction.toMulEquiv β x) a = x a
                  def MulDistribMulAction.toMulEquiv {α : Type u} (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] (x : α) :
                  β ≃* β

                  Each element of the group defines a multiplicative monoid isomorphism.

                  This is a stronger version of MulAction.toPerm.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def MulDistribMulAction.toMulAut (α : Type u) (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] :
                    α →* MulAut β

                    Each element of the group defines a multiplicative monoid isomorphism.

                    This is a stronger version of MulAction.toPermHom.

                    Equations
                    Instances For
                      theorem arrowAddAction.proof_2 {G : Type u_3} {A : Type u_1} {B : Type u_2} [SubtractionMonoid G] [AddAction G A] (x : G) (y : G) (f : AB) :
                      (fun (a : A) => f (-(x + y) +ᵥ a)) = fun (a : A) => f (-y +ᵥ (-x +ᵥ a))
                      theorem arrowAddAction.proof_1 {G : Type u_3} {A : Type u_1} {B : Type u_2} [SubtractionMonoid G] [AddAction G A] (f : AB) :
                      (fun (x : A) => f (-0 +ᵥ x)) = f
                      def arrowAddAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [SubtractionMonoid G] [AddAction G A] :
                      AddAction G (AB)

                      If G acts on A, then it acts also on A → B, by (g +ᵥ F) a = F (g⁻¹ +ᵥ a)

                      Equations
                      Instances For
                        @[simp]
                        theorem arrowAction_smul {G : Type u_1} {A : Type u_2} {B : Type u_3} [DivisionMonoid G] [MulAction G A] (g : G) (F : AB) (a : A) :
                        SMul.smul g F a = F (g⁻¹ a)
                        @[simp]
                        theorem arrowAddAction_vadd {G : Type u_1} {A : Type u_2} {B : Type u_3} [SubtractionMonoid G] [AddAction G A] (g : G) (F : AB) (a : A) :
                        VAdd.vadd g F a = F (-g +ᵥ a)
                        def arrowAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [DivisionMonoid G] [MulAction G A] :
                        MulAction G (AB)

                        If G acts on A, then it acts also on A → B, by (g • F) a = F (g⁻¹ • a).

                        Equations
                        Instances For
                          def arrowMulDistribMulAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [MulAction G A] [Monoid B] :

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

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

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

                            Equations
                            Instances For
                              theorem IsAddUnit.vadd_left_cancel {α : Type u} {β : Type v} [AddMonoid α] [AddAction α β] {a : α} (ha : IsAddUnit a) {x : β} {y : β} :
                              a +ᵥ x = a +ᵥ y x = y
                              abbrev IsAddUnit.vadd_left_cancel.match_1 {α : Type u_1} [AddMonoid α] {a : α} (motive : IsAddUnit aProp) :
                              ∀ (ha : IsAddUnit a), (∀ (u : AddUnits α) (hu : u = a), motive )motive ha
                              Equations
                              • =
                              Instances For
                                theorem IsUnit.smul_left_cancel {α : Type u} {β : Type v} [Monoid α] [MulAction α β] {a : α} (ha : IsUnit a) {x : β} {y : β} :
                                a x = a y x = y
                                @[simp]
                                theorem IsUnit.smul_eq_zero {α : Type u} {β : Type v} [Monoid α] [AddMonoid β] [DistribMulAction α β] {u : α} (hu : IsUnit u) {x : β} :
                                u x = 0 x = 0
                                @[simp]
                                theorem isUnit_smul_iff {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α) (m : β) :
                                theorem IsUnit.smul_sub_iff_sub_inv_smul {α : Type u} {β : Type v} [Group α] [Monoid β] [AddGroup β] [DistribMulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (r : α) (a : β) :
                                IsUnit (r 1 - a) IsUnit (1 - r⁻¹ a)