mathlib3 documentation

group_theory.group_action.group

Group actions applied to various types of group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]

monoid.to_mul_action is faithful on cancellative monoids.

@[protected, instance]

add_monoid.to_add_action is faithful on additive cancellative monoids.

@[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
@[simp]
theorem add_action.to_perm_apply {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) (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 β.

Equations
@[simp]
theorem mul_action.to_perm_symm_apply {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (x : β) :
@[simp]
theorem add_action.to_perm_symm_apply {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) (x : β) :
@[simp]
theorem mul_action.to_perm_apply {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (x : β) :

add_action.to_perm is injective on faithful actions.

mul_action.to_perm is injective on faithful actions.

@[simp]
theorem mul_action.to_perm_hom_apply (α : Type u) (β : Type v) [group α] [mul_action α β] (a : α) :
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
@[simp]
@[protected, instance]

The tautological action by equiv.perm α on α.

This generalizes function.End.apply_mul_action.

Equations
@[protected, simp]
theorem equiv.perm.smul_def {α : Type u_1} (f : equiv.perm α) (a : α) :
f a = f a
@[protected, instance]

equiv.perm.apply_mul_action is faithful.

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 smul_zpow {α : Type u} {β : Type v} [group α] [mul_action α β] [group β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) (p : ) :
(c x) ^ p = c ^ p x ^ p
@[simp]
theorem commute.smul_right_iff {α : Type u} {β : Type v} [group α] [mul_action α β] [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β] {a b : β} (r : α) :
commute a (r b) commute a b
@[simp]
theorem commute.smul_left_iff {α : Type u} {β : Type v} [group α] [mul_action α β] [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β] {a b : β} (r : α) :
commute (r a) b commute a b
@[protected]
theorem mul_action.bijective {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) :
@[protected]
theorem add_action.bijective {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) :
@[protected]
theorem mul_action.injective {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) :
@[protected]
theorem add_action.injective {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) :
@[protected]
theorem add_action.surjective {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) :
@[protected]
theorem mul_action.surjective {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) :
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
@[protected, instance]

monoid.to_mul_action is faithful on nontrivial cancellative monoids with zero.

@[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 commute.smul_right_iff₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β] {a b : β} {c : α} (hc : c 0) :
commute a (c b) commute a b
@[simp]
theorem commute.smul_left_iff₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β] {a b : β} {c : α} (hc : c 0) :
commute (c a) b commute a b
@[protected]
theorem mul_action.bijective₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) :
@[protected]
theorem mul_action.injective₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) :
@[protected]
theorem mul_action.surjective₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) :
def distrib_mul_action.to_add_equiv {α : Type u} (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] (x : α) :
β ≃+ β

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of mul_action.to_perm.

Equations
@[simp]
theorem distrib_mul_action.to_add_equiv_symm_apply {α : Type u} (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] (x : α) (ᾰ : β) :
@[simp]
theorem distrib_mul_action.to_add_equiv_apply {α : Type u} (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] (x : α) (ᾰ : β) :
def distrib_mul_action.to_add_equiv₀ {α : Type u_1} (β : Type u_2) [group_with_zero α] [add_monoid β] [distrib_mul_action α β] (x : α) (hx : x 0) :
β ≃+ β

Each non-zero element of a group_with_zero defines an additive monoid isomorphism of an add_monoid on which it acts distributively.

This is a stronger version of distrib_mul_action.to_add_monoid_hom.

Equations
def distrib_mul_action.to_add_aut (α : Type u) (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] :

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of mul_action.to_perm_hom.

Equations
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 mul_distrib_mul_action.to_mul_equiv_apply {α : Type u} (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] (x : α) (ᾰ : β) :
@[simp]
theorem mul_distrib_mul_action.to_mul_equiv_symm_apply {α : Type u} (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] (x : α) (ᾰ : β) :
def mul_distrib_mul_action.to_mul_equiv {α : Type u} (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] (x : α) :
β ≃* β

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of mul_action.to_perm.

Equations
def mul_distrib_mul_action.to_mul_aut (α : Type u) (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] :

Each element of the group defines an multiplicative monoid isomorphism.

This is a stronger version of mul_action.to_perm_hom.

Equations
@[simp]
theorem arrow_add_action_to_has_vadd_vadd {G : Type u_1} {A : Type u_2} {B : Type u_3} [subtraction_monoid G] [add_action G A] (g : G) (F : A B) (a : A) :
(g +ᵥ F) a = F (-g +ᵥ a)
@[simp]
theorem arrow_action_to_has_smul_smul {G : Type u_1} {A : Type u_2} {B : Type u_3} [division_monoid 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} [division_monoid 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
def arrow_add_action {G : Type u_1} {A : Type u_2} {B : Type u_3} [subtraction_monoid G] [add_action G A] :
add_action G (A B)

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

Equations
def arrow_mul_distrib_mul_action {G : Type u_1} {A : Type u_2} {B : Type u_3} [group G] [mul_action G A] [monoid B] :

When B is a monoid, arrow_action is additionally a mul_distrib_mul_action.

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] [monoid H] (x : G) (ᾰ : A H) (ᾰ_1 : A) :
(mul_equiv.symm (mul_aut_arrow x)) ᾰ_1 = (x⁻¹⁻¹ ᾰ_1)
@[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] [monoid H] (x : G) (ᾰ : A H) (ᾰ_1 : A) :
(mul_aut_arrow x) ᾰ_1 = (x⁻¹ ᾰ_1)
def mul_aut_arrow {G : Type u_1} {A : Type u_2} {H : Type u_3} [group G] [mul_action G A] [monoid 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
@[simp]
theorem is_unit_smul_iff {α : Type u} {β : Type v} [group α] [monoid β] [mul_action α β] [smul_comm_class α β β] [is_scalar_tower α β β] (g : α) (m : β) :
theorem is_unit.smul_sub_iff_sub_inv_smul {α : Type u} {β : Type v} [group α] [monoid β] [add_group β] [distrib_mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] (r : α) (a : β) :
is_unit (r 1 - a) is_unit (1 - r⁻¹ a)