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 Mathlib/GroupTheory/Submonoid/Pointwise.lean.

Other than section set_acting_on_submodules, most of the lemmas in this file are direct copies of lemmas from Mathlib/GroupTheory/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.

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 : Submodule R M) (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 : Submodule R M) (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) : Submodule.span R (-s) = -Submodule.span R s

@[simp]

theorem Submodule.neg_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (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 : Submodule R M) (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 (x x_1 : Submodule R M) => x ⊔ x_1 }

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 : Submodule R M) (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.instCanonicallyOrderedAddCommMonoidSubmodule {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : CanonicallyOrderedAddCommMonoid (Submodule R M)

Equations

• Submodule.instCanonicallyOrderedAddCommMonoidSubmodule = let __src := Submodule.pointwiseAddCommMonoid; let __src_1 := Submodule.completeLattice; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

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) : Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S

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

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

Equations

• ⋯ = ⋯

@[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 = let __src := Submodule.pointwiseDistribMulAction; 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 principal, 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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (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

theorem Submodule.set_smul_mono_right {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) {p : Submodule R M} {q : Submodule R M} (le : p ≤ q) : s • p ≤ s • q

theorem Submodule.set_smul_mono_left {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) {s : Set 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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] {s : Set S} {t : Set S} {p : Submodule R M} {q : Submodule R M} (le_set : s ≤ t) (le_submodule : p ≤ q) : s • p ≤ t • q

theorem Submodule.set_smul_inductionOn {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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 principal 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 principal, 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 = Submodule.map (Submodule.subtype N ∘ₗ (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 = ↑(Finsupp.sum c fun (r : R) (m : ↥N) => r • m)

@[simp]

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

@[simp]

theorem Submodule.set_smul_bot {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] (N : Submodule R M) [SMulCommClass R R M] (r : R) : {r} • N = r • N

theorem Submodule.mem_singleton_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) [SMulCommClass R S M] (r : S) (x : M) : x ∈ {r} • N ↔ ∃ m ∈ N, x = r • m

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 ⋯ ⋯

theorem Submodule.set_smul_eq_iSup {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 M] : sR • N = ⨆ r ∈ sR, r • N

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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) (s : Set S) (t : Set S) : (s ⊔ t) • N = s • N ⊔ t • N

theorem Submodule.coe_span_smul {R' : Type u_5} {M' : Type u_6} [CommSemiring R'] [AddCommMonoid M'] [Module R' M'] (s : Set R') (N : Submodule R' M') : ↑(Ideal.span s) • N = s • N