# mathlibdocumentation

algebra.smul_with_zero

# Introduce smul_with_zero#

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

In particular, for Types R and M, both containing 0, we define smul_with_zero 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 monoid_with_zero, we introduce the typeclass mul_action_with_zero 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 monoid_with_zero, acting as zero;
• associativity of the monoid.

We also add an instance:

• any monoid_with_zero has a mul_action_with_zero R R acting on itself.

## Main declarations #

• smul_monoid_with_zero_hom: Scalar multiplication bundled as a morphism of monoids with zero.
@[class]
structure smul_with_zero (R : Type u_1) (M : Type u_3) [has_zero R] [has_zero M] :
Type (max u_1 u_3)
• to_has_scalar : M
• smul_zero : ∀ (r : R), r 0 = 0
• zero_smul : ∀ (m : M), 0 m = 0

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

Instances
@[protected, instance]
def mul_zero_class.to_smul_with_zero (R : Type u_1)  :
Equations
@[protected, instance]

Like mul_zero_class.to_smul_with_zero, but multiplies on the right.

Equations
@[protected, instance]
Equations
@[simp]
theorem zero_smul (R : Type u_1) {M : Type u_3} [has_zero R] [has_zero M] [ M] (m : M) :
0 m = 0
@[simp]
theorem smul_zero' {R : Type u_1} (M : Type u_3) [has_zero R] [has_zero M] [ M] (r : R) :
r 0 = 0

Note that this lemma has different typeclass assumptions to smul_zero.

@[protected]
def function.injective.smul_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero R] [has_zero M] [ M] [has_zero M'] [ M'] (f : zero_hom M' M) (hf : function.injective f) (smul : ∀ (a : R) (b : M'), f (a b) = a f b) :
M'

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

Equations
@[protected]
def function.surjective.smul_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero R] [has_zero M] [ M] [has_zero M'] [ M'] (f : M') (hf : function.surjective f) (smul : ∀ (a : R) (b : M), f (a b) = a f b) :
M'

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

Equations
def smul_with_zero.comp_hom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [has_zero R] [has_zero M] [ M] [has_zero R'] (f : zero_hom R' R) :
M

Compose a smul_with_zero with a zero_hom, with action f r' • m

Equations
@[class]
structure mul_action_with_zero (R : Type u_1) (M : Type u_3) [has_zero M] :
Type (max u_1 u_3)
• to_mul_action : M
• smul_zero : ∀ (r : R), r 0 = 0
• zero_smul : ∀ (m : M), 0 m = 0

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

Instances
@[protected, instance]
def mul_action_with_zero.to_smul_with_zero (R : Type u_1) (M : Type u_3) [has_zero M] [m : M] :
Equations
@[protected, instance]

See also semiring.to_module

Equations
@[protected, instance]

Like monoid_with_zero.to_mul_action_with_zero, but multiplies on the right. See also semiring.to_opposite_module

Equations
@[protected]
def function.injective.mul_action_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero M] [ M] [has_zero M'] [ M'] (f : zero_hom M' M) (hf : function.injective f) (smul : ∀ (a : R) (b : M'), f (a b) = a f b) :

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

Equations
@[protected]
def function.surjective.mul_action_with_zero {R : Type u_1} {M : Type u_3} {M' : Type u_4} [has_zero M] [ M] [has_zero M'] [ M'] (f : M') (hf : function.surjective f) (smul : ∀ (a : R) (b : M), f (a b) = a f b) :

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

Equations
def mul_action_with_zero.comp_hom {R : Type u_1} {R' : Type u_2} (M : Type u_3) [monoid_with_zero R'] [has_zero M] [ M] (f : R' →*₀ R) :

Compose a mul_action_with_zero with a monoid_with_zero_hom, with action f r' • m

Equations
theorem smul_inv₀ {α : Type u_5} {β : Type u_6} [ β] [ β] [ β] (c : α) (x : β) :
@[simp]
theorem smul_monoid_with_zero_hom_apply {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] (ᾰ : α × β) :
def smul_monoid_with_zero_hom {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] :
α × β →*₀ β

Scalar multiplication as a monoid homomorphism with zero.

Equations