mathlib documentation

group_theory.group_action.group

Group actions applied to various types of group #

This file contains lemmas about smul on group_with_zero, and group.

@[simp]
theorem inv_smul_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (c : α) (x : β) :
c⁻¹ c x = x
@[simp]
theorem neg_vadd_vadd {α : Type u} {β : Type v} [add_group α] [add_action α β] (c : α) (x : β) :
-c +ᵥ (c +ᵥ x) = x
@[simp]
theorem vadd_neg_vadd {α : Type u} {β : Type v} [add_group α] [add_action α β] (c : α) (x : β) :
c +ᵥ (-c +ᵥ x) = x
@[simp]
theorem smul_inv_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (c : α) (x : β) :
c c⁻¹ x = x
def mul_action.to_perm {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) :

Given an action of a group α on β, each g : α defines a permutation of β.

Equations
def add_action.to_perm {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) :

Given an action of an additive group α on β, each g : α defines a permutation of β.

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

Given an action of a group α on a set β, each g : α defines a permutation of β.

Equations
def add_action.to_perm_hom (β : Type v) (α : Type u_1) [add_group α] [add_action α β] :

Given an action of a additive group α on a set β, each g : α defines a permutation of β.

Equations
theorem neg_vadd_eq_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {a : α} {x y : β} :
-a +ᵥ x = y x = a +ᵥ y
theorem inv_smul_eq_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a : α} {x y : β} :
a⁻¹ x = y x = a y
theorem eq_inv_smul_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a : α} {x y : β} :
x = a⁻¹ y a x = y
theorem eq_neg_vadd_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {a : α} {x y : β} :
x = -a +ᵥ y a +ᵥ x = y
theorem smul_inv {α : Type u} {β : Type v} [group α] [mul_action α β] [group β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :
theorem mul_action.bijective {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) :
function.bijective (λ (b : β), g b)
theorem add_action.bijective {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) :
function.bijective (λ (b : β), g +ᵥ b)
theorem mul_action.injective {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) :
function.injective (λ (b : β), g b)
theorem add_action.injective {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) :
function.injective (λ (b : β), g +ᵥ b)
theorem vadd_left_cancel {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) {x y : β} (h : g +ᵥ x = g +ᵥ y) :
x = y
theorem smul_left_cancel {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) {x y : β} (h : g x = g y) :
x = y
@[simp]
theorem vadd_left_cancel_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) {x y : β} :
g +ᵥ x = g +ᵥ y x = y
@[simp]
theorem smul_left_cancel_iff {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) {x y : β} :
g x = g y x = y
theorem smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) {x y : β} :
g x = y x = g⁻¹ y
theorem vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) {x y : β} :
g +ᵥ x = y x = -g +ᵥ y
@[simp]
theorem inv_smul_smul' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {c : α} (hc : c 0) (x : β) :
c⁻¹ c x = x
@[simp]
theorem smul_inv_smul' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {c : α} (hc : c 0) (x : β) :
c c⁻¹ x = x
theorem inv_smul_eq_iff' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) {x y : β} :
a⁻¹ x = y x = a y
theorem eq_inv_smul_iff' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) {x y : β} :
x = a⁻¹ y a x = y
theorem smul_eq_zero_iff_eq {α : Type u} {β : Type v} [group α] [add_monoid β] [distrib_mul_action α β] (a : α) {x : β} :
a x = 0 x = 0
theorem smul_ne_zero_iff_ne {α : Type u} {β : Type v} [group α] [add_monoid β] [distrib_mul_action α β] (a : α) {x : β} :
a x 0 x 0
theorem smul_eq_zero_iff_eq' {α : Type u} {β : Type v} [group_with_zero α] [add_monoid β] [distrib_mul_action α β] {a : α} (ha : a 0) {x : β} :
a x = 0 x = 0
theorem smul_ne_zero_iff_ne' {α : Type u} {β : Type v} [group_with_zero α] [add_monoid β] [distrib_mul_action α β] {a : α} (ha : a 0) {x : β} :
a x 0 x 0
@[simp]
theorem arrow_action_to_has_scalar_smul {G : Type u_1} {A : Type u_2} {B : Type u_3} [group G] [mul_action G A] (g : G) (F : A → B) (a : A) :
(g F) a = F (g⁻¹ a)
def arrow_action {G : Type u_1} {A : Type u_2} {B : Type u_3} [group G] [mul_action G A] :
mul_action G (A → B)

If G acts on A, then it acts also on A → B, by (g • F) a = F (g⁻¹ • a).

Equations
@[simp]
theorem mul_aut_arrow_apply_symm_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [group G] [mul_action G A] [group H] (g : G) (F : A → H) (ᾰ : A) :
@[simp]
theorem mul_aut_arrow_apply_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [group G] [mul_action G A] [group H] (g : G) (F : A → H) (ᾰ : A) :
(mul_aut_arrow g) F = (g F)
def mul_aut_arrow {G : Type u_1} {A : Type u_2} {H : Type u_3} [group G] [mul_action G A] [group H] :
G →* mul_aut (A → H)

Given groups G H with G acting on A, G acts by multiplicative automorphisms on A → H.

Equations
theorem is_add_unit.vadd_left_cancel {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {a : α} (ha : is_add_unit a) {x y : β} :
a +ᵥ x = a +ᵥ y x = y
theorem is_unit.smul_left_cancel {α : Type u} {β : Type v} [monoid α] [mul_action α β] {a : α} (ha : is_unit a) {x y : β} :
a x = a y x = y
@[simp]
theorem is_unit.smul_eq_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] {u : α} (hu : is_unit u) {x : β} :
u x = 0 x = 0