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 #
The orbit of an element under an action.
Equations
- mul_action.orbit α b = set.range (λ (x : α), x • b)
The orbit of an element under an action.
Equations
- add_action.orbit α b = set.range (λ (x : α), x +ᵥ b)
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 : α) :
x • b ∈ mul_action.orbit α b
@[simp]
theorem
add_action.mem_orbit
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(b : β)
(x : α) :
x +ᵥ b ∈ add_action.orbit α b
@[simp]
theorem
mul_action.mem_orbit_self
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
(b : β) :
b ∈ mul_action.orbit α b
@[simp]
theorem
add_action.mem_orbit_self
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(b : β) :
b ∈ add_action.orbit α b
theorem
mul_action.orbit_nonempty
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
(b : β) :
(mul_action.orbit α b).nonempty
theorem
add_action.orbit_nonempty
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(b : β) :
(add_action.orbit α b).nonempty
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)
theorem
mul_action.maps_to_smul_orbit
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
(a : α)
(b : β) :
set.maps_to (has_scalar.smul a) (mul_action.orbit α b) (mul_action.orbit α b)
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
theorem
mul_action.smul_orbit_subset
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
(a : α)
(b : β) :
a • mul_action.orbit α b ⊆ mul_action.orbit α b
theorem
mul_action.orbit_smul_subset
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
(a : α)
(b : β) :
mul_action.orbit α (a • b) ⊆ mul_action.orbit α b
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
@[protected, instance]
def
mul_action.orbit.mul_action
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
{b : β} :
mul_action α ↥(mul_action.orbit α b)
Equations
- mul_action.orbit.mul_action = {to_has_scalar := {smul := λ (a : α), set.maps_to.restrict (has_scalar.smul a) (mul_action.orbit α b) (mul_action.orbit α b) _}, one_smul := _, mul_smul := _}
@[protected, instance]
def
add_action.orbit.add_action
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
{b : β} :
add_action α ↥(add_action.orbit α b)
Equations
- add_action.orbit.add_action = {to_has_vadd := {vadd := λ (a : α), set.maps_to.restrict (has_vadd.vadd a) (add_action.orbit α b) (add_action.orbit α b) _}, zero_vadd := _, add_vadd := _}
@[simp]
theorem
add_action.orbit.coe_vadd
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
{b : β}
{a : α}
{b' : ↥(add_action.orbit α b)} :
@[simp]
theorem
mul_action.orbit.coe_smul
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
{b : β}
{a : α}
{b' : ↥(mul_action.orbit α b)} :
The set of elements fixed under the whole action.
Equations
- add_action.fixed_points α β = {b : β | ∀ (x : α), x +ᵥ b = 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
- add_action.fixed_by α β g = {x : β | g +ᵥ x = x}
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
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 α 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
The stabilizer of a point b as a submonoid of α.
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 α.
@[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
@[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
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 : β) :
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
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
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, mul_mem' := _, one_mem' := _, inv_mem' := _}
The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.
Equations
- add_action.stabilizer α b = {carrier := (add_action.stabilizer.add_submonoid α b).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}
@[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
@[simp]
theorem
mul_action.mem_stabilizer_iff
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
{b : β}
{a : α} :
a ∈ mul_action.stabilizer α b ↔ a • b = b
@[simp]
theorem
mul_action.smul_orbit
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
(a : α)
(b : β) :
a • mul_action.orbit α b = mul_action.orbit α b
@[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
@[simp]
theorem
mul_action.orbit_smul
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
(a : α)
(b : β) :
mul_action.orbit α (a • b) = mul_action.orbit α b
@[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
@[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 : β} :
mul_action.orbit α a = mul_action.orbit α b ↔ a ∈ mul_action.orbit α b
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
theorem
add_action.mem_orbit_vadd
(α : Type u)
{β : Type v}
[add_group α]
[add_action α β]
(g : α)
(a : β) :
a ∈ add_action.orbit α (g +ᵥ a)
theorem
mul_action.mem_orbit_smul
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(g : α)
(a : β) :
a ∈ mul_action.orbit α (g • a)
theorem
mul_action.smul_mem_orbit_smul
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(g h : α)
(a : β) :
g • a ∈ mul_action.orbit α (h • a)
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)
The relation 'in the same orbit'.
Equations
- mul_action.orbit_rel α β = {r := λ (a b : β), a ∈ mul_action.orbit α b, iseqv := _}
The relation 'in the same orbit'.
Equations
- add_action.orbit_rel α β = {r := λ (a b : β), a ∈ add_action.orbit α b, iseqv := _}
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_scalar.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 α.
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
theorem
add_action.image_inter_image_iff
{α : Type u}
{β : Type v}
[add_group α]
[add_action α β]
(U V : set β) :
theorem
mul_action.image_inter_image_iff
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
(U V : set β) :
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
- mul_action.self_equiv_sigma_orbits' α β hφ = (equiv.sigma_preimage_equiv quotient.mk').symm.trans (equiv.sigma_congr_right (λ («ω» : quotient (mul_action.orbit_rel α β)), equiv.subtype_equiv_right _))
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
- add_action.self_equiv_sigma_orbits' α β hφ = (equiv.sigma_preimage_equiv quotient.mk').symm.trans (equiv.sigma_congr_right (λ («ω» : quotient (add_action.orbit_rel α β)), equiv.subtype_equiv_right _))
noncomputable
def
mul_action.self_equiv_sigma_orbits
(α : Type u)
(β : Type v)
[group α]
[mul_action α β] :
β ≃ Σ («ω» : quotient (mul_action.orbit_rel α β)), ↥(mul_action.orbit α «ω».out')
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 α β] :
β ≃ Σ («ω» : quotient (add_action.orbit_rel α β)), ↥(add_action.orbit α «ω».out')
Decomposition of a type X as a disjoint union of its orbits under an additive group
action.
Equations
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⁻¹.
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
- mul_action.stabilizer_equiv_stabilizer_of_orbit_rel h = let g : α := classical.some h in have hg : g • y = x, from _, have this : mul_action.stabilizer α x = subgroup.map (mul_equiv.to_monoid_hom (⇑mul_aut.conj g)) (mul_action.stabilizer α y), from _, (mul_equiv.subgroup_congr this).trans (mul_equiv.subgroup_map (⇑mul_aut.conj g) (mul_action.stabilizer α y)).symm
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).
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
- add_action.stabilizer_equiv_stabilizer_of_orbit_rel h = let g : α := classical.some h in have hg : g +ᵥ y = x, from _, have this : add_action.stabilizer α x = add_subgroup.map (add_equiv.to_add_monoid_hom (⇑add_aut.conj g)) (add_action.stabilizer α y), from _, (add_equiv.add_subgroup_congr this).trans (add_equiv.add_subgroup_map (⇑add_aut.conj g) (add_action.stabilizer α y)).symm
@[class]
structure
mul_action.quotient_action
{α : Type u}
(β : Type v)
[group α]
[monoid β]
[mul_action β α]
(H : subgroup α) :
Prop
A typeclass for when a mul_action β α descends to the quotient α ⧸ H.
@[class]
structure
add_action.quotient_action
{α : Type u_1}
(β : Type u_2)
[add_group α]
[add_monoid β]
[add_action β α]
(H : add_subgroup α) :
Prop
A typeclass for when an add_action β α descends to the quotient α ⧸ H.
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
add_action.quotient
{α : Type u}
(β : Type v)
[add_group α]
[add_monoid β]
[add_action β α]
(H : add_subgroup α)
[add_action.quotient_action β H] :
add_action β (α ⧸ H)
Equations
- add_action.quotient β H = {to_has_vadd := {vadd := λ (b : β), quotient.map' (has_vadd.vadd b) _}, zero_vadd := _, add_vadd := _}
@[protected, instance]
def
mul_action.quotient
{α : Type u}
(β : Type v)
[group α]
[monoid β]
[mul_action β α]
(H : subgroup α)
[mul_action.quotient_action β H] :
mul_action β (α ⧸ H)
Equations
- mul_action.quotient β H = {to_has_scalar := {smul := λ (b : β), quotient.map' (has_scalar.smul b) _}, one_smul := _, mul_smul := _}
@[simp]
theorem
mul_action.quotient.smul_mk
{α : Type u}
{β : Type v}
[group α]
[monoid β]
[mul_action β α]
(H : subgroup α)
[mul_action.quotient_action β H]
(a : β)
(x : α) :
a • quotient_group.mk x = quotient_group.mk (a • x)
@[simp]
theorem
add_action.quotient.vadd_mk
{α : Type u}
{β : Type v}
[add_group α]
[add_monoid β]
[add_action β α]
(H : add_subgroup α)
[add_action.quotient_action β H]
(a : β)
(x : α) :
a +ᵥ quotient_add_group.mk x = quotient_add_group.mk (a +ᵥ x)
@[simp]
theorem
mul_action.quotient.smul_coe
{α : Type u}
{β : Type v}
[group α]
[monoid β]
[mul_action β α]
(H : subgroup α)
[mul_action.quotient_action β H]
(a : β)
(x : α) :
@[simp]
theorem
add_action.quotient.vadd_coe
{α : Type u}
{β : Type v}
[add_group α]
[add_monoid β]
[add_action β α]
(H : add_subgroup α)
[add_action.quotient_action β H]
(a : β)
(x : α) :
The canonical map to the left cosets.
Equations
- mul_action_hom.to_quotient H = {to_fun := coe coe_to_lift, map_smul' := _}
@[simp]
theorem
mul_action_hom.to_quotient_apply
{α : Type u}
[group α]
(H : subgroup α)
(g : α) :
⇑(mul_action_hom.to_quotient H) g = ↑g
@[protected, instance]
def
mul_action.mul_left_cosets_comp_subtype_val
{α : Type u}
[group α]
(H I : subgroup α) :
mul_action ↥I (α ⧸ H)
Equations
@[protected, instance]
def
add_action.add_left_cosets_comp_subtype_val
{α : Type u}
[add_group α]
(H I : add_subgroup α) :
add_action ↥I (α ⧸ H)
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
- add_action.of_quotient_stabilizer α x g = quotient.lift_on' g (λ (_x : α), _x +ᵥ x) _
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
- mul_action.of_quotient_stabilizer α x g = quotient.lift_on' g (λ (_x : α), _x • x) _
@[simp]
theorem
add_action.of_quotient_stabilizer_mk
(α : Type u)
{β : Type v}
[add_group α]
[add_action α β]
(x : β)
(g : α) :
add_action.of_quotient_stabilizer α x (quotient_add_group.mk g) = g +ᵥ 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 : α ⧸ 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) :
add_action.of_quotient_stabilizer α x (g +ᵥ g') = g +ᵥ add_action.of_quotient_stabilizer α x g'
theorem
mul_action.of_quotient_stabilizer_smul
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(x : β)
(g : α)
(g' : α ⧸ 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 : β) :
theorem
add_action.injective_of_quotient_stabilizer
(α : Type u)
{β : Type v}
[add_group α]
[add_action α β]
(x : β) :
noncomputable
def
add_action.orbit_equiv_quotient_stabilizer
(α : Type u)
{β : Type v}
[add_group α]
[add_action α β]
(b : β) :
↥(add_action.orbit α b) ≃ α ⧸ add_action.stabilizer α b
Orbit-stabilizer theorem.
Equations
- add_action.orbit_equiv_quotient_stabilizer α b = (equiv.of_bijective (λ (g : α ⧸ add_action.stabilizer α b), ⟨add_action.of_quotient_stabilizer α b g, _⟩) _).symm
noncomputable
def
mul_action.orbit_equiv_quotient_stabilizer
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(b : β) :
↥(mul_action.orbit α b) ≃ α ⧸ mul_action.stabilizer α b
Orbit-stabilizer theorem.
Equations
- mul_action.orbit_equiv_quotient_stabilizer α b = (equiv.of_bijective (λ (g : α ⧸ mul_action.stabilizer α b), ⟨mul_action.of_quotient_stabilizer α b g, _⟩) _).symm
noncomputable
def
add_action.orbit_sum_stabilizer_equiv_add_group
(α : Type u)
{β : Type v}
[add_group α]
[add_action α β]
(b : β) :
↥(add_action.orbit α b) × ↥(add_action.stabilizer α b) ≃ α
Orbit-stabilizer theorem.
noncomputable
def
mul_action.orbit_prod_stabilizer_equiv_group
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(b : β) :
↥(mul_action.orbit α b) × ↥(mul_action.stabilizer α b) ≃ α
Orbit-stabilizer theorem.
theorem
add_action.card_orbit_add_card_stabilizer_eq_card_add_group
(α : Type u)
{β : Type v}
[add_group α]
[add_action α β]
(b : β)
[fintype α]
[fintype ↥(add_action.orbit α b)]
[fintype ↥(add_action.stabilizer α b)] :
(fintype.card ↥(add_action.orbit α b)) * fintype.card ↥(add_action.stabilizer α b) = fintype.card α
Orbit-stabilizer theorem.
theorem
mul_action.card_orbit_mul_card_stabilizer_eq_card_group
(α : Type u)
{β : Type v}
[group α]
[mul_action α β]
(b : β)
[fintype α]
[fintype ↥(mul_action.orbit α b)]
[fintype ↥(mul_action.stabilizer α b)] :
(fintype.card ↥(mul_action.orbit α b)) * fintype.card ↥(mul_action.stabilizer α b) = fintype.card α
Orbit-stabilizer theorem.
@[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]
theorem
add_action.stabilizer_quotient
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
add_action.stabilizer G ↑0 = H
@[simp]
theorem
mul_action.stabilizer_quotient
{G : Type u_1}
[group G]
(H : subgroup G) :
mul_action.stabilizer G ↑1 = H
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
- mul_action.self_equiv_sigma_orbits_quotient_stabilizer' α β hφ = (mul_action.self_equiv_sigma_orbits' α β hφ).trans (equiv.sigma_congr_right (λ («ω» : quotient (mul_action.orbit_rel α β)), mul_action.orbit_equiv_quotient_stabilizer α (φ «ω»)))
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
- add_action.self_equiv_sigma_orbits_quotient_stabilizer' α β hφ = (add_action.self_equiv_sigma_orbits' α β hφ).trans (equiv.sigma_congr_right (λ («ω» : quotient (add_action.orbit_rel α β)), add_action.orbit_equiv_quotient_stabilizer α (φ «ω»)))
theorem
add_action.card_eq_sum_card_add_group_sub_card_stabilizer'
(α : Type u)
(β : Type v)
[add_group α]
[add_action α β]
[fintype α]
[fintype β]
[fintype (quotient (add_action.orbit_rel α β))]
[Π (b : β), fintype ↥(add_action.stabilizer α b)]
{φ : quotient (add_action.orbit_rel α β) → β}
(hφ : function.left_inverse quotient.mk' φ) :
fintype.card β = ∑ («ω» : quotient (add_action.orbit_rel α β)), fintype.card α / fintype.card ↥(add_action.stabilizer α (φ «ω»))
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'.
theorem
mul_action.card_eq_sum_card_group_div_card_stabilizer'
(α : Type u)
(β : Type v)
[group α]
[mul_action α β]
[fintype α]
[fintype β]
[fintype (quotient (mul_action.orbit_rel α β))]
[Π (b : β), fintype ↥(mul_action.stabilizer α b)]
{φ : quotient (mul_action.orbit_rel α β) → β}
(hφ : function.left_inverse quotient.mk' φ) :
fintype.card β = ∑ («ω» : quotient (mul_action.orbit_rel α β)), fintype.card α / fintype.card ↥(mul_action.stabilizer α (φ «ω»))
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 α β] :
β ≃ Σ («ω» : quotient (add_action.orbit_rel α β)), α ⧸ add_action.stabilizer α «ω».out'
Class formula. This is a special case of
add_action.self_equiv_sigma_orbits_quotient_stabilizer' with φ = quotient.out'.
noncomputable
def
mul_action.self_equiv_sigma_orbits_quotient_stabilizer
(α : Type u)
(β : Type v)
[group α]
[mul_action α β] :
β ≃ Σ («ω» : quotient (mul_action.orbit_rel α β)), α ⧸ mul_action.stabilizer α «ω».out'
Class formula. This is a special case of
mul_action.self_equiv_sigma_orbits_quotient_stabilizer' with φ = quotient.out'.
theorem
mul_action.card_eq_sum_card_group_div_card_stabilizer
(α : Type u)
(β : Type v)
[group α]
[mul_action α β]
[fintype α]
[fintype β]
[fintype (quotient (mul_action.orbit_rel α β))]
[Π (b : β), fintype ↥(mul_action.stabilizer α b)] :
fintype.card β = ∑ («ω» : quotient (mul_action.orbit_rel α β)), fintype.card α / fintype.card ↥(mul_action.stabilizer α «ω».out')
Class formula for a finite group acting on a finite type.
theorem
add_action.card_eq_sum_card_add_group_sub_card_stabilizer
(α : Type u)
(β : Type v)
[add_group α]
[add_action α β]
[fintype α]
[fintype β]
[fintype (quotient (add_action.orbit_rel α β))]
[Π (b : β), fintype ↥(add_action.stabilizer α b)] :
fintype.card β = ∑ («ω» : quotient (add_action.orbit_rel α β)), fintype.card α / fintype.card ↥(add_action.stabilizer α «ω».out')
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
- add_action.sigma_fixed_by_equiv_orbits_sum_add_group α β = ((((((((equiv.subtype_prod_equiv_sigma_subtype (λ (a : α) (x : β), x ∈ add_action.fixed_by α β a)).symm.trans ((equiv.prod_comm α β).subtype_equiv _)).trans (equiv.subtype_prod_equiv_sigma_subtype (λ (b : β) (a : α), a ∈ add_action.stabilizer α b))).trans (add_action.self_equiv_sigma_orbits α β).sigma_congr_left').trans (equiv.sigma_assoc (λ («ω» : quotient (add_action.orbit_rel α β)) (b : ↥(add_action.orbit α «ω».out')), ↥(add_action.stabilizer α ↑b)))).trans (equiv.sigma_congr_right (λ («ω» : quotient (add_action.orbit_rel α β)), equiv.sigma_congr_right (λ (_x : ↥(add_action.orbit α «ω».out')), add_action.sigma_fixed_by_equiv_orbits_sum_add_group._match_1 α β «ω» _x)))).trans (equiv.sigma_congr_right (λ («ω» : quotient (add_action.orbit_rel α β)), equiv.sigma_equiv_prod ↥(add_action.orbit α «ω».out') ↥(add_action.stabilizer α «ω».out')))).trans (equiv.sigma_congr_right (λ («ω» : quotient (add_action.orbit_rel α β)), add_action.orbit_sum_stabilizer_equiv_add_group α «ω».out'))).trans (equiv.sigma_equiv_prod (quotient (add_action.orbit_rel α β)) α)
- add_action.sigma_fixed_by_equiv_orbits_sum_add_group._match_1 α β «ω» ⟨b, hb⟩ = (add_action.stabilizer_equiv_stabilizer_of_orbit_rel hb).to_equiv
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
- mul_action.sigma_fixed_by_equiv_orbits_prod_group α β = ((((((((equiv.subtype_prod_equiv_sigma_subtype (λ (a : α) (x : β), x ∈ mul_action.fixed_by α β a)).symm.trans ((equiv.prod_comm α β).subtype_equiv _)).trans (equiv.subtype_prod_equiv_sigma_subtype (λ (b : β) (a : α), a ∈ mul_action.stabilizer α b))).trans (mul_action.self_equiv_sigma_orbits α β).sigma_congr_left').trans (equiv.sigma_assoc (λ («ω» : quotient (mul_action.orbit_rel α β)) (b : ↥(mul_action.orbit α «ω».out')), ↥(mul_action.stabilizer α ↑b)))).trans (equiv.sigma_congr_right (λ («ω» : quotient (mul_action.orbit_rel α β)), equiv.sigma_congr_right (λ (_x : ↥(mul_action.orbit α «ω».out')), mul_action.sigma_fixed_by_equiv_orbits_prod_group._match_1 α β «ω» _x)))).trans (equiv.sigma_congr_right (λ («ω» : quotient (mul_action.orbit_rel α β)), equiv.sigma_equiv_prod ↥(mul_action.orbit α «ω».out') ↥(mul_action.stabilizer α «ω».out')))).trans (equiv.sigma_congr_right (λ («ω» : quotient (mul_action.orbit_rel α β)), mul_action.orbit_prod_stabilizer_equiv_group α «ω».out'))).trans (equiv.sigma_equiv_prod (quotient (mul_action.orbit_rel α β)) α)
- mul_action.sigma_fixed_by_equiv_orbits_prod_group._match_1 α β «ω» ⟨b, hb⟩ = (mul_action.stabilizer_equiv_stabilizer_of_orbit_rel hb).to_equiv
theorem
add_action.sum_card_fixed_by_eq_card_orbits_add_card_add_group
(α : Type u)
(β : Type v)
[add_group α]
[add_action α β]
[fintype α]
[Π (a : α), fintype ↥(add_action.fixed_by α β a)]
[fintype (quotient (add_action.orbit_rel α β))] :
∑ (a : α), fintype.card ↥(add_action.fixed_by α β a) = (fintype.card (quotient (add_action.orbit_rel α β))) * fintype.card α
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.
theorem
mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group
(α : Type u)
(β : Type v)
[group α]
[mul_action α β]
[fintype α]
[Π (a : α), fintype ↥(mul_action.fixed_by α β a)]
[fintype (quotient (mul_action.orbit_rel α β))] :
∑ (a : α), fintype.card ↥(mul_action.fixed_by α β a) = (fintype.card (quotient (mul_action.orbit_rel α β))) * fintype.card α
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]
def
add_action.is_pretransitive_quotient
(G : Type u_1)
[add_group G]
(H : add_subgroup G) :
add_action.is_pretransitive G (G ⧸ H)
@[protected, instance]
def
mul_action.is_pretransitive_quotient
(G : Type u_1)
[group G]
(H : subgroup G) :
mul_action.is_pretransitive G (G ⧸ H)
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.
theorem
subgroup.normal_core_eq_ker
{G : Type u_1}
[group G]
(H : subgroup G) :
H.normal_core = (mul_action.to_perm_hom G (G ⧸ H)).ker
@[protected, instance]
noncomputable
def
subgroup.fintype_quotient_normal_core
{G : Type u_1}
[group G]
(H : subgroup G)
[fintype (G ⧸ H)] :
fintype (G ⧸ H.normal_core)
Equations
- H.fintype_quotient_normal_core = _.mpr (fintype.of_equiv ↥((mul_action.to_perm_hom G (G ⧸ H)).range) (quotient_group.quotient_ker_equiv_range (mul_action.to_perm_hom G (G ⧸ H))).symm.to_equiv)