Documentation

Mathlib.Algebra.Group.Action.Basic

More lemmas about group actions #

This file contains lemmas about group actions that require more imports than Mathlib.Algebra.Group.Action.Defs offers.

def AddAction.toPerm {α : Type u_1} {β : Type u_2} [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 AddAction.toPerm_symm_apply {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (a : α) (x : β) :
    @[simp]
    theorem MulAction.toPerm_symm_apply {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (a : α) (x : β) :
    @[simp]
    theorem MulAction.toPerm_apply {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (a : α) (x : β) :
    @[simp]
    theorem AddAction.toPerm_apply {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (a : α) (x : β) :
    def MulAction.toPerm {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [AddGroup α] [AddAction α β] [FaithfulVAdd α β] :
      Function.Injective AddAction.toPerm

      AddAction.toPerm is injective on faithful actions.

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

      MulAction.toPerm is injective on faithful actions.

      @[simp]
      theorem MulAction.toPermHom_apply (α : Type u_1) (β : Type u_2) [Group α] [MulAction α β] (a : α) :
      def MulAction.toPermHom (α : Type u_1) (β : Type u_2) [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_symm_apply (β : Type u_2) (α : Type u_4) [AddGroup α] [AddAction α β] (a : α) (x : β) :
        (Equiv.symm ((AddAction.toPermHom β α) a)) x = (Multiplicative.ofAdd a)⁻¹ x
        @[simp]
        theorem AddAction.toPermHom_apply_apply (β : Type u_2) (α : Type u_4) [AddGroup α] [AddAction α β] (a : α) (x : β) :
        ((AddAction.toPermHom β α) a) x = a +ᵥ x
        def AddAction.toPermHom (β : Type u_2) (α : Type u_4) [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_4) :

          The tautological action by Equiv.Perm α on α.

          This generalizes Function.End.applyMulAction.

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

          Equiv.Perm.applyMulAction is faithful.

          Equations
          • =
          theorem AddAction.bijective {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (g : α) :
          Function.Bijective fun (x : β) => g +ᵥ x
          theorem MulAction.bijective {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (g : α) :
          Function.Bijective fun (x : β) => g x
          theorem AddAction.injective {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (g : α) :
          Function.Injective fun (x : β) => g +ᵥ x
          theorem MulAction.injective {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (g : α) :
          Function.Injective fun (x : β) => g x
          theorem AddAction.surjective {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (g : α) :
          Function.Surjective fun (x : β) => g +ᵥ x
          theorem MulAction.surjective {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (g : α) :
          Function.Surjective fun (x : β) => g x
          theorem vadd_left_cancel {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} (h : g +ᵥ x = g +ᵥ y) :
          x = y
          theorem smul_left_cancel {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (g : α) {x : β} {y : β} (h : g x = g y) :
          x = y
          @[simp]
          theorem vadd_left_cancel_iff {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} :
          g +ᵥ x = g +ᵥ y x = y
          @[simp]
          theorem smul_left_cancel_iff {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (g : α) {x : β} {y : β} :
          g x = g y x = y
          theorem vadd_eq_iff_eq_neg_vadd {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} :
          g +ᵥ x = y x = -g +ᵥ y
          theorem smul_eq_iff_eq_inv_smul {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (g : α) {x : β} {y : β} :
          g x = y x = g⁻¹ y
          @[simp]
          theorem invOf_smul_smul {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] :
          c c x = x
          @[simp]
          theorem smul_invOf_smul {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] :
          c c x = x
          theorem invOf_smul_eq_iff {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] {c : α} {x : β} {y : β} [Invertible c] :
          c x = y x = c y
          theorem smul_eq_iff_eq_invOf_smul {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] {c : α} {x : β} {y : β} [Invertible c] :
          c x = y x = c y
          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
          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))
          def arrowAddAction {G : Type u_4} {A : Type u_5} {B : Type u_6} [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_4} {A : Type u_5} {B : Type u_6} [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_4} {A : Type u_5} {B : Type u_6} [SubtractionMonoid G] [AddAction G A] (g : G) (F : AB) (a : A) :
            VAdd.vadd g F a = F (-g +ᵥ a)
            def arrowAction {G : Type u_4} {A : Type u_5} {B : Type u_6} [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
              theorem IsAddUnit.vadd_left_cancel {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] {a : α} (ha : IsAddUnit a) {x : β} {y : β} :
              a +ᵥ x = a +ᵥ y x = y
              theorem IsUnit.smul_left_cancel {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] {a : α} (ha : IsUnit a) {x : β} {y : β} :
              a x = a y x = y
              @[simp]
              theorem isUnit_smul_iff {α : Type u_1} {β : Type u_2} [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α) (m : β) :