mathlib documentation

algebra.module.submodule_pointwise

Pointwise instances on submodules #

This file provides the actions

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

@[instance]
def submodule.pointwise_add_comm_monoid {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[simp]
theorem submodule.add_eq_sup {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (p q : submodule R M) :
p + q = p q
@[simp]
theorem submodule.zero_eq_bot {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
0 =
@[instance]
def submodule.pointwise_distrib_mul_action {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] [monoid α] [distrib_mul_action α M] [smul_comm_class α R 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] [add_comm_monoid M] [module R M] [monoid α] [distrib_mul_action α M] [smul_comm_class α R M] (a : α) (S : submodule R 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] [add_comm_monoid M] [module R M] [monoid α] [distrib_mul_action α M] [smul_comm_class α R M] (a : α) (S : submodule R M) :
@[simp]
theorem submodule.pointwise_smul_to_add_subgroup {α : Type u_1} [monoid α] {R : Type u_2} {M : Type u_3} [ring R] [add_comm_group M] [distrib_mul_action α M] [module R M] [smul_comm_class α R M] (a : α) (S : submodule R M) :
theorem submodule.smul_mem_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] [monoid α] [distrib_mul_action α M] [smul_comm_class α R M] (m : M) (a : α) (S : submodule R M) :
m Sa m a S
@[simp]
theorem submodule.smul_le_self_of_tower {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M] (a : α) (S : submodule R M) :
a S S
@[instance]
def submodule.pointwise_mul_action_with_zero {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] [semiring α] [module α M] [smul_comm_class α R 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