Documentation

Mathlib.Algebra.SMulWithZero

Introduce SMulWithZero #

In analogy with the usual monoid action on a Type M, we introduce an action of a MonoidWithZero on a Type with 0.

In particular, for Types R and M, both containing 0, we define SMulWithZero R M to be the typeclass where the products r • 0 and 0 • m vanish for all r : R and all m : M.

Moreover, in the case in which R is a MonoidWithZero, we introduce the typeclass MulActionWithZero R M, mimicking group actions and having an absorbing 0 in R. Thus, the action is required to be compatible with

We also add an instance:

Main declarations #

source
class SMulWithZero (R : Type u_1) (M : Type u_3) [Zero R] [Zero M] extends SMulZeroClass R M :
Type (max u_1 u_3)

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

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

    Scalar multiplication by the scalar 0 is 0.

Instances
source
instance MulZeroClass.toSMulWithZero (R : Type u_1) [MulZeroClass R] :
SMulWithZero R R
Equations
source
instance MulZeroClass.toOppositeSMulWithZero (R : Type u_1) [MulZeroClass R] :
SMulWithZero Rᵐᵒᵖ R

Like MulZeroClass.toSMulWithZero, but multiplies on the right.

Equations
source
@[simp]
theorem zero_smul (R : Type u_1) {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] (m : M) :
0 • m = 0
source
theorem smul_eq_zero_of_left {R : Type u_1} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] {a : R} (h : a = 0) (b : M) :
a • b = 0
source
theorem left_ne_zero_of_smul {R : Type u_1} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] {a : R} {b : M} :
a • b ≠ 0 → a ≠ 0
source
@[reducible, inline]
abbrev Function.Injective.smulWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [Zero R] [Zero M] [SMulWithZero R M] [Zero M'] [SMul R M'] (f : ZeroHom M' M) (hf : Injective ⇑f) (smul : ∀ (a : R) (b : M'), f (a • b) = a • f b) :
SMulWithZero R M'

Pullback a SMulWithZero structure along an injective zero-preserving homomorphism. See note [reducible non-instances].

Equations
source
@[reducible, inline]
abbrev Function.Surjective.smulWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [Zero R] [Zero M] [SMulWithZero R M] [Zero M'] [SMul R M'] (f : ZeroHom M M') (hf : Surjective ⇑f) (smul : ∀ (a : R) (b : M), f (a • b) = a • f b) :
SMulWithZero R M'

Pushforward a SMulWithZero structure along a surjective zero-preserving homomorphism. See note [reducible non-instances].

Equations
source
def SMulWithZero.compHom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [Zero R] [Zero M] [SMulWithZero R M] [Zero R'] (f : ZeroHom R' R) :
SMulWithZero R' M

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

Equations
source
instance AddMonoid.natSMulWithZero {M : Type u_3} [AddMonoid M] :
SMulWithZero ℕ M
Equations
source
instance AddGroup.intSMulWithZero {M : Type u_3} [AddGroup M] :
SMulWithZero ℤ M
Equations
source
class MulActionWithZero (R : Type u_1) (M : Type u_3) [MonoidWithZero R] [Zero M] extends MulAction R M :
Type (max u_1 u_3)

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

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

    Scalar multiplication by any element send 0 to 0.

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

    Scalar multiplication by the scalar 0 is 0.

Instances
source
@[instance 100]
instance MulActionWithZero.toSMulWithZero (R : Type u_5) (M : Type u_6) {x✝ : MonoidWithZero R} {x✝¹ : Zero M} [m : MulActionWithZero R M] :
SMulWithZero R M
Equations
source
instance MonoidWithZero.toMulActionWithZero (R : Type u_1) [MonoidWithZero R] :
MulActionWithZero R R

See also Semiring.toModule

Equations
source
instance MonoidWithZero.toOppositeMulActionWithZero (R : Type u_1) [MonoidWithZero R] :
MulActionWithZero Rᵐᵒᵖ R

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

Equations
source
theorem MulActionWithZero.subsingleton (R : Type u_1) (M : Type u_3) [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Subsingleton R] :
Subsingleton M
source
theorem MulActionWithZero.nontrivial (R : Type u_1) (M : Type u_3) [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] :
Nontrivial R
source
theorem ite_zero_smul {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] (p : Prop) [Decidable p] (a : R) (b : M) :
(if p then a else 0) • b = if p then a • b else 0
source
theorem boole_smul {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] (p : Prop) [Decidable p] (a : M) :
(if p then 1 else 0) • a = if p then a else 0
source
theorem Pi.single_apply_smul {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] {ι : Type u_5} [DecidableEq ι] (x : M) (i j : ι) :
single i 1 j • x = single i x j
source
@[reducible, inline]
abbrev Function.Injective.mulActionWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Zero M'] [SMul R M'] (f : ZeroHom M' M) (hf : Injective ⇑f) (smul : ∀ (a : R) (b : M'), f (a • b) = a • f b) :
MulActionWithZero R M'

Pullback a MulActionWithZero structure along an injective zero-preserving homomorphism. See note [reducible non-instances].

Equations
source
@[reducible, inline]
abbrev Function.Surjective.mulActionWithZero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Zero M'] [SMul R M'] (f : ZeroHom M M') (hf : Surjective ⇑f) (smul : ∀ (a : R) (b : M), f (a • b) = a • f b) :
MulActionWithZero R M'

Pushforward a MulActionWithZero structure along a surjective zero-preserving homomorphism. See note [reducible non-instances].

Equations
source
def MulActionWithZero.compHom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [MonoidWithZero R] [MonoidWithZero R'] [Zero M] [MulActionWithZero R M] (f : R' →*₀ R) :
MulActionWithZero R' M

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

Equations
source
theorem smul_inv₀ {α : Type u_5} {β : Type u_6} [GroupWithZero α] [GroupWithZero β] [MulActionWithZero α β] [SMulCommClass α β β] [IsScalarTower α β β] (c : α) (x : β) :
(c • x)⁻¹ = c⁻¹ • x⁻¹