mathlib documentation

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

We also add an instance:

source
@[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 : has_scalar R 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
source
@[protected, instance]
def mul_zero_class.to_smul_with_zero (R : Type u_1) [mul_zero_class R] :
smul_with_zero R R
Equations
source
@[protected, instance]
def mul_zero_class.to_opposite_smul_with_zero (R : Type u_1) [mul_zero_class R] :
smul_with_zero Rᵐᵒᵖ R

Like mul_zero_class.to_smul_with_zero, but multiplies on the right.

Equations
source
@[protected, instance]
def add_monoid.to_smul_with_zero (M : Type u_3) [add_monoid M] :
smul_with_zero ℕ M
Equations
source
@[simp]
theorem zero_smul (R : Type u_1) {M : Type u_3} [has_zero R] [has_zero M] [smul_with_zero R M] (m : M) :
0 • m = 0
source
@[simp]
theorem smul_zero' {R : Type u_1} (M : Type u_3) [has_zero R] [has_zero M] [smul_with_zero R M] (r : R) :
r • 0 = 0

Note that this lemma has different typeclass assumptions to smul_zero.

source
@[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] [smul_with_zero R M] [has_zero M'] [has_scalar R M'] (f : zero_hom M' M) (hf : function.injective ⇑f) (smul : ∀ (a : R) (b : M'), ⇑f (a • b) = a • ⇑f b) :
smul_with_zero R M'

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

Equations
source
@[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] [smul_with_zero R M] [has_zero M'] [has_scalar R M'] (f : zero_hom M M') (hf : function.surjective ⇑f) (smul : ∀ (a : R) (b : M), ⇑f (a • b) = a • ⇑f b) :
smul_with_zero R M'

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

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

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

Equations
source
@[class]
structure mul_action_with_zero (R : Type u_1) (M : Type u_3) [monoid_with_zero R] [has_zero M] :
Type (max u_1 u_3)
  • to_mul_action : mul_action R 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
source
@[protected, instance]
def mul_action_with_zero.to_smul_with_zero (R : Type u_1) (M : Type u_3) [monoid_with_zero R] [has_zero M] [m : mul_action_with_zero R M] :
smul_with_zero R M
Equations
source
@[protected, instance]
def monoid_with_zero.to_mul_action_with_zero (R : Type u_1) [monoid_with_zero R] :
mul_action_with_zero R R

See also semiring.to_module

Equations
source
@[protected, instance]
def monoid_with_zero.to_opposite_mul_action_with_zero (R : Type u_1) [monoid_with_zero R] :
mul_action_with_zero Rᵐᵒᵖ R

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

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

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

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

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

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

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

Equations