Group actions applied to various types of group #
This file contains lemmas about smul on units, group_with_zero, and group.
@[simp]
theorem
add_units.neg_vadd_vadd
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(u : add_units α)
(x : β) :
@[simp]
theorem
add_units.vadd_neg_vadd
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(u : add_units α)
(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 β.
If a monoid α acts on β, then each u : units α defines a permutation of β.
def
units.smul_perm_hom
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β] :
units α →* equiv.perm β
If a monoid α acts on β, then each u : units α defines a permutation of β.
Equations
- units.smul_perm_hom = {to_fun := units.smul_perm _inst_2, map_one' := _, map_mul' := _}
def
add_units.vadd_perm_hom
{β : Type v}
{M : Type u_1}
[add_monoid M]
[add_action M β] :
add_units M →+ additive (equiv.perm β)
If an additive monoid α acts on β, then each u : add_units α defines a permutation
of β.
Equations
- add_units.vadd_perm_hom = {to_fun := λ (u : add_units M), ⇑additive.of_mul u.vadd_perm, map_zero' := _, map_add' := _}
@[simp]
theorem
add_units.vadd_left_cancel
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(u : add_units α)
{x y : β} :
theorem
add_units.vadd_eq_iff_eq_neg_vadd
{α : Type u}
{β : Type v}
[add_monoid α]
[add_action α β]
(u : add_units α)
{x y : β} :
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
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 : β} :
@[simp]
@[simp]
@[simp]
@[simp]
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 : β} :
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 : β} :
@[simp]
theorem
smul_left_cancel_iff
{α : Type u}
{β : Type v}
[group α]
[mul_action α β]
(g : α)
{x y : β} :
theorem
units.smul_eq_zero
{α : Type u}
{β : Type v}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
(u : units α)
{x : β} :
theorem
units.smul_ne_zero
{α : Type u}
{β : Type v}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
(u : units α)
{x : β} :
@[simp]
theorem
is_unit.smul_eq_zero
{α : Type u}
{β : Type v}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
{u : α}
(hu : is_unit u)
{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.