Documentation

Mathlib.GroupTheory.GroupAction.Basic

Basic properties of group actions #

This file primarily concerns itself with orbits, stabilizers, and other objects defined in terms of actions. Despite this file being called basic, low-level helper lemmas for algebraic manipulation of belong elsewhere.

Main definitions #

def AddAction.orbit (M : Type u) [AddMonoid M] {α : Type v} [AddAction M α] (a : α) :
Set α

The orbit of an element under an action.

Equations
Instances For
    def MulAction.orbit (M : Type u) [Monoid M] {α : Type v} [MulAction M α] (a : α) :
    Set α

    The orbit of an element under an action.

    Equations
    Instances For
      theorem AddAction.mem_orbit_iff {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a₁ : α} {a₂ : α} :
      a₂ AddAction.orbit M a₁ ∃ (x : M), x +ᵥ a₁ = a₂
      theorem MulAction.mem_orbit_iff {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a₁ : α} {a₂ : α} :
      a₂ MulAction.orbit M a₁ ∃ (x : M), x a₁ = a₂
      @[simp]
      theorem AddAction.mem_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (a : α) (m : M) :
      @[simp]
      theorem MulAction.mem_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (a : α) (m : M) :
      @[simp]
      theorem AddAction.mem_orbit_self {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (a : α) :
      @[simp]
      theorem MulAction.mem_orbit_self {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (a : α) :
      theorem AddAction.orbit_nonempty {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (a : α) :
      (AddAction.orbit M a).Nonempty
      theorem MulAction.orbit_nonempty {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (a : α) :
      (MulAction.orbit M a).Nonempty
      theorem AddAction.mapsTo_vadd_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (m : M) (a : α) :
      Set.MapsTo (fun (x : α) => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a)
      theorem MulAction.mapsTo_smul_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (m : M) (a : α) :
      Set.MapsTo (fun (x : α) => m x) (MulAction.orbit M a) (MulAction.orbit M a)
      theorem AddAction.vadd_orbit_subset {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (m : M) (a : α) :
      theorem MulAction.smul_orbit_subset {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (m : M) (a : α) :
      theorem AddAction.orbit_vadd_subset {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (m : M) (a : α) :
      theorem MulAction.orbit_smul_subset {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (m : M) (a : α) :
      theorem AddAction.instElemOrbit.proof_1 {M : Type u_2} [AddMonoid M] {α : Type u_1} [AddAction M α] {a : α} (m : (AddAction.orbit M a)) :
      0 +ᵥ m = m
      instance AddAction.instElemOrbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} :
      Equations
      theorem AddAction.instElemOrbit.proof_2 {M : Type u_2} [AddMonoid M] {α : Type u_1} [AddAction M α] {a : α} (m : M) (m' : M) (a' : (AddAction.orbit M a)) :
      m + m' +ᵥ a' = m +ᵥ (m' +ᵥ a')
      instance MulAction.instElemOrbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} :
      Equations
      @[simp]
      theorem AddAction.orbit.coe_vadd {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} {m : M} {a' : (AddAction.orbit M a)} :
      (m +ᵥ a') = m +ᵥ a'
      @[simp]
      theorem MulAction.orbit.coe_smul {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} {m : M} {a' : (MulAction.orbit M a)} :
      (m a') = m a'
      theorem AddAction.orbit_addSubmonoid_subset {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (S : AddSubmonoid M) (a : α) :
      theorem MulAction.orbit_submonoid_subset {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (S : Submonoid M) (a : α) :
      theorem AddAction.mem_orbit_of_mem_orbit_addSubmonoid {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {S : AddSubmonoid M} {a : α} {b : α} (h : a AddAction.orbit (S) b) :
      theorem MulAction.mem_orbit_of_mem_orbit_submonoid {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {S : Submonoid M} {a : α} {b : α} (h : a MulAction.orbit (S) b) :
      theorem AddAction.fst_mem_orbit_of_mem_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {β : Type u_1} [AddAction M β] {x : α × β} {y : α × β} (h : x AddAction.orbit M y) :
      theorem MulAction.fst_mem_orbit_of_mem_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {β : Type u_1} [MulAction M β] {x : α × β} {y : α × β} (h : x MulAction.orbit M y) :
      theorem AddAction.snd_mem_orbit_of_mem_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {β : Type u_1} [AddAction M β] {x : α × β} {y : α × β} (h : x AddAction.orbit M y) :
      theorem MulAction.snd_mem_orbit_of_mem_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {β : Type u_1} [MulAction M β] {x : α × β} {y : α × β} (h : x MulAction.orbit M y) :
      theorem AddAction.orbit_eq_univ (M : Type u) [AddMonoid M] {α : Type v} [AddAction M α] [AddAction.IsPretransitive M α] (a : α) :
      AddAction.orbit M a = Set.univ
      theorem MulAction.orbit_eq_univ (M : Type u) [Monoid M] {α : Type v} [MulAction M α] [MulAction.IsPretransitive M α] (a : α) :
      MulAction.orbit M a = Set.univ
      def AddAction.fixedPoints (M : Type u) [AddMonoid M] (α : Type v) [AddAction M α] :
      Set α

      The set of elements fixed under the whole action.

      Equations
      Instances For
        def MulAction.fixedPoints (M : Type u) [Monoid M] (α : Type v) [MulAction M α] :
        Set α

        The set of elements fixed under the whole action.

        Equations
        Instances For
          def AddAction.fixedBy {M : Type u} [AddMonoid M] (α : Type v) [AddAction M α] (m : M) :
          Set α

          fixedBy m is the set of elements fixed by m.

          Equations
          Instances For
            def MulAction.fixedBy {M : Type u} [Monoid M] (α : Type v) [MulAction M α] (m : M) :
            Set α

            fixedBy m is the set of elements fixed by m.

            Equations
            Instances For
              @[simp]
              theorem AddAction.mem_fixedPoints {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} :
              a AddAction.fixedPoints M α ∀ (m : M), m +ᵥ a = a
              @[simp]
              theorem MulAction.mem_fixedPoints {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} :
              a MulAction.fixedPoints M α ∀ (m : M), m a = a
              @[simp]
              theorem AddAction.mem_fixedBy {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {m : M} {a : α} :
              @[simp]
              theorem MulAction.mem_fixedBy {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {m : M} {a : α} :
              abbrev AddAction.mem_fixedPoints'.match_1 {M : Type u_1} [AddMonoid M] {α : Type u_2} [AddAction M α] {a : α} :
              ∀ (x : α) (motive : (∃ (x_1 : M), x_1 +ᵥ a = x)Prop) (x_1 : ∃ (x_1 : M), x_1 +ᵥ a = x), (∀ (m : M) (hm : m +ᵥ a = x), motive )motive x_1
              Equations
              • =
              Instances For
                theorem AddAction.mem_fixedPoints' {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} :
                a AddAction.fixedPoints M α a'AddAction.orbit M a, a' = a
                theorem MulAction.mem_fixedPoints' {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} :
                a MulAction.fixedPoints M α a'MulAction.orbit M a, a' = a
                abbrev AddAction.mem_fixedPoints_iff_card_orbit_eq_one.match_1 {M : Type u_2} [AddMonoid M] {α : Type u_1} [AddAction M α] {a : α} (motive : (AddAction.orbit M a)Prop) :
                ∀ (x : (AddAction.orbit M a)), (∀ (a_1 : α) (x : M) (hx : (fun (m : M) => m +ᵥ a) x = a_1), motive a_1, )motive x
                Equations
                • =
                Instances For
                  def AddAction.stabilizerAddSubmonoid (M : Type u) [AddMonoid M] {α : Type v} [AddAction M α] (a : α) :

                  The stabilizer of a point a as an additive submonoid of M.

                  Equations
                  Instances For
                    theorem AddAction.stabilizerAddSubmonoid.proof_1 (M : Type u_2) [AddMonoid M] {α : Type u_1} [AddAction M α] (a : α) {m : M} {m' : M} (ha : m +ᵥ a = a) (hb : m' +ᵥ a = a) :
                    m + m' +ᵥ a = a
                    def MulAction.stabilizerSubmonoid (M : Type u) [Monoid M] {α : Type v} [MulAction M α] (a : α) :

                    The stabilizer of a point a as a submonoid of M.

                    Equations
                    Instances For
                      @[simp]
                      theorem AddAction.mem_stabilizerAddSubmonoid_iff {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} {m : M} :
                      @[simp]
                      theorem MulAction.mem_stabilizerSubmonoid_iff {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} {m : M} :
                      def FixedPoints.submonoid (M : Type u) (α : Type v) [Monoid M] [Monoid α] [MulDistribMulAction M α] :

                      The submonoid of elements fixed under the whole action.

                      Equations
                      Instances For
                        @[simp]
                        theorem FixedPoints.mem_submonoid (M : Type u) (α : Type v) [Monoid M] [Monoid α] [MulDistribMulAction M α] (a : α) :
                        a FixedPoints.submonoid M α ∀ (m : M), m a = a
                        def FixedPoints.subgroup (M : Type u) (α : Type v) [Monoid M] [Group α] [MulDistribMulAction M α] :

                        The subgroup of elements fixed under the whole action.

                        Equations
                        Instances For

                          The notation for FixedPoints.subgroup, chosen to resemble αᴹ.

                          Equations
                          Instances For
                            @[simp]
                            theorem FixedPoints.mem_subgroup (M : Type u) (α : Type v) [Monoid M] [Group α] [MulDistribMulAction M α] (a : α) :
                            a FixedPoints.subgroup M α ∀ (m : M), m a = a
                            @[simp]

                            The additive submonoid of elements fixed under the whole action.

                            Equations
                            Instances For
                              @[simp]
                              theorem FixedPoints.mem_addSubmonoid (M : Type u) (α : Type v) [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : α) :
                              a FixedPoints.addSubmonoid M α ∀ (m : M), m a = a

                              The additive subgroup of elements fixed under the whole action.

                              Equations
                              Instances For

                                The notation for FixedPoints.addSubgroup, chosen to resemble αᴹ.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem FixedPoints.mem_addSubgroup (M : Type u) (α : Type v) [Monoid M] [AddGroup α] [DistribMulAction M α] (a : α) :
                                  a α^+M ∀ (m : M), m a = a
                                  @[simp]
                                  theorem FixedPoints.addSubgroup_toAddSubmonoid (M : Type u) (α : Type v) [Monoid M] [AddGroup α] [DistribMulAction M α] :
                                  (α^+M).toAddSubmonoid = FixedPoints.addSubmonoid M α
                                  theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [Monoid M] [NonUnitalNonAssocRing R] [DistribMulAction M R] (k : M) (h : ∀ (x : R), k x = 0x = 0) {a : R} {b : R} (h' : k a = k b) :
                                  a = b

                                  smul by a k : M over a ring is injective, if k is not a zero divisor. The general theory of such k is elaborated by IsSMulRegular. The typeclass that restricts all terms of M to have this property is NoZeroSMulDivisors.

                                  @[simp]
                                  theorem AddAction.vadd_orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) :
                                  @[simp]
                                  theorem MulAction.smul_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) :
                                  @[simp]
                                  theorem AddAction.orbit_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) :
                                  @[simp]
                                  theorem MulAction.orbit_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) :

                                  The action of an additive group on an orbit is transitive.

                                  Equations
                                  • =
                                  instance MulAction.instIsPretransitiveElemOrbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (a : α) :

                                  The action of a group on an orbit is transitive.

                                  Equations
                                  • =
                                  abbrev AddAction.orbit_eq_iff.match_1 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] {a : α} {b : α} (motive : a AddAction.orbit G bProp) :
                                  ∀ (x : a AddAction.orbit G b), (∀ (w : G) (hc : (fun (m : G) => m +ᵥ b) w = a), motive )motive x
                                  Equations
                                  • =
                                  Instances For
                                    theorem AddAction.orbit_eq_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} :
                                    theorem MulAction.orbit_eq_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} :
                                    theorem AddAction.mem_orbit_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) :
                                    theorem MulAction.mem_orbit_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) :
                                    theorem AddAction.vadd_mem_orbit_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (h : G) (a : α) :
                                    theorem MulAction.smul_mem_orbit_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (h : G) (a : α) :
                                    theorem AddAction.orbit_addSubgroup_subset {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H : AddSubgroup G) (a : α) :
                                    theorem MulAction.orbit_subgroup_subset {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) (a : α) :
                                    theorem AddAction.mem_orbit_of_mem_orbit_addSubgroup {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {a : α} {b : α} (h : a AddAction.orbit (H) b) :
                                    theorem MulAction.mem_orbit_of_mem_orbit_subgroup {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {a : α} {b : α} (h : a MulAction.orbit (H) b) :
                                    theorem AddAction.mem_orbit_symm {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a₁ : α} {a₂ : α} :
                                    a₁ AddAction.orbit G a₂ a₂ AddAction.orbit G a₁
                                    theorem MulAction.mem_orbit_symm {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a₁ : α} {a₂ : α} :
                                    a₁ MulAction.orbit G a₂ a₂ MulAction.orbit G a₁
                                    theorem AddAction.mem_addSubgroup_orbit_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : α} {a : (AddAction.orbit G x)} {b : (AddAction.orbit G x)} :
                                    a AddAction.orbit (H) b a AddAction.orbit H b
                                    theorem MulAction.mem_subgroup_orbit_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : α} {a : (MulAction.orbit G x)} {b : (MulAction.orbit G x)} :
                                    a MulAction.orbit (H) b a MulAction.orbit H b
                                    def AddAction.orbitRel (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] :

                                    The relation 'in the same orbit'.

                                    Equations
                                    Instances For
                                      theorem AddAction.orbitRel.proof_1 (G : Type u_2) (α : Type u_1) [AddGroup G] [AddAction G α] :
                                      Equivalence fun (a b : α) => a AddAction.orbit G b
                                      def MulAction.orbitRel (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] :

                                      The relation 'in the same orbit'.

                                      Equations
                                      Instances For
                                        theorem AddAction.orbitRel_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} :
                                        theorem MulAction.orbitRel_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} :
                                        theorem AddAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} :
                                        theorem MulAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} :
                                        theorem MulAction.orbitRel_subgroup_le {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) :
                                        theorem AddAction.quotient_preimage_image_eq_union_add {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (U : Set α) :
                                        Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun (x : α) => g +ᵥ x) '' U

                                        When you take a set U in α, push it down to the quotient, and pull back, you get the union of the orbit of U under G.

                                        theorem MulAction.quotient_preimage_image_eq_union_mul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (U : Set α) :
                                        Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun (x : α) => g x) '' U

                                        When you take a set U in α, push it down to the quotient, and pull back, you get the union of the orbit of U under G.

                                        theorem AddAction.disjoint_image_image_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {U : Set α} {V : Set α} :
                                        Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) xU, ∀ (g : G), g +ᵥ xV
                                        theorem MulAction.disjoint_image_image_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {U : Set α} {V : Set α} :
                                        Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) xU, ∀ (g : G), g xV
                                        theorem AddAction.image_inter_image_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (U : Set α) (V : Set α) :
                                        Quotient.mk' '' U Quotient.mk' '' V = xU, ∀ (g : G), g +ᵥ xV
                                        theorem MulAction.image_inter_image_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (U : Set α) (V : Set α) :
                                        Quotient.mk' '' U Quotient.mk' '' V = xU, ∀ (g : G), g xV
                                        @[reducible]
                                        def AddAction.orbitRel.Quotient (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] :
                                        Type u_2

                                        The quotient by AddAction.orbitRel, given a name to enable dot notation.

                                        Equations
                                        Instances For
                                          @[reducible]
                                          def MulAction.orbitRel.Quotient (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] :
                                          Type u_2

                                          The quotient by MulAction.orbitRel, given a name to enable dot notation.

                                          Equations
                                          Instances For

                                            An additive action is pretransitive if and only if the quotient by AddAction.orbitRel is a subsingleton.

                                            An action is pretransitive if and only if the quotient by MulAction.orbitRel is a subsingleton.

                                            If α is non-empty, an additive action is pretransitive if and only if the quotient has exactly one element.

                                            If α is non-empty, an action is pretransitive if and only if the quotient has exactly one element.

                                            The orbit corresponding to an element of the quotient by AddAction.orbitRel

                                            Equations
                                            Instances For
                                              theorem AddAction.orbitRel.Quotient.orbit.proof_1 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] :
                                              ∀ (x x_1 : α), x AddAction.orbit G x_1AddAction.orbit G x = AddAction.orbit G x_1
                                              def MulAction.orbitRel.Quotient.orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) :
                                              Set α

                                              The orbit corresponding to an element of the quotient by MulAction.orbitRel

                                              Equations
                                              Instances For
                                                theorem AddAction.orbitRel.Quotient.mem_orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {x : AddAction.orbitRel.Quotient G α} :
                                                a x.orbit Quotient.mk'' a = x
                                                theorem MulAction.orbitRel.Quotient.mem_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {x : MulAction.orbitRel.Quotient G α} :
                                                a x.orbit Quotient.mk'' a = x
                                                theorem AddAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) {φ : AddAction.orbitRel.Quotient G αα} (hφ : Function.RightInverse φ Quotient.mk') :
                                                x.orbit = AddAction.orbit G (φ x)

                                                Note that hφ = Quotient.out_eq' is a useful choice here.

                                                theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) {φ : MulAction.orbitRel.Quotient G αα} (hφ : Function.RightInverse φ Quotient.mk') :
                                                x.orbit = MulAction.orbit G (φ x)

                                                Note that hφ = Quotient.out_eq' is a useful choice here.

                                                theorem AddAction.orbitRel.Quotient.orbit_injective {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] :
                                                Function.Injective AddAction.orbitRel.Quotient.orbit
                                                theorem MulAction.orbitRel.Quotient.orbit_injective {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] :
                                                Function.Injective MulAction.orbitRel.Quotient.orbit
                                                @[simp]
                                                theorem AddAction.orbitRel.Quotient.orbit_inj {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {x : AddAction.orbitRel.Quotient G α} {y : AddAction.orbitRel.Quotient G α} :
                                                x.orbit = y.orbit x = y
                                                @[simp]
                                                theorem MulAction.orbitRel.Quotient.orbit_inj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {x : MulAction.orbitRel.Quotient G α} {y : MulAction.orbitRel.Quotient G α} :
                                                x.orbit = y.orbit x = y
                                                theorem AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {a : α} {b : α} (h : a = b) :
                                                a = b
                                                theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {a : α} {b : α} (h : a = b) :
                                                a = b
                                                theorem AddAction.orbitRel.Quotient.orbit_nonempty {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) :
                                                x.orbit.Nonempty
                                                theorem MulAction.orbitRel.Quotient.orbit_nonempty {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) :
                                                x.orbit.Nonempty
                                                theorem AddAction.orbitRel.Quotient.mapsTo_vadd_orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (x : AddAction.orbitRel.Quotient G α) :
                                                Set.MapsTo (fun (x : α) => g +ᵥ x) x.orbit x.orbit
                                                theorem MulAction.orbitRel.Quotient.mapsTo_smul_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (x : MulAction.orbitRel.Quotient G α) :
                                                Set.MapsTo (fun (x : α) => g x) x.orbit x.orbit
                                                instance AddAction.instElemOrbit_1 {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) :
                                                AddAction G x.orbit
                                                Equations
                                                theorem AddAction.instElemOrbit_1.proof_1 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) (a : x.orbit) :
                                                0 +ᵥ a = a
                                                theorem AddAction.instElemOrbit_1.proof_2 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) (g : G) (g' : G) (a' : x.orbit) :
                                                g + g' +ᵥ a' = g +ᵥ (g' +ᵥ a')
                                                instance MulAction.instElemOrbit_1 {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) :
                                                MulAction G x.orbit
                                                Equations
                                                @[simp]
                                                theorem AddAction.orbitRel.Quotient.orbit.coe_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {x : AddAction.orbitRel.Quotient G α} {a : x.orbit} :
                                                (g +ᵥ a) = g +ᵥ a
                                                @[simp]
                                                theorem MulAction.orbitRel.Quotient.orbit.coe_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {x : MulAction.orbitRel.Quotient G α} {a : x.orbit} :
                                                (g a) = g a
                                                Equations
                                                • =
                                                Equations
                                                • =
                                                @[simp]
                                                theorem AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : AddAction.orbitRel.Quotient G α} {a : x.orbit} {b : x.orbit} :
                                                a AddAction.orbit H b a AddAction.orbit (H) b
                                                @[simp]
                                                theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : MulAction.orbitRel.Quotient G α} {a : x.orbit} {b : x.orbit} :
                                                a MulAction.orbit H b a MulAction.orbit (H) b
                                                theorem AddAction.orbitRel.Quotient.addSubgroup_quotient_eq_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : AddAction.orbitRel.Quotient G α} {a : x.orbit} {b : x.orbit} :
                                                a = b a = b
                                                theorem MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : MulAction.orbitRel.Quotient G α} {a : x.orbit} {b : x.orbit} :
                                                a = b a = b
                                                theorem AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff' {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : AddAction.orbitRel.Quotient G α} {a : x.orbit} {b : x.orbit} {c : α} (h : a = b) :
                                                a AddAction.orbit (H) c b AddAction.orbit (H) c
                                                theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff' {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : MulAction.orbitRel.Quotient G α} {a : x.orbit} {b : x.orbit} {c : α} (h : a = b) :
                                                a MulAction.orbit (H) c b MulAction.orbit (H) c
                                                def AddAction.selfEquivSigmaOrbits' (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] :
                                                α (ω : AddAction.orbitRel.Quotient G α) × ω.orbit

                                                Decomposition of a type X as a disjoint union of its orbits under an additive group action.

                                                This version is expressed in terms of AddAction.orbitRel.Quotient.orbit instead of AddAction.orbit, to avoid mentioning Quotient.out'.

                                                Equations
                                                Instances For
                                                  theorem AddAction.selfEquivSigmaOrbits'.proof_1 (G : Type u_2) (α : Type u_1) [AddGroup G] [AddAction G α] :
                                                  ∀ (x : AddAction.orbitRel.Quotient G α) (x_1 : α), Quotient.mk'' x_1 = x x_1 x.orbit
                                                  def MulAction.selfEquivSigmaOrbits' (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] :
                                                  α (ω : MulAction.orbitRel.Quotient G α) × ω.orbit

                                                  Decomposition of a type X as a disjoint union of its orbits under a group action.

                                                  This version is expressed in terms of MulAction.orbitRel.Quotient.orbit instead of MulAction.orbit, to avoid mentioning Quotient.out'.

                                                  Equations
                                                  Instances For

                                                    Decomposition of a type X as a disjoint union of its orbits under an additive group action.

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

                                                      Decomposition of a type X as a disjoint union of its orbits under a group action.

                                                      Equations
                                                      Instances For
                                                        theorem AddAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] :
                                                        theorem MulAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] :
                                                        theorem AddAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] :
                                                        theorem MulAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] :
                                                        def AddAction.stabilizer (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] (a : α) :

                                                        The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.

                                                        Equations
                                                        Instances For
                                                          theorem AddAction.stabilizer.proof_1 (G : Type u_2) {α : Type u_1} [AddGroup G] [AddAction G α] (a : α) {m : G} (ha : m +ᵥ a = a) :
                                                          -m +ᵥ a = a
                                                          def MulAction.stabilizer (G : Type u_1) {α : Type u_2} [Group G] [MulAction G α] (a : α) :

                                                          The stabilizer of an element under an action, i.e. what sends the element to itself. A subgroup.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem AddAction.mem_stabilizer_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {g : G} :
                                                            @[simp]
                                                            theorem MulAction.mem_stabilizer_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} :
                                                            theorem AddAction.le_stabilizer_vadd_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G α] [AddAction G β] [VAdd α β] [VAddAssocClass G α β] (a : α) (b : β) :
                                                            theorem MulAction.le_stabilizer_smul_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] [MulAction G β] [SMul α β] [IsScalarTower G α β] (a : α) (b : β) :
                                                            theorem AddAction.le_stabilizer_vadd_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G β] [VAdd α β] [VAddCommClass G α β] (a : α) (b : β) :
                                                            theorem MulAction.le_stabilizer_smul_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G β] [SMul α β] [SMulCommClass G α β] (a : α) (b : β) :
                                                            @[simp]
                                                            theorem AddAction.stabilizer_vadd_eq_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G α] [AddAction G β] [VAdd α β] [VAddAssocClass G α β] (a : α) (b : β) (h : Function.Injective fun (x : α) => x +ᵥ b) :
                                                            @[simp]
                                                            theorem MulAction.stabilizer_smul_eq_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] [MulAction G β] [SMul α β] [IsScalarTower G α β] (a : α) (b : β) (h : Function.Injective fun (x : α) => x b) :
                                                            @[simp]
                                                            theorem AddAction.stabilizer_vadd_eq_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G β] [AddGroup α] [AddAction α β] [VAddCommClass G α β] (a : α) (b : β) :
                                                            @[simp]
                                                            theorem MulAction.stabilizer_smul_eq_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G β] [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) :
                                                            @[simp]
                                                            theorem AddAction.stabilizer_add_eq_left {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [AddGroup α] [VAddAssocClass G α α] (a : α) (b : α) :
                                                            @[simp]
                                                            theorem MulAction.stabilizer_mul_eq_left {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [Group α] [IsScalarTower G α α] (a : α) (b : α) :
                                                            @[simp]
                                                            theorem AddAction.stabilizer_add_eq_right {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [AddGroup α] [VAddCommClass G α α] (a : α) (b : α) :
                                                            @[simp]
                                                            theorem MulAction.stabilizer_mul_eq_right {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [Group α] [SMulCommClass G α α] (a : α) (b : α) :
                                                            theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) :

                                                            If the stabilizer of a is S, then the stabilizer of g • a is gSg⁻¹.

                                                            noncomputable def MulAction.stabilizerEquivStabilizerOfOrbitRel {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} (h : (MulAction.orbitRel G α).Rel a b) :

                                                            A bijection between the stabilizers of two elements in the same orbit.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For

                                                              If the stabilizer of x is S, then the stabilizer of g +ᵥ x is g + S + (-g).

                                                              noncomputable def AddAction.stabilizerEquivStabilizerOfOrbitRel {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} (h : (AddAction.orbitRel G α).Rel a b) :

                                                              A bijection between the stabilizers of two elements in the same orbit.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                theorem Equiv.swap_mem_stabilizer {α : Type u_1} [DecidableEq α] {S : Set α} {a : α} {b : α} :
                                                                theorem MulAction.le_stabilizer_iff_smul_le {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (H : Subgroup G) :
                                                                H MulAction.stabilizer G s gH, g s s

                                                                To prove inclusion of a subgroup in a stabilizer, it is enough to prove inclusions.

                                                                theorem MulAction.mem_stabilizer_of_finite_iff_smul_le {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (hs : s.Finite) (g : G) :

                                                                To prove membership to stabilizer of a finite set, it is enough to prove one inclusion.

                                                                theorem MulAction.mem_stabilizer_of_finite_iff_le_smul {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (hs : s.Finite) (g : G) :

                                                                To prove membership to stabilizer of a finite set, it is enough to prove one inclusion.