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

• the unit of the monoid, acting as the identity;
• the zero of the MonoidWithZero, acting as zero;
• associativity of the monoid.

We also add an instance:

• any MonoidWithZero has a MulActionWithZero R R acting on itself.

Main declarations

• smulMonoidWithZeroHom: Scalar multiplication bundled as a morphism of monoids with zero.

ink

class SMulWithZero (R : Type u_1) (M : Type u_2) [inst : Zero R] [inst : Zero M] extends SMulZeroClass : Type (maxu_1u_2)

• Scalar multiplication by the scalar 0 is 0.

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

SMulWithZero is a class consisting of a Type R with 0 ∈ R∈ 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.

ink

instance MulZeroClass.toSMulWithZero (R : Type u_1) [inst : MulZeroClass R] : SMulWithZero R R

Equations

• MulZeroClass.toSMulWithZero R = SMulWithZero.mk (_ : ∀ (a : R), 0 * a = 0)

ink

instance MulZeroClass.toOppositeSMulWithZero (R : Type u_1) [inst : MulZeroClass R] : SMulWithZero Rᵐᵒᵖ R

Like MulZeroClass.toSMulWithZero, but multiplies on the right.

Equations

• MulZeroClass.toOppositeSMulWithZero R = SMulWithZero.mk (_ : ∀ (a : R), a * 0 = 0)

ink

@[simp]

theorem zero_smul (R : Type u_2) {M : Type u_1} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] (m : M) : 0 • m = 0

ink

theorem smul_eq_zero_of_left {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] {a : R} (h : a = 0) (b : M) : a • b = 0

ink

theorem smul_eq_zero_of_right {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] {b : M} (a : R) (h : b = 0) : a • b = 0

ink

theorem left_ne_zero_of_smul {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] {a : R} {b : M} : a • b ≠ 0 → a ≠ 0

ink

theorem right_ne_zero_of_smul {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] {a : R} {b : M} : a • b ≠ 0 → b ≠ 0

ink

def Function.Injective.smulWithZero {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] [inst : Zero M'] [inst : SMul R M'] (f : ZeroHom M' M) (hf : Function.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

• Function.Injective.smulWithZero f hf smul = SMulWithZero.mk (_ : ∀ (a : M'), 0 • a = 0)

ink

def Function.Surjective.smulWithZero {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] [inst : Zero M'] [inst : SMul R M'] (f : ZeroHom M M') (hf : Function.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

• Function.Surjective.smulWithZero f hf smul = SMulWithZero.mk (_ : ∀ (m : M'), 0 • m = 0)

ink

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

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

Equations

• SMulWithZero.compHom M f = SMulWithZero.mk (_ : ∀ (m : M), ↑f 0 • m = 0)

ink

instance AddMonoid.natSMulWithZero {M : Type u_1} [inst : AddMonoid M] : SMulWithZero ℕ M

Equations

• AddMonoid.natSMulWithZero = SMulWithZero.mk (_ : ∀ (a : M), 0 • a = 0)

ink

instance AddGroup.intSMulWithZero {M : Type u_1} [inst : AddGroup M] : SMulWithZero ℤ M

Equations

• AddGroup.intSMulWithZero = SMulWithZero.mk (_ : ∀ (a : M), 0 • a = 0)

ink

class MulActionWithZero (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst : Zero M] extends MulAction : Type (maxu_1u_2)

• Scalar multiplication by any element send 0 to 0.

  smul_zero : ∀ (r : R), r • 0 = 0

• Scalar multiplication by the scalar 0 is 0.

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

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∈ R, and with associativity of multiplication on the monoid M.

ink

instance MulActionWithZero.toSMulWithZero (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst : Zero M] [m : MulActionWithZero R M] : SMulWithZero R M

Equations

• MulActionWithZero.toSMulWithZero R M = SMulWithZero.mk (_ : ∀ (m : M), 0 • m = 0)

ink

instance MonoidWithZero.toMulActionWithZero (R : Type u_1) [inst : MonoidWithZero R] : MulActionWithZero R R

See also Semiring.toModule

Equations

• MonoidWithZero.toMulActionWithZero R = let src := MulZeroClass.toSMulWithZero R; let src_1 := Monoid.toMulAction R; MulActionWithZero.mk (_ : ∀ (a : R), a • 0 = 0) (_ : ∀ (m : R), 0 • m = 0)

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

theorem MulActionWithZero.subsingleton (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] [inst : Subsingleton R] : Subsingleton M

ink

theorem MulActionWithZero.nontrivial (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] [inst : Nontrivial M] : Nontrivial R

ink

def Function.Injective.mulActionWithZero {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] [inst : Zero M'] [inst : SMul R M'] (f : ZeroHom M' M) (hf : Function.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

• One or more equations did not get rendered due to their size.

ink

def Function.Surjective.mulActionWithZero {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] [inst : Zero M'] [inst : SMul R M'] (f : ZeroHom M M') (hf : Function.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

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• MulActionWithZero.compHom M f = let src := SMulWithZero.compHom M ↑f; MulActionWithZero.mk (_ : ∀ (a : R'), a • 0 = 0) (_ : ∀ (m : M), 0 • m = 0)

ink

theorem smul_inv₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : GroupWithZero β] [inst : MulActionWithZero α β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] (c : α) (x : β) : (c • x)⁻¹ = c⁻¹ • x⁻¹

ink

@[simp]

theorem smulMonoidWithZeroHom_apply {α : Type u_1} {β : Type u_2} [inst : MonoidWithZero α] [inst : MulZeroOneClass β] [inst : MulActionWithZero α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] : ∀ (a : α × β), ↑smulMonoidWithZeroHom a = OneHom.toFun (↑smulMonoidHom) a

ink

def smulMonoidWithZeroHom {α : Type u_1} {β : Type u_2} [inst : MonoidWithZero α] [inst : MulZeroOneClass β] [inst : MulActionWithZero α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] : α × β →*₀ β

Scalar multiplication as a monoid homomorphism with zero.

Equations

• One or more equations did not get rendered due to their size.