group_theory.group_action.group

source

@[protected, instance]

def right_cancel_monoid.to_has_faithful_scalar {α : Type u} [right_cancel_monoid α] :

has_faithful_scalar α α

monoid.to_mul_action is faithful on cancellative monoids.

source

@[protected, instance]

def add_right_cancel_monoid.to_has_faithful_scalar {α : Type u} [add_right_cancel_monoid α] :

has_faithful_vadd α α

add_monoid.to_add_action is faithful on additive cancellative monoids.

source

@[simp]

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

c⁻¹ • c • x = x

source

@[simp]

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

-c +ᵥ (c +ᵥ x) = x

source

@[simp]

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

c +ᵥ (-c +ᵥ x) = x

source

@[simp]

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

c • c⁻¹ • x = x

source

@[simp]

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

⇑(add_action.to_perm a) x = a +ᵥ x

source

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

equiv.perm β

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

Equations

mul_action.to_perm a = {to_fun := λ (x : β), a • x, inv_fun := λ (x : β), a⁻¹ • x, left_inv := _, right_inv := _}

source

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

equiv.perm β

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

Equations

add_action.to_perm a = {to_fun := λ (x : β), a +ᵥ x, inv_fun := λ (x : β), -a +ᵥ x, left_inv := _, right_inv := _}

source

@[simp]

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

⇑(equiv.symm (mul_action.to_perm a)) x = a⁻¹ • x

source

@[simp]

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

⇑(equiv.symm (add_action.to_perm a)) x = -a +ᵥ x

source

@[simp]

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

⇑(mul_action.to_perm a) x = a • x

source

theorem add_action.to_perm_injective {α : Type u} {β : Type v} [add_group α] [add_action α β] [has_faithful_vadd α β] :

function.injective add_action.to_perm

source

theorem mul_action.to_perm_injective {α : Type u} {β : Type v} [group α] [mul_action α β] [has_faithful_scalar α β] :

function.injective mul_action.to_perm

mul_action.to_perm is injective on faithful actions.

source

@[simp]

theorem mul_action.to_perm_hom_apply (α : Type u) (β : Type v) [group α] [mul_action α β] (a : α) :

⇑(mul_action.to_perm_hom α β) a = mul_action.to_perm a

source

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

α →* equiv.perm β

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

Equations

mul_action.to_perm_hom α β = {to_fun := mul_action.to_perm _inst_2, map_one' := _, map_mul' := _}

source

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

α →+ additive (equiv.perm β)

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

Equations

add_action.to_perm_hom β α = {to_fun := λ (a : α), ⇑additive.of_mul (add_action.to_perm a), map_zero' := _, map_add' := _}

source

@[simp]

theorem add_action.to_perm_hom_apply (β : Type v) (α : Type u_1) [add_group α] [add_action α β] (a : α) :

⇑(add_action.to_perm_hom β α) a = ⇑additive.of_mul (add_action.to_perm a)

source

@[protected, instance]

def equiv.perm.apply_mul_action (α : Type u_1) :

mul_action (equiv.perm α) α

The tautological action by equiv.perm α on α.

This generalizes function.End.apply_mul_action.

Equations

equiv.perm.apply_mul_action α = {to_has_scalar := {smul := λ (f : equiv.perm α) (a : α), ⇑f a}, one_smul := _, mul_smul := _}

source

@[protected, simp]

theorem equiv.perm.smul_def {α : Type u_1} (f : equiv.perm α) (a : α) :

f • a = ⇑f a

source

@[protected, instance]

def equiv.perm.apply_has_faithful_scalar (α : Type u_1) :

has_faithful_scalar (equiv.perm α) α

equiv.perm.apply_mul_action is faithful.

source

theorem neg_vadd_eq_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {a : α} {x y : β} :

-a +ᵥ x = y ↔ x = a +ᵥ y

source

theorem inv_smul_eq_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a : α} {x y : β} :

a⁻¹ • x = y ↔ x = a • y

source

theorem eq_inv_smul_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a : α} {x y : β} :

x = a⁻¹ • y ↔ a • x = y

source

theorem eq_neg_vadd_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {a : α} {x y : β} :

x = -a +ᵥ y ↔ a +ᵥ x = y

source

theorem smul_inv {α : Type u} {β : Type v} [group α] [mul_action α β] [group β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :

(c • x)⁻¹ = c⁻¹ • x⁻¹

source

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

source

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

source

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

source

@[protected]

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

function.bijective (λ (b : β), g • b)

source

@[protected]

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

function.bijective (λ (b : β), g +ᵥ b)

source

@[protected]

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

function.injective (λ (b : β), g • b)

source

@[protected]

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

function.injective (λ (b : β), g +ᵥ b)

source

theorem vadd_left_cancel {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) {x y : β} (h : g +ᵥ x = g +ᵥ y) :

x = y

source

theorem smul_left_cancel {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) {x y : β} (h : g • x = g • y) :

x = y

source

@[simp]

theorem vadd_left_cancel_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) {x y : β} :

g +ᵥ x = g +ᵥ y ↔ x = y

source

@[simp]

theorem smul_left_cancel_iff {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) {x y : β} :

g • x = g • y ↔ x = y

source

theorem smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) {x y : β} :

g • x = y ↔ x = g⁻¹ • y

source

theorem vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) {x y : β} :

g +ᵥ x = y ↔ x = -g +ᵥ y

source

@[protected, instance]

def cancel_monoid_with_zero.to_has_faithful_scalar {α : Type u} [cancel_monoid_with_zero α] [nontrivial α] :

has_faithful_scalar α α

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

source

@[simp]

theorem inv_smul_smul₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {c : α} (hc : c ≠ 0) (x : β) :

c⁻¹ • c • x = x

source

@[simp]

theorem smul_inv_smul₀ {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {c : α} (hc : c ≠ 0) (x : β) :

c • c⁻¹ • x = x

source

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

source

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

source

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

source

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

source

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

distrib_mul_action.to_add_equiv β x = {to_fun := (distrib_mul_action.to_add_monoid_hom β x).to_fun, inv_fun := (⇑(mul_action.to_perm_hom α β) x).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem distrib_mul_action.to_add_equiv_symm_apply {α : Type u} (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] (x : α) (ᾰ : β) :

⇑((distrib_mul_action.to_add_equiv β x).symm) ᾰ = x⁻¹ • ᾰ

source

@[simp]

theorem distrib_mul_action.to_add_equiv_apply {α : Type u} (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] (x : α) (ᾰ : β) :

⇑(distrib_mul_action.to_add_equiv β x) ᾰ = x • ᾰ

source

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

α →* add_aut β

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of mul_action.to_perm_hom.

Equations

distrib_mul_action.to_add_aut α β = {to_fun := distrib_mul_action.to_add_equiv β _inst_3, map_one' := _, map_mul' := _}

source

@[simp]

theorem distrib_mul_action.to_add_aut_apply (α : Type u) (β : Type v) [group α] [add_monoid β] [distrib_mul_action α β] (x : α) :

⇑(distrib_mul_action.to_add_aut α β) x = distrib_mul_action.to_add_equiv β x

source

theorem smul_eq_zero_iff_eq {α : Type u} {β : Type v} [group α] [add_monoid β] [distrib_mul_action α β] (a : α) {x : β} :

a • x = 0 ↔ x = 0

source

theorem smul_ne_zero_iff_ne {α : Type u} {β : Type v} [group α] [add_monoid β] [distrib_mul_action α β] (a : α) {x : β} :

a • x ≠ 0 ↔ x ≠ 0

source

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

source

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

source

@[simp]

theorem mul_distrib_mul_action.to_mul_equiv_apply {α : Type u} (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] (x : α) (ᾰ : β) :

⇑(mul_distrib_mul_action.to_mul_equiv β x) ᾰ = x • ᾰ

source

@[simp]

theorem mul_distrib_mul_action.to_mul_equiv_symm_apply {α : Type u} (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] (x : α) (ᾰ : β) :

⇑((mul_distrib_mul_action.to_mul_equiv β x).symm) ᾰ = x⁻¹ • ᾰ

source

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

mul_distrib_mul_action.to_mul_equiv β x = {to_fun := (mul_distrib_mul_action.to_monoid_hom β x).to_fun, inv_fun := (⇑(mul_action.to_perm_hom α β) x).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

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

α →* mul_aut β

Each element of the group defines an multiplicative monoid isomorphism.

This is a stronger version of mul_action.to_perm_hom.

Equations

mul_distrib_mul_action.to_mul_aut α β = {to_fun := mul_distrib_mul_action.to_mul_equiv β _inst_3, map_one' := _, map_mul' := _}

source

@[simp]

theorem mul_distrib_mul_action.to_mul_aut_apply (α : Type u) (β : Type v) [group α] [monoid β] [mul_distrib_mul_action α β] (x : α) :

⇑(mul_distrib_mul_action.to_mul_aut α β) x = mul_distrib_mul_action.to_mul_equiv β x

source

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

source

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

arrow_action = {to_has_scalar := {smul := λ (g : G) (F : A → B) (a : A), F (g⁻¹ • a)}, one_smul := _, mul_smul := _}

source

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] :

mul_distrib_mul_action G (A → B)

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

Equations

arrow_mul_distrib_mul_action = {to_mul_action := arrow_action _inst_2, smul_mul := _, smul_one := _}

source

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

source

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

source

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

mul_aut_arrow = mul_distrib_mul_action.to_mul_aut G (A → H)

source

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

source

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

source

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

source

@[simp]

theorem is_unit_smul_iff {α : Type u} {β : Type v} [group α] [monoid β] [mul_action α β] [smul_comm_class α β β] [is_scalar_tower α β β] (g : α) (m : β) :

is_unit (g • m) ↔ is_unit m

source

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)

mathlib documentation

Group actions applied to various types of group #