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:

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

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) :

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

Equations
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) :

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] [smul_with_zero R M] [has_zero R'] (f : zero_hom R' R) :

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) [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
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) :

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

Equations
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) :

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] [monoid_with_zero R'] [has_zero M] [mul_action_with_zero R M] (f : monoid_with_zero_hom R' R) :

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

Equations