NYLL
Module

FiniteOpenSectionSubmodule.lean

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

Module documentation

Finite section families on an actual open subscheme

The original sections on an open are transported to the top of that open subscheme by the native restriction comparison. The finite free image construction produces an actual quasicoherent finite-type local submodule, and each specified original section has an actual lift through its inclusion. This is the local input for extending finite affine generators globally.

Imports3
Imported by2

Declarations

def

openTopSectionsIso

L31 ↗
AlgebraicGeometry.Scheme.Modules.openTopSectionsIso
Documentation

Actual sections on the top of an open subscheme are the original sections on that open.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
def openTopSectionsIso {X : Scheme.{u}} (F : X.Modules) (U : X.Opens) :
    Γ(F.restrict U.ι, ⊤) ≅ Γ(F, U)
theorem

exists_finiteType_restriction_submodule_lifting_sections

L39 ↗
AlgebraicGeometry.Scheme.Modules.exists_finiteType_restriction_submodule_lifting_sections
Documentation

Finitely many actual sections on an open lift through a finite-type quasicoherent submodule on the open subscheme.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem exists_finiteType_restriction_submodule_lifting_sections
    {X : Scheme.{u}} (F : X.Modules) [F.IsQuasicoherent] (U : X.Opens)
    {I : Type u} [Finite I] (s : I → F.val.obj (op U)) :
    ∃ N : ((sheafOfModulesEquivalence U.toScheme).functor.obj
        (F.restrict U.ι)).Submodule,
      N.toSheafOfModules.IsQuasicoherent ∧ N.toSheafOfModules.IsFiniteType ∧
        ∀ i : I, ∃ t : N.toSheafOfModules.val.obj (op ⊤),
          (openTopSectionsIso F U).hom ((N.ι.val.app (op ⊤)).hom t) = s i

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