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
def add_action.orbit (α : Type u) {β : Type v} [add_monoid α] [add_action α β] (b : β) :
set β

The orbit of an element under an action.

Equations
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 α β] :
mul_action.fixed_points α β = ⋂ (g : α), mul_action.fixed_by α β g
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
@[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 α bb' = 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 α 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
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
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]
def mul_action.orbit.is_pretransitive {α : Type u} {β : Type v} [group α] [mul_action α β] (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 α] [add_action α β] (x : β) :

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
def mul_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [group α] [mul_action α β] {φ : quotient (mul_action.orbit_rel α β) → β} (hφ : function.right_inverse φ quotient.mk') :
β Σ (ω : quotient (mul_action.orbit_rel α β)), (mul_action.orbit α (φ ω))

Decomposition of a type X as a disjoint union of its orbits under a group action. This version works with any right inverse to quotient.mk' in order to stay computable. In most cases you'll want to use quotient.out', so we provide mul_action.self_equiv_sigma_orbits as a special case.

Equations
def add_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [add_group α] [add_action α β] {φ : quotient (add_action.orbit_rel α β) → β} (hφ : function.right_inverse φ quotient.mk') :
β Σ (ω : quotient (add_action.orbit_rel α β)), (add_action.orbit α (φ ω))

Decomposition of a type X as a disjoint union of its orbits under an additive group action. This version works with any right inverse to quotient.mk' in order to stay computable. In most cases you'll want to use quotient.out', so we provide add_action.self_equiv_sigma_orbits as a special case.

Equations
noncomputable 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.

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

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
def mul_action.mul_left_cosets {α : Type u} [group α] (H : subgroup α) (x : α) (y : α H) :
α H

Action on left cosets.

Equations
def add_action.add_left_cosets {α : Type u} [add_group α] (H : add_subgroup α) (x : α) (y : α H) :
α H

Action on left cosets.

Equations
@[protected, instance]
def add_action.quotient {α : Type u} [add_group α] (H : add_subgroup α) :
add_action α H)
Equations
@[protected, instance]
def mul_action.quotient {α : Type u} [group α] (H : subgroup α) :
mul_action α H)
Equations
@[simp]
theorem mul_action.quotient.smul_mk {α : Type u} [group α] (H : subgroup α) (a x : α) :
@[simp]
theorem add_action.quotient.vadd_mk {α : Type u} [add_group α] (H : add_subgroup α) (a x : α) :
@[simp]
theorem mul_action.quotient.smul_coe {α : Type u} [group α] (H : subgroup α) (a x : α) :
a x = a * x
@[simp]
theorem add_action.quotient.vadd_coe {α : Type u} [add_group α] (H : add_subgroup α) (a x : α) :
a +ᵥ x = (a + x)
@[protected, instance]
def mul_action.mul_left_cosets_comp_subtype_val {α : Type u} [group α] (H I : subgroup α) :
Equations
def add_action.of_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α add_action.stabilizer α x) :
β

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

Equations
def mul_action.of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α mul_action.stabilizer α x) :
β

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

Equations
@[simp]
theorem add_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α) :
@[simp]
theorem mul_action.of_quotient_stabilizer_mk (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) :
theorem mul_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α mul_action.stabilizer α x) :
theorem add_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α add_action.stabilizer α x) :
theorem add_action.of_quotient_stabilizer_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α) (g' : α add_action.stabilizer α x) :
theorem mul_action.of_quotient_stabilizer_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α) (g' : α mul_action.stabilizer α x) :
noncomputable def add_action.orbit_equiv_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) :

Orbit-stabilizer theorem.

Equations
noncomputable def mul_action.orbit_equiv_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) :

Orbit-stabilizer theorem.

Equations
@[simp]
theorem add_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) (a : α) :
@[simp]
theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) (a : α) :
@[simp]
@[simp]
theorem mul_action.stabilizer_quotient {G : Type u_1} [group G] (H : subgroup G) :
noncomputable def mul_action.self_equiv_sigma_orbits_quotient_stabilizer' (α : Type u) (β : Type v) [group α] [mul_action α β] {φ : quotient (mul_action.orbit_rel α β) → β} (hφ : function.left_inverse quotient.mk' φ) :
β Σ (ω : quotient (mul_action.orbit_rel α β)), α mul_action.stabilizer α (φ ω)

Class formula : given G a group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be quotient.out', so we provide mul_action.self_equiv_sigma_orbits_quotient_stabilizer as a special case.

Equations
noncomputable def add_action.self_equiv_sigma_orbits_quotient_stabilizer' (α : Type u) (β : Type v) [add_group α] [add_action α β] {φ : quotient (add_action.orbit_rel α β) → β} (hφ : function.left_inverse quotient.mk' φ) :
β Σ (ω : quotient (add_action.orbit_rel α β)), α add_action.stabilizer α (φ ω)

Class formula : given G an additive group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be quotient.out', so we provide add_action.self_equiv_sigma_orbits_quotient_stabilizer as a special case.

Equations

Class formula for a finite group acting on a finite type. See add_action.card_eq_sum_card_add_group_div_card_stabilizer for a specialized version using quotient.out'.

Class formula for a finite group acting on a finite type. See mul_action.card_eq_sum_card_group_div_card_stabilizer for a specialized version using quotient.out'.

noncomputable def add_action.self_equiv_sigma_orbits_quotient_stabilizer (α : Type u) (β : Type v) [add_group α] [add_action α β] :

Class formula. This is a special case of add_action.self_equiv_sigma_orbits_quotient_stabilizer' with φ = quotient.out'.

Equations
noncomputable def mul_action.self_equiv_sigma_orbits_quotient_stabilizer (α : Type u) (β : Type v) [group α] [mul_action α β] :

Class formula. This is a special case of mul_action.self_equiv_sigma_orbits_quotient_stabilizer' with φ = quotient.out'.

Equations

Class formula for a finite group acting on a finite type.

Class formula for a finite group acting on a finite type.

noncomputable def add_action.sigma_fixed_by_equiv_orbits_sum_add_group (α : Type u) (β : Type v) [add_group α] [add_action α β] :
(Σ (a : α), (add_action.fixed_by α β a)) quotient (add_action.orbit_rel α β) × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is an additive group acting on X and X/Gdenotes the quotient of X by the relation orbit_rel G X.

Equations
noncomputable def mul_action.sigma_fixed_by_equiv_orbits_prod_group (α : Type u) (β : Type v) [group α] [mul_action α β] :
(Σ (a : α), (mul_action.fixed_by α β a)) quotient (mul_action.orbit_rel α β) × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is a group acting on X and X/Gdenotes the quotient of X by the relation orbit_rel G X.

Equations

Burnside's lemma : given a finite additive group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

Burnside's lemma : given a finite group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

@[protected, instance]
@[protected, instance]
theorem list.smul_sum {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] {r : α} {l : list β} :
theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [distrib_mul_action M R] (k : M) (h : ∀ (x : R), k x = 0x = 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.

theorem list.smul_prod {α : Type u} {β : Type v} [monoid α] [monoid β] [mul_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
theorem multiset.smul_prod {α : Type u} {β : Type v} [monoid α] [comm_monoid β] [mul_distrib_mul_action α β] {r : α} {s : multiset β} :
theorem finset.smul_prod {α : Type u} {β : Type v} {γ : Type w} [monoid α] [comm_monoid β] [mul_distrib_mul_action α β] {r : α} {f : γ → β} {s : finset γ} :
r ∏ (x : γ) in s, f x = ∏ (x : γ) in s, r f x
theorem subgroup.normal_core_eq_ker {G : Type u_1} [group G] (H : subgroup G) :