Documentation

Mathlib.GroupTheory.GroupAction.Defs

Definition of orbit, fixedPoints and stabilizer #

This file defines orbits, stabilizers, and other objects defined in terms of actions.

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
def MulAction.orbit (M : Type u) [Monoid M] {α : Type v} [MulAction M α] (a : α) :
Set α

The orbit of an element under an action.

Equations
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 : α) :
instance AddAction.instElemOrbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} :
Equations
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) :
def AddAction.fixedPoints (M : Type u) [AddMonoid M] (α : Type v) [AddAction M α] :
Set α

The set of elements fixed under the whole action.

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

The set of elements fixed under the whole action.

Equations
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
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
@[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 : α} :
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
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
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
@[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
@[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
@[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
@[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
@[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 α
@[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 : α) :
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 : α) :
instance AddAction.instAddAction {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H : AddSubgroup G) :
AddAction (↥H) α
Equations
instance MulAction.instMulAction {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) :
MulAction (↥H) α
Equations
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
def MulAction.orbitRel (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] :

The relation 'in the same orbit'.

Equations
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 : α} :
@[deprecated]
theorem MulAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} :

Alias of MulAction.orbitRel_apply.

@[deprecated]
theorem AddAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} :
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, inline]
abbrev 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
@[reducible, inline]
abbrev 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

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

Equations
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
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
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
@[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
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

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

Equations
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
theorem AddAction.univ_eq_iUnion_orbit (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] :
Set.univ = ⋃ (x : AddAction.orbitRel.Quotient G α), x.orbit

Decomposition of a type X as a disjoint union of its orbits under an additive group action. Phrased as a set union. See AddAction.selfEquivSigmaOrbits for the type isomorphism.

theorem MulAction.univ_eq_iUnion_orbit (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] :
Set.univ = ⋃ (x : MulAction.orbitRel.Quotient G α), x.orbit

Decomposition of a type X as a disjoint union of its orbits under a group action. Phrased as a set union. See MulAction.selfEquivSigmaOrbits for the type isomorphism.

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
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
@[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 {α : Type u_2} {β : Type u_3} {G' : Type u_4} [AddGroup G'] [VAdd α β] [AddAction G' β] [VAddCommClass G' α β] (a : α) (b : β) :
theorem MulAction.le_stabilizer_smul_right {α : Type u_2} {β : Type u_3} {G' : Type u_4} [Group G'] [SMul α β] [MulAction G' β] [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_3} [AddGroup G] [AddAction G β] {α : Type u_4} [AddGroup α] [AddAction α β] [VAddCommClass G α β] (a : α) (b : β) :
@[simp]
theorem MulAction.stabilizer_smul_eq_right {G : Type u_1} {β : Type u_3} [Group G] [MulAction G β] {α : Type u_4} [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 : α) :