Documentation

Mathlib.Algebra.Module.Submodule.Pointwise

Pointwise instances on `Submodule`s #

This file provides:

Submodule.pointwiseNeg

and the actions

which matches the action of Set.mulActionSet.

This file also provides:

Submodule.pointwiseSetSMulSubmodule: for R-module M, a s : Set R can act on N : Submodule R M by defining s • N to be the smallest submodule containing all a • n where a ∈ s and n ∈ N.

These actions are available in the Pointwise locale.

Implementation notes #

For an R-module M, The action of a subset of R acting on a submodule of M introduced in section set_acting_on_submodules does not have a counterpart in the file Mathlib.Algebra.Group.Submonoid.Pointwise.

Other than section set_acting_on_submodules, most of the lemmas in this file are direct copies of lemmas from the file Mathlib.Algebra.Group.Submonoid.Pointwise.

def Submodule.pointwiseNeg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] :

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

Submodule.pointwiseNeg = { neg := fun (p : Submodule R M) => let __src := -p.toAddSubmonoid; { toAddSubmonoid := __src, smul_mem' := ⋯ } }

@[simp]

theorem Submodule.coe_set_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) :

↑(-S) = -↑S

@[simp]

theorem Submodule.neg_toAddSubmonoid {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) :

(-S).toAddSubmonoid = -S.toAddSubmonoid

@[simp]

theorem Submodule.mem_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {g : M} {S : Submodule R M} :

g ∈ -S ↔ -g ∈ S

def Submodule.involutivePointwiseNeg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] :

InvolutiveNeg (Submodule R M)

Submodule.pointwiseNeg is involutive.

This is available as an instance in the Pointwise locale.

Equations

Submodule.involutivePointwiseNeg = InvolutiveNeg.mk ⋯

@[simp]

theorem Submodule.neg_le_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup 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] [AddCommGroup M] [Module R M] (S T : Submodule R M) :

-S ≤ T ↔ S ≤ -T

def Submodule.negOrderIso {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] :

Submodule R M ≃o Submodule R M

Submodule.pointwiseNeg as an order isomorphism.

Equations

Submodule.negOrderIso = { toEquiv := Equiv.neg (Submodule R M), map_rel_iff' := ⋯ }

theorem Submodule.closure_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (s : Set M) :

span R (-s) = -span R s

@[simp]

theorem Submodule.neg_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup 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] [AddCommGroup 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] [AddCommGroup M] [Module R M] :

@[simp]

theorem Submodule.neg_top {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] :

@[simp]

theorem Submodule.neg_iInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {ι : Sort u_4} (S : ι → Submodule R M) :

-⨅ (i : ι), S i = ⨅ (i : ι), -S i

@[simp]

theorem Submodule.neg_iSup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {ι : Sort u_4} (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] [AddCommGroup M] [Module R M] (p : Submodule R M) :

-p = p

instance Submodule.pointwiseZero {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

Zero (Submodule R M)

Equations

Submodule.pointwiseZero = { zero := ⊥ }

instance Submodule.pointwiseAdd {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

Add (Submodule R M)

Equations

Submodule.pointwiseAdd = { add := fun (x1 x2 : Submodule R M) => x1 ⊔ x2 }

instance Submodule.pointwiseAddCommMonoid {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

AddCommMonoid (Submodule R M)

Equations

Submodule.pointwiseAddCommMonoid = AddCommMonoid.mk ⋯

@[simp]

theorem Submodule.add_eq_sup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] :

instance Submodule.instOrderedAddCommMonoid {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

OrderedAddCommMonoid (Submodule R M)

Equations

Submodule.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

instance Submodule.instCanonicallyOrderedAdd {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

CanonicallyOrderedAdd (Submodule R M)

def Submodule.pointwiseDistribMulAction {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] :

DistribMulAction α (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.pointwiseDistribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem Submodule.coe_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (S : Submodule R M) :

↑(a • S) = a • ↑S

@[simp]

theorem Submodule.pointwise_smul_toAddSubmonoid {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (S : Submodule R M) :

(a • S).toAddSubmonoid = a • S.toAddSubmonoid

@[simp]

theorem Submodule.pointwise_smul_toAddSubgroup {α : Type u_1} [Monoid α] {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [DistribMulAction α M] [Module R M] [SMulCommClass α R M] (a : α) (S : Submodule R M) :

(a • S).toAddSubgroup = a • S.toAddSubgroup

theorem Submodule.smul_mem_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (m : M) (a : α) (S : Submodule R M) :

m ∈ S → a • m ∈ a • S

instance Submodule.instCovariantClassHSMulLe {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] :

CovariantClass α (Submodule R M) HSMul.hSMul LE.le

@[simp]

theorem Submodule.smul_bot' {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) :

a • ⊥ = ⊥

See also Submodule.smul_bot.

theorem Submodule.smul_sup' {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α 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] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (s : Set M) :

a • span R s = span R (a • s)

theorem Submodule.smul_def {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (S : Submodule R M) :

a • S = span R (a • ↑S)

theorem Submodule.span_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (s : Set M) :

span R (a • s) = a • span R s

instance Submodule.pointwiseCentralScalar {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] [DistribMulAction αᵐᵒᵖ M] [SMulCommClass αᵐᵒᵖ R M] [IsCentralScalar α M] :

IsCentralScalar α (Submodule R M)

@[simp]

theorem Submodule.smul_le_self_of_tower {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Semiring α] [Module α R] [Module α M] [SMulCommClass α R M] [IsScalarTower α R M] (a : α) (S : Submodule R M) :

a • S ≤ S

def Submodule.pointwiseMulActionWithZero {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring α] [Module α M] [SMulCommClass α R M] :

MulActionWithZero α (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.pointwiseDistribMulAction. Note that add_smul does not hold so this cannot be stated as a Module.

Equations

Submodule.pointwiseMulActionWithZero = MulActionWithZero.mk ⋯ ⋯

Sets acting on Submodules #

Let R be a (semi)ring and M an R-module. Let S be a monoid which acts on M distributively, then subsets of S can act on submodules of M. For subset s ⊆ S and submodule N ≤ M, we define s • N to be the smallest submodule containing all r • n where r ∈ s and n ∈ N.

Results #

For arbitrary monoids S acting distributively on M, there is an induction principle for s • N: To prove P holds for all s • N, it is enough to prove:

for all r ∈ s and n ∈ N, P (r • n);
for all r and m ∈ s • N, P (r • n);
for all m₁, m₂, P m₁ and P m₂ implies P (m₁ + m₂);
P 0.

To invoke this induction principle, use induction x, hx using Submodule.set_smul_inductionOn where x : M and hx : x ∈ s • N

When we consider subset of R acting on M

Submodule.pointwiseSetDistribMulAction : the action described above is distributive.
Submodule.mem_set_smul : x ∈ s • N iff x can be written as r₀ n₀ + ... + rₖ nₖ where rᵢ ∈ s and nᵢ ∈ N.
Submodule.coe_span_smul: s • N is the same as ⟨s⟩ • N where ⟨s⟩ is the ideal spanned by s.

Notes #

If we assume the addition on subsets of R is the ⊔ and subtraction ⊓ i.e. use SetSemiring, then this action actually gives a module structure on submodules of M over subsets of R.
If we generalize so that r • N makes sense for all r : S, then Submodule.singleton_set_smul and Submodule.singleton_set_smul can be generalized as well.

def Submodule.pointwiseSetSMul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] :

SMul (Set S) (Submodule R M)

Let s ⊆ R be a set and N ≤ M be a submodule, then s • N is the smallest submodule containing all r • n where r ∈ s and n ∈ N.

Equations

Submodule.pointwiseSetSMul = { smul := fun (s : Set S) (N : Submodule R M) => sInf {p : Submodule R M | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} }

theorem Submodule.mem_set_smul_def {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (x : M) :

x ∈ s • N ↔ x ∈ sInf {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}

theorem Submodule.mem_set_smul_of_mem_mem {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] {s : Set S} {N : Submodule R M} {r : S} {m : M} (mem1 : r ∈ s) (mem2 : m ∈ N) :

r • m ∈ s • N

theorem Submodule.set_smul_le {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (s : Set S) (N p : Submodule R M) (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) :

s • N ≤ p

theorem Submodule.set_smul_le_iff {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (s : Set S) (N p : Submodule R M) :

s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

theorem Submodule.set_smul_eq_of_le {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (s : Set S) (N p : Submodule R M) (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) (le : p ≤ s • N) :

s • N = p

instance Submodule.instCovariantClassSetHSMulLe {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] :

CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le

theorem Submodule.set_smul_mono_left {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (N : Submodule R M) {s t : Set S} (le : s ≤ t) :

s • N ≤ t • N

theorem Submodule.set_smul_le_of_le_le {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] {s t : Set S} {p q : Submodule R M} (le_set : s ≤ t) (le_submodule : p ≤ q) :

s • p ≤ t • q

theorem Submodule.set_smul_eq_iSup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : Set S) (N : Submodule R M) :

s • N = ⨆ a ∈ s, a • N

theorem Submodule.set_smul_span {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : Set S) (t : Set M) :

s • span R t = span R (s • t)

theorem Submodule.span_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : Set S) (t : Set M) :

span R (s • t) = s • span R t

theorem Submodule.set_smul_inductionOn {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] {s : Set S} {N : Submodule R M} {motive : (x : M) → x ∈ s • N → Prop} (x : M) (hx : x ∈ s • N) (smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯) (smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯) (add : ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N), motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯) (zero : motive 0 ⋯) :

motive x hx

Induction principle for set acting on submodules. To prove P holds for all s • N, it is enough to prove:

for all r ∈ s and n ∈ N, P (r • n);
for all r and m ∈ s • N, P (r • n);
for all m₁, m₂, P m₁ and P m₂ implies P (m₁ + m₂);
P 0.

To invoke this induction principle, use induction x, hx using Submodule.set_smul_inductionOn where x : M and hx : x ∈ s • N

theorem Submodule.set_smul_eq_map {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (sR : Set R) (N : Submodule R M) [SMulCommClass R R ↥N] :

sR • N = map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

theorem Submodule.mem_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (sR : Set R) (N : Submodule R M) (x : M) [SMulCommClass R R ↥N] :

x ∈ sR • N ↔ ∃ (c : R →₀ ↥N), ↑c.support ⊆ sR ∧ x = ↑(c.sum fun (r : R) (m : ↥N) => r • m)

@[simp]

theorem Submodule.empty_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (N : Submodule R M) :

∅ • N = ⊥

@[simp]

theorem Submodule.set_smul_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (s : Set S) :

s • ⊥ = ⊥

theorem Submodule.singleton_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (N : Submodule R M) [SMulCommClass S R M] (r : S) :

{r} • N = r • N

theorem Submodule.mem_singleton_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (N : Submodule R M) [SMulCommClass R S M] (r : S) (x : M) :

x ∈ {r} • N ↔ ∃ m ∈ N, x = r • m

theorem Submodule.smul_inductionOn_pointwise {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (N : Submodule R M) [SMulCommClass S R M] {a : S} {p : (x : M) → x ∈ a • N → Prop} (smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯) (smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯) (add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) {x : M} (hx : x ∈ a • N) :

p x hx

def Submodule.pointwiseSetMulAction {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] :

MulAction (Set R) (Submodule R M)

A subset of a ring R has a multiplicative action on submodules of a module over R.

Equations

Submodule.pointwiseSetMulAction = MulAction.mk ⋯ ⋯

def Submodule.pointwiseSetDistribMulAction {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [SMulCommClass R R M] :

DistribMulAction (Set R) (Submodule R M)

In a ring, sets acts on submodules.

Equations

Submodule.pointwiseSetDistribMulAction = DistribMulAction.mk ⋯ ⋯

theorem Submodule.sup_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Monoid S] [DistribMulAction S M] (N : Submodule R M) (s t : Set S) :

(s ⊔ t) • N = s • N ⊔ t • N