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].

Equations

• Function.Injective.smulZeroClass f hf smul = SMulZeroClass.mk ⋯

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

Equations

• f.smulZeroClass smul = SMulZeroClass.mk ⋯

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

Equations

• Function.Surjective.smulZeroClassLeft f hf hsmul = SMulZeroClass.mk ⋯

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

Equations

• SMulZeroClass.compFun A f = SMulZeroClass.mk ⋯

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.

Equations

• SMulZeroClass.toZeroHom A x = { toFun := fun (x_1 : A) => x • x_1, map_zero' := ⋯ }

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

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

Equations

• MulZeroClass.toSMulWithZero M₀ = SMulWithZero.mk ⋯

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

Like MulZeroClass.toSMulWithZero, but multiplies on the right.

Equations

• MulZeroClass.toOppositeSMulWithZero M₀ = SMulWithZero.mk ⋯

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

Equations

• Function.Injective.smulWithZero f hf smul = SMulWithZero.mk ⋯

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

Equations

• Function.Surjective.smulWithZero f hf smul = SMulWithZero.mk ⋯

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

Equations

• SMulWithZero.compHom A f = SMulWithZero.mk ⋯

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

Equations

• AddMonoid.natSMulWithZero = SMulWithZero.mk ⋯

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

Equations

• AddGroup.intSMulWithZero = SMulWithZero.mk ⋯

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
• one_smul (b : A) : 1 • b = b
• mul_smul (x y : M₀) (b : A) : (x * y) • b = x • y • 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.

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

Equations

• MulActionWithZero.toSMulWithZero M₀ A = SMulWithZero.mk ⋯

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

See also Semiring.toModule

Equations

• MonoidWithZero.toMulActionWithZero M₀ = MulActionWithZero.mk ⋯ ⋯

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

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

Equations

• MonoidWithZero.toOppositeMulActionWithZero M₀ = MulActionWithZero.mk ⋯ ⋯

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.

Equations

• Function.Injective.mulActionWithZero f hf smul = MulActionWithZero.mk ⋯ ⋯

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

Equations

• Function.Surjective.mulActionWithZero f hf smul = MulActionWithZero.mk ⋯ ⋯

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

Equations

• MulActionWithZero.compHom A f = MulActionWithZero.mk ⋯ ⋯

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 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₂

instance AddMonoidHom.smulZeroClass {M : Type u_1} {A : Type u_7} {B : Type u_9} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] : SMulZeroClass M (B →+ A)

Equations

• AddMonoidHom.smulZeroClass = SMulZeroClass.mk ⋯

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

Equations

• Function.Injective.distribSMul f hf smul = DistribSMul.mk ⋯

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

Equations

• Function.Surjective.distribSMul f hf smul = DistribSMul.mk ⋯

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

Equations

• Function.Surjective.distribSMulLeft f hf hsmul = DistribSMul.mk ⋯

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

Equations

• DistribSMul.compFun A f = DistribSMul.mk ⋯

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.

Equations

• DistribSMul.toAddMonoidHom A x = { toFun := fun (x_1 : A) => x • x_1, map_zero' := ⋯, map_add' := ⋯ }

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

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. This generalizes group modules.

• smul : M → A → A
• one_smul (b : A) : 1 • b = b
• mul_smul (x y : M) (b : A) : (x * y) • b = x • y • 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

@[instance 100]

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

Equations

• DistribMulAction.toDistribSMul = DistribSMul.mk ⋯

Since Lean 3 does not have definitional eta for structures, we have to 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].

Equations

• Function.Injective.distribMulAction f hf smul = DistribMulAction.mk ⋯ ⋯

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

Equations

• Function.Surjective.distribMulAction f hf smul = DistribMulAction.mk ⋯ ⋯

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.

Equations

• DistribMulAction.toAddMonoidHom A x = DistribSMul.toAddMonoidHom A x

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

Equations

• DistribMulAction.toAddMonoidEnd M A = { toFun := DistribMulAction.toAddMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }

@[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 = toAddMonoidHom A x

instance AddMonoid.nat_smulCommClass (M : Type u_1) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] : SMulCommClass ℕ M A

instance AddMonoid.nat_smulCommClass' (M : Type u_1) (A : Type u_7) [Monoid M] [AddMonoid A] [DistribMulAction M A] : SMulCommClass M ℕ A

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

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

@[simp]

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

theorem smul_sub {M : Type u_1} {A : Type u_7} [Monoid M] [AddGroup A] [DistribMulAction 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