Module

QuasicoherentSubmoduleOverExtension.lean

Nyll.SchemeTheory.Modules.QuasicoherentSubmoduleOverExtension

10 declarations indexed from sourceView source ↗

Module documentation

Literal extension of quasicoherent subsheaves on an open subscheme

The input and restriction use the actual sectionwise submodules on the slice site. The kernel of the map to the direct image of the quotient extends the input, and the embedded restriction isomorphism gives equality of the native submodules. This is the submodule assertion of Stacks 01PE(2).

Imports11

Nyll.SchemeTheory.Modules.QuasicoherentExtension
Nyll.SchemeTheory.Modules.KernelSubmoduleScheme
Nyll.SchemeTheory.Modules.SubmoduleGluingQuasicoherent
Nyll.SchemeTheory.Modules.SubmoduleEmbeddedIso
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.Topology.Sheaves.Module
Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
Mathlib.CategoryTheory.Sites.CoverPreserving
Mathlib.CategoryTheory.Sites.Over

Imported by3

theorem

isQuasicoherent_sheafOfModulesEquivOver

L36 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_sheafOfModulesEquivOver

Source context 4 commands

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

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

Lean source · statement

theorem isQuasicoherent_sheafOfModulesEquivOver
    {X : TopCat.{u}} (V : TopologicalSpace.Opens X) (R : X.Sheaf RingCat.{u})
    (M : SheafOfModules.{u} (R.over V)) [M.IsQuasicoherent] :
    ((V.sheafOfModulesEquivOver R).functor.obj M).IsQuasicoherent

def

submoduleOverInclusion

L62 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverInclusion

Source context 4 commands

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

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

Lean source · statement

def submoduleOverInclusion
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    (overEquiv V).functor.obj N.toSheafOfModules ⟶ F.restrict V.ι

instance

submoduleOverInclusion_mono

L67 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverInclusion_mono

Source context 4 commands

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

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

Lean source · statement

instance submoduleOverInclusion_mono
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    Mono (submoduleOverInclusion F V N)

def

extendQuasicoherentSubmoduleOver

L83 ↗

AlgebraicGeometry.Scheme.Modules.extendQuasicoherentSubmoduleOver

Documentation

The actual global subsheaf obtained from the quotient of the prescribed subsheaf on the open subscheme.

Source context 4 commands

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

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

Lean source · statement

def extendQuasicoherentSubmoduleOver
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    F.Submodule

def

submoduleOverKernelIso

L88 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverKernelIso

Source context 4 commands

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

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

Lean source · statement

def submoduleOverKernelIso
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    ((extendQuasicoherentSubmoduleOver F V N).over V).toSheafOfModules ≅
      ((sheafOfModulesEquivalence X).functor.obj
        (kernel (submoduleExtensionMap V.ι F (submoduleOverInclusion F V N)))).over V

theorem

submoduleOverKernelIso_hom_ι

L97 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverKernelIso_hom_ι

Source context 4 commands

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

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

Lean source · statement

theorem submoduleOverKernelIso_hom_ι
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    (submoduleOverKernelIso F V N).hom ≫
      ((sheafOfModulesEquivalence X).functor.map
        (kernel.ι (submoduleExtensionMap V.ι F (submoduleOverInclusion F V N)))).over V =
      ((extendQuasicoherentSubmoduleOver F V N).over V).ι

def

submoduleOverExtensionSchemeIso

L117 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverExtensionSchemeIso

Source context 4 commands

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

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

Lean source · statement

def submoduleOverExtensionSchemeIso
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    (overEquiv V).functor.obj
        ((extendQuasicoherentSubmoduleOver F V N).over V).toSheafOfModules ≅
      (overEquiv V).functor.obj N.toSheafOfModules

theorem

submoduleOverExtensionSchemeIso_hom_ι

L127 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverExtensionSchemeIso_hom_ι

Source context 4 commands

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

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

Lean source · statement

theorem submoduleOverExtensionSchemeIso_hom_ι
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    (submoduleOverExtensionSchemeIso F V N).hom ≫ submoduleOverInclusion F V N =
      (overEquiv V).functor.map ((extendQuasicoherentSubmoduleOver F V N).over V).ι ≫
        ((overFunctorEquiv V).app F).hom

theorem

extendQuasicoherentSubmoduleOver_over

L161 ↗

AlgebraicGeometry.Scheme.Modules.extendQuasicoherentSubmoduleOver_over

Documentation

The constructed extension restricts to the prescribed actual submodule. The equality is in the native slice-site submodule lattice.

Source context 4 commands

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

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

Lean source · statement

theorem extendQuasicoherentSubmoduleOver_over
    {X : Scheme.{u}} (F : X.Modules) (V : X.Opens) (N : (F.over V).Submodule) :
    (extendQuasicoherentSubmoduleOver F V N).over V = N

theorem

isQuasicoherent_extendQuasicoherentSubmoduleOver

L182 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_extendQuasicoherentSubmoduleOver

Documentation

The actual subsheaf extension is quasicoherent when the open immersion is quasi-compact and the ambient and prescribed modules are quasicoherent.

Source context 4 commands

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

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

Lean source · statement

theorem isQuasicoherent_extendQuasicoherentSubmoduleOver
    {X : Scheme.{u}} (F : X.Modules) [F.IsQuasicoherent]
    (V : X.Opens) [QuasiCompact V.ι] (N : (F.over V).Submodule)
    (hN : N.toSheafOfModules.IsQuasicoherent) :
    (extendQuasicoherentSubmoduleOver F V N).toSheafOfModules.IsQuasicoherent

Module documentation

Literal extension of quasicoherent subsheaves on an open subscheme

Declarations