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.
@[protected, instance]
def
submodule.pointwise_add_comm_monoid
{R : Type u_2}
{M : Type u_3}
[semiring R]
[add_comm_monoid M]
[module R M] :
add_comm_monoid (submodule R M)
Equations
- submodule.pointwise_add_comm_monoid = {add := has_sup.sup (semilattice_sup.to_has_sup (submodule R M)), add_assoc := _, zero := ⊥, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default ⊥ has_sup.sup submodule.pointwise_add_comm_monoid._proof_4 submodule.pointwise_add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[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) :
@[simp]
theorem
submodule.zero_eq_bot
{R : Type u_2}
{M : Type u_3}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[protected, 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] :
distrib_mul_action α (submodule 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
- submodule.pointwise_distrib_mul_action = {to_mul_action := {to_has_scalar := {smul := λ (a : α) (S : submodule R M), submodule.map (distrib_mul_action.to_linear_map R M a) S}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[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) :
@[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) :
(a • S).to_add_submonoid = a • S.to_add_submonoid
@[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) :
(a • S).to_add_subgroup = a • S.to_add_subgroup
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) :
@[protected, instance]
def
submodule.pointwise_central_scalar
{α : 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]
[distrib_mul_action αᵐᵒᵖ M]
[smul_comm_class αᵐᵒᵖ R M]
[is_central_scalar α M] :
is_central_scalar α (submodule R M)
@[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) :
@[protected, 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] :
mul_action_with_zero α (submodule 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.