Documentation

Mathlib.GroupTheory.GroupAction.Group

Group actions applied to various types of group #

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

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_apply {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a 0) (b : β) :
(Equiv.smulRight ha) b = 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
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
              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
                  @[simp]
                  theorem IsUnit.smul_eq_zero {α : Type u} {β : Type v} [Monoid α] [AddMonoid β] [DistribMulAction α β] {u : α} (hu : IsUnit u) {x : β} :
                  u x = 0 x = 0
                  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)