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:

• SMulZeroClass is a typeclass for an action that preserves zero
• DistribSMul M A is a typeclass for an action on an additive monoid (AddZeroClass) that preserves addition and zero
• 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.

Notation

• a • b is used as notation for SMul.smul 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

class SMulZeroClass (M : Type u_12) (A : Type u_13) [Zero A] extends SMul M A : Type (max u_12 u_13)

Typeclass for scalar multiplication that preserves 0 on the right.

• smul : M → A → A
• smul_zero (a : M) : a • 0 = 0

  Multiplying 0 by a scalar gives 0

@[simp]

theorem smul_zero {M : Type u_1} {A : Type u_7} [Zero A] [SMulZeroClass M A] (a : M) : a • 0 = 0

theorem smul_ite_zero {M : Type u_1} {A : Type u_7} [Zero A] [SMulZeroClass M A] (p : Prop) [Decidable p] (a : M) (b : A) : (a • if p then b else 0) = if p then a • b else 0

theorem smul_eq_zero_of_right {M : Type u_1} {A : Type u_7} [Zero A] [SMulZeroClass M A] (a : M) {b : A} (h : b = 0) : a • b = 0

theorem right_ne_zero_of_smul {M : Type u_1} {A : Type u_7} [Zero A] [SMulZeroClass M A] {a : M} {b : A} : a • b ≠ 0 → b ≠ 0

@[reducible, inline]

abbrev Function.Injective.smulZeroClass {M : Type u_1} {A : Type u_7} {B : Type u_9} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom B A) (hf : Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : SMulZeroClass M B

Pullback a zero-preserving scalar multiplication along an injective zero-preserving map. See note [reducible non-instances].

@[reducible, inline]

abbrev ZeroHom.smulZeroClass {M : Type u_1} {A : Type u_7} {B : Type u_9} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : SMulZeroClass M B

Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.smulZeroClassLeft {R : Type u_12} {S : Type u_13} {M : Type u_14} [Zero M] [SMulZeroClass R M] [SMul S M] (f : R → S) (hf : Surjective f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : SMulZeroClass S M

Push forward the multiplication of R on M along a compatible surjective map f : R → S.

See also Function.Surjective.distribMulActionLeft.

@[reducible, inline]

abbrev SMulZeroClass.compFun {M : Type u_1} {N : Type u_6} (A : Type u_7) [Zero A] [SMulZeroClass M A] (f : N → M) : SMulZeroClass N A

Compose a SMulZeroClass with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

def SMulZeroClass.toZeroHom {M : Type u_1} (A : Type u_7) [Zero A] [SMulZeroClass M A] (x : M) : ZeroHom A A

Each element of the scalars defines a zero-preserving map.

@[simp]

theorem SMulZeroClass.toZeroHom_apply {M : Type u_1} (A : Type u_7) [Zero A] [SMulZeroClass M A] (x : M) (x✝ : A) : (toZeroHom A x) x✝ = x • x✝

class SMulWithZero (M₀ : Type u_2) (A : Type u_7) [Zero M₀] [Zero A] extends SMulZeroClass M₀ A : Type (max u_2 u_7)

SMulWithZero is a class consisting of a Type M₀ with 0 ∈ M₀ and a scalar multiplication of M₀ on a Type A with 0, such that the equality r • m = 0 holds if at least one among r or m equals 0.

• smul : M₀ → A → A
• smul_zero (a : M₀) : a • 0 = 0
• zero_smul (m : A) : 0 • m = 0

  Scalar multiplication by the scalar 0 is 0.

@[implicit_reducible]

instance MulZeroClass.toSMulWithZero (M₀ : Type u_2) [MulZeroClass M₀] : SMulWithZero M₀ M₀

@[implicit_reducible]

instance MulZeroClass.toOppositeSMulWithZero (M₀ : Type u_2) [MulZeroClass M₀] : SMulWithZero M₀ᵐᵒᵖ M₀

Like MulZeroClass.toSMulWithZero, but multiplies on the right.

@[simp]

theorem zero_smul (M₀ : Type u_2) {A : Type u_7} [Zero M₀] [Zero A] [SMulWithZero M₀ A] (m : A) : 0 • m = 0

theorem smul_eq_zero_of_left {M₀ : Type u_2} {A : Type u_7} [Zero M₀] [Zero A] [SMulWithZero M₀ A] {a : M₀} (h : a = 0) (b : A) : a • b = 0

theorem left_ne_zero_of_smul {M₀ : Type u_2} {A : Type u_7} [Zero M₀] [Zero A] [SMulWithZero M₀ A] {a : M₀} {b : A} : a • b ≠ 0 → a ≠ 0

@[reducible, inline]

abbrev Function.Injective.smulWithZero {M₀ : Type u_2} {A : Type u_7} {A' : Type u_8} [Zero M₀] [Zero A] [SMulWithZero M₀ A] [Zero A'] [SMul M₀ A'] (f : ZeroHom A' A) (hf : Injective ⇑f) (smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b) : SMulWithZero M₀ A'

Pullback a SMulWithZero structure along an injective zero-preserving homomorphism.

@[reducible, inline]

abbrev Function.Surjective.smulWithZero {M₀ : Type u_2} {A : Type u_7} {A' : Type u_8} [Zero M₀] [Zero A] [SMulWithZero M₀ A] [Zero A'] [SMul M₀ A'] (f : ZeroHom A A') (hf : Surjective ⇑f) (smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b) : SMulWithZero M₀ A'

Pushforward a SMulWithZero structure along a surjective zero-preserving homomorphism.

@[implicit_reducible]

def SMulWithZero.compHom {M₀ : Type u_2} {M₀' : Type u_3} (A : Type u_7) [Zero M₀] [Zero A] [SMulWithZero M₀ A] [Zero M₀'] (f : ZeroHom M₀' M₀) : SMulWithZero M₀' A

Compose a SMulWithZero with a ZeroHom, with action f r' • m

@[implicit_reducible]

instance AddMonoid.natSMulWithZero {A : Type u_7} [AddMonoid A] : SMulWithZero ℕ A

@[implicit_reducible]

instance AddGroup.intSMulWithZero {A : Type u_7} [AddGroup A] : SMulWithZero ℤ A

class MulActionWithZero (M₀ : Type u_2) (A : Type u_7) [MonoidWithZero M₀] [Zero A] extends MulAction M₀ A : Type (max u_2 u_7)

An action of a monoid with zero M₀ on a Type A, also with 0, extends MulAction and is compatible with 0 (both in M₀ and in A), with 1 ∈ M₀, and with associativity of multiplication on the monoid A.

• smul : M₀ → A → A
• mul_smul (x y : M₀) (b : A) : (x * y) • b = x • y • b
• one_smul (b : A) : 1 • b = b
• smul_zero (r : M₀) : r • 0 = 0

  Scalar multiplication by any element send 0 to 0.

• zero_smul (m : A) : 0 • m = 0

  Scalar multiplication by the scalar 0 is 0.

@[implicit_reducible, instance 100]

instance MulActionWithZero.toSMulWithZero (M₀ : Type u_12) (A : Type u_13) {x✝ : MonoidWithZero M₀} {x✝¹ : Zero A} [m : MulActionWithZero M₀ A] : SMulWithZero M₀ A

@[implicit_reducible]

instance MonoidWithZero.toMulActionWithZero (M₀ : Type u_2) [MonoidWithZero M₀] : MulActionWithZero M₀ M₀

See also Semiring.toModule

@[implicit_reducible]

instance MonoidWithZero.toOppositeMulActionWithZero (M₀ : Type u_2) [MonoidWithZero M₀] : MulActionWithZero M₀ᵐᵒᵖ M₀

Like MonoidWithZero.toMulActionWithZero, but multiplies on the right. See also Semiring.toOppositeModule

theorem MulActionWithZero.subsingleton (M₀ : Type u_2) (A : Type u_7) [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] [Subsingleton M₀] : Subsingleton A

theorem MulActionWithZero.nontrivial (M₀ : Type u_2) (A : Type u_7) [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] [Nontrivial A] : Nontrivial M₀

theorem ite_zero_smul {M₀ : Type u_2} {A : Type u_7} [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] (p : Prop) [Decidable p] (a : M₀) (b : A) : (if p then a else 0) • b = if p then a • b else 0

theorem boole_smul {M₀ : Type u_2} {A : Type u_7} [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] (p : Prop) [Decidable p] (a : A) : (if p then 1 else 0) • a = if p then a else 0

theorem Pi.single_apply_smul {M₀ : Type u_2} {A : Type u_7} [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] {ι : Type u_12} [DecidableEq ι] (x : A) (i j : ι) : single i 1 j • x = single i x j

@[reducible, inline]

abbrev Function.Injective.mulActionWithZero {M₀ : Type u_2} {A : Type u_7} {A' : Type u_8} [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] [Zero A'] [SMul M₀ A'] (f : ZeroHom A' A) (hf : Injective ⇑f) (smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b) : MulActionWithZero M₀ A'

Pullback a MulActionWithZero structure along an injective zero-preserving homomorphism.

@[reducible, inline]

abbrev Function.Surjective.mulActionWithZero {M₀ : Type u_2} {A : Type u_7} {A' : Type u_8} [MonoidWithZero M₀] [Zero A] [MulActionWithZero M₀ A] [Zero A'] [SMul M₀ A'] (f : ZeroHom A A') (hf : Surjective ⇑f) (smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b) : MulActionWithZero M₀ A'

Pushforward a MulActionWithZero structure along a surjective zero-preserving homomorphism.

@[implicit_reducible]

def MulActionWithZero.compHom {M₀ : Type u_2} {M₀' : Type u_3} (A : Type u_7) [MonoidWithZero M₀] [MonoidWithZero M₀'] [Zero A] [MulActionWithZero M₀ A] (f : M₀' →*₀ M₀) : MulActionWithZero M₀' A

Compose a MulActionWithZero with a MonoidWithZeroHom, with action f r' • m

theorem smul_inv₀ {G₀ : Type u_4} {G₀' : Type u_5} [GroupWithZero G₀] [GroupWithZero G₀'] [MulActionWithZero G₀ G₀'] [SMulCommClass G₀ G₀' G₀'] [IsScalarTower G₀ G₀' G₀'] (c : G₀) (x : G₀') : (c • x)⁻¹ = c⁻¹ • x⁻¹

class DistribSMul (M : Type u_12) (A : Type u_13) [AddZeroClass A] extends SMulZeroClass M A : Type (max u_12 u_13)

Typeclass for scalar multiplication that preserves 0 and + on the right.

This is exactly DistribMulAction without the MulAction part.

• smul : M → A → A
• smul_zero (a : M) : a • 0 = 0
• smul_add (a : M) (x y : A) : a • (x + y) = a • x + a • y

  Scalar multiplication distributes across addition

theorem DistribSMul.ext {M : Type u_12} {A : Type u_13} {inst✝ : AddZeroClass A} {x y : DistribSMul M A} (smul : SMul.smul = SMul.smul) : x = y

theorem DistribSMul.ext_iff {M : Type u_12} {A : Type u_13} {inst✝ : AddZeroClass A} {x y : DistribSMul M A} : x = y ↔ SMul.smul = SMul.smul

@[simp]

theorem smul_add {M : Type u_1} {A : Type u_7} [AddZeroClass A] [DistribSMul M A] (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂

@[reducible, inline]

abbrev Function.Injective.distribSMul {M : Type u_1} {A : Type u_7} {B : Type u_9} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : B →+ A) (hf : Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : DistribSMul M B

Pullback a distributive scalar multiplication along an injective additive monoid homomorphism. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.distribSMul {M : Type u_1} {A : Type u_7} {B : Type u_9} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : A →+ B) (hf : Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : DistribSMul M B

Pushforward a distributive scalar multiplication along a surjective additive monoid homomorphism. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.distribSMulLeft {R : Type u_12} {S : Type u_13} {M : Type u_14} [AddZeroClass M] [DistribSMul R M] [SMul S M] (f : R → S) (hf : Surjective f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : DistribSMul S M

Push forward the multiplication of R on M along a compatible surjective map f : R → S.

See also Function.Surjective.distribMulActionLeft.

@[reducible, inline]

abbrev DistribSMul.compFun {M : Type u_1} {N : Type u_6} (A : Type u_7) [AddZeroClass A] [DistribSMul M A] (f : N → M) : DistribSMul N A

Compose a DistribSMul with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

def DistribSMul.toAddMonoidHom {M : Type u_1} (A : Type u_7) [AddZeroClass A] [DistribSMul M A] (x : M) : A →+ A

Each element of the scalars defines an additive monoid homomorphism.

@[simp]

theorem DistribSMul.toAddMonoidHom_apply {M : Type u_1} (A : Type u_7) [AddZeroClass A] [DistribSMul M A] (x : M) (x✝ : A) : (toAddMonoidHom A x) x✝ = x • x✝

instance AddMonoid.nat_smulCommClass {M : Type u_12} {A : Type u_13} [AddMonoid A] [DistribSMul M A] : SMulCommClass ℕ M A

instance AddMonoid.nat_smulCommClass' {M : Type u_12} {A : Type u_13} [AddMonoid A] [DistribSMul M A] : SMulCommClass M ℕ A

class DistribMulAction (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] extends MulAction M A : Type (max u_12 u_13)

Typeclass for multiplicative actions on additive structures.

For example, if G is a group (with group law written as multiplication) and A is an abelian group (with group law written as addition), then to give A a G-module structure (for example, to use the theory of group cohomology) is to say [DistribMulAction G A]. Note in that we do not use the Module typeclass for G-modules, as the Module typeclass is for modules over a ring rather than a group.

Mathematically, DistribMulAction G A is equivalent to giving A the structure of a ℤ[G]-module.

• smul : M → A → A
• mul_smul (x y : M) (b : A) : (x * y) • b = x • y • b
• one_smul (b : A) : 1 • b = b
• smul_zero (a : M) : a • 0 = 0

  Multiplying 0 by a scalar gives 0

• smul_add (a : M) (x y : A) : a • (x + y) = a • x + a • y

  Scalar multiplication distributes across addition

theorem DistribMulAction.ext {M : Type u_12} {A : Type u_13} {inst✝ : Monoid M} {inst✝¹ : AddMonoid A} {x y : DistribMulAction M A} (smul : SMul.smul = SMul.smul) : x = y

theorem DistribMulAction.ext_iff {M : Type u_12} {A : Type u_13} {inst✝ : Monoid M} {inst✝¹ : AddMonoid A} {x y : DistribMulAction M A} : x = y ↔ SMul.smul = SMul.smul

@[implicit_reducible, instance 100]

instance DistribMulAction.toDistribSMul {M : Type u_1} {A : Type u_7} [Monoid M] [AddMonoid A] [DistribMulAction M A] : DistribSMul M A

We make sure that the definition of DistribMulAction.toDistribSMul was done correctly, and the two paths from DistribMulAction to SMul are indeed definitionally equal.

@[reducible, inline]

abbrev Function.Injective.distribMulAction {M : Type u_1} {A : Type u_7} {B : Type u_9} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : B →+ A) (hf : Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : DistribMulAction M B

Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.distribMulAction {M : Type u_1} {A : Type u_7} {B : Type u_9} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : A →+ B) (hf : Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : DistribMulAction M B

Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].

@[deprecated DistribSMul.toAddMonoidHom (since := "2026-01-07")]

def DistribMulAction.toAddMonoidHom {M : Type u_1} (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : A →+ A

Each element of the monoid defines an additive monoid homomorphism.

@[simp]

theorem DistribMulAction.toAddMonoidHom_apply {M : Type u_1} (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) (x✝ : A) : (toAddMonoidHom A x) x✝ = x • x✝

def DistribMulAction.toAddMonoidEnd (M : Type u_1) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] : M →* AddMonoid.End A

Each element of the monoid defines an additive monoid homomorphism.

@[simp]

theorem DistribMulAction.toAddMonoidEnd_apply (M : Type u_1) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : (toAddMonoidEnd M A) x = DistribSMul.toAddMonoidHom A x

instance AddGroup.int_smulCommClass {M : Type u_1} {A : Type u_7} [AddGroup A] [DistribSMul M A] : SMulCommClass ℤ M A

instance AddGroup.int_smulCommClass' {M : Type u_1} {A : Type u_7} [AddGroup A] [DistribSMul M A] : SMulCommClass M ℤ A

@[simp]

theorem smul_neg {M : Type u_1} {A : Type u_7} [AddGroup A] [DistribSMul M A] (r : M) (x : A) : r • -x = -(r • x)

theorem smul_sub {M : Type u_1} {A : Type u_7} [AddGroup A] [DistribSMul M A] (r : M) (x y : A) : r • (x - y) = r • x - r • y

theorem smul_eq_zero_iff_eq {α : Type u_10} {β : Type u_11} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} : a • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_ne {α : Type u_10} {β : Type u_11} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} : a • x ≠ 0 ↔ x ≠ 0

@[implicit_reducible]

instance instSMulZeroClass {α : Type u_10} {β : Type u_11} [Group α] [GroupWithZero β] [MulDistribMulAction α β] : SMulZeroClass α β

@[simp]

theorem smul_inv₀' {α : Type u_10} {β : Type u_11} [Group α] [GroupWithZero β] [MulDistribMulAction α β] (g : α) (x : β) : g • x⁻¹ = (g • x)⁻¹

A version of smul_inv' for groups with zero.

theorem smul_div₀' {α : Type u_10} {β : Type u_11} [Group α] [GroupWithZero β] [MulDistribMulAction α β] (g : α) (x y : β) : g • (x / y) = g • x / g • y