NYLL
Module

FiniteSubmoduleExtension.lean

Nyll.SchemeTheory.Modules.FiniteSubmoduleExtension
2 declarations indexed from sourceView source ↗

Module documentation

Finite quasicoherent submodule extension on qcqs schemes

The compact-open induction adds one affine chart at a time. Its invariant is an actual global quasicoherent submodule, finite type on the prescribed open together with all charts already added, and unchanged on that prescribed open. Each step constructs the affine refinement, glues the two actual restrictions, and applies the native quasicoherent extension.

At the top open, cover-locality gives global finite type. Applying this to the actual quasicoherent extension of any prescribed native submodule proves the original extension statement of Stacks Tag 01PF.

Imports9
Imported by2

Declarations

theorem

exists_finiteType_submodule_eq_over_of_qcqs

L42 ↗
AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_eq_over_of_qcqs
Documentation

A global quasicoherent submodule finite type on a compact open has a global finite-type quasicoherent replacement with exactly the same restriction.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite TopologicalSpace
open SheafOfModules.Submodule
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finiteType_submodule_eq_over_of_qcqs
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent] (H : F.Submodule)
    [H.toSheafOfModules.IsQuasicoherent]
    (U : X.Opens) (hU : IsCompact (U : Set X))
    (hHft : (H.toSheafOfModules.over U).IsFiniteType) :
    ∃ N : F.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧ N.over U = H.over U
theorem

exists_finiteType_submodule_extension_of_qcqs

L89 ↗
AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_extension_of_qcqs
Documentation

Stacks Tag 01PF: a finite-type quasicoherent native submodule on a quasi-compact open of a qcqs scheme extends to a global finite-type quasicoherent native submodule with literal equality on that open.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite TopologicalSpace
open SheafOfModules.Submodule
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finiteType_submodule_extension_of_qcqs
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent]
    (U : X.Opens) (hU : IsCompact (U : Set X)) (G : (F.over U).Submodule)
    (hGqc : G.toSheafOfModules.IsQuasicoherent)
    (hGft : G.toSheafOfModules.IsFiniteType) :
    ∃ N : F.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧ N.over U = G

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.