Module

QuasicoherentExtension.lean

Nyll.SchemeTheory.Modules.QuasicoherentExtension

7 declarations indexed from sourceView source ↗

Module documentation

Extending actual quasicoherent subobjects across a quasi-compact open

For a monomorphism φ : G ⟶ F|U, the extension is the actual kernel of F ⟶ j_*coker φ. The restriction adjunction identifies this kernel over U with G, and the identification respects the given inclusion in F|U.

This is the geometric kernel construction for Stacks, Tag 01PE(2).

Imports6

Nyll.SchemeTheory.Modules.QuasicoherentKernelGlobal
Nyll.SchemeTheory.Modules.QuasicoherentCokernel
Nyll.SchemeTheory.Modules.QuasicoherentPushforward
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.CategoryTheory.Abelian.Basic
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Imported by4

def

submoduleExtensionMap

L33 ↗

AlgebraicGeometry.Scheme.Modules.submoduleExtensionMap

Documentation

The actual map to the direct image of the quotient by a local subobject.

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 submoduleExtensionMap {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    (F : X.Modules) {G : U.Modules} (φ : G ⟶ F.restrict j) :
    F ⟶ (pushforward j).obj (cokernel φ)

theorem

submoduleExtensionMap_restrict_counit

L38 ↗

AlgebraicGeometry.Scheme.Modules.submoduleExtensionMap_restrict_counit

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 submoduleExtensionMap_restrict_counit
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    (F : X.Modules) {G : U.Modules} (φ : G ⟶ F.restrict j) :
    (restrictFunctor j).map (submoduleExtensionMap j F φ) ≫
      (restrictAdjunction j).counit.app (cokernel φ) = cokernel.π φ

def

monoCokernelKernelIso

L59 ↗

AlgebraicGeometry.Scheme.Modules.monoCokernelKernelIso

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 monoCokernelKernelIso
    {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) [Mono φ] :
    kernel (cokernel.π φ) ≅ M

theorem

monoCokernelKernelIso_hom_ι

L66 ↗

AlgebraicGeometry.Scheme.Modules.monoCokernelKernelIso_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 monoCokernelKernelIso_hom_ι
    {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) [Mono φ] :
    (monoCokernelKernelIso φ).hom ≫ φ = kernel.ι (cokernel.π φ)

def

submoduleExtensionRestrictIso

L75 ↗

AlgebraicGeometry.Scheme.Modules.submoduleExtensionRestrictIso

Documentation

Restricting the actual kernel extension recovers the original monomorphism's source.

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 submoduleExtensionRestrictIso
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    (F : X.Modules) {G : U.Modules} (φ : G ⟶ F.restrict j) [Mono φ] :
    (kernel (submoduleExtensionMap j F φ)).restrict j ≅ G

theorem

submoduleExtensionRestrictIso_hom_ι

L97 ↗

AlgebraicGeometry.Scheme.Modules.submoduleExtensionRestrictIso_hom_ι

Documentation

The restriction identification preserves the actual inclusions into F|U.

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

theorem

isQuasicoherent_kernel_submoduleExtensionMap

L108 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_kernel_submoduleExtensionMap

Documentation

The actual kernel extension is quasicoherent when the open immersion is quasi-compact and both original 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_kernel_submoduleExtensionMap
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    (F : X.Modules) [F.IsQuasicoherent] {G : U.Modules} [G.IsQuasicoherent]
    (φ : G ⟶ F.restrict j) :
    (kernel (submoduleExtensionMap j F φ)).IsQuasicoherent

Module documentation

Extending actual quasicoherent subobjects across a quasi-compact open

Declarations

submoduleExtensionMap

submoduleExtensionMap_restrict_counit

monoCokernelKernelIso

monoCokernelKernelIso_hom_ι

submoduleExtensionRestrictIso

submoduleExtensionRestrictIso_hom_ι

isQuasicoherent_kernel_submoduleExtensionMap