Module

AffineChartFiniteSubmoduleExtension.lean

Nyll.SchemeTheory.Modules.AffineChartFiniteSubmoduleExtension

4 declarations indexed from sourceView source ↗

Module documentation

Extending a finite quasicoherent submodule across one affine chart

The canonical spectrum of the affine chart supplies finite extraction on the compact overlap. Its actual inclusion is transported back along the affine isomorphism and extended by the kernel of the quotient direct image. The resulting global subsheaf is finite type on the chart and agrees with the original subsheaf on the entire overlap, as a native submodule.

Imports9

Nyll.SchemeTheory.Modules.AffineFiniteSubmoduleOnOpen
Nyll.SchemeTheory.Modules.FiniteTypeSchemeRestriction
Nyll.SchemeTheory.Modules.SubmoduleTopRestriction
Nyll.SchemeTheory.Modules.KernelSubmoduleRestriction
Nyll.SchemeTheory.Modules.QuasicoherentExtension
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Imported by2

def

restrictFunctorAlongLEIso

L35 ↗

AlgebraicGeometry.Scheme.Modules.restrictFunctorAlongLEIso

Source context 4 commands

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

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

Lean source · statement

def restrictFunctorAlongLEIso
    {X : Scheme.{u}} {U V : X.Opens} (h : U ≤ V) :
    restrictFunctor V.ι ⋙ restrictFunctor (X.homOfLE h) ≅ restrictFunctor U.ι

theorem

finiteType_of_schemeIso

L41 ↗

AlgebraicGeometry.Scheme.Modules.finiteType_of_schemeIso

Source context 4 commands

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

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

Lean source · statement

theorem finiteType_of_schemeIso
    {X : Scheme.{u}} {M N : X.Modules} (e : M ≅ N) (hM : M.IsFiniteType) :
    N.IsFiniteType

theorem

mono_submoduleAsModuleInclusion

L50 ↗

AlgebraicGeometry.Scheme.Modules.mono_submoduleAsModuleInclusion

Source context 4 commands

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

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

Lean source · statement

theorem mono_submoduleAsModuleInclusion
    {X : Scheme.{u}} {F : X.Modules} (N : F.Submodule) :
    Mono (submoduleAsModuleInclusion N)

theorem

exists_finiteType_affineChart_extension

L60 ↗

AlgebraicGeometry.Scheme.Modules.exists_finiteType_affineChart_extension

Documentation

Extend over one affine chart while retaining the exact original subsheaf on the overlap with the compact open where it was already finite type.

Source context 4 commands

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

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

Lean source · statement

theorem exists_finiteType_affineChart_extension
    {X : Scheme.{u}} [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent] (N : F.Submodule)
    [N.toSheafOfModules.IsQuasicoherent]
    (T : X.Opens) (hT : IsCompact (T : Set X))
    (V : X.Opens) (hV : IsAffineOpen V)
    (hNft : (N.toSheafOfModules.over T).IsFiniteType) :
    ∃ P : F.Submodule, P.toSheafOfModules.IsQuasicoherent ∧
      (P.toSheafOfModules.over V).IsFiniteType ∧ P.over (T ⊓ V) = N.over (T ⊓ V)

Module documentation

Extending a finite quasicoherent submodule across one affine chart

Declarations

restrictFunctorAlongLEIso

finiteType_of_schemeIso

mono_submoduleAsModuleInclusion

exists_finiteType_affineChart_extension