Module

KernelSubmoduleRestriction.lean

Nyll.SchemeTheory.Modules.KernelSubmoduleRestriction

4 declarations indexed from sourceView source ↗

Module documentation

Restricting the actual kernel subsheaf extension

The native kernel submodule and the geometric kernel have the same actual inclusion. Transporting that comparison along open restriction gives the embedded geometric restriction isomorphism needed for affine extraction and for preservation of prescribed local generators.

Imports3

Imported by3

def

kernelSubmoduleAsModuleIso

L30 ↗

AlgebraicGeometry.Scheme.Modules.kernelSubmoduleAsModuleIso

Documentation

The actual kernel submodule, regarded as a scheme module, is the categorical kernel.

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 kernelSubmoduleAsModuleIso
    {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) :
    submoduleAsModule (kernelSubmodule φ) ≅ kernel φ

theorem

kernelSubmoduleAsModuleIso_hom_ι

L36 ↗

AlgebraicGeometry.Scheme.Modules.kernelSubmoduleAsModuleIso_hom_ι

Documentation

The actual native and categorical kernel inclusions agree under the comparison.

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 kernelSubmoduleAsModuleIso_hom_ι
    {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) :
    (kernelSubmoduleAsModuleIso φ).hom ≫ kernel.ι φ =
      submoduleAsModuleInclusion (kernelSubmodule φ)

def

kernelSubmoduleExtensionRestrictIso

L48 ↗

AlgebraicGeometry.Scheme.Modules.kernelSubmoduleExtensionRestrictIso

Documentation

Restriction of the actual native kernel extension recovers the source of the original monomorphism 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 kernelSubmoduleExtensionRestrictIso
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    (F : X.Modules) {G : U.Modules} (φ : G ⟶ F.restrict j) [Mono φ] :
    (submoduleAsModule (kernelSubmodule (submoduleExtensionMap j F φ))).restrict j ≅ G

theorem

kernelSubmoduleExtensionRestrictIso_hom_ι

L56 ↗

AlgebraicGeometry.Scheme.Modules.kernelSubmoduleExtensionRestrictIso_hom_ι

Documentation

The recovered source has its original inclusion in the restricted ambient module.

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 kernelSubmoduleExtensionRestrictIso_hom_ι
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    (F : X.Modules) {G : U.Modules} (φ : G ⟶ F.restrict j) [Mono φ] :
    (kernelSubmoduleExtensionRestrictIso j F φ).hom ≫ φ =
      (restrictFunctor j).map
        (submoduleAsModuleInclusion (kernelSubmodule (submoduleExtensionMap j F φ)))

Module documentation

Restricting the actual kernel subsheaf extension

Declarations

kernelSubmoduleAsModuleIso

kernelSubmoduleAsModuleIso_hom_ι

kernelSubmoduleExtensionRestrictIso

kernelSubmoduleExtensionRestrictIso_hom_ι