mathlib3 documentation

algebra.smul_with_zero

Introduce smul_with_zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

Main declarations #

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

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 of this typeclass
Instances of other typeclasses for smul_with_zero
  • smul_with_zero.has_sizeof_inst
@[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
theorem smul_eq_zero_of_left {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [smul_with_zero R M] {a : R} (h : a = 0) (b : M) :
a b = 0
theorem smul_eq_zero_of_right {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [smul_with_zero R M] {b : M} (a : R) (h : b = 0) :
a b = 0
theorem left_ne_zero_of_smul {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [smul_with_zero R M] {a : R} {b : M} :
a b 0 a 0
theorem right_ne_zero_of_smul {R : Type u_1} {M : Type u_3} [has_zero R] [has_zero M] [smul_with_zero R M] {a : R} {b : M} :
a b 0 b 0
@[protected, reducible]
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_smul 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
@[protected, reducible]
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_smul 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)

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 of this typeclass
Instances of other typeclasses for mul_action_with_zero
  • mul_action_with_zero.has_sizeof_inst
@[protected]
@[protected, reducible]
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_smul 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
@[protected, reducible]
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_smul 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
theorem smul_inv₀ {α : Type u_5} {β : Type u_6} [group_with_zero α] [group_with_zero β] [mul_action_with_zero α β] [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :
def smul_monoid_with_zero_hom {α : Type u_1} {β : Type u_2} [monoid_with_zero α] [mul_zero_one_class β] [mul_action_with_zero α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
α × β →*₀ β

Scalar multiplication as a monoid homomorphism with zero.

Equations