Pointwise instances on Submodules

This file provides:

• Submodule.pointwiseNeg

and the actions

• Submodule.pointwiseDistribMulAction
• Submodule.pointwiseMulActionWithZero

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 files Mathlib/Algebra/Group/Submonoid/Pointwise.lean and Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean.

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

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.

@[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.

@[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.

theorem Submodule.span_neg_eq_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)

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

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

@[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] : 0 = ⊥

instance Submodule.instIsOrderedAddMonoid {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : IsOrderedAddMonoid (Submodule R M)

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.

@[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.mem_smul_pointwise_iff_exists {α : 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 ∈ a • S ↔ ∃ b ∈ S, a • b = m

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_iSup' {α : 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 : α) {ι : Sort u_4} (f : ι → Submodule R M) : a • ⨆ (i : ι), f i = ⨆ (i : ι), a • f i

See also Submodule.smul_iSup.

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} [Monoid α] [SMul α R] [DistribMulAction α 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.

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.

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) (DistribSMul.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

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

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

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