Module

FiniteTypeSubopen.lean

Nyll.SchemeTheory.Modules.FiniteTypeSubopen

3 declarations indexed from sourceView source ↗

Module documentation

Finite type on subopens

Restriction to a smaller open is obtained within the larger slice site, then transported by the actual equivalence of iterated slice sites.

Imports3

Nyll.SchemeTheory.Modules.FiniteTypeIteratedSlice
Nyll.SchemeTheory.Modules.FiniteTypeRestriction
Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by3

theorem

iterated_over

L27 ↗

SheafOfModules.IsFiniteType.iterated_over

Documentation

The iterated restriction has finite type when the direct restriction does.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace SheafOfModules

Lean source · statement

theorem IsFiniteType.iterated_over {X : Scheme.{u}}
    (M : SheafOfModules.{u} X.ringCatSheaf) {U V : X.Opens}
    (hUV : U ≤ V) (hM : (M.over U).IsFiniteType) :
    ((M.over V).over (Over.mk (homOfLE hUV))).IsFiniteType

theorem

over_of_le

L34 ↗

SheafOfModules.IsFiniteType.over_of_le

Documentation

Finite type on an open is inherited by every smaller open.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace SheafOfModules

Lean source · statement

theorem IsFiniteType.over_of_le {X : Scheme.{u}}
    (M : SheafOfModules.{u} X.ringCatSheaf) {U V : X.Opens}
    (hUV : U ≤ V) (hM : (M.over V).IsFiniteType) : (M.over U).IsFiniteType

theorem

isQuasicoherent_iterated_over

L41 ↗

SheafOfModules.isQuasicoherent_iterated_over

Documentation

The iterated restriction is quasicoherent when the direct restriction is.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace SheafOfModules

Lean source · statement

theorem isQuasicoherent_iterated_over {X : Scheme.{u}}
    (M : SheafOfModules.{u} X.ringCatSheaf) {U V : X.Opens}
    (hUV : U ≤ V) (hM : (M.over U).IsQuasicoherent) :
    ((M.over V).over (Over.mk (homOfLE hUV))).IsQuasicoherent

Module documentation

Finite type on subopens

Declarations

iterated_over

over_of_le

isQuasicoherent_iterated_over