Module

AffineFiniteSubmoduleExtension.lean

Nyll.SchemeTheory.Modules.AffineFiniteSubmoduleExtension

1 declaration indexed from sourceView source ↗

Module documentation

Finite-type extraction on finitely many principal opens

Starting with an actual quasicoherent native submodule, extract finitely many global numerator sections using the existing finite localization theorem. Their actual affine tilde morphism has full range on the specified principal opens. Its image inside the original ambient module is therefore a finite-type quasicoherent submodule with exactly the prescribed local restrictions. The principal opens need not cover the whole spectrum.

This is the affine extraction step of Stacks Tag 01PF, after Tag 01PE has supplied the actual quasicoherent extension.

Imports5

Imported by2

theorem

exists_finiteType_submodule_eq_on_basicOpens

L38 ↗

AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_eq_on_basicOpens

Documentation

An actual quasicoherent submodule with finitely generated localizations on finitely many principal opens admits a finite-type quasicoherent submodule agreeing on all those opens.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem exists_finiteType_submodule_eq_on_basicOpens {R : CommRingCat.{u}}
    (F : SheafOfModules.{u} (Spec R).ringCatSheaf) [F.IsQuasicoherent] (H : F.Submodule)
    [H.toSheafOfModules.IsQuasicoherent]
    {ι : Type v} [Finite ι] (r : ι → R)
    (hFinite : ∀ i : ι,
      ((⊤ : Submodule R ((moduleSpecΓFunctor (R := R)).obj
        ((sheafOfModulesEquivalence (Spec R)).inverse.obj H.toSheafOfModules))).localized
          (Submonoid.powers (r i))).FG) :
    ∃ N : F.Submodule, N ≤ H ∧ N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧
      ∀ i : ι, N.over (PrimeSpectrum.basicOpen (r i)) =
        H.over (PrimeSpectrum.basicOpen (r i))

Module documentation

Finite-type extraction on finitely many principal opens

Declarations

exists_finiteType_submodule_eq_on_basicOpens