Module

LocalizedSubmoduleComparison.lean

Nyll.SchemeTheory.RingTheory.LocalizedSubmoduleComparison

1 declaration indexed from sourceView source ↗

Module documentation

Full localized submodules in the actual localization module

If a submodule becomes the whole canonical localized module, it also becomes the whole of any actual localization. The proof transfers actual fraction representatives along the localized identity map. This is the comparison needed to use finite-generator extraction for sheaf sections.

Imports1

Mathlib.Algebra.Module.LocalizedModule.Submodule

Imported by2

theorem

localized₀_eq_top_of_localized_eq_top

L26 ↗

Submodule.localized₀_eq_top_of_localized_eq_top

Documentation

Fullness of the canonical localized submodule gives fullness in the actual localized module, with its supplied localization map.

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 localized₀_eq_top_of_localized_eq_top
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    {N : Type w} [AddCommGroup N] [Module R N]
    (S : Submonoid R) (K : Submodule R M) (f : M →ₗ[R] N) [IsLocalizedModule S f]
    (hK : K.localized S = ⊤) : K.localized₀ S f = ⊤

Module documentation

Full localized submodules in the actual localization module

Declarations

localized₀_eq_top_of_localized_eq_top