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

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_smul_zero_class : smul_zero_class R M
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 of this typeclass

Instances of other typeclasses for smul_with_zero

smul_with_zero.has_sizeof_inst

@[protected, instance]

def mul_zero_class.to_smul_with_zero (R : Type u_1) [mul_zero_class R] :

smul_with_zero R R

Equations

mul_zero_class.to_smul_with_zero R = {to_smul_zero_class := {to_has_smul := {smul := has_mul.mul (mul_zero_class.to_has_mul R)}, smul_zero := _}, zero_smul := _}

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

mul_zero_class.to_opposite_smul_with_zero R = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul (has_mul.to_has_opposite_smul R)}, smul_zero := _}, zero_smul := _}

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

smul_with_zero R M'

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

Equations

function.injective.smul_with_zero f hf smul = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul _inst_6}, smul_zero := _}, zero_smul := _}

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

smul_with_zero R M'

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

Equations

function.surjective.smul_with_zero f hf smul = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul _inst_6}, smul_zero := _}, zero_smul := _}

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

smul_with_zero.comp_hom M f = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul ∘ ⇑f}, smul_zero := _}, zero_smul := _}

@[protected, instance]

def add_monoid.nat_smul_with_zero {M : Type u_3} [add_monoid M] :

smul_with_zero ℕ M

Equations

add_monoid.nat_smul_with_zero = {to_smul_zero_class := {to_has_smul := add_monoid.has_smul_nat _inst_1, smul_zero := _}, zero_smul := _}

@[protected, instance]

def add_group.int_smul_with_zero {M : Type u_3} [add_group M] :

smul_with_zero ℤ M

Equations

add_group.int_smul_with_zero = {to_smul_zero_class := {to_has_smul := sub_neg_monoid.has_smul_int (subtraction_monoid.to_sub_neg_monoid M), smul_zero := _}, zero_smul := _}

@[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 of this typeclass

Instances of other typeclasses for mul_action_with_zero

mul_action_with_zero.has_sizeof_inst

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

mul_action_with_zero.to_smul_with_zero R M = {to_smul_zero_class := {to_has_smul := mul_action.to_has_smul mul_action_with_zero.to_mul_action, smul_zero := _}, zero_smul := _}

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

monoid_with_zero.to_mul_action_with_zero R = {to_mul_action := {to_has_smul := smul_zero_class.to_has_smul smul_with_zero.to_smul_zero_class, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

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

monoid_with_zero.to_opposite_mul_action_with_zero R = {to_mul_action := {to_has_smul := smul_zero_class.to_has_smul smul_with_zero.to_smul_zero_class, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

@[protected]

theorem mul_action_with_zero.subsingleton (R : Type u_1) (M : Type u_3) [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] [subsingleton R] :

@[protected]

theorem mul_action_with_zero.nontrivial (R : Type u_1) (M : Type u_3) [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] [nontrivial M] :

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

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

function.injective.mul_action_with_zero f hf smul = {to_mul_action := {to_has_smul := mul_action.to_has_smul (function.injective.mul_action ⇑f hf smul), one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

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

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

function.surjective.mul_action_with_zero f hf smul = {to_mul_action := {to_has_smul := mul_action.to_has_smul (function.surjective.mul_action ⇑f hf smul), one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

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

mul_action_with_zero.comp_hom M f = {to_mul_action := {to_has_smul := {smul := has_smul.smul ∘ ⇑f}, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

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

(c • x)⁻¹ = c⁻¹ • x⁻¹

@[simp]

theorem smul_monoid_with_zero_hom_apply {α : Type u_1} {β : Type u_2} [monoid_with_zero α] [mul_zero_one_class β] [mul_action_with_zero α β] [is_scalar_tower α β β] [smul_comm_class α β β] (ᾰ : α × β) :

⇑smul_monoid_with_zero_hom ᾰ = smul_monoid_hom.to_fun ᾰ

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

smul_monoid_with_zero_hom = {to_fun := smul_monoid_hom.to_fun, map_zero' := _, map_one' := _, map_mul' := _}