NYLL
Module

FiniteLocalSectionExtension.lean

Nyll.SchemeTheory.Modules.FiniteLocalSectionExtension
1 declaration indexed from sourceView source ↗

Module documentation

Actual quasicoherent extensions containing finite local section families

The finite free image on an open subscheme is inserted into the actual quotient-kernel construction. Its restriction is the original image, so the extension is finite type on that open and contains the original specified sections there. These are the actual inputs for the global finite-type extraction theorem.

Imports5
Imported by2

Declarations

theorem

exists_quasicoherent_submodule_finiteType_over_containing_sections

L33 ↗
AlgebraicGeometry.Scheme.Modules.exists_quasicoherent_submodule_finiteType_over_containing_sections
Documentation

Finitely many sections on a quasi-compact open belong to a global quasicoherent submodule which is finite type on that open.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_quasicoherent_submodule_finiteType_over_containing_sections
    {X : Scheme.{u}} (F : X.Modules) [F.IsQuasicoherent] (U : X.Opens)
    [QuasiCompact U.ι] {I : Type u} [Finite I] (s : I → F.val.obj (op U)) :
    ∃ H : F.Submodule, H.toSheafOfModules.IsQuasicoherent ∧
      (H.toSheafOfModules.over U).IsFiniteType ∧
      ∀ i : I, s i ∈ H.toSubmodule.obj (op U)

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