More lemmas about group actions

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

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 := ⋯ }

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 := ⋯ }

@[simp]

theorem MulAction.toPerm_symm_apply {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (a : α) (x : β) : (Equiv.symm (toPerm a)) x = a⁻¹ • x

@[simp]

theorem AddAction.toPerm_apply {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (a : α) (x : β) : (toPerm a) x = a +ᵥ x

@[simp]

theorem AddAction.toPerm_symm_apply {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (a : α) (x : β) : (Equiv.symm (toPerm a)) x = -a +ᵥ x

@[simp]

theorem MulAction.toPerm_apply {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (a : α) (x : β) : (toPerm a) x = a • x

theorem MulAction.toPerm_injective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] [FaithfulSMul α β] : Function.Injective toPerm

MulAction.toPerm is injective on faithful actions.

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

AddAction.toPerm is injective on faithful actions.

theorem MulAction.bijective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) : Function.Bijective fun (x : β) => g • x

theorem AddAction.bijective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) : Function.Bijective fun (x : β) => g +ᵥ x

theorem MulAction.injective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) : Function.Injective fun (x : β) => g • x

theorem AddAction.injective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) : Function.Injective fun (x : β) => g +ᵥ x

theorem MulAction.surjective {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) : Function.Surjective fun (x : β) => g • x

theorem AddAction.surjective {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) : Function.Surjective fun (x : β) => g +ᵥ x

theorem smul_left_cancel {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) {x y : β} (h : g • x = g • y) : x = y

theorem vadd_left_cancel {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) {x y : β} (h : g +ᵥ x = g +ᵥ y) : x = y

@[simp]

theorem smul_left_cancel_iff {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) {x y : β} : g • x = g • y ↔ x = y

@[simp]

theorem vadd_left_cancel_iff {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) {x y : β} : g +ᵥ x = g +ᵥ y ↔ x = y

theorem smul_eq_iff_eq_inv_smul {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] (g : α) {x y : β} : g • x = y ↔ x = g⁻¹ • y

theorem vadd_eq_iff_eq_neg_vadd {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] (g : α) {x y : β} : g +ᵥ x = y ↔ x = -g +ᵥ y

theorem isCancelSMul_iff_eq_one_of_smul_eq {α : Type u_5} {β : Type u_6} [Group α] [MulAction α β] : IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1

theorem isCancelVAdd_iff_eq_zero_of_vadd_eq {α : Type u_5} {β : Type u_6} [AddGroup α] [AddAction α β] : IsCancelVAdd α β ↔ ∀ (g : α) (x : β), g +ᵥ x = x → g = 0

@[simp]

theorem invOf_smul_smul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] : ⅟c • c • x = x

@[simp]

theorem smul_invOf_smul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] : c • ⅟c • x = x

theorem invOf_smul_eq_iff {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] {c : α} {x y : β} [Invertible c] : ⅟c • x = y ↔ x = c • y

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

@[instance_reducible]

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), mul_smul := ⋯, one_smul := ⋯ }

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

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

@[instance_reducible]

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), add_vadd := ⋯, zero_vadd := ⋯ }

@[instance_reducible]

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_one := ⋯, smul_mul := ⋯ }

theorem IsUnit.smul_bijective {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] {m : α} (hm : IsUnit m) : Function.Bijective fun (a : β) => m • a

theorem IsAddUnit.vadd_bijective {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction α β] {m : α} (hm : IsAddUnit m) : Function.Bijective fun (a : β) => m +ᵥ a

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

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

@[simp]

theorem isUnit_smul_iff {α : Type u_5} {β : Type u_6} [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α) (m : β) : IsUnit (g • m) ↔ IsUnit m

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' := ⋯ }

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' := ⋯ }

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

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

@[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_one := ⋯, smul_mul := ⋯ }

@[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_one := ⋯, smul_mul := ⋯ }

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' := ⋯ }

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

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

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' := ⋯ }

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

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

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

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