# Documentation

Mathlib.Algebra.Module.Submodule.Pointwise

# Pointwise instances on Submodules #

This file provides:

• Submodule.pointwiseNeg

and the actions

• Submodule.pointwiseDistribMulAction
• Submodule.pointwiseMulActionWithZero

which matches the action of Set.mulActionSet.

These actions are available in the Pointwise locale.

## Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from GroupTheory/Submonoid/Pointwise.lean.

def Submodule.pointwiseNeg {R : Type u_2} {M : Type u_3} [] [] [Module R M] :
Neg ()

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.

Instances For
@[simp]
theorem Submodule.coe_set_neg {R : Type u_2} {M : Type u_3} [] [] [Module R M] (S : ) :
↑(-S) = -S
@[simp]
theorem Submodule.neg_toAddSubmonoid {R : Type u_2} {M : Type u_3} [] [] [Module R M] (S : ) :
@[simp]
theorem Submodule.mem_neg {R : Type u_2} {M : Type u_3} [] [] [Module R M] {g : M} {S : } :
g -S -g S
def Submodule.involutivePointwiseNeg {R : Type u_2} {M : Type u_3} [] [] [Module R M] :

Submodule.pointwiseNeg is involutive.

This is available as an instance in the Pointwise locale.

Instances For
@[simp]
theorem Submodule.neg_le_neg {R : Type u_2} {M : Type u_3} [] [] [Module R M] (S : ) (T : ) :
-S -T S T
theorem Submodule.neg_le {R : Type u_2} {M : Type u_3} [] [] [Module R M] (S : ) (T : ) :
-S T S -T
def Submodule.negOrderIso {R : Type u_2} {M : Type u_3} [] [] [Module R M] :

Submodule.pointwiseNeg as an order isomorphism.

Instances For
theorem Submodule.closure_neg {R : Type u_2} {M : Type u_3} [] [] [Module R M] (s : Set M) :
@[simp]
theorem Submodule.neg_inf {R : Type u_2} {M : Type u_3} [] [] [Module R M] (S : ) (T : ) :
-(S T) = -S -T
@[simp]
theorem Submodule.neg_sup {R : Type u_2} {M : Type u_3} [] [] [Module R M] (S : ) (T : ) :
-(S T) = -S -T
@[simp]
theorem Submodule.neg_bot {R : Type u_2} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.neg_top {R : Type u_2} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.neg_iInf {R : Type u_2} {M : Type u_3} [] [] [Module R M] {ι : Sort u_4} (S : ι) :
-⨅ (i : ι), S i = ⨅ (i : ι), -S i
@[simp]
theorem Submodule.neg_iSup {R : Type u_2} {M : Type u_3} [] [] [Module R M] {ι : Sort u_4} (S : ι) :
-⨆ (i : ι), S i = ⨆ (i : ι), -S i
@[simp]
theorem Submodule.neg_eq_self {R : Type u_2} {M : Type u_3} [Ring R] [] [Module R M] (p : ) :
-p = p
instance Submodule.pointwiseAddCommMonoid {R : Type u_2} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.add_eq_sup {R : Type u_2} {M : Type u_3} [] [] [Module R M] (p : ) (q : ) :
p + q = p q
@[simp]
theorem Submodule.zero_eq_bot {R : Type u_2} {M : Type u_3} [] [] [Module R M] :
0 =
def Submodule.pointwiseDistribMulAction {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module 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.

Instances For
@[simp]
theorem Submodule.coe_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] (a : α) (S : ) :
↑(a S) = a S
@[simp]
theorem Submodule.pointwise_smul_toAddSubmonoid {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] (a : α) (S : ) :
@[simp]
theorem Submodule.pointwise_smul_toAddSubgroup {α : Type u_1} [] {R : Type u_4} {M : Type u_5} [Ring R] [] [] [Module R M] [] (a : α) (S : ) :
theorem Submodule.smul_mem_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] (m : M) (a : α) (S : ) :
m Sa m a S
@[simp]
theorem Submodule.smul_bot' {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] (a : α) :

See also Submodule.smul_bot.

theorem Submodule.smul_sup' {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] (a : α) (S : ) (T : ) :
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} [] [] [Module R M] [] [] [] (a : α) (s : Set M) :
theorem Submodule.span_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] (a : α) (s : Set M) :
Submodule.span R (a s) = a
instance Submodule.pointwiseCentralScalar {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] [] [] [] :
@[simp]
theorem Submodule.smul_le_self_of_tower {R : Type u_2} {M : Type u_3} [] [] [Module R M] {α : Type u_4} [] [Module α R] [Module α M] [] [] (a : α) (S : ) :
a S S
def Submodule.pointwiseMulActionWithZero {α : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [Module α 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.pointwiseDistribMulAction. Note that add_smul does not hold so this cannot be stated as a Module.

Instances For