Module

QuasicoherentImage.lean

Nyll.SchemeTheory.Modules.QuasicoherentImage

4 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of native image subsheaves

The identity-action equivalence transports the actual kernel and cokernel theorems for scheme modules to native sheaves. The native image is then the actual kernel of the actual cokernel projection.

Imports5

Nyll.SchemeTheory.Modules.ImageSubmodule
Nyll.SchemeTheory.Modules.QuasicoherentKernelGlobal
Nyll.SchemeTheory.Modules.QuasicoherentCokernel
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Imported by4

instance

schemeEquivalence_preservesZeroMorphisms

L29 ↗

SheafOfModules.schemeEquivalence_preservesZeroMorphisms

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules

Lean source · full declaration

instance schemeEquivalence_preservesZeroMorphisms (X : Scheme.{u}) :
    (Scheme.Modules.sheafOfModulesEquivalence X).functor.PreservesZeroMorphisms where
  map_zero _ _ := rfl

theorem

isQuasicoherent_kernel_native

L34 ↗

SheafOfModules.isQuasicoherent_kernel_native

Documentation

Native categorical kernels of quasicoherent sheaves on schemes are quasicoherent.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules

Lean source · statement

theorem isQuasicoherent_kernel_native {X : Scheme.{u}}
    {M N : SheafOfModules.{u} X.ringCatSheaf}
    [M.IsQuasicoherent] [N.IsQuasicoherent] (f : M ⟶ N) :
    (kernel f).IsQuasicoherent

theorem

isQuasicoherent_cokernel_native

L48 ↗

SheafOfModules.isQuasicoherent_cokernel_native

Documentation

Native categorical cokernels of quasicoherent sheaves on schemes are quasicoherent.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules

Lean source · statement

theorem isQuasicoherent_cokernel_native {X : Scheme.{u}}
    {M N : SheafOfModules.{u} X.ringCatSheaf}
    [M.IsQuasicoherent] [N.IsQuasicoherent] (f : M ⟶ N) :
    (cokernel f).IsQuasicoherent

theorem

isQuasicoherent_imageSubmodule

L62 ↗

SheafOfModules.isQuasicoherent_imageSubmodule

Documentation

The actual native image submodule of a map of quasicoherent sheaves is quasicoherent.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules

Lean source · statement

theorem isQuasicoherent_imageSubmodule {X : Scheme.{u}}
    {M N : SheafOfModules.{u} X.ringCatSheaf}
    [M.IsQuasicoherent] [N.IsQuasicoherent] (f : M ⟶ N) :
    (imageSubmodule f).toSheafOfModules.IsQuasicoherent

Module documentation

Quasicoherence of native image subsheaves

Declarations

schemeEquivalence_preservesZeroMorphisms

isQuasicoherent_kernel_native

isQuasicoherent_cokernel_native

isQuasicoherent_imageSubmodule