Module

ModuleFiniteLocalizationModel.lean

Nyll.SchemeTheory.RingTheory.ModuleFiniteLocalizationModel

1 declaration indexed from sourceView source ↗

Module documentation

A finite submodule agreeing on finitely many principal opens

When a submodule is finitely generated on finitely many principal opens, choose numerator representatives for all those local generators. Their finite span is a submodule of the original module and has exactly the same localizations on the chosen opens. The opens need not cover the whole spectrum, and the original submodule need not be finitely generated.

This is the affine finite-generator extraction in Stacks, Tag 01PF, Lemma 28.23.2. That lemma supplies finite-type submodule extension for the module approximation used by Tags 01PI, 01PJ and 0817. This file proves the ring-local extraction, not quasicoherent-sheaf extension or gluing.

Imports6

Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.Algebra.Module.LocalizedModule.Submodule
Mathlib.Basic.Finite.Sigma
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.Tactic.Choose

Imported by2

theorem

exists_fg_le_localized_eq_finite

L39 ↗

Submodule.exists_fg_le_localized_eq_finite

Documentation

A finite family of principal localizations which are finitely generated is recovered by one actual finitely generated submodule of the original. No covering condition on the chosen principal opens is required.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w
namespace Submodule

Lean source · statement

theorem exists_fg_le_localized_eq_finite
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    {ι : Type w} [Finite ι] (r : ι → R) (N : Submodule R M)
    (h : ∀ i : ι, (N.localized (Submonoid.powers (r i))).FG) :
    ∃ K : Submodule R M, K.FG ∧ K ≤ N ∧
      ∀ i : ι, K.localized (Submonoid.powers (r i)) =
        N.localized (Submonoid.powers (r i))

Module documentation

A finite submodule agreeing on finitely many principal opens

Declarations

exists_fg_le_localized_eq_finite