Module

QuasicoherentKernelGlobal.lean

Nyll.SchemeTheory.Modules.QuasicoherentKernelGlobal

3 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of kernels on schemes

Restriction preserves the actual categorical kernel. Affine kernel quasicoherence supplies the hypotheses of the shared affine-presentation criterion, which constructs the global quasicoherent data.

Imports11

Nyll.SchemeTheory.Modules.QuasicoherentKernel
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Mathlib.Topology.Sheaves.Module
Mathlib.CategoryTheory.Adjunction.Limits

Imported by3

theorem

preservesFiniteLimits_restrictFunctor

L37 ↗

AlgebraicGeometry.Scheme.Modules.preservesFiniteLimits_restrictFunctor

Documentation

Restriction along an open immersion preserves finite limits, by the actual native sheaf pushforward adjunction defining the restriction.

Source context 4 commands

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

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

Lean source · statement

theorem preservesFiniteLimits_restrictFunctor
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
    PreservesFiniteLimits (restrictFunctor f)

instance

restrictFunctor_preservesZeroMorphisms_kernel

L57 ↗

AlgebraicGeometry.Scheme.Modules.restrictFunctor_preservesZeroMorphisms_kernel

Source context 4 commands

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

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

Lean source · full declaration

instance restrictFunctor_preservesZeroMorphisms_kernel
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
    (restrictFunctor f).PreservesZeroMorphisms where
  map_zero _ _ := rfl

theorem

isQuasicoherent_kernel

L65 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_kernel

Documentation

The actual categorical kernel of any morphism of quasicoherent modules on a scheme is quasicoherent. No separation or compactness assumption is needed.

Source context 4 commands

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

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

Lean source · statement

theorem isQuasicoherent_kernel
    {X : Scheme.{u}} {M N : X.Modules}
    [M.IsQuasicoherent] [N.IsQuasicoherent] (φ : M ⟶ N) :
    (kernel φ).IsQuasicoherent

Module documentation

Quasicoherence of kernels on schemes

Declarations

preservesFiniteLimits_restrictFunctor

restrictFunctor_preservesZeroMorphisms_kernel

isQuasicoherent_kernel