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 := (↑(DistribSMul.toAddMonoidHom A x)).toFun, invFun := ((MulAction.toPermHom G A) x).invFun, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

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

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

def DistribMulAction.toAddAut (G : Type u_1) (A : Type u_3) [Group G] [AddMonoid A] [DistribMulAction G A] : G →* Multiplicative (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) : (toAddAut G A) x = 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✝

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)

theorem div_smul_div_comm {G : Type u_1} {G₀ : Type u_2} [Group G] [GroupWithZero G₀] [MulAction G G₀] [IsScalarTower G G₀ G₀] [SMulCommClass G G₀ G₀] (g h : G) (a b : G₀) : (g / h) • (a / b) = g • a / h • b

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