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 #

• MulAction.orbit
• MulAction.fixedPoints
• MulAction.fixedBy
• MulAction.stabilizer
def AddAction.orbit (M : Type u) [] {α : Type v} [] (a : α) :
Set α

The orbit of an element under an action.

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

The orbit of an element under an action.

Equations
Instances For
theorem AddAction.mem_orbit_iff {M : Type u} [] {α : Type v} [] {a₁ : α} {a₂ : α} :
a₂ ∃ (x : M), x +ᵥ a₁ = a₂
theorem MulAction.mem_orbit_iff {M : Type u} [] {α : Type v} [] {a₁ : α} {a₂ : α} :
a₂ ∃ (x : M), x a₁ = a₂
@[simp]
theorem AddAction.mem_orbit {M : Type u} [] {α : Type v} [] (a : α) (m : M) :
m +ᵥ a
@[simp]
theorem MulAction.mem_orbit {M : Type u} [] {α : Type v} [] (a : α) (m : M) :
m a
@[simp]
theorem AddAction.mem_orbit_self {M : Type u} [] {α : Type v} [] (a : α) :
a
@[simp]
theorem MulAction.mem_orbit_self {M : Type u} [] {α : Type v} [] (a : α) :
a
theorem AddAction.orbit_nonempty {M : Type u} [] {α : Type v} [] (a : α) :
theorem MulAction.orbit_nonempty {M : Type u} [] {α : Type v} [] (a : α) :
(MulAction.orbit M a).Nonempty
theorem AddAction.mapsTo_vadd_orbit {M : Type u} [] {α : Type v} [] (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} [] {α : Type v} [] (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} [] {α : Type v} [] (m : M) (a : α) :
theorem MulAction.smul_orbit_subset {M : Type u} [] {α : Type v} [] (m : M) (a : α) :
m
theorem AddAction.orbit_vadd_subset {M : Type u} [] {α : Type v} [] (m : M) (a : α) :
theorem MulAction.orbit_smul_subset {M : Type u} [] {α : Type v} [] (m : M) (a : α) :
theorem AddAction.instElemOrbit.proof_2 {M : Type u_2} [] {α : Type u_1} [] {a : α} (m : M) (m' : M) (a' : (AddAction.orbit M a)) :
m + m' +ᵥ a' = m +ᵥ (m' +ᵥ a')
theorem AddAction.instElemOrbit.proof_1 {M : Type u_2} [] {α : Type u_1} [] {a : α} (m : (AddAction.orbit M a)) :
0 +ᵥ m = m
instance AddAction.instElemOrbit {M : Type u} [] {α : Type v} [] {a : α} :
Equations
instance MulAction.instElemOrbit {M : Type u} [] {α : Type v} [] {a : α} :
Equations
• MulAction.instElemOrbit =
@[simp]
theorem AddAction.orbit.coe_vadd {M : Type u} [] {α : Type v} [] {a : α} {m : M} {a' : (AddAction.orbit M a)} :
(m +ᵥ a') = m +ᵥ a'
@[simp]
theorem MulAction.orbit.coe_smul {M : Type u} [] {α : Type v} [] {a : α} {m : M} {a' : (MulAction.orbit M a)} :
(m a') = m a'
theorem AddAction.orbit_addSubmonoid_subset {M : Type u} [] {α : Type v} [] (S : ) (a : α) :
AddAction.orbit { x : M // x S } a
theorem MulAction.orbit_submonoid_subset {M : Type u} [] {α : Type v} [] (S : ) (a : α) :
MulAction.orbit { x : M // x S } a
theorem AddAction.mem_orbit_of_mem_orbit_addSubmonoid {M : Type u} [] {α : Type v} [] {S : } {a : α} {b : α} (h : a AddAction.orbit { x : M // x S } b) :
a
theorem MulAction.mem_orbit_of_mem_orbit_submonoid {M : Type u} [] {α : Type v} [] {S : } {a : α} {b : α} (h : a MulAction.orbit { x : M // x S } b) :
a
theorem AddAction.fst_mem_orbit_of_mem_orbit {M : Type u} [] {α : Type v} [] {β : Type u_1} [] {x : α × β} {y : α × β} (h : x ) :
theorem MulAction.fst_mem_orbit_of_mem_orbit {M : Type u} [] {α : Type v} [] {β : Type u_1} [] {x : α × β} {y : α × β} (h : x ) :
theorem AddAction.snd_mem_orbit_of_mem_orbit {M : Type u} [] {α : Type v} [] {β : Type u_1} [] {x : α × β} {y : α × β} (h : x ) :
theorem MulAction.snd_mem_orbit_of_mem_orbit {M : Type u} [] {α : Type v} [] {β : Type u_1} [] {x : α × β} {y : α × β} (h : x ) :
theorem AddAction.orbit_eq_univ (M : Type u) [] {α : Type v} [] (a : α) :
= Set.univ
theorem MulAction.orbit_eq_univ (M : Type u) [] {α : Type v} [] (a : α) :
= Set.univ
def AddAction.fixedPoints (M : Type u) [] (α : Type v) [] :
Set α

The set of elements fixed under the whole action.

Equations
• = {a : α | ∀ (m : M), m +ᵥ a = a}
Instances For
def MulAction.fixedPoints (M : Type u) [] (α : Type v) [] :
Set α

The set of elements fixed under the whole action.

Equations
• = {a : α | ∀ (m : M), m a = a}
Instances For
def AddAction.fixedBy {M : Type u} [] (α : Type v) [] (m : M) :
Set α

fixedBy m is the set of elements fixed by m.

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

fixedBy m is the set of elements fixed by m.

Equations
• = {x : α | m x = x}
Instances For
theorem AddAction.fixed_eq_iInter_fixedBy (M : Type u) [] (α : Type v) [] :
= ⋂ (m : M),
theorem MulAction.fixed_eq_iInter_fixedBy (M : Type u) [] (α : Type v) [] :
= ⋂ (m : M),
@[simp]
theorem AddAction.mem_fixedPoints {M : Type u} [] {α : Type v} [] {a : α} :
∀ (m : M), m +ᵥ a = a
@[simp]
theorem MulAction.mem_fixedPoints {M : Type u} [] {α : Type v} [] {a : α} :
∀ (m : M), m a = a
@[simp]
theorem AddAction.mem_fixedBy {M : Type u} [] {α : Type v} [] {m : M} {a : α} :
a m +ᵥ a = a
@[simp]
theorem MulAction.mem_fixedBy {M : Type u} [] {α : Type v} [] {m : M} {a : α} :
a m a = a
theorem AddAction.mem_fixedPoints' {M : Type u} [] {α : Type v} [] {a : α} :
a', a' = a
theorem MulAction.mem_fixedPoints' {M : Type u} [] {α : Type v} [] {a : α} :
a', a' = a
def AddAction.stabilizerAddSubmonoid (M : Type u) [] {α : Type v} [] (a : α) :

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

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

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

Equations
• = { carrier := {m : M | m a = a}, mul_mem' := , one_mem' := }
Instances For
Equations
instance MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq {M : Type u} [] {α : Type v} [] [] (a : α) :
DecidablePred fun (x : M) =>
Equations
@[simp]
theorem AddAction.mem_stabilizerAddSubmonoid_iff {M : Type u} [] {α : Type v} [] {a : α} {m : M} :
m +ᵥ a = a
@[simp]
theorem MulAction.mem_stabilizerSubmonoid_iff {M : Type u} [] {α : Type v} [] {a : α} {m : M} :
m a = a
def FixedPoints.submonoid (M : Type u) (α : Type v) [] [] [] :

The submonoid of elements fixed under the whole action.

Equations
• = { carrier := , mul_mem' := , one_mem' := }
Instances For
@[simp]
theorem FixedPoints.mem_submonoid (M : Type u) (α : Type v) [] [] [] (a : α) :
∀ (m : M), m a = a
def FixedPoints.subgroup (M : Type u) (α : Type v) [] [] [] :

The subgroup of elements fixed under the whole action.

Equations
• = { toSubmonoid := , inv_mem' := }
Instances For

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

Equations
Instances For
@[simp]
theorem FixedPoints.mem_subgroup (M : Type u) (α : Type v) [] [] [] (a : α) :
∀ (m : M), m a = a
@[simp]
theorem FixedPoints.subgroup_toSubmonoid (M : Type u) (α : Type v) [] [] [] :
.toSubmonoid =
def FixedPoints.addSubmonoid (M : Type u) (α : Type v) [] [] [] :

The additive submonoid of elements fixed under the whole action.

Equations
• = { carrier := , add_mem' := , zero_mem' := }
Instances For
@[simp]
theorem FixedPoints.mem_addSubmonoid (M : Type u) (α : Type v) [] [] [] (a : α) :
∀ (m : M), m a = a
def FixedPoints.addSubgroup (M : Type u) (α : Type v) [] [] [] :

The additive subgroup of elements fixed under the whole action.

Equations
• α^+M = { toAddSubmonoid := , neg_mem' := }
Instances For

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

Equations
Instances For
@[simp]
theorem FixedPoints.mem_addSubgroup (M : Type u) (α : Type v) [] [] [] (a : α) :
a α^+M ∀ (m : M), m a = a
@[simp]
theorem FixedPoints.addSubgroup_toAddSubmonoid (M : Type u) (α : Type v) [] [] [] :
theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [] [] (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} [] [] (g : G) (a : α) :
g +ᵥ =
@[simp]
theorem MulAction.smul_orbit {G : Type u_1} {α : Type u_2} [] [] (g : G) (a : α) :
g =
@[simp]
theorem AddAction.orbit_vadd {G : Type u_1} {α : Type u_2} [] [] (g : G) (a : α) :
@[simp]
theorem MulAction.orbit_smul {G : Type u_1} {α : Type u_2} [] [] (g : G) (a : α) :
instance AddAction.instIsPretransitiveElemOrbit {G : Type u_1} {α : Type u_2} [] [] (a : α) :

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

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

The action of a group on an orbit is transitive.

Equations
• =
theorem AddAction.orbit_eq_iff {G : Type u_1} {α : Type u_2} [] [] {a : α} {b : α} :
= a
theorem MulAction.orbit_eq_iff {G : Type u_1} {α : Type u_2} [] [] {a : α} {b : α} :
= a
theorem AddAction.mem_orbit_vadd {G : Type u_1} {α : Type u_2} [] [] (g : G) (a : α) :
theorem MulAction.mem_orbit_smul {G : Type u_1} {α : Type u_2} [] [] (g : G) (a : α) :
theorem AddAction.vadd_mem_orbit_vadd {G : Type u_1} {α : Type u_2} [] [] (g : G) (h : G) (a : α) :
theorem MulAction.smul_mem_orbit_smul {G : Type u_1} {α : Type u_2} [] [] (g : G) (h : G) (a : α) :
instance AddAction.instAddAction {G : Type u_1} {α : Type u_2} [] [] (H : ) :
AddAction { x : G // x H } α
Equations
instance MulAction.instMulAction {G : Type u_1} {α : Type u_2} [] [] (H : ) :
MulAction { x : G // x H } α
Equations
theorem AddAction.orbit_addSubgroup_subset {G : Type u_1} {α : Type u_2} [] [] (H : ) (a : α) :
AddAction.orbit { x : G // x H } a
theorem MulAction.orbit_subgroup_subset {G : Type u_1} {α : Type u_2} [] [] (H : ) (a : α) :
MulAction.orbit { x : G // x H } a
theorem AddAction.mem_orbit_of_mem_orbit_addSubgroup {G : Type u_1} {α : Type u_2} [] [] {H : } {a : α} {b : α} (h : a AddAction.orbit { x : G // x H } b) :
a
theorem MulAction.mem_orbit_of_mem_orbit_subgroup {G : Type u_1} {α : Type u_2} [] [] {H : } {a : α} {b : α} (h : a MulAction.orbit { x : G // x H } b) :
a
theorem AddAction.mem_orbit_symm {G : Type u_1} {α : Type u_2} [] [] {a₁ : α} {a₂ : α} :
a₁ a₂
theorem MulAction.mem_orbit_symm {G : Type u_1} {α : Type u_2} [] [] {a₁ : α} {a₂ : α} :
a₁ a₂
theorem AddAction.mem_addSubgroup_orbit_iff {G : Type u_1} {α : Type u_2} [] [] {H : } {x : α} {a : (AddAction.orbit G x)} {b : (AddAction.orbit G x)} :
a AddAction.orbit { x : G // x H } b a AddAction.orbit { x : G // x H } b
theorem MulAction.mem_subgroup_orbit_iff {G : Type u_1} {α : Type u_2} [] [] {H : } {x : α} {a : (MulAction.orbit G x)} {b : (MulAction.orbit G x)} :
a MulAction.orbit { x : G // x H } b a MulAction.orbit { x : G // x H } b
theorem AddAction.orbitRel.proof_1 (G : Type u_2) (α : Type u_1) [] [] :
Equivalence fun (a b : α) => a
def AddAction.orbitRel (G : Type u_1) (α : Type u_2) [] [] :

The relation 'in the same orbit'.

Equations
• = { r := fun (a b : α) => a , iseqv := }
Instances For
def MulAction.orbitRel (G : Type u_1) (α : Type u_2) [] [] :

The relation 'in the same orbit'.

Equations
• = { r := fun (a b : α) => a , iseqv := }
Instances For
theorem AddAction.orbitRel_apply {G : Type u_1} {α : Type u_2} [] [] {a : α} {b : α} :
.Rel a b a
theorem MulAction.orbitRel_apply {G : Type u_1} {α : Type u_2} [] [] {a : α} {b : α} :
.Rel a b a
theorem AddAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [] [] {a : α} {b : α} :
theorem MulAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [] [] {a : α} {b : α} :
theorem AddAction.orbitRel_addSubgroup_le {G : Type u_1} {α : Type u_2} [] [] (H : ) :
AddAction.orbitRel { x : G // x H } α
theorem MulAction.orbitRel_subgroup_le {G : Type u_1} {α : Type u_2} [] [] (H : ) :
MulAction.orbitRel { x : G // x H } α
theorem AddAction.orbitRel_addSubgroupOf {G : Type u_1} {α : Type u_2} [] [] (H : ) (K : ) :
AddAction.orbitRel { x : { x : G // x K } // x H.addSubgroupOf K } α = AddAction.orbitRel { x : G // x H K } α
theorem MulAction.orbitRel_subgroupOf {G : Type u_1} {α : Type u_2} [] [] (H : ) (K : ) :
MulAction.orbitRel { x : { x : G // x K } // x H.subgroupOf K } α = MulAction.orbitRel { x : G // x H K } α
theorem AddAction.quotient_preimage_image_eq_union_add {G : Type u_1} {α : Type u_2} [] [] (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} [] [] (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} [] [] {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} [] [] {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} [] [] (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} [] [] (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) [] [] :
Type u_2

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

Equations
Instances For
@[reducible, inline]
abbrev MulAction.orbitRel.Quotient (G : Type u_1) (α : Type u_2) [] [] :
Type u_2

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

Equations
Instances For
theorem AddAction.pretransitive_iff_subsingleton_quotient (G : Type u_1) (α : Type u_2) [] [] :

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

theorem MulAction.pretransitive_iff_subsingleton_quotient (G : Type u_1) (α : Type u_2) [] [] :

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

theorem AddAction.pretransitive_iff_unique_quotient_of_nonempty (G : Type u_1) (α : Type u_2) [] [] [] :

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

theorem MulAction.pretransitive_iff_unique_quotient_of_nonempty (G : Type u_1) (α : Type u_2) [] [] [] :

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

theorem AddAction.orbitRel.Quotient.orbit.proof_1 {G : Type u_2} {α : Type u_1} [] [] :
∀ (x x_1 : α), x AddAction.orbit G x_1 = AddAction.orbit G x_1
def AddAction.orbitRel.Quotient.orbit {G : Type u_1} {α : Type u_2} [] [] (x : ) :
Set α

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

Equations
• x.orbit =
Instances For
def MulAction.orbitRel.Quotient.orbit {G : Type u_1} {α : Type u_2} [] [] (x : ) :
Set α

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

Equations
• x.orbit =
Instances For
@[simp]
theorem AddAction.orbitRel.Quotient.orbit_mk {G : Type u_1} {α : Type u_2} [] [] (a : α) :
@[simp]
theorem MulAction.orbitRel.Quotient.orbit_mk {G : Type u_1} {α : Type u_2} [] [] (a : α) :
theorem AddAction.orbitRel.Quotient.mem_orbit {G : Type u_1} {α : Type u_2} [] [] {a : α} {x : } :
a x.orbit
theorem MulAction.orbitRel.Quotient.mem_orbit {G : Type u_1} {α : Type u_2} [] [] {a : α} {x : } :
a x.orbit
theorem AddAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u_1} {α : Type u_2} [] [] (x : ) {φ : } (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} [] [] (x : ) {φ : } (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} [] [] :
theorem MulAction.orbitRel.Quotient.orbit_injective {G : Type u_1} {α : Type u_2} [] [] :
Function.Injective MulAction.orbitRel.Quotient.orbit
@[simp]
theorem AddAction.orbitRel.Quotient.orbit_inj {G : Type u_1} {α : Type u_2} [] [] {x : } {y : } :
x.orbit = y.orbit x = y
@[simp]
theorem MulAction.orbitRel.Quotient.orbit_inj {G : Type u_1} {α : Type u_2} [] [] {x : } {y : } :
x.orbit = y.orbit x = y
theorem AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq {G : Type u_1} {α : Type u_2} [] [] {H : } {a : α} {b : α} (h : a = b) :
a = b
theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq {G : Type u_1} {α : Type u_2} [] [] {H : } {a : α} {b : α} (h : a = b) :
a = b
theorem AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq' {G : Type u_1} {α : Type u_2} [] [] {H : } {a : α} {b : α} (h : ) :
theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq' {G : Type u_1} {α : Type u_2} [] [] {H : } {a : α} {b : α} (h : ) :
theorem AddAction.orbitRel.Quotient.orbit_nonempty {G : Type u_1} {α : Type u_2} [] [] (x : ) :
x.orbit.Nonempty
theorem MulAction.orbitRel.Quotient.orbit_nonempty {G : Type u_1} {α : Type u_2} [] [] (x : ) :
x.orbit.Nonempty
theorem AddAction.orbitRel.Quotient.mapsTo_vadd_orbit {G : Type u_1} {α : Type u_2} [] [] (g : G) (x : ) :
Set.MapsTo (fun (x : α) => g +ᵥ x) x.orbit x.orbit
theorem MulAction.orbitRel.Quotient.mapsTo_smul_orbit {G : Type u_1} {α : Type u_2} [] [] (g : G) (x : ) :
Set.MapsTo (fun (x : α) => g x) x.orbit x.orbit
theorem AddAction.instElemOrbit_1.proof_1 {G : Type u_2} {α : Type u_1} [] [] (x : ) (a : x.orbit) :
0 +ᵥ a = a
instance AddAction.instElemOrbit_1 {G : Type u_1} {α : Type u_2} [] [] (x : ) :
Equations
theorem AddAction.instElemOrbit_1.proof_2 {G : Type u_2} {α : Type u_1} [] [] (x : ) (g : G) (g' : G) (a' : x.orbit) :
g + g' +ᵥ a' = g +ᵥ (g' +ᵥ a')
instance MulAction.instElemOrbit_1 {G : Type u_1} {α : Type u_2} [] [] (x : ) :
MulAction G x.orbit
Equations
@[simp]
theorem AddAction.orbitRel.Quotient.orbit.coe_vadd {G : Type u_1} {α : Type u_2} [] [] {g : G} {x : } {a : x.orbit} :
(g +ᵥ a) = g +ᵥ a
@[simp]
theorem MulAction.orbitRel.Quotient.orbit.coe_smul {G : Type u_1} {α : Type u_2} [] [] {g : G} {x : } {a : x.orbit} :
(g a) = g a
instance AddAction.instIsPretransitiveElemOrbit_1 {G : Type u_1} {α : Type u_2} [] [] (x : ) :
Equations
• =
instance MulAction.instIsPretransitiveElemOrbit_1 {G : Type u_1} {α : Type u_2} [] [] (x : ) :
Equations
• =
@[simp]
theorem AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff {G : Type u_1} {α : Type u_2} [] [] {H : } {x : } {a : x.orbit} {b : x.orbit} :
a AddAction.orbit { x : G // x H } b a AddAction.orbit { x : G // x H } b
@[simp]
theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff {G : Type u_1} {α : Type u_2} [] [] {H : } {x : } {a : x.orbit} {b : x.orbit} :
a MulAction.orbit { x : G // x H } b a MulAction.orbit { x : G // x H } b
theorem AddAction.orbitRel.Quotient.addSubgroup_quotient_eq_iff {G : Type u_1} {α : Type u_2} [] [] {H : } {x : } {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} [] [] {H : } {x : } {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} [] [] {H : } {x : } {a : x.orbit} {b : x.orbit} {c : α} (h : a = b) :
a AddAction.orbit { x : G // x H } c b AddAction.orbit { x : G // x H } c
theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff' {G : Type u_1} {α : Type u_2} [] [] {H : } {x : } {a : x.orbit} {b : x.orbit} {c : α} (h : a = b) :
a MulAction.orbit { x : G // x H } c b MulAction.orbit { x : G // x H } c
def AddAction.selfEquivSigmaOrbits' (G : Type u_1) (α : Type u_2) [] [] :
α (ω : ) × ω.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) [] [] :
∀ (x : ) (x_1 : α), = x x_1 x.orbit
def MulAction.selfEquivSigmaOrbits' (G : Type u_1) (α : Type u_2) [] [] :
α (ω : ) × ω.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
theorem AddAction.selfEquivSigmaOrbits.proof_1 (G : Type u_2) (α : Type u_1) [] [] :
∀ (x : ), x.orbit =
def AddAction.selfEquivSigmaOrbits (G : Type u_1) (α : Type u_2) [] [] :
α (ω : ) × (AddAction.orbit G )

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) [] [] :
α (ω : ) × (MulAction.orbit 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) [] [] [] :
theorem MulAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [] [] [] :
theorem AddAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [] [] [] :
theorem MulAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [] [] [] :
theorem AddAction.stabilizer.proof_1 (G : Type u_2) {α : Type u_1} [] [] (a : α) {m : G} (ha : m +ᵥ a = a) :
-m +ᵥ a = a
def AddAction.stabilizer (G : Type u_1) {α : Type u_2} [] [] (a : α) :

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

Equations
• = { toAddSubmonoid := , neg_mem' := }
Instances For
def MulAction.stabilizer (G : Type u_1) {α : Type u_2} [] [] (a : α) :

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

Equations
• = { toSubmonoid := , inv_mem' := }
Instances For
instance AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq {G : Type u_1} {α : Type u_2} [] [] [] (a : α) :
DecidablePred fun (x : G) =>
Equations
instance MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq {G : Type u_1} {α : Type u_2} [] [] [] (a : α) :
DecidablePred fun (x : G) =>
Equations
@[simp]
theorem AddAction.mem_stabilizer_iff {G : Type u_1} {α : Type u_2} [] [] {a : α} {g : G} :
g +ᵥ a = a
@[simp]
theorem MulAction.mem_stabilizer_iff {G : Type u_1} {α : Type u_2} [] [] {a : α} {g : G} :
g a = a
theorem AddAction.le_stabilizer_vadd_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [VAdd α β] [] (a : α) (b : β) :
theorem MulAction.le_stabilizer_smul_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [SMul α β] [] (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} [] [] [] [VAdd α β] [] (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} [] [] [] [SMul α β] [] (a : α) (b : β) (h : Function.Injective fun (x : α) => x b) :
@[simp]
theorem AddAction.stabilizer_vadd_eq_right {G : Type u_1} {β : Type u_3} [] [] {α : Type u_4} [] [] [] (a : α) (b : β) :
@[simp]
theorem MulAction.stabilizer_smul_eq_right {G : Type u_1} {β : Type u_3} [] [] {α : Type u_4} [] [] [] (a : α) (b : β) :
@[simp]
theorem AddAction.stabilizer_add_eq_left {G : Type u_1} {α : Type u_2} [] [] [] [] (a : α) (b : α) :
@[simp]
theorem MulAction.stabilizer_mul_eq_left {G : Type u_1} {α : Type u_2} [] [] [] [] (a : α) (b : α) :
@[simp]
theorem AddAction.stabilizer_add_eq_right {G : Type u_1} {α : Type u_2} [] [] [] [] (a : α) (b : α) :
@[simp]
theorem MulAction.stabilizer_mul_eq_right {G : Type u_1} {α : Type u_2} [] [] [] [] (a : α) (b : α) :
theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [] [] (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} [] [] {a : α} {b : α} (h : .Rel a b) :
{ x : G // } ≃* { x : G // }

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

Equations
Instances For
theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [] [] (g : G) (a : α) :

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} [] [] {a : α} {b : α} (h : .Rel a b) :
{ x : G // } ≃+ { x : G // }

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

Equations
Instances For
theorem Equiv.swap_mem_stabilizer {α : Type u_1} [] {S : Set α} {a : α} {b : α} :
(a S b S)
theorem MulAction.le_stabilizer_iff_smul_le {G : Type u_1} [] {α : Type u_2} [] (s : Set α) (H : ) :
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} [] {α : Type u_2} [] (s : Set α) (hs : s.Finite) (g : G) :
g s s

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} [] {α : Type u_2} [] (s : Set α) (hs : s.Finite) (g : G) :
s g s

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