mathlib documentation

group_theory.group_action.group

Group actions applied to various types of group #

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

@[simp]
theorem units.inv_smul_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) (x : β) :
@[simp]
theorem add_units.neg_vadd_vadd {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (u : add_units α) (x : β) :
-u +ᵥ (u +ᵥ x) = x
@[simp]
theorem units.smul_inv_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) (x : β) :
@[simp]
theorem add_units.vadd_neg_vadd {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (u : add_units α) (x : β) :
u +ᵥ (-u +ᵥ x) = x
def add_units.vadd_perm {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (u : add_units α) :

If an additive monoid α acts on β, then each u : add_units α defines a permutation of β.

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

If a monoid α acts on β, then each u : units α defines a permutation of β.

Equations
def units.smul_perm_hom {α : Type u} {β : Type v} [monoid α] [mul_action α β] :

If a monoid α acts on β, then each u : units α defines a permutation of β.

Equations
def add_units.vadd_perm_hom {β : Type v} {M : Type u_1} [add_monoid M] [add_action M β] :

If an additive monoid α acts on β, then each u : add_units α defines a permutation of β.

Equations
@[simp]
theorem add_units.vadd_left_cancel {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (u : add_units α) {x y : β} :
u +ᵥ x = u +ᵥ y x = y
@[simp]
theorem units.smul_left_cancel {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) {x y : β} :
u x = u y x = y
theorem units.smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) {x y : β} :
u x = y x = u⁻¹ y
theorem add_units.vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (u : add_units α) {x y : β} :
u +ᵥ x = y x = -u +ᵥ y
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 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
@[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
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
def mul_action.to_perm (α : Type u) (β : Type v) [group α] [mul_action α β] :

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

Equations
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 units.smul_eq_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (u : units α) {x : β} :
u x = 0 x = 0
theorem units.smul_ne_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (u : units α) {x : β} :
u x 0 x 0
@[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
@[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