Basic properties of group actions #
The orbit of an element under an action.
Equations
- mul_action.orbit α b = set.range (λ (x : α), x • 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 : α) :
x • b ∈ mul_action.orbit α b
@[simp]
theorem
mul_action.mem_orbit_self
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
(b : β) :
b ∈ mul_action.orbit α b
The set of elements fixed under the whole action.
Equations
- mul_action.fixed_points α β = {b : β | ∀ (x : α), x • b = b}
fixed_by g is the subfield of elements fixed by g.
Equations
- mul_action.fixed_by α β g = {x : β | g • x = x}
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 α b → b' = b
The stabilizer of a point b as a submonoid of α.
@[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
The stabilizer of an element under an action, i.e. what sends the element to itself. A subgroup.
Equations
- mul_action.stabilizer α b = {carrier := (mul_action.stabilizer.submonoid α b).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _}
@[simp]
theorem
mul_action.mem_stabilizer_iff
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
{b : β}
{a : α} :
a ∈ mul_action.stabilizer α b ↔ a • b = b
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
@[simp]
theorem
mul_action.mem_orbit_smul
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(g : α)
(a : β) :
a ∈ mul_action.orbit α (g • a)
@[simp]
theorem
mul_action.smul_mem_orbit_smul
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(g h : α)
(a : β) :
g • a ∈ mul_action.orbit α (h • a)
The relation "in the same orbit".
Equations
- mul_action.orbit_rel α β = {r := λ (a b : β), a ∈ mul_action.orbit α b, iseqv := _}
def
mul_action.mul_left_cosets
{α : Type u}
[group α]
(H : subgroup α)
(x : α)
(y : quotient_group.quotient H) :
Action on left cosets.
Equations
- mul_action.mul_left_cosets H x y = quotient.lift_on' y (λ (y : α), quotient_group.mk (x * y)) _
@[instance]
Equations
- mul_action.quotient H = {to_has_scalar := {smul := mul_action.mul_left_cosets H}, one_smul := _, mul_smul := _}
@[simp]
theorem
mul_action.quotient.smul_mk
{α : Type u}
[group α]
(H : subgroup α)
(a x : α) :
a • quotient_group.mk x = quotient_group.mk (a * x)
@[instance]
Equations
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
- mul_action.of_quotient_stabilizer α x g = quotient.lift_on' g (λ (_x : α), _x • x) _
@[simp]
theorem
mul_action.of_quotient_stabilizer_mk
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(x : β)
(g : α) :
mul_action.of_quotient_stabilizer α x (quotient_group.mk g) = g • x
theorem
mul_action.of_quotient_stabilizer_mem_orbit
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(x : β)
(g : quotient_group.quotient (mul_action.stabilizer α x)) :
theorem
mul_action.of_quotient_stabilizer_smul
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(x : β)
(g : α)
(g' : quotient_group.quotient (mul_action.stabilizer α x)) :
mul_action.of_quotient_stabilizer α x (g • g') = g • mul_action.of_quotient_stabilizer α x g'
theorem
mul_action.injective_of_quotient_stabilizer
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(x : β) :
def
mul_action.orbit_equiv_quotient_stabilizer
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(b : β) :
Orbit-stabilizer theorem.
Equations
- mul_action.orbit_equiv_quotient_stabilizer α b = (equiv.of_bijective (λ (g : quotient_group.quotient (mul_action.stabilizer α b)), ⟨mul_action.of_quotient_stabilizer α b g, _⟩) _).symm
@[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) :
mul_action.stabilizer G ↑1 = H
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 β} :
r • s.sum = (multiset.map (has_scalar.smul r) s).sum
theorem
finset.smul_sum
{α : Type u}
{β : Type v}
{γ : Type w}
[monoid α]
[add_comm_monoid β]
[distrib_mul_action α β]
{r : α}
{f : γ → β}
{s : finset γ} :
@[class]
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) :
@[instance]