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

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

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

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

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

@[simp]

theorem DistribMulAction.toAddEquiv_apply {G : Type u_1} (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) (a✝ : A) : (DistribMulAction.toAddEquiv A x) a✝ = x • a✝

@[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) : (DistribMulAction.toAddEquiv A x).symm a✝ = x⁻¹ • a✝

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

@[simp]

theorem DistribMulAction.toAddAut_apply (G : Type u_1) (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] (x : G) : (DistribMulAction.toAddAut G A) x = DistribMulAction.toAddEquiv A x

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

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

def MulDistribMulAction.toMulEquiv {G : Type u_1} (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) : M ≃* M

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPerm.

Equations

• MulDistribMulAction.toMulEquiv M x = { toFun := (↑(MulDistribMulAction.toMonoidHom M x)).toFun, invFun := ((MulAction.toPermHom G M) x).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMulEquiv_apply {G : Type u_1} (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) (a✝ : M) : (MulDistribMulAction.toMulEquiv M x) a✝ = x • a✝

@[simp]

theorem MulDistribMulAction.toMulEquiv_symm_apply {G : Type u_1} (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) (a✝ : M) : (MulDistribMulAction.toMulEquiv M x).symm a✝ = x⁻¹ • a✝

def MulDistribMulAction.toMulAut (G : Type u_1) (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] : G →* MulAut M

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPermHom.

Equations

• MulDistribMulAction.toMulAut G M = { toFun := MulDistribMulAction.toMulEquiv M, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMulAut_apply (G : Type u_1) (M : Type u_4) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) : (MulDistribMulAction.toMulAut G M) x = MulDistribMulAction.toMulEquiv M x

instance MulAut.applyMulDistribMulAction {M : Type u_4} [Monoid M] : MulDistribMulAction (MulAut M) M

The tautological action by MulAut M on M.

This generalizes Function.End.applyMulAction.

Equations

• MulAut.applyMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

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 = DistribMulAction.mk ⋯ ⋯

def arrowMulDistribMulAction {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] : MulDistribMulAction G (A → M)

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

Equations

• arrowMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

def mulAutArrow {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] : G →* MulAut (A → M)

Given groups G H with G acting on A, G acts by multiplicative automorphisms on A → H.

Equations

• mulAutArrow = MulDistribMulAction.toMulAut G (A → M)

@[simp]

theorem mulAutArrow_apply_apply {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) (a✝ : A → M) (a✝¹ : A) : (mulAutArrow x) a✝ a✝¹ = (x • a✝) a✝¹

@[simp]

theorem mulAutArrow_apply_symm_apply {G : Type u_1} {A : Type u_3} {M : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) (a✝ : A → M) (a✝¹ : A) : (MulEquiv.symm (mulAutArrow x)) a✝ a✝¹ = (x⁻¹ • a✝) a✝¹

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)