mathlib3 documentation

algebra.module.submodule.pointwise

Pointwise instances on submodules #

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

This file provides:

and the actions

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from group_theory/submonoid/pointwise.lean.

@[protected]
def submodule.has_pointwise_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :

The submodule with every element negated. Note if R is a ring and not just a semiring, this is a no-op, as shown by submodule.neg_eq_self.

Recall that When R is the semiring corresponding to the nonnegative elements of R', submodule R' M is the type of cones of M. This instance reflects such cones about 0.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem submodule.coe_set_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (S : submodule R M) :
@[simp]
@[simp]
theorem submodule.mem_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] {g : M} {S : submodule R M} :
g -S -g S
@[protected]

submodule.has_pointwise_neg is involutive.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem submodule.neg_le_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (S T : submodule R M) :
-S -T S T
theorem submodule.neg_le {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (S T : submodule R M) :
-S T S -T
theorem submodule.closure_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (s : set M) :
@[simp]
theorem submodule.neg_inf {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (S T : submodule R M) :
-(S T) = -S -T
@[simp]
theorem submodule.neg_sup {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (S T : submodule R M) :
-(S T) = -S -T
@[simp]
theorem submodule.neg_bot {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
@[simp]
theorem submodule.neg_top {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
@[simp]
theorem submodule.neg_infi {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] {ι : Sort u_1} (S : ι submodule R M) :
(- (i : ι), S i) = (i : ι), -S i
@[simp]
theorem submodule.neg_supr {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] {ι : Sort u_1} (S : ι submodule R M) :
(- (i : ι), S i) = (i : ι), -S i
@[simp]
theorem submodule.neg_eq_self {R : Type u_2} {M : Type u_3} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
-p = p
@[protected, instance]
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 =
@[protected]

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 S a m a S
@[simp]
theorem submodule.smul_bot' {α : 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 : α) :

See also submodule.smul_bot.

theorem submodule.smul_sup' {α : 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 T : submodule R M) :
a (S T) = a S a T

See also submodule.smul_sup.

theorem submodule.smul_span {α : 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 : set M) :
theorem submodule.span_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 : set M) :
@[protected, instance]
@[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
@[protected]
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