mathlib documentation

group_theory.group_action.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 #

source
def mul_action.orbit (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :
set β

The orbit of an element under an action.

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

The orbit of an element under an action.

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

The set of elements fixed under the whole action.

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

The set of elements fixed under the whole action.

Equations
source
def add_action.fixed_by (α : Type u) (β : Type v) [add_monoid α] [add_action α β] (g : α) :
set β

fixed_by g is the subfield of elements fixed by g.

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

fixed_by g is the subfield of elements fixed by g.

Equations
source
theorem mul_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [monoid α] [mul_action α β] :
mul_action.fixed_points α β = ⋂ (g : α), mul_action.fixed_by α β g
source
theorem add_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [add_monoid α] [add_action α β] :
add_action.fixed_points α β = ⋂ (g : α), add_action.fixed_by α β g
source
@[simp]
theorem mul_action.mem_fixed_points {α : Type u} (β : Type v) [monoid α] [mul_action α β] {b : β} :
b ∈ mul_action.fixed_points α β ↔ ∀ (x : α), x • b = b
source
@[simp]
theorem add_action.mem_fixed_points {α : Type u} (β : Type v) [add_monoid α] [add_action α β] {b : β} :
b ∈ add_action.fixed_points α β ↔ ∀ (x : α), x +ᵥ b = b
source
@[simp]
theorem mul_action.mem_fixed_by {α : Type u} (β : Type v) [monoid α] [mul_action α β] {g : α} {b : β} :
b ∈ mul_action.fixed_by α β g ↔ g • b = b
source
@[simp]
theorem add_action.mem_fixed_by {α : Type u} (β : Type v) [add_monoid α] [add_action α β] {g : α} {b : β} :
b ∈ add_action.fixed_by α β g ↔ g +ᵥ b = b
source
theorem mul_action.mem_fixed_points' {α : Type u} (β : Type v) [monoid α] [mul_action α β] {b : β} :
b ∈ mul_action.fixed_points α β ↔ ∀ (b' : β), b' ∈ mul_action.orbit α b → b' = b
source
theorem add_action.mem_fixed_points' {α : Type u} (β : Type v) [add_monoid α] [add_action α β] {b : β} :
b ∈ add_action.fixed_points α β ↔ ∀ (b' : β), b' ∈ add_action.orbit α b → b' = b
source
def mul_action.stabilizer.submonoid (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :
submonoid α

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

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

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

Equations
source
@[simp]
theorem add_action.mem_stabilizer_add_submonoid_iff (α : Type u) {β : Type v} [add_monoid α] [add_action α β] {b : β} {a : α} :
a ∈ add_action.stabilizer.add_submonoid α b ↔ a +ᵥ b = b
source
@[simp]
theorem mul_action.mem_stabilizer_submonoid_iff (α : Type u) {β : Type v} [monoid α] [mul_action α β] {b : β} {a : α} :
a ∈ mul_action.stabilizer.submonoid α b ↔ a • b = b
source
theorem add_action.orbit_eq_univ (α : Type u) {β : Type v} [add_monoid α] [add_action α β] [add_action.is_pretransitive α β] (x : β) :
add_action.orbit α x = set.univ
source
theorem mul_action.orbit_eq_univ (α : Type u) {β : Type v} [monoid α] [mul_action α β] [mul_action.is_pretransitive α β] (x : β) :
mul_action.orbit α x = set.univ
source
theorem add_action.mem_fixed_points_iff_card_orbit_eq_zero {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {a : β} [fintype ↥(add_action.orbit α a)] :
a ∈ add_action.fixed_points α β ↔ fintype.card ↥(add_action.orbit α a) = 1
source
theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one {α : Type u} {β : Type v} [monoid α] [mul_action α β] {a : β} [fintype ↥(mul_action.orbit α a)] :
a ∈ mul_action.fixed_points α β ↔ fintype.card ↥(mul_action.orbit α a) = 1
source
def mul_action.stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) :
subgroup α

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

Equations
source
def add_action.stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) :
add_subgroup α

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

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

The action of a group on an orbit is transitive.

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

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

source
theorem mul_action.orbit_eq_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a b : β} :
mul_action.orbit α a = mul_action.orbit α b ↔ a ∈ mul_action.orbit α b
source
theorem add_action.orbit_eq_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {a b : β} :
add_action.orbit α a = add_action.orbit α b ↔ a ∈ add_action.orbit α b
source
theorem add_action.mem_orbit_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (g : α) (a : β) :
a ∈ add_action.orbit α (g +ᵥ a)
source
theorem mul_action.mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g : α) (a : β) :
a ∈ mul_action.orbit α (g • a)
source
theorem mul_action.smul_mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g h : α) (a : β) :
g • a ∈ mul_action.orbit α (h • a)
source
theorem add_action.vadd_mem_orbit_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (g h : α) (a : β) :
g +ᵥ a ∈ add_action.orbit α (h +ᵥ a)
source
def mul_action.orbit_rel (α : Type u) (β : Type v) [group α] [mul_action α β] :
setoid β

The relation 'in the same orbit'.

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

The relation 'in the same orbit'.

Equations
source
theorem mul_action.quotient_preimage_image_eq_union_mul {α : Type u} {β : Type v} [group α] [mul_action α β] (U : set β) :
quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ (a : α), has_smul.smul a '' 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 α.

source
theorem add_action.quotient_preimage_image_eq_union_add {α : Type u} {β : Type v} [add_group α] [add_action α β] (U : set β) :
quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ (a : α), has_vadd.vadd a '' 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 α.

source
theorem add_action.disjoint_image_image_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {U V : set β} :
disjoint (quotient.mk '' U) (quotient.mk '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a +ᵥ x ∉ V
source
theorem mul_action.disjoint_image_image_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {U V : set β} :
disjoint (quotient.mk '' U) (quotient.mk '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a • x ∉ V
source
theorem add_action.image_inter_image_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] (U V : set β) :
quotient.mk '' U ∩ quotient.mk '' V = ∅ ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a +ᵥ x ∉ V
source
theorem mul_action.image_inter_image_iff {α : Type u} {β : Type v} [group α] [mul_action α β] (U V : set β) :
quotient.mk '' U ∩ quotient.mk '' V = ∅ ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a • x ∉ V
source
@[reducible]
def add_action.orbit_rel.quotient (α : Type u) (β : Type v) [add_group α] [add_action α β] :
Type v

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem mul_action.orbit_rel.quotient.orbit_mk {α : Type u} {β : Type v} [group α] [mul_action α β] (b : β) :
mul_action.orbit_rel.quotient.orbit (quotient.mk' b) = mul_action.orbit α b
source
@[simp]
theorem add_action.orbit_rel.quotient.orbit_mk {α : Type u} {β : Type v} [add_group α] [add_action α β] (b : β) :
add_action.orbit_rel.quotient.orbit (quotient.mk' b) = add_action.orbit α b
source
theorem add_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [add_group α] [add_action α β] {b : β} {x : add_action.orbit_rel.quotient α β} :
b ∈ x.orbit ↔ quotient.mk' b = x
source
theorem mul_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {x : mul_action.orbit_rel.quotient α β} :
b ∈ x.orbit ↔ quotient.mk' b = x
source
theorem add_action.orbit_rel.quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [add_group α] [add_action α β] (x : add_action.orbit_rel.quotient α β) {φ : add_action.orbit_rel.quotient α β → β} (hφ : function.right_inverse φ quotient.mk') :
x.orbit = add_action.orbit α (φ x)

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

source
theorem mul_action.orbit_rel.quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [group α] [mul_action α β] (x : mul_action.orbit_rel.quotient α β) {φ : mul_action.orbit_rel.quotient α β → β} (hφ : function.right_inverse φ quotient.mk') :
x.orbit = mul_action.orbit α (φ x)

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

source
def mul_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [group α] [mul_action α β] :
β ≃ Σ (ω : mul_action.orbit_rel.quotient α β), ↥(ω.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
source
def add_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [add_group α] [add_action α β] :
β ≃ Σ (ω : add_action.orbit_rel.quotient α β), ↥(ω.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
source
def mul_action.self_equiv_sigma_orbits (α : Type u) (β : Type v) [group α] [mul_action α β] :
β ≃ Σ (ω : mul_action.orbit_rel.quotient α β), ↥(mul_action.orbit α (quotient.out' ω))

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

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

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

Equations
source
theorem mul_action.stabilizer_smul_eq_stabilizer_map_conj {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) (x : β) :
mul_action.stabilizer α (g • x) = subgroup.map (mul_equiv.to_monoid_hom (⇑mul_aut.conj g)) (mul_action.stabilizer α x)

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

source
noncomputable def mul_action.stabilizer_equiv_stabilizer_of_orbit_rel {α : Type u} {β : Type v} [group α] [mul_action α β] {x y : β} (h : (mul_action.orbit_rel α β).rel x y) :
↥(mul_action.stabilizer α x) ≃* ↥(mul_action.stabilizer α y)

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

Equations
source
theorem add_action.stabilizer_vadd_eq_stabilizer_map_conj {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) (x : β) :
add_action.stabilizer α (g +ᵥ x) = add_subgroup.map (add_equiv.to_add_monoid_hom (⇑add_aut.conj g)) (add_action.stabilizer α x)

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

source
noncomputable def add_action.stabilizer_equiv_stabilizer_of_orbit_rel {α : Type u} {β : Type v} [add_group α] [add_action α β] {x y : β} (h : (add_action.orbit_rel α β).rel x y) :
↥(add_action.stabilizer α x) ≃+ ↥(add_action.stabilizer α y)

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

Equations
source
theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [monoid M] [non_unital_non_assoc_ring R] [distrib_mul_action 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.