Group actions applied to various types of group #
This file contains lemmas about smul on group_with_zero, and group.
@[simp]
@[simp]
@[simp]
@[simp]
Given an action of a group α on β, each g : α defines a permutation of β.
Given an action of an additive group α on β, each g : α defines a permutation of β.
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' := _}
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' := _}
theorem
neg_vadd_eq_iff
{α : Type u}
{β : Type v}
[add_group α]
[add_action α β]
{a : α}
{x y : β} :
theorem
eq_neg_vadd_iff
{α : Type u}
{β : Type v}
[add_group α]
[add_action α β]
{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 : β} :
@[simp]
theorem
smul_left_cancel_iff
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
(g : α)
{x y : β} :
theorem
smul_eq_iff_eq_inv_smul
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
(g : α)
{x y : β} :
theorem
vadd_eq_iff_eq_neg_vadd
{α : Type u}
{β : Type v}
[add_group α]
[add_action α β]
(g : α)
{x y : β} :
@[simp]
theorem
inv_smul_smul'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{c : α}
(hc : c ≠ 0)
(x : β) :
@[simp]
theorem
smul_inv_smul'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{c : α}
(hc : c ≠ 0)
(x : β) :
theorem
inv_smul_eq_iff'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{x y : β} :
theorem
eq_inv_smul_iff'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{x y : β} :
theorem
smul_eq_zero_iff_eq
{α : Type u}
{β : Type v}
[group α]
[add_monoid β]
[distrib_mul_action α β]
(a : α)
{x : β} :
theorem
smul_ne_zero_iff_ne
{α : Type u}
{β : Type v}
[group α]
[add_monoid β]
[distrib_mul_action α β]
(a : α)
{x : β} :
theorem
smul_eq_zero_iff_eq'
{α : Type u}
{β : Type v}
[group_with_zero α]
[add_monoid β]
[distrib_mul_action α β]
{a : α}
(ha : a ≠ 0)
{x : β} :
theorem
smul_ne_zero_iff_ne'
{α : Type u}
{β : Type v}
[group_with_zero α]
[add_monoid β]
[distrib_mul_action α β]
{a : α}
(ha : a ≠ 0)
{x : β} :
@[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) :
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 := _}
@[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) :
⇑(mul_equiv.symm (⇑mul_aut_arrow g)) F ᾰ = (g⁻¹ • F) ᾰ
@[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] :
Given groups G H with G acting on A, G acts by
multiplicative automorphisms on A → H.
theorem
is_add_unit.vadd_left_cancel
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
{a : α}
(ha : is_add_unit a)
{x y : β} :
theorem
is_unit.smul_left_cancel
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
{a : α}
(ha : is_unit a)
{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 : β} :