mathlib3documentation

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:

• submodule.has_pointwise_neg

and 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.

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] [ 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] [ M] (S : M) :
@[simp]
theorem submodule.neg_to_add_submonoid {R : Type u_2} {M : Type u_3} [semiring R] [ M] (S : M) :
@[simp]
theorem submodule.mem_neg {R : Type u_2} {M : Type u_3} [semiring R] [ M] {g : M} {S : M} :
g -S -g S
@[protected]
def submodule.has_involutive_pointwise_neg {R : Type u_2} {M : Type u_3} [semiring R] [ M] :

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] [ M] (S T : M) :
-S -T S T
theorem submodule.neg_le {R : Type u_2} {M : Type u_3} [semiring R] [ M] (S T : M) :
-S T S -T
def submodule.neg_order_iso {R : Type u_2} {M : Type u_3} [semiring R] [ M] :
M ≃o M

submodule.has_pointwise_neg as an order isomorphism.

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

See also submodule.smul_bot.

theorem submodule.smul_sup' {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] (a : α) (S T : 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] [ M] [monoid α] [ M] [ M] (a : α) (s : set M) :
a = (a s)
theorem submodule.span_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [semiring R] [ M] [monoid α] [ M] [ M] (a : α) (s : set M) :
(a s) = a
@[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]
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