Module

SubmoduleRestrictionComparison.lean

Nyll.SchemeTheory.Modules.SubmoduleRestrictionComparison

5 declarations indexed from sourceView source ↗

Module documentation

Comparing native submodule restrictions with open-subscheme modules

The comparison is built from the actual sectionwise restriction of the submodule and the canonical slice-to-open equivalence. Its inclusion identity lets geometric restriction isomorphisms give literal equality of the native restricted submodules.

Imports4

Nyll.SchemeTheory.Modules.QuasicoherentLocal
Nyll.SchemeTheory.Modules.SubmoduleGluingQuasicoherent
Nyll.SchemeTheory.Modules.SubmoduleEmbeddedIso
Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by4

def

submoduleAsModule

L30 ↗

AlgebraicGeometry.Scheme.Modules.submoduleAsModule

Documentation

The actual module of a native submodule, regarded in the scheme-module category.

Source context 4 commands

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

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

Lean source · statement

def submoduleAsModule {X : Scheme.{u}} {F : X.Modules} (N : F.Submodule) : X.Modules

def

submoduleAsModuleInclusion

L35 ↗

AlgebraicGeometry.Scheme.Modules.submoduleAsModuleInclusion

Documentation

The native inclusion in the scheme-module category. The identity-action equivalence preserves the actual ambient module and the actual section maps.

Source context 4 commands

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

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

Lean source · statement

def submoduleAsModuleInclusion {X : Scheme.{u}} {F : X.Modules} (N : F.Submodule) :
    submoduleAsModule N ⟶ F

def

submoduleOverRestrictIso

L41 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverRestrictIso

Documentation

The actual native restriction, viewed on the open subscheme, is the geometric restriction of the submodule's module.

Source context 4 commands

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

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

Lean source · statement

def submoduleOverRestrictIso
    {X : Scheme.{u}} {F : X.Modules} (N : F.Submodule) (U : X.Opens) :
    (overEquiv U).functor.obj (N.over U).toSheafOfModules ≅
      (submoduleAsModule N).restrict U.ι

theorem

submoduleOverRestrictIso_hom_ι

L49 ↗

AlgebraicGeometry.Scheme.Modules.submoduleOverRestrictIso_hom_ι

Documentation

The native and geometric restriction comparisons preserve the actual inclusions.

Source context 4 commands

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

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

Lean source · statement

theorem submoduleOverRestrictIso_hom_ι
    {X : Scheme.{u}} {F : X.Modules} (N : F.Submodule) (U : X.Opens) :
    (submoduleOverRestrictIso N U).hom ≫
        (restrictFunctor U.ι).map (submoduleAsModuleInclusion N) =
      (overEquiv U).functor.map (N.over U).ι ≫ ((overFunctorEquiv U).app F).hom

theorem

submodule_over_eq_of_restrictIso

L71 ↗

AlgebraicGeometry.Scheme.Modules.submodule_over_eq_of_restrictIso

Documentation

An actual isomorphism between geometric restrictions, preserving the inclusions, gives equality of the actual native submodules on the slice.

Source context 4 commands

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

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

Lean source · statement

theorem submodule_over_eq_of_restrictIso
    {X : Scheme.{u}} {F : X.Modules} (N P : F.Submodule) (U : X.Opens)
    (e : (submoduleAsModule N).restrict U.ι ≅ (submoduleAsModule P).restrict U.ι)
    (he : e.hom ≫ (restrictFunctor U.ι).map (submoduleAsModuleInclusion P) =
      (restrictFunctor U.ι).map (submoduleAsModuleInclusion N)) :
    N.over U = P.over U

Module documentation

Comparing native submodule restrictions with open-subscheme modules

Declarations

submoduleAsModule

submoduleAsModuleInclusion

submoduleOverRestrictIso

submoduleOverRestrictIso_hom_ι

submodule_over_eq_of_restrictIso