Module

KernelSubmoduleScheme.lean

Nyll.SchemeTheory.Modules.KernelSubmoduleScheme

4 declarations indexed from sourceView source ↗

Module documentation

Actual kernel submodules on schemes

The native sectionwise kernel subsheaf is transported through the identity-action equivalence with the category of scheme modules. The comparison with the actual categorical kernel respects the inclusion into the original module.

Imports4

Nyll.SchemeTheory.Modules.KernelSubmodule
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Imported by3

instance

sheafOfModulesEquivalence_functor_preservesZeroMorphisms

AlgebraicGeometry.Scheme.Modules.sheafOfModulesEquivalence_functor_preservesZeroMorphisms

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 · full declaration

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

def

kernelSubmodule

AlgebraicGeometry.Scheme.Modules.kernelSubmodule

Documentation

The native submodule of sections killed by a morphism of scheme modules.

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

def

kernelSubmoduleIso

AlgebraicGeometry.Scheme.Modules.kernelSubmoduleIso

Documentation

The actual module of the sectionwise kernel submodule is the image of the categorical kernel under the identity-action native sheaf equivalence.

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 kernelSubmoduleIso {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) :
    (kernelSubmodule φ).toSheafOfModules ≅
      (sheafOfModulesEquivalence X).functor.obj (kernel φ)

theorem

kernelSubmoduleIso_hom_ι

AlgebraicGeometry.Scheme.Modules.kernelSubmoduleIso_hom_ι

Documentation

The categorical-kernel comparison identifies its inclusion with the actual inclusion of the pointwise kernel submodule.

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 kernelSubmoduleIso_hom_ι {X : Scheme.{u}} {M N : X.Modules}
    (φ : M ⟶ N) :
    (kernelSubmoduleIso φ).hom ≫
      (sheafOfModulesEquivalence X).functor.map (kernel.ι φ) =
      (kernelSubmodule φ).ι