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.

source
@[protected]
def submodule.has_pointwise_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
has_neg (submodule 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
source
@[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) :
↑-S = -↑S
source
@[simp]
theorem submodule.neg_to_add_submonoid {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (S : submodule R M) :
(-S).to_add_submonoid = -S.to_add_submonoid
source
@[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
source
@[protected]
def submodule.has_involutive_pointwise_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
has_involutive_neg (submodule R M)

submodule.has_pointwise_neg is involutive.

This is available as an instance in the pointwise locale.

Equations
source
@[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
source
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
source
def submodule.neg_order_iso {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
submodule R M ≃o submodule R M

submodule.has_pointwise_neg as an order isomorphism.

Equations
source
theorem submodule.closure_neg {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] (s : set M) :
submodule.span R (-s) = -submodule.span R s
source
@[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
source
@[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
source
@[simp]
theorem submodule.neg_bot {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
-⊥ = ⊥
source
@[simp]
theorem submodule.neg_top {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_group M] [module R M] :
-⊤ = ⊤
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem submodule.zero_eq_bot {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
0 = ⊥
source
@[protected, instance]
def submodule.canonically_ordered_add_monoid {R : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
canonically_ordered_add_monoid (submodule R M)
Equations
source
@[protected]
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
source
@[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
source
@[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
source
@[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
source
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
source
@[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 : α) :
a • ⊥ = ⊥

See also submodule.smul_bot.

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

source
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) :
a • submodule.span R s = submodule.span R (a • s)
source
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) :
submodule.span R (a • s) = a • submodule.span R s
source
@[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)
source
@[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
source
@[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] :
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.

Equations