# mathlib3documentation

group_theory.group_action.basic

# Basic properties of group actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• mul_action.orbit
• mul_action.fixed_points
• mul_action.fixed_by
• mul_action.stabilizer
def mul_action.orbit (α : Type u) {β : Type v} [monoid α] [ β] (b : β) :
set β

The orbit of an element under an action.

Equations
Instances for ↥mul_action.orbit
def add_action.orbit (α : Type u) {β : Type v} [add_monoid α] [ β] (b : β) :
set β

The orbit of an element under an action.

Equations
Instances for ↥add_action.orbit
theorem add_action.mem_orbit_iff {α : Type u} {β : Type v} [add_monoid α] [ β] {b₁ b₂ : β} :
b₂ b₁ (x : α), x +ᵥ b₁ = b₂
theorem mul_action.mem_orbit_iff {α : Type u} {β : Type v} [monoid α] [ β] {b₁ b₂ : β} :
b₂ b₁ (x : α), x b₁ = b₂
@[simp]
theorem mul_action.mem_orbit {α : Type u} {β : Type v} [monoid α] [ β] (b : β) (x : α) :
x b
@[simp]
theorem add_action.mem_orbit {α : Type u} {β : Type v} [add_monoid α] [ β] (b : β) (x : α) :
x +ᵥ b
@[simp]
theorem mul_action.mem_orbit_self {α : Type u} {β : Type v} [monoid α] [ β] (b : β) :
b
@[simp]
theorem add_action.mem_orbit_self {α : Type u} {β : Type v} [add_monoid α] [ β] (b : β) :
b
theorem mul_action.orbit_nonempty {α : Type u} {β : Type v} [monoid α] [ β] (b : β) :
theorem add_action.orbit_nonempty {α : Type u} {β : Type v} [add_monoid α] [ β] (b : β) :
theorem add_action.maps_to_vadd_orbit {α : Type u} {β : Type v} [add_monoid α] [ β] (a : α) (b : β) :
b) b)
theorem mul_action.maps_to_smul_orbit {α : Type u} {β : Type v} [monoid α] [ β] (a : α) (b : β) :
b) b)
theorem add_action.vadd_orbit_subset {α : Type u} {β : Type v} [add_monoid α] [ β] (a : α) (b : β) :
theorem mul_action.smul_orbit_subset {α : Type u} {β : Type v} [monoid α] [ β] (a : α) (b : β) :
a
theorem mul_action.orbit_smul_subset {α : Type u} {β : Type v} [monoid α] [ β] (a : α) (b : β) :
(a b)
theorem add_action.orbit_vadd_subset {α : Type u} {β : Type v} [add_monoid α] [ β] (a : α) (b : β) :
(a +ᵥ b)
@[protected, instance]
def mul_action.orbit.mul_action {α : Type u} {β : Type v} [monoid α] [ β] {b : β} :
b)
Equations
@[protected, instance]
def add_action.orbit.add_action {α : Type u} {β : Type v} [add_monoid α] [ β] {b : β} :
b)
Equations
@[simp]
theorem add_action.orbit.coe_vadd {α : Type u} {β : Type v} [add_monoid α] [ β] {b : β} {a : α} {b' : b)} :
(a +ᵥ b') = a +ᵥ b'
@[simp]
theorem mul_action.orbit.coe_smul {α : Type u} {β : Type v} [monoid α] [ β] {b : β} {a : α} {b' : b)} :
(a b') = a b'
def add_action.fixed_points (α : Type u) (β : Type v) [add_monoid α] [ β] :
set β

The set of elements fixed under the whole action.

Equations
def mul_action.fixed_points (α : Type u) (β : Type v) [monoid α] [ β] :
set β

The set of elements fixed under the whole action.

Equations
• = {b : β | (x : α), x b = b}
def add_action.fixed_by (α : Type u) (β : Type v) [add_monoid α] [ β] (g : α) :
set β

fixed_by g is the subfield of elements fixed by g.

Equations
def mul_action.fixed_by (α : Type u) (β : Type v) [monoid α] [ β] (g : α) :
set β

fixed_by g is the subfield of elements fixed by g.

Equations
• g = {x : β | g x = x}
theorem mul_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [monoid α] [ β] :
= (g : α), g
theorem add_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [add_monoid α] [ β] :
= (g : α), g
@[simp]
theorem mul_action.mem_fixed_points {α : Type u} (β : Type v) [monoid α] [ β] {b : β} :
(x : α), x b = b
@[simp]
theorem add_action.mem_fixed_points {α : Type u} (β : Type v) [add_monoid α] [ β] {b : β} :
(x : α), x +ᵥ b = b
@[simp]
theorem mul_action.mem_fixed_by {α : Type u} (β : Type v) [monoid α] [ β] {g : α} {b : β} :
b g g b = b
@[simp]
theorem add_action.mem_fixed_by {α : Type u} (β : Type v) [add_monoid α] [ β] {g : α} {b : β} :
b g g +ᵥ b = b
theorem mul_action.mem_fixed_points' {α : Type u} (β : Type v) [monoid α] [ β] {b : β} :
(b' : β), b' b' = b
theorem add_action.mem_fixed_points' {α : Type u} (β : Type v) [add_monoid α] [ β] {b : β} :
(b' : β), b' b' = b
def mul_action.stabilizer.submonoid (α : Type u) {β : Type v} [monoid α] [ β] (b : β) :

The stabilizer of a point b as a submonoid of α.

Equations
def add_action.stabilizer.add_submonoid (α : Type u) {β : Type v} [add_monoid α] [ β] (b : β) :

The stabilizer of a point b as an additive submonoid of α.

Equations
@[simp]
theorem add_action.mem_stabilizer_add_submonoid_iff (α : Type u) {β : Type v} [add_monoid α] [ β] {b : β} {a : α} :
a +ᵥ b = b
@[simp]
theorem mul_action.mem_stabilizer_submonoid_iff (α : Type u) {β : Type v} [monoid α] [ β] {b : β} {a : α} :
a b = b
theorem add_action.orbit_eq_univ (α : Type u) {β : Type v} [add_monoid α] [ β] (x : β) :
theorem mul_action.orbit_eq_univ (α : Type u) {β : Type v} [monoid α] [ β] (x : β) :
theorem add_action.mem_fixed_points_iff_card_orbit_eq_zero {α : Type u} {β : Type v} [add_monoid α] [ β] {a : β} [fintype a)] :
= 1
theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one {α : Type u} {β : Type v} [monoid α] [ β] {a : β} [fintype a)] :
= 1
def mul_action.stabilizer (α : Type u) {β : Type v} [group α] [ β] (b : β) :

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

Equations
Instances for ↥mul_action.stabilizer
def add_action.stabilizer (α : Type u) {β : Type v} [add_group α] [ β] (b : β) :

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

Equations
@[simp]
theorem add_action.mem_stabilizer_iff {α : Type u} {β : Type v} [add_group α] [ β] {b : β} {a : α} :
a +ᵥ b = b
@[simp]
theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [group α] [ β] {b : β} {a : α} :
a b = b
@[simp]
theorem mul_action.smul_orbit {α : Type u} {β : Type v} [group α] [ β] (a : α) (b : β) :
a =
@[simp]
theorem add_action.vadd_orbit {α : Type u} {β : Type v} [add_group α] [ β] (a : α) (b : β) :
a +ᵥ =
@[simp]
theorem mul_action.orbit_smul {α : Type u} {β : Type v} [group α] [ β] (a : α) (b : β) :
(a b) =
@[simp]
theorem add_action.orbit_vadd {α : Type u} {β : Type v} [add_group α] [ β] (a : α) (b : β) :
(a +ᵥ b) =
@[protected, instance]
def mul_action.orbit.is_pretransitive {α : Type u} {β : Type v} [group α] [ β] (x : β) :

The action of a group on an orbit is transitive.

@[protected, instance]
def add_action.orbit.is_pretransitive {α : Type u} {β : Type v} [add_group α] [ β] (x : β) :

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

theorem mul_action.orbit_eq_iff {α : Type u} {β : Type v} [group α] [ β] {a b : β} :
a
theorem add_action.orbit_eq_iff {α : Type u} {β : Type v} [add_group α] [ β] {a b : β} :
a
theorem add_action.mem_orbit_vadd (α : Type u) {β : Type v} [add_group α] [ β] (g : α) (a : β) :
a (g +ᵥ a)
theorem mul_action.mem_orbit_smul (α : Type u) {β : Type v} [group α] [ β] (g : α) (a : β) :
a (g a)
theorem mul_action.smul_mem_orbit_smul (α : Type u) {β : Type v} [group α] [ β] (g h : α) (a : β) :
g a (h a)
g +ᵥ a (h +ᵥ a)
def mul_action.orbit_rel (α : Type u) (β : Type v) [group α] [ β] :

The relation 'in the same orbit'.

Equations
def add_action.orbit_rel (α : Type u) (β : Type v) [add_group α] [ β] :

The relation 'in the same orbit'.

Equations
theorem mul_action.orbit_rel_apply {α : Type u} {β : Type v} [group α] [ β] {x y : β} :
β).rel x y x
theorem add_action.orbit_rel_apply {α : Type u} {β : Type v} [add_group α] [ β] {x y : β} :
β).rel x y x
theorem mul_action.quotient_preimage_image_eq_union_mul {α : Type u} {β : Type v} [group α] [ β] (U : set β) :
= (a : α),

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 α.

theorem add_action.quotient_preimage_image_eq_union_add {α : Type u} {β : Type v} [add_group α] [ β] (U : set β) :
= (a : α),

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 α.

theorem add_action.disjoint_image_image_iff {α : Type u} {β : Type v} [add_group α] [ β] {U V : set β} :
(x : β), x U (a : α), a +ᵥ x V
theorem mul_action.disjoint_image_image_iff {α : Type u} {β : Type v} [group α] [ β] {U V : set β} :
(x : β), x U (a : α), a x V
theorem add_action.image_inter_image_iff {α : Type u} {β : Type v} [add_group α] [ β] (U V : set β) :
= (x : β), x U (a : α), a +ᵥ x V
theorem mul_action.image_inter_image_iff {α : Type u} {β : Type v} [group α] [ β] (U V : set β) :
= (x : β), x U (a : α), a x V
@[reducible]
def add_action.orbit_rel.quotient (α : Type u) (β : Type v) [add_group α] [ β] :

The quotient by add_action.orbit_rel, given a name to enable dot notation.

Equations
@[reducible]
def mul_action.orbit_rel.quotient (α : Type u) (β : Type v) [group α] [ β] :

The quotient by mul_action.orbit_rel, given a name to enable dot notation.

Equations
def mul_action.orbit_rel.quotient.orbit {α : Type u} {β : Type v} [group α] [ β] (x : β) :
set β

The orbit corresponding to an element of the quotient by mul_action.orbit_rel

Equations
• x.orbit = mul_action.orbit_rel.quotient.orbit._proof_1
def add_action.orbit_rel.quotient.orbit {α : Type u} {β : Type v} [add_group α] [ β] (x : β) :
set β

The orbit corresponding to an element of the quotient by add_action.orbit_rel

Equations
@[simp]
theorem mul_action.orbit_rel.quotient.orbit_mk {α : Type u} {β : Type v} [group α] [ β] (b : β) :
@[simp]
theorem add_action.orbit_rel.quotient.orbit_mk {α : Type u} {β : Type v} [add_group α] [ β] (b : β) :
theorem add_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [add_group α] [ β] {b : β} {x : β} :
theorem mul_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [group α] [ β] {b : β} {x : β} :
theorem add_action.orbit_rel.quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [add_group α] [ β] (x : β) {φ : β}  :
x.orbit = (φ x)

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

theorem mul_action.orbit_rel.quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [group α] [ β] (x : β) {φ : β}  :
x.orbit = (φ x)

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

def mul_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [group α] [ β] :
β Σ (ω : , (ω.orbit)

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

This version is expressed in terms of mul_action.orbit_rel.quotient.orbit instead of mul_action.orbit, to avoid mentioning quotient.out'.

Equations
def add_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [add_group α] [ β] :
β Σ (ω : , (ω.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 add_action.orbit_rel.quotient.orbit instead of add_action.orbit, to avoid mentioning quotient.out'.

Equations
def mul_action.self_equiv_sigma_orbits (α : Type u) (β : Type v) [group α] [ β] :
β Σ (ω : , (quotient.out' ω))

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

Equations
def add_action.self_equiv_sigma_orbits (α : Type u) (β : Type v) [add_group α] [ β] :
β Σ (ω : , (quotient.out' ω))

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

Equations
theorem mul_action.stabilizer_smul_eq_stabilizer_map_conj {α : Type u} {β : Type v} [group α] [ β] (g : α) (x : β) :
(g x) =

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

noncomputable def mul_action.stabilizer_equiv_stabilizer_of_orbit_rel {α : Type u} {β : Type v} [group α] [ β] {x y : β} (h : β).rel x y) :

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

Equations
theorem add_action.stabilizer_vadd_eq_stabilizer_map_conj {α : Type u} {β : Type v} [add_group α] [ β] (g : α) (x : β) :

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

noncomputable def add_action.stabilizer_equiv_stabilizer_of_orbit_rel {α : Type u} {β : Type v} [add_group α] [ β] {x y : β} (h : β).rel x y) :

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

Equations
theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [monoid M] [ R] (k : M) (h : (x : R), k x = 0 x = 0) {a 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 is_smul_regular. The typeclass that restricts all terms of M to have this property is no_zero_smul_divisors.