Clearing a denominator against a radical membership

Submodule.exists_pow_smul_mem_of_isLocalized_radical is the commutative-algebra step behind "a section over a basic open extends after multiplying by a power of the defining element". If an element lands in a submodule after localizing at every member of a family s, then some power of any element of (span s).radical carries it into the submodule on the nose.

The proof is a single observation: the set of ring elements carrying m into N is the ideal N.comap (toSpanSingleton R M m), localizing at r says exactly that some power of r lies in that ideal, and radical membership then transports the conclusion from span s to d.

Provenance

This statement was proved as a private lemma inside the Čech affine-vanishing file, where it was needed once. It is stated here instead because it is pure commutative algebra with no Čech content, and because the projective-space section-extension argument (#585) was expected to need it without wanting the cohomology stack it was buried in. Nothing about the proof changed in the move.

That expectation did not hold: #585 closed without using this lemma at all — the overlap step it was meant for is settled by separatedness on the degree-two chart of gᵢ gⱼ instead. The Čech affine-vanishing argument remains its live consumer, and the statement is still worth having on its own terms.

It is not in Mathlib at the current pin under this or any neighbouring name, and it is upstream-candidate material.

Tags

localization, radical, submodule, denominator clearing

theorem Submodule.exists_pow_smul_mem_of_isLocalized_radical {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) {d : R} (hd : d ∈ (Ideal.span s).radical) (Mₚ : ↑s → Type u_3) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {m : M} {N : Submodule R M} (h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N) : ∃ (n : ℕ), d ^ n • m ∈ N

If an element lands in a submodule after localization at every element of s, then a power of every element of (span s).radical carries it into the submodule.

The family s is the one a basic-open cover produces, and d is the element whose basic open is being covered; radical membership is what "the cover is a cover" supplies.