mathlib3 documentation

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 #

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
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
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₂
theorem mul_action.mem_orbit_iff {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b₁ b₂ : β} :
b₂ mul_action.orbit α b₁ (x : α), x b₁ = b₂
@[simp]
theorem mul_action.mem_orbit {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) (x : α) :
@[simp]
theorem add_action.mem_orbit {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) (x : α) :
@[simp]
theorem mul_action.mem_orbit_self {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :
@[simp]
theorem add_action.mem_orbit_self {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) :
theorem mul_action.orbit_nonempty {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :
theorem add_action.orbit_nonempty {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) :
theorem add_action.maps_to_vadd_orbit {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (a : α) (b : β) :
theorem mul_action.maps_to_smul_orbit {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :
theorem add_action.vadd_orbit_subset {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (a : α) (b : β) :
theorem mul_action.smul_orbit_subset {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :
theorem mul_action.orbit_smul_subset {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :
theorem add_action.orbit_vadd_subset {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (a : α) (b : β) :
@[protected, instance]
def mul_action.orbit.mul_action {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b : β} :
Equations
@[protected, instance]
def add_action.orbit.add_action {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {b : β} :
Equations
@[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'
@[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'
def add_action.fixed_points (α : Type u) (β : Type v) [add_monoid α] [add_action α β] :
set β

The set of elements fixed under the whole action.

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

The set of elements fixed under the whole action.

Equations
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
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
theorem mul_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [monoid α] [mul_action α β] :
@[simp]
theorem mul_action.mem_fixed_points {α : Type u} (β : Type v) [monoid α] [mul_action α β] {b : β} :
b mul_action.fixed_points α β (x : α), x b = b
@[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
@[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
@[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
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
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
def mul_action.stabilizer.submonoid (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :

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

Equations
def add_action.stabilizer.add_submonoid (α : Type u) {β : Type v} [add_monoid α] [add_action α β] (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 α] [add_action α β] {b : β} {a : α} :
@[simp]
theorem mul_action.mem_stabilizer_submonoid_iff (α : Type u) {β : Type v} [monoid α] [mul_action α β] {b : β} {a : α} :
theorem add_action.orbit_eq_univ (α : Type u) {β : Type v} [add_monoid α] [add_action α β] [add_action.is_pretransitive α β] (x : β) :
theorem mul_action.orbit_eq_univ (α : Type u) {β : Type v} [monoid α] [mul_action α β] [mul_action.is_pretransitive α β] (x : β) :
def mul_action.stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (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 α] [add_action α β] (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 α] [add_action α β] {b : β} {a : α} :
@[simp]
theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {a : α} :
@[simp]
theorem mul_action.smul_orbit {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (b : β) :
@[simp]
theorem add_action.vadd_orbit {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) (b : β) :
@[simp]
theorem mul_action.orbit_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (b : β) :
@[simp]
theorem add_action.orbit_vadd {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) (b : β) :
@[protected, instance]

The action of a group on an orbit is transitive.

@[protected, instance]

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

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

The relation 'in the same orbit'.

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

The relation 'in the same orbit'.

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

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

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 α] [add_action α β] {U V : set β} :
disjoint (quotient.mk '' U) (quotient.mk '' V) (x : β), x U (a : α), a +ᵥ x V
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
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
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
@[reducible]
def add_action.orbit_rel.quotient (α : Type u) (β : Type v) [add_group α] [add_action α β] :

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 α] [mul_action α β] :

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 α] [mul_action α β] (x : mul_action.orbit_rel.quotient α β) :
set β

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

Equations

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

Equations
theorem add_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [add_group α] [add_action α β] {b : β} {x : add_action.orbit_rel.quotient α β} :
theorem mul_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {x : mul_action.orbit_rel.quotient α β} :

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

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

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

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

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

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

Equations

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

Equations

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 α] [mul_action α β] {x y : β} (h : (mul_action.orbit_rel α β).rel x y) :

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

Equations

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 α] [add_action α β] {x y : β} (h : (add_action.orbit_rel α β).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] [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.