Module

FiniteSectionSubmodule.lean

Nyll.SchemeTheory.Modules.FiniteSectionSubmodule

7 declarations indexed from sourceView source ↗

Module documentation

Actual finite-type subsheaves containing finitely many global sections

A family of actual global sections defines a morphism from the free sheaf through freeHomEquiv. Its native image contains the given sections. For a finite family the source is finite type and quasicoherent, so the image in a quasicoherent ambient module has both properties. This supplies the local input to finite-type submodule extension without an additional affine comparison assumption.

Imports2

Nyll.SchemeTheory.Modules.QuasicoherentImage
Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree

Imported by2

def

topSection

L32 ↗

SheafOfModules.topSection

Documentation

A section on the top open gives the actual compatible family on all opens.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

def topSection (s : M.val.obj (op ⊤)) : M.sections

theorem

topSection_top

L39 ↗

SheafOfModules.topSection_top

Documentation

The compatible family retains the original top section.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

theorem topSection_top (s : M.val.obj (op ⊤)) : (M.topSection s).val (op ⊤) = s

def

sectionFamilySubmodule

L45 ↗

SheafOfModules.sectionFamilySubmodule

Documentation

The native image of the morphism specified by an actual section family.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

def sectionFamilySubmodule {I : Type u} (s : I → M.sections) : M.Submodule

theorem

mem_sectionFamilySubmodule

L49 ↗

SheafOfModules.mem_sectionFamilySubmodule

Documentation

Each specified section belongs to the constructed image on every open.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

theorem mem_sectionFamilySubmodule {I : Type u} (s : I → M.sections) (i : I)
    (U : X.Opens) : (s i).val (op U) ∈ (M.sectionFamilySubmodule s).toSubmodule.obj (op U)

theorem

isFiniteType_sectionFamilySubmodule

L62 ↗

SheafOfModules.isFiniteType_sectionFamilySubmodule

Documentation

A finite family generates a finite-type actual image subsheaf.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

theorem isFiniteType_sectionFamilySubmodule {I : Type u} [Finite I]
    (s : I → M.sections) : (M.sectionFamilySubmodule s).toSheafOfModules.IsFiniteType

theorem

isQuasicoherent_sectionFamilySubmodule

L78 ↗

SheafOfModules.isQuasicoherent_sectionFamilySubmodule

Documentation

The generated image is quasicoherent in a quasicoherent ambient module.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

theorem isQuasicoherent_sectionFamilySubmodule [M.IsQuasicoherent]
    {I : Type u} (s : I → M.sections) :
    (M.sectionFamilySubmodule s).toSheafOfModules.IsQuasicoherent

theorem

exists_finiteType_submodule_containing_top

L86 ↗

SheafOfModules.exists_finiteType_submodule_containing_top

Documentation

Any finitely generated submodule of actual global sections is contained in a finite-type quasicoherent native subsheaf.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace SheafOfModules
variable {X : Scheme.{u}} (M : SheafOfModules.{u} X.ringCatSheaf)

Lean source · statement

theorem exists_finiteType_submodule_containing_top [M.IsQuasicoherent]
    (K : _root_.Submodule (X.ringCatSheaf.obj.obj (op ⊤)) (M.val.obj (op ⊤))) (hK : K.FG) :
    ∃ N : M.Submodule, N.toSheafOfModules.IsQuasicoherent ∧
      N.toSheafOfModules.IsFiniteType ∧ K ≤ N.toSubmodule.obj (op ⊤)

Module documentation

Actual finite-type subsheaves containing finitely many global sections

Declarations

topSection

topSection_top

sectionFamilySubmodule

mem_sectionFamilySubmodule

isFiniteType_sectionFamilySubmodule

isQuasicoherent_sectionFamilySubmodule

exists_finiteType_submodule_containing_top