NYLL
Module

FiniteAffineSectionSubmodule.lean

Nyll.SchemeTheory.Modules.FiniteAffineSectionSubmodule
4 declarations indexed from sourceView source ↗

Module documentation

Finite quasicoherent submodules containing finite affine-local generators

For each selected affine open, finitely many actual section generators are included in the actual quotient-kernel extension of their finite free image. The proved finite-type extension theorem replaces this by a global finite-type quasicoherent submodule with the same restriction. The actual finite join retains all of the prescribed generators. The selected opens need not cover the scheme.

Imports5
Imported by2

Declarations

theorem

exists_finiteType_submodule_containing_sections_of_isCompact

L34 ↗
AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_containing_sections_of_isCompact
Documentation

A finite family on a compact open of a qcqs scheme belongs to a global finite-type quasicoherent native submodule.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finiteType_submodule_containing_sections_of_isCompact
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : SheafOfModules.{u} X.ringCatSheaf) [F.IsQuasicoherent]
    (U : X.Opens) (hU : IsCompact (U : Set X))
    {I : Type u} [Finite I] (s : I → F.val.obj (op U)) :
    ∃ N : F.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧ ∀ i : I, s i ∈ N.toSubmodule.obj (op U)
theorem

exists_finiteType_submodule_containing_fg_sections

L59 ↗
AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_containing_fg_sections
Documentation

A finitely generated actual section submodule on a compact open is contained in a global finite-type quasicoherent native submodule.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finiteType_submodule_containing_fg_sections
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : SheafOfModules.{u} X.ringCatSheaf) [F.IsQuasicoherent]
    (U : X.Opens) (hU : IsCompact (U : Set X))
    (K : Submodule (X.ringCatSheaf.obj.obj (op U)) (F.val.obj (op U))) (hK : K.FG) :
    ∃ N : F.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧ K ≤ N.toSubmodule.obj (op U)
theorem

exists_finiteType_submodule_containing_affine_sections

L76 ↗
AlgebraicGeometry.Scheme.Modules.exists_finiteType_submodule_containing_affine_sections
Documentation

Finitely many finitely generated affine-local section submodules all belong to one actual finite-type quasicoherent native submodule.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finiteType_submodule_containing_affine_sections
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : SheafOfModules.{u} X.ringCatSheaf) [F.IsQuasicoherent]
    {I : Type v} [Finite I] (V : I → X.AffineZariskiSite)
    (K : ∀ i : I, Submodule (X.ringCatSheaf.obj.obj (op (V i).1))
      (F.val.obj (op (V i).1))) (hK : ∀ i : I, (K i).FG) :
    ∃ N : F.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧
      ∀ i : I, K i ≤ N.toSubmodule.obj (op (V i).1)
theorem

exists_finite_quasicoherent_submodule_containing_affine_sections

L101 ↗
AlgebraicGeometry.Scheme.Modules.exists_finite_quasicoherent_submodule_containing_affine_sections
Documentation

On a qcqs scheme, finitely many specified finitely generated affine section submodules are contained in one actual quasicoherent submodule whose section module on every affine open is finitely generated.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finite_quasicoherent_submodule_containing_affine_sections
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : SheafOfModules.{u} X.ringCatSheaf) [F.IsQuasicoherent]
    {I : Type v} [Finite I] (V : I → X.AffineZariskiSite)
    (K : ∀ i : I, Submodule (X.ringCatSheaf.obj.obj (op (V i).1))
      (F.val.obj (op (V i).1))) (hK : ∀ i : I, (K i).FG) :
    ∃ N : F.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      (∀ W : X.AffineZariskiSite, (N.toSubmodule.obj (op W.1)).FG) ∧
      ∀ i : I, K i ≤ N.toSubmodule.obj (op (V i).1)

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