Results for pointwise instances on Submodules using Finsupp

This file provides the following results in the Pointwise locale:

When we consider subsets 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.

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)

@[implicit_reducible]

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.

Equations

• Submodule.pointwiseSetMulAction = { toSMul := Submodule.pointwiseSetSMul, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

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.

Equations

• Submodule.pointwiseSetDistribMulAction = { toMulAction := Submodule.pointwiseSetMulAction, smul_zero := ⋯, smul_add := ⋯ }