group_theory.group_action.basic

source

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

set β

The orbit of an element under an action.

Equations

mul_action.orbit α b = set.range (λ (x : α), x • b)

Instances for ↥mul_action.orbit

source

def add_action.orbit (α : Type u) {β : Type v} [add_monoid α] [add_action α β] (b : β) :

set β

The orbit of an element under an action.

Equations

add_action.orbit α b = set.range (λ (x : α), x +ᵥ b)

Instances for ↥add_action.orbit

source

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₂

source

theorem mul_action.mem_orbit_iff {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b₁ b₂ : β} :

b₂ ∈ mul_action.orbit α b₁ ↔ ∃ (x : α), x • b₁ = b₂

source

@[simp]

theorem mul_action.mem_orbit {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) (x : α) :

x • b ∈ mul_action.orbit α b

source

@[simp]

theorem add_action.mem_orbit {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) (x : α) :

x +ᵥ b ∈ add_action.orbit α b

source

@[simp]

theorem mul_action.mem_orbit_self {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :

b ∈ mul_action.orbit α b

source

@[simp]

theorem add_action.mem_orbit_self {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) :

b ∈ add_action.orbit α b

source

theorem mul_action.orbit_nonempty {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :

(mul_action.orbit α b).nonempty

source

theorem add_action.orbit_nonempty {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) :

(add_action.orbit α b).nonempty

source

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)

source

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)

source

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

source

theorem mul_action.smul_orbit_subset {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :

a • mul_action.orbit α b ⊆ mul_action.orbit α b

source

theorem mul_action.orbit_smul_subset {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :

mul_action.orbit α (a • b) ⊆ mul_action.orbit α b

source

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

source

@[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 := _}

source

@[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 := _}

source

@[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'

source

@[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'

source

def add_action.fixed_points (α : Type u) (β : Type v) [add_monoid α] [add_action α β] :

set β

The set of elements fixed under the whole action.

Equations

add_action.fixed_points α β = {b : β | ∀ (x : α), x +ᵥ b = b}

source

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

set β

The set of elements fixed under the whole action.

Equations

mul_action.fixed_points α β = {b : β | ∀ (x : α), x • b = b}

source

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

add_action.fixed_by α β g = {x : β | g +ᵥ x = x}

source

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

mul_action.fixed_by α β g = {x : β | g • x = x}

source

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

source

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

source

@[simp]

theorem mul_action.mem_fixed_points {α : Type u} (β : Type v) [monoid α] [mul_action α β] {b : β} :

b ∈ mul_action.fixed_points α β ↔ ∀ (x : α), x • b = b

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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

submonoid α

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

Equations

mul_action.stabilizer.submonoid α b = {carrier := {a : α | a • b = b}, mul_mem' := _, one_mem' := _}

source

def add_action.stabilizer.add_submonoid (α : Type u) {β : Type v} [add_monoid α] [add_action α β] (b : β) :

add_submonoid α

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

Equations

add_action.stabilizer.add_submonoid α b = {carrier := {a : α | a +ᵥ b = b}, add_mem' := _, zero_mem' := _}

source

@[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

source

@[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

source

theorem add_action.orbit_eq_univ (α : Type u) {β : Type v} [add_monoid α] [add_action α β] [add_action.is_pretransitive α β] (x : β) :

add_action.orbit α x = set.univ

source

theorem mul_action.orbit_eq_univ (α : Type u) {β : Type v} [monoid α] [mul_action α β] [mul_action.is_pretransitive α β] (x : β) :

mul_action.orbit α x = set.univ

source

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

source

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

source

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

subgroup α

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' := _}

source

def add_action.stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) :

add_subgroup α

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' := _}

source

@[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

source

@[simp]

theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {a : α} :

a ∈ mul_action.stabilizer α b ↔ a • b = b

source

@[simp]

theorem mul_action.smul_orbit {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (b : β) :

a • mul_action.orbit α b = mul_action.orbit α b

source

@[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

source

@[simp]

theorem mul_action.orbit_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (b : β) :

mul_action.orbit α (a • b) = mul_action.orbit α b

source

@[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

source

@[protected, instance]

def mul_action.orbit.is_pretransitive {α : Type u} {β : Type v} [group α] [mul_action α β] (x : β) :

mul_action.is_pretransitive α ↥(mul_action.orbit α x)

The action of a group on an orbit is transitive.

source

@[protected, instance]

def add_action.orbit.is_pretransitive {α : Type u} {β : Type v} [add_group α] [add_action α β] (x : β) :

add_action.is_pretransitive α ↥(add_action.orbit α x)

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

source

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

source

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

source

theorem add_action.mem_orbit_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (g : α) (a : β) :

a ∈ add_action.orbit α (g +ᵥ a)

source

theorem mul_action.mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g : α) (a : β) :

a ∈ mul_action.orbit α (g • a)

source

theorem mul_action.smul_mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g h : α) (a : β) :

g • a ∈ mul_action.orbit α (h • a)

source

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)

source

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

setoid β

The relation 'in the same orbit'.

Equations

mul_action.orbit_rel α β = {r := λ (a b : β), a ∈ mul_action.orbit α b, iseqv := _}

source

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

setoid β

The relation 'in the same orbit'.

Equations

add_action.orbit_rel α β = {r := λ (a b : β), a ∈ add_action.orbit α b, iseqv := _}

source

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

source

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

source

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

source

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

source

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_fiber_equiv quotient.mk').symm.trans (equiv.sigma_congr_right (λ (ω : quotient (mul_action.orbit_rel α β)), equiv.subtype_equiv_right _))

source

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_fiber_equiv quotient.mk').symm.trans (equiv.sigma_congr_right (λ (ω : quotient (add_action.orbit_rel α β)), equiv.subtype_equiv_right _))

source

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

mul_action.self_equiv_sigma_orbits α β = mul_action.self_equiv_sigma_orbits' α β _

source

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

add_action.self_equiv_sigma_orbits α β = add_action.self_equiv_sigma_orbits' α β _

source

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⁻¹.

source

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

source

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

source

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

source

@[class]

structure mul_action.quotient_action {α : Type u} (β : Type v) [group α] [monoid β] [mul_action β α] (H : subgroup α) :

Prop

inv_mul_mem : ∀ (b : β) {a a' : α}, a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H

A typeclass for when a mul_action β α descends to the quotient α ⧸ H.

Instances of this typeclass

source

@[class]

structure add_action.quotient_action {α : Type u_1} (β : Type u_2) [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) :

Prop

inv_mul_mem : ∀ (b : β) {a a' : α}, -a + a' ∈ H → -(b +ᵥ a) + (b +ᵥ a') ∈ H

A typeclass for when an add_action β α descends to the quotient α ⧸ H.

Instances of this typeclass

source

@[protected, instance]

def mul_action.left_quotient_action {α : Type u} [group α] (H : subgroup α) :

mul_action.quotient_action α H

source

@[protected, instance]

def add_action.left_quotient_action {α : Type u} [add_group α] (H : add_subgroup α) :

add_action.quotient_action α H

source

@[protected, instance]

def add_action.right_quotient_action {α : Type u} [add_group α] (H : add_subgroup α) :

add_action.quotient_action ↥(H.normalizer.opposite) H

source

@[protected, instance]

def mul_action.right_quotient_action {α : Type u} [group α] (H : subgroup α) :

mul_action.quotient_action ↥(H.normalizer.opposite) H

source

@[protected, instance]

def add_action.right_quotient_action' {α : Type u} [add_group α] (H : add_subgroup α) [hH : H.normal] :

add_action.quotient_action αᵃᵒᵖ H

source

@[protected, instance]

def mul_action.right_quotient_action' {α : Type u} [group α] (H : subgroup α) [hH : H.normal] :

mul_action.quotient_action αᵐᵒᵖ H

source

@[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 := _}

source

@[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 := _}

source

@[simp]

theorem mul_action.quotient.smul_mk {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (a : α) :

b • quotient_group.mk a = quotient_group.mk (b • a)

source

@[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] (b : β) (a : α) :

b +ᵥ quotient_add_group.mk a = quotient_add_group.mk (b +ᵥ a)

source

@[simp]

theorem mul_action.quotient.smul_coe {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (a : α) :

b • ↑a = ↑(b • a)

source

@[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] (b : β) (a : α) :

b +ᵥ ↑a = ↑(b +ᵥ a)

source

@[simp]

theorem mul_action.quotient.mk_smul_out' {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (q : α ⧸ H) :

quotient_group.mk (b • quotient.out' q) = b • q

source

@[simp]

theorem add_action.quotient.mk_vadd_out' {α : Type u} {β : Type v} [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] (b : β) (q : α ⧸ H) :

quotient_add_group.mk (b +ᵥ quotient.out' q) = b +ᵥ q

source

@[simp]

theorem mul_action.quotient.coe_smul_out' {α : Type u} {β : Type v} [group α] [monoid β] [mul_action β α] (H : subgroup α) [mul_action.quotient_action β H] (b : β) (q : α ⧸ H) :

↑(b • quotient.out' q) = b • q

source

@[simp]

theorem add_action.quotient.coe_vadd_out' {α : Type u} {β : Type v} [add_group α] [add_monoid β] [add_action β α] (H : add_subgroup α) [add_action.quotient_action β H] (b : β) (q : α ⧸ H) :

↑(b +ᵥ quotient.out' q) = b +ᵥ q

source

def mul_action_hom.to_quotient {α : Type u} [group α] (H : subgroup α) :

α →[α] α ⧸ H

The canonical map to the left cosets.

Equations

mul_action_hom.to_quotient H = {to_fun := coe coe_to_lift, map_smul' := _}

source

@[simp]

theorem mul_action_hom.to_quotient_apply {α : Type u} [group α] (H : subgroup α) (g : α) :

⇑(mul_action_hom.to_quotient H) g = ↑g

source

@[protected, instance]

def mul_action.mul_left_cosets_comp_subtype_val {α : Type u} [group α] (H I : subgroup α) :

mul_action ↥I (α ⧸ H)

Equations

mul_action.mul_left_cosets_comp_subtype_val H I = mul_action.comp_hom (α ⧸ H) I.subtype

source

@[protected, instance]

def add_action.add_left_cosets_comp_subtype_val {α : Type u} [add_group α] (H I : add_subgroup α) :

add_action ↥I (α ⧸ H)

Equations

add_action.add_left_cosets_comp_subtype_val H I = add_action.comp_hom (α ⧸ H) I.subtype

source

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) _

source

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) _

source

@[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

source

@[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

source

theorem mul_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) (g : α ⧸ mul_action.stabilizer α x) :

mul_action.of_quotient_stabilizer α x g ∈ mul_action.orbit α x

source

theorem add_action.of_quotient_stabilizer_mem_orbit (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) (g : α ⧸ add_action.stabilizer α x) :

add_action.of_quotient_stabilizer α x g ∈ add_action.orbit α x

source

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'

source

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'

source

theorem mul_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (x : β) :

function.injective (mul_action.of_quotient_stabilizer α x)

source

theorem add_action.injective_of_quotient_stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (x : β) :

function.injective (add_action.of_quotient_stabilizer α x)

source

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

source

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

source

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.

Equations

add_action.orbit_sum_stabilizer_equiv_add_group α b = ((add_action.orbit_equiv_quotient_stabilizer α b).prod_congr (equiv.refl ↥(add_action.stabilizer α b))).trans add_subgroup.add_group_equiv_quotient_times_add_subgroup.symm

source

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.

Equations

mul_action.orbit_prod_stabilizer_equiv_group α b = ((mul_action.orbit_equiv_quotient_stabilizer α b).prod_congr (equiv.refl ↥(mul_action.stabilizer α b))).trans subgroup.group_equiv_quotient_times_subgroup.symm

source

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.

source

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.

source

@[simp]

theorem add_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) (a : α) :

↑(⇑((add_action.orbit_equiv_quotient_stabilizer α b).symm) ↑a) = a +ᵥ b

source

@[simp]

theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) (a : α) :

↑(⇑((mul_action.orbit_equiv_quotient_stabilizer α b).symm) ↑a) = a • b

source

@[simp]

theorem add_action.stabilizer_quotient {G : Type u_1} [add_group G] (H : add_subgroup G) :

add_action.stabilizer G ↑0 = H

source

@[simp]

theorem mul_action.stabilizer_quotient {G : Type u_1} [group G] (H : subgroup G) :

mul_action.stabilizer G ↑1 = H

source

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 α (φ ω)))

source

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 α (φ ω)))

source

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 β = finset.univ.sum (λ (ω : 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'.

source

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 β = finset.univ.sum (λ (ω : 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'.

source

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

Equations

add_action.self_equiv_sigma_orbits_quotient_stabilizer α β = add_action.self_equiv_sigma_orbits_quotient_stabilizer' α β _

source

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

Equations

mul_action.self_equiv_sigma_orbits_quotient_stabilizer α β = mul_action.self_equiv_sigma_orbits_quotient_stabilizer' α β _

source

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 β = finset.univ.sum (λ (ω : quotient (mul_action.orbit_rel α β)), fintype.card α / fintype.card ↥(mul_action.stabilizer α ω.out'))

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

source

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 β = finset.univ.sum (λ (ω : quotient (add_action.orbit_rel α β)), fintype.card α / fintype.card ↥(add_action.stabilizer α ω.out'))

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

source

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

source

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

source

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

finset.univ.sum (λ (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.

source

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

finset.univ.sum (λ (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.

source

@[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)

source

@[protected, instance]

def mul_action.is_pretransitive_quotient (G : Type u_1) [group G] (H : subgroup G) :

mul_action.is_pretransitive G (G ⧸ H)

source

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.

source

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

source

@[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)

mathlib documentation

Basic properties of group actions #

Main definitions #