Pointwise scalar actions on submodules

This file also records how scalar products that fix or annihilate a scalar control its pointwise image of the whole module. The image-membership result needs only a distributive monoid action.

Let S be a subring of a commutative ring A, M an A-module and M₀ an S-submodule of M. This file collects the elementary facts about the family rⁿ • M₀, for r : S, in Mathlib's pointwise action on submodules.

The family is written out as rⁿ • M₀ rather than wrapped in a definition of its own: Submodule.mem_smul_pointwise_iff_exists already characterises membership and Submodule.smul_le_self_of_tower already gives the shrinking, so a wrapper would only oblige this file to restate both.

Main results

• Submodule.pow_smul_mem_pow_smul: the ambient-scalar bridge — an element of M₀ scaled by sⁿ : A lands in ⟨s, _⟩ⁿ • M₀, so a consumer speaking A needs no coercion plumbing.
• Submodule.pow_smul_antitone: the family is antitone in the exponent.
• Submodule.pow_add_smul_mem: M₀ absorbs further powers of a scalar drawn from S.

theorem Submodule.pow_smul_mem_pow_smul {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommMonoid M] [Module A M] {S : Subring A} (M₀ : Submodule (↥S) M) {s : A} (hs0 : s ∈ S) {y : M} (hy : y ∈ M₀) (n : ℕ) : s ^ n • y ∈ ⟨s, hs0⟩ ^ n • M₀

The ambient-scalar bridge. Membership in rⁿ • M₀ is stated in Mathlib's terms with the subring scalar r : S, while a caller typically holds the ambient s : A. This is the crossing, so the coercion plumbing is done once here.

Only this direction holds: the converse would need multiplication by sⁿ to be injective.

Not @[simp]: the left-hand side is already reducible by Submodule.mem_smul_pointwise_iff_exists, so simp would rather rewrite it than close it, and the simpNF linter says so. This is a bridge to apply, not a normalisation.

theorem Submodule.pow_smul_antitone {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommMonoid M] [Module A M] {S : Subring A} (M₀ : Submodule (↥S) M) {r : ↥S} : Antitone fun (n : ℕ) => r ^ n • M₀

The family rⁿ • M₀ is antitone in n. Raising the exponent multiplies by a further r, and Submodule.smul_le_self_of_tower says that shrinks the submodule.

theorem Submodule.pow_add_smul_mem {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommMonoid M] [Module A M] {S : Subring A} (M₀ : Submodule (↥S) M) {s : A} (hs0 : s ∈ S) (j k : ℕ) (z : M) (hz : s ^ k • z ∈ M₀) : s ^ (j + k) • z ∈ M₀

A submodule over a subring absorbs further powers of a scalar from that subring: raising the exponent cannot leave M₀, because the extra factor is itself a scalar from S.

theorem Submodule.smul_mem_pow_smul {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommMonoid M] [Module A M] {S : Subring A} (M₀ : Submodule (↥S) M) {s : A} (hs0 : s ∈ S) {b : A} (hb : b ∈ S) {c : A} {m : M} {n k : ℕ} (hcb : s ^ (n + k) • b = c) (hk : s ^ k • m ∈ M₀) : c • m ∈ ⟨s, hs0⟩ ^ n • M₀

Scaling into sⁿ • M₀. If c factors as s ^ (n + k) • b with b : S, and s ^ k • m already lies in M₀, then c • m lies in sⁿ • M₀.

This is the step that both a submodules-basis smul condition and a module-filter-basis smul_right' axiom reduce to, which is why it is stated once here rather than inline at each.

theorem TauCeti.smul_mem_smul_top_of_mul_eq_self {S : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring S] [Monoid R] [AddCommMonoid M] [Module S M] [DistribMulAction R M] [SMulCommClass R S M] {f r : R} (hr : f * r = r) (x : M) : r • x ∈ f • ⊤

An element r fixed on the left by f carries the whole module into f • M: if f * r = r then every multiple of r lies in f • M. No idempotency is needed.

theorem TauCeti.smul_eq_zero_of_mul_eq_zero_of_mem_smul_top {S : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring S] [Semiring R] [AddCommMonoid M] [Module S M] [Module R M] [SMulCommClass R S M] {r e : R} (hr : r * e = 0) {x : M} (hx : x ∈ e • ⊤) : r • x = 0

An element that kills e on the right annihilates e • M: if r * e = 0 then r sends every element of e • M to zero. No idempotency is needed.