# Definitions of group actions #

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes `SMul` and its additive version `VAdd`:

- `MulAction M α` and its additive version `AddAction G P` are typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classes `SMul` and `VAdd` that are defined in `Algebra.Group.Defs`;
- `DistribMulAction M A` is a typeclass for an action of a multiplicative monoid on an additive monoid such that `a • (b + c) = a • b + a • c` and `a • 0 = 0`.

The hierarchy is extended further by `Module`, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,

- `SMulCommClass M N α` and its additive version `VAddCommClass M N α`;
- `IsScalarTower M N α` and its additive version `VAddAssocClass M N α`;
- `IsCentralScalar M α` and its additive version `IsCentralVAdd M N α`.

## Notation #

- `a • b` is used as notation for `SMul.smul a b`.
- `a +ᵥ b` is used as notation for `VAdd.vadd a b`.

## Implementation details #

This file should avoid depending on other parts of `GroupTheory`, to avoid import cycles. More sophisticated lemmas belong in `GroupTheory.GroupAction`.

## Tags #

group action

source
theorem MulAction.bijective₀ {G₀ : Type u_2} {α : Type u_8} [GroupWithZero G₀] [MulAction G₀ α] {a : G₀} (ha : a ≠ 0) :
Function.Bijective fun (x : α) => a • x
source
theorem MulAction.injective₀ {G₀ : Type u_2} {α : Type u_8} [GroupWithZero G₀] [MulAction G₀ α] {a : G₀} (ha : a ≠ 0) :
Function.Injective fun (x : α) => a • x
source
theorem MulAction.surjective₀ {G₀ : Type u_2} {α : Type u_8} [GroupWithZero G₀] [MulAction G₀ α] {a : G₀} (ha : a ≠ 0) :
Function.Surjective fun (x : α) => a • x
source
def DistribMulAction.toAddEquiv {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) :
A ≃+ A

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of `MulAction.toPerm`.

Equations

- DistribMulAction.toAddEquiv A x = { toFun := (↑(DistribMulAction.toAddMonoidHom A x)).toFun, invFun := ((MulAction.toPermHom G A) x).invFun, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem DistribMulAction.toAddEquiv_symm_apply {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) (a✝ : A) :
(toAddEquiv A x).symm a✝ = x⁻¹ • a✝
source
@[simp]
theorem DistribMulAction.toAddEquiv_apply {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) (a✝ : A) :
(toAddEquiv A x) a✝ = x • a✝
source
def DistribMulAction.toAddAut (G : Type u_1) (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] :
G →* AddAut A

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of `MulAction.toPermHom`.

Equations

- DistribMulAction.toAddAut G A = { toFun := DistribMulAction.toAddEquiv A, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem DistribMulAction.toAddAut_apply (G : Type u_1) (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) :
(toAddAut G A) x = toAddEquiv A x
source
def smulMonoidWithZeroHom {M₀ : Type u_5} {N₀ : Type u_6} [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] :
M₀ × N₀ →*₀ N₀

Scalar multiplication as a monoid homomorphism with zero.

Equations

- smulMonoidWithZeroHom = { toFun := (↑smulMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem smulMonoidWithZeroHom_apply {M₀ : Type u_5} {N₀ : Type u_6} [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] (a✝ : M₀ × N₀) :
smulMonoidWithZeroHom a✝ = (↑smulMonoidHom).toFun a✝
source
instance AddAut.applyDistribMulAction {A : Type u_3} [AddMonoid A] :
DistribMulAction (AddAut A) A

The tautological action by `AddAut A` on `A`.

This generalizes `Function.End.applyMulAction`.

Equations

- AddAut.applyDistribMulAction = { smul := fun (x1 : AddAut A) (x2 : A) => x1 x2, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

source
theorem IsUnit.smul_sub_iff_sub_inv_smul {G : Type u_1} {R : Type u_7} [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R] [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R) :
IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
source
@[simp]
theorem smul_zpow₀' {G : Type u_1} {G₀ : Type u_2} [Group G] [GroupWithZero G₀] [MulDistribMulAction G G₀] (g : G) (x : G₀) (n : ℤ) :
g • x ^ n = (g • x) ^ n