# More lemmas about group actions #

This file contains lemmas about group actions that require more imports than `Mathlib/Algebra/Group/Action/Defs.lean` offers.

source
def MulAction.toPerm {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (a : α) :
Equiv.Perm β

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

Equations

- MulAction.toPerm a = { toFun := fun (x : β) => a • x, invFun := fun (x : β) => a⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
def AddAction.toPerm {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (a : α) :
Equiv.Perm β

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

Equations

- AddAction.toPerm a = { toFun := fun (x : β) => a +ᵥ x, invFun := fun (x : β) => -a +ᵥ x, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem MulAction.toPerm_apply {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (a : α) (x : β) :
(toPerm a) x = a • x
source
@[simp]
theorem AddAction.toPerm_apply {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (a : α) (x : β) :
(toPerm a) x = a +ᵥ x
source
@[simp]
theorem MulAction.toPerm_symm_apply {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (a : α) (x : β) :
(Equiv.symm (toPerm a)) x = a⁻¹ • x
source
@[simp]
theorem AddAction.toPerm_symm_apply {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (a : α) (x : β) :
(Equiv.symm (toPerm a)) x = -a +ᵥ x
source
theorem MulAction.toPerm_injective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] [FaithfulSMul α β] :
Function.Injective toPerm

`MulAction.toPerm` is injective on faithful actions.

source
theorem AddAction.toPerm_injective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] [FaithfulVAdd α β] :
Function.Injective toPerm

`AddAction.toPerm` is injective on faithful actions.

source
theorem MulAction.bijective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) :
Function.Bijective fun (x : β) => g • x
source
theorem AddAction.bijective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) :
Function.Bijective fun (x : β) => g +ᵥ x
source
theorem MulAction.injective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) :
Function.Injective fun (x : β) => g • x
source
theorem AddAction.injective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) :
Function.Injective fun (x : β) => g +ᵥ x
source
theorem MulAction.surjective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) :
Function.Surjective fun (x : β) => g • x
source
theorem AddAction.surjective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) :
Function.Surjective fun (x : β) => g +ᵥ x
source
theorem smul_left_cancel {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) {x y : β} (h : g • x = g • y) :
x = y
source
theorem vadd_left_cancel {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) {x y : β} (h : g +ᵥ x = g +ᵥ y) :
x = y
source
@[simp]
theorem smul_left_cancel_iff {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) {x y : β} :
g • x = g • y ↔ x = y
source
@[simp]
theorem vadd_left_cancel_iff {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) {x y : β} :
g +ᵥ x = g +ᵥ y ↔ x = y
source
theorem smul_eq_iff_eq_inv_smul {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) {x y : β} :
g • x = y ↔ x = g⁻¹ • y
source
theorem vadd_eq_iff_eq_neg_vadd {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) {x y : β} :
g +ᵥ x = y ↔ x = -g +ᵥ y
source
theorem isCancelSMul_iff_eq_one_of_smul_eq {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] :
IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1
source
theorem isCancelVAdd_iff_eq_zero_of_vadd_eq {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] :
IsCancelVAdd α β ↔ ∀ (g : α) (x : β), g +ᵥ x = x → g = 0
source
@[simp]
theorem invOf_smul_smul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] :
⅟ c • c • x = x
source
@[simp]
theorem smul_invOf_smul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] :
c • ⅟ c • x = x
source
theorem invOf_smul_eq_iff {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] {c : α} {x y : β} [Invertible c] :
⅟ c • x = y ↔ x = c • y
source
theorem smul_eq_iff_eq_invOf_smul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] {c : α} {x y : β} [Invertible c] :
c • x = y ↔ x = ⅟ c • y
source
def arrowAction {G : Type u_7} {A : Type u_8} {B : Type u_9} [DivisionMonoid G] [MulAction G A] :
MulAction G (A → B)

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

Equations

- arrowAction = { smul := fun (g : G) (F : A → B) (a : A) => F (g⁻¹ • a), one_smul := ⋯, mul_smul := ⋯ }

Instances For

source
def arrowAddAction {G : Type u_7} {A : Type u_8} {B : Type u_9} [SubtractionMonoid G] [AddAction G A] :
AddAction G (A → B)

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

Equations

- arrowAddAction = { vadd := fun (g : G) (F : A → B) (a : A) => F (-g +ᵥ a), zero_vadd := ⋯, add_vadd := ⋯ }

Instances For

source
@[simp]
theorem arrowAddAction_vadd {G : Type u_7} {A : Type u_8} {B : Type u_9} [SubtractionMonoid G] [AddAction G A] (g : G) (F : A → B) (a : A) :
VAdd.vadd g F a = F (-g +ᵥ a)
source
@[simp]
theorem arrowAction_smul {G : Type u_7} {A : Type u_8} {B : Type u_9} [DivisionMonoid G] [MulAction G A] (g : G) (F : A → B) (a : A) :
SMul.smul g F a = F (g⁻¹ • a)
source
def arrowMulDistribMulAction {M : Type u_2} {G : Type u_7} {A : Type u_8} [DivisionMonoid G] [MulAction G A] [Monoid M] :
MulDistribMulAction G (A → M)

When `M` is a monoid, `ArrowAction` is additionally a `MulDistribMulAction`.

Equations

- arrowMulDistribMulAction = { toMulAction := arrowAction, smul_mul := ⋯, smul_one := ⋯ }

Instances For

source
theorem IsUnit.smul_bijective {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] {m : α} (hm : IsUnit m) :
Function.Bijective fun (a : β) => m • a
source
theorem IsAddUnit.vadd_bijective {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction α β] {m : α} (hm : IsAddUnit m) :
Function.Bijective fun (a : β) => m +ᵥ a
source
theorem IsUnit.smul_left_cancel {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] {a : α} (ha : IsUnit a) {x y : β} :
a • x = a • y ↔ x = y
source
theorem IsAddUnit.vadd_left_cancel {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction α β] {a : α} (ha : IsAddUnit a) {x y : β} :
a +ᵥ x = a +ᵥ y ↔ x = y
source
@[simp]
theorem isUnit_smul_iff {α : Type u_5} {β : Type u_6} [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α) (m : β) :
IsUnit (g • m) ↔ IsUnit m
source
def MulAction.toFun (M : Type u_2) (α : Type u_5) [Monoid M] [MulAction M α] :
α ↪ M → α

Embedding of `α` into functions `M → α` induced by a multiplicative action of `M` on `α`.

Equations

- MulAction.toFun M α = { toFun := fun (y : α) (x : M) => x • y, inj' := ⋯ }

Instances For

source
def AddAction.toFun (M : Type u_2) (α : Type u_5) [AddMonoid M] [AddAction M α] :
α ↪ M → α

Embedding of `α` into functions `M → α` induced by an additive action of `M` on `α`.

Equations

- AddAction.toFun M α = { toFun := fun (y : α) (x : M) => x +ᵥ y, inj' := ⋯ }

Instances For

source
@[simp]
theorem MulAction.toFun_apply {M : Type u_2} {α : Type u_5} [Monoid M] [MulAction M α] (x : M) (y : α) :
(toFun M α) y x = x • y
source
@[simp]
theorem AddAction.toFun_apply {M : Type u_2} {α : Type u_5} [AddMonoid M] [AddAction M α] (x : M) (y : α) :
(toFun M α) y x = x +ᵥ y
source
@[reducible, inline]
abbrev Function.Injective.mulDistribMulAction {M : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : B →* A) (hf : Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) :
MulDistribMulAction M B

Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism.

Equations

- Function.Injective.mulDistribMulAction f hf smul = { toMulAction := Function.Injective.mulAction (⇑f) hf smul, smul_mul := ⋯, smul_one := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Surjective.mulDistribMulAction {M : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : A →* B) (hf : Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) :
MulDistribMulAction M B

Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism.

Equations

- Function.Surjective.mulDistribMulAction f hf smul = { toMulAction := Function.Surjective.mulAction (⇑f) hf smul, smul_mul := ⋯, smul_one := ⋯ }

Instances For

source
def MulDistribMulAction.toMonoidHom {M : Type u_2} (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) :
A →* A

Scalar multiplication by `r` as a `MonoidHom`.

Equations

- MulDistribMulAction.toMonoidHom A r = { toFun := fun (x : A) => r • x, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem MulDistribMulAction.toMonoidHom_apply {M : Type u_2} (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x✝ : A) :
(toMonoidHom A r) x✝ = r • x✝
source
@[simp]
theorem smul_pow' {M : Type u_2} {A : Type u_3} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) (n : ℕ) :
r • x ^ n = (r • x) ^ n
source
def MulDistribMulAction.toMonoidEnd (M : Type u_2) (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] :
M →* Monoid.End A

Each element of the monoid defines a monoid homomorphism.

Equations

- MulDistribMulAction.toMonoidEnd M A = { toFun := MulDistribMulAction.toMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem MulDistribMulAction.toMonoidEnd_apply (M : Type u_2) (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) :
(toMonoidEnd M A) r = toMonoidHom A r
source
@[simp]
theorem smul_inv' {M : Type u_2} {A : Type u_3} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) :
r • x⁻¹ = (r • x)⁻¹
source
theorem smul_div' {M : Type u_2} {A : Type u_3} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x y : A) :
r • (x / y) = r • x / r • y
source
theorem smul_zpow' {M : Type u_2} {A : Type u_3} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) (z : ℤ) :
r • x ^ z = (r • x) ^ z