mathlib documentation

group_theory.group_action.basic

Basic properties of group actions #

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

The orbit of an element under an action.

Equations
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 mul_action.mem_orbit_self {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :
def mul_action.fixed_points (α : Type u) (β : Type v) [monoid α] [mul_action α β] :
set β

The set of elements fixed under the whole action.

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 α β] :
mul_action.fixed_points α β = ⋂ (g : α), mul_action.fixed_by α β g
@[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 mul_action.mem_fixed_by {α : Type u} (β : Type v) [monoid α] [mul_action α β] {g : α} {b : β} :
b mul_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 α bb' = 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
@[simp]
theorem mul_action.mem_stabilizer_submonoid_iff (α : Type u) {β : Type v} [monoid α] [mul_action α β] {b : β} {a : α} :
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
@[simp]
theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {a : α} :
theorem mul_action.orbit_eq_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a b : β} :
@[simp]
theorem mul_action.mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g : α) (a : β) :
@[simp]
theorem mul_action.smul_mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g h : α) (a : β) :
def mul_action.orbit_rel (α : Type u) (β : Type v) [group α] [mul_action α β] :

The relation "in the same orbit".

Equations
def mul_action.mul_left_cosets {α : Type u} [group α] (H : subgroup α) (x : α) (y : quotient_group.quotient H) :

Action on left cosets.

Equations
@[instance]
def mul_action.quotient {α : Type u} [group α] (H : subgroup α) :
Equations
@[simp]
theorem mul_action.quotient.smul_mk {α : Type u} [group α] (H : subgroup α) (a x : α) :
@[simp]
theorem mul_action.quotient.smul_coe {α : Type u} [group α] (H : subgroup α) (a x : α) :
a x = a * x
def mul_action.of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : quotient_group.quotient (mul_action.stabilizer α x)) :
β

The canonical map from the quotient of the stabilizer to the set.

Equations
@[simp]
theorem mul_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) :
theorem mul_action.of_quotient_stabilizer_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) (g' : quotient_group.quotient (mul_action.stabilizer α x)) :
@[simp]
theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) (a : α) :
@[simp]
theorem mul_action.stabilizer_quotient {G : Type u_1} [group G] (H : subgroup G) :
theorem list.smul_sum {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] {r : α} {l : list β} :
theorem multiset.smul_sum {α : Type u} {β : Type v} [monoid α] [add_comm_monoid β] [distrib_mul_action α β] {r : α} {s : multiset β} :
theorem finset.smul_sum {α : Type u} {β : Type v} {γ : Type w} [monoid α] [add_comm_monoid β] [distrib_mul_action α β] {r : α} {f : γ → β} {s : finset γ} :
r ∑ (x : γ) in s, f x = ∑ (x : γ) in s, r f x
@[class]
structure is_pretransitive (G : Type u_1) (X : Type u_2) [monoid G] [mul_action G X] :
Prop
  • exists_smul_eq : ∀ (x y : X), ∃ (g : G), g x = y

G acts pretransitively on X if for any x y there is g such that g • x = y. A transitive action should furthermore have X nonempty.

Instances
theorem exists_smul_eq (M : Type u_1) {X : Type u_2} [monoid M] [mul_action M X] [is_pretransitive M X] (x y : X) :
∃ (m : M), m x = y
@[instance]