Module

AffineFiniteSubmoduleOnOpen.lean

Nyll.SchemeTheory.Modules.AffineFiniteSubmoduleOnOpen

1 declaration indexed from sourceView source ↗

Module documentation

Finite-type affine submodules preserving a quasi-compact restriction

An actual quasicoherent submodule which is finite type on a quasi-compact open contains a globally finite-type quasicoherent submodule with the same restriction to that open. Compactness supplies finitely many principal opens. Native finite type on each of them supplies finite generation of the actual canonical localization; finite numerator extraction then gives the submodule, and sheaf membership locality identifies its restriction.

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

Imports4

Imported by2

theorem

exists_finiteType_submodule_eq_over_of_isCompact

L37 ↗

AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_eq_over_of_isCompact

Documentation

On an affine spectrum, a quasicoherent submodule which is finite type on a quasi-compact open contains a finite-type quasicoherent submodule whose actual restriction to that open is unchanged.

Source context 4 commands

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

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

Lean source · statement

theorem exists_finiteType_submodule_eq_over_of_isCompact {R : CommRingCat.{u}}
    (F : SheafOfModules.{u} (Spec R).ringCatSheaf) [F.IsQuasicoherent] (H : F.Submodule)
    [H.toSheafOfModules.IsQuasicoherent] (U : (Spec R).Opens)
    (hU : IsCompact (U : Set (Spec R)))
    (hFT : (H.toSheafOfModules.over U).IsFiniteType) :
    ∃ N : F.Submodule, N ≤ H ∧ N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧ N.over U = H.over U

Module documentation

Finite-type affine submodules preserving a quasi-compact restriction

Declarations

exists_finiteType_submodule_eq_over_of_isCompact