# mathlibdocumentation

algebra.module.submodule_pointwise

# Pointwise instances on submodules #

This file provides the actions

• submodule.pointwise_distrib_mul_action
• submodule.pointwise_mul_action_with_zero

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

@[protected, instance]
def submodule.pointwise_add_comm_monoid {R : Type u_2} {M : Type u_3} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.add_eq_sup {R : Type u_2} {M : Type u_3} [semiring R] [ M] (p q : M) :
p + q = p q
@[simp]
theorem submodule.zero_eq_bot {R : Type u_2} {M : Type u_3} [semiring R] [ M] :
0 =
@[protected, instance]
def submodule.pointwise_distrib_mul_action {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] :
M)

The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem submodule.coe_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] (a : α) (S : M) :
(a S) = a S
@[simp]
theorem submodule.pointwise_smul_to_add_submonoid {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] (a : α) (S : M) :
@[simp]
theorem submodule.pointwise_smul_to_add_subgroup {α : Type u_1} [monoid α] {R : Type u_2} {M : Type u_3} [ring R] [ M] [ M] [ M] (a : α) (S : M) :
theorem submodule.smul_mem_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] (m : M) (a : α) (S : M) :
m Sa m a S
@[protected, instance]
def submodule.pointwise_central_scalar {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] [ M] [ M] :
M)
@[simp]
theorem submodule.smul_le_self_of_tower {R : Type u_2} {M : Type u_3} [semiring R] [ M] {α : Type u_1} [semiring α] [ R] [ M] [ M] [ M] (a : α) (S : M) :
a S S
@[protected, instance]
def submodule.pointwise_mul_action_with_zero {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [semiring α] [ M] [ M] :
M)

The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

This is a stronger version of submodule.pointwise_distrib_mul_action. Note that add_smul does not hold so this cannot be stated as a module.

Equations