The abelian category of coherent sheaves

On a locally noetherian scheme, coherent module sheaves contain zero and are closed under finite products, kernels, and cokernels. Mathlib's full-subcategory infrastructure therefore makes Coh X abelian. The inclusion into all module sheaves creates kernels and cokernels, hence preserves finite limits and finite colimits and is exact.

Main results

• Coh.abelian;
• Coh.exactInclusion;
• Coh.shortExact_map_ι.

instance AlgebraicGeometry.Scheme.coherent_containsZero (X : Scheme) : X.coherent.ContainsZero

The coherent property contains a zero module sheaf.

instance AlgebraicGeometry.Scheme.coherent_isClosedUnderBinaryProducts (X : Scheme) : X.coherent.IsClosedUnderBinaryProducts

Coherent module sheaves are closed under binary products.

instance AlgebraicGeometry.Scheme.coherent_isClosedUnderFiniteProducts (X : Scheme) : X.coherent.IsClosedUnderFiniteProducts

Coherent module sheaves are closed under finite products.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Coh.preadditive (X : Scheme) : CategoryTheory.Preadditive (Coh X)

The preadditive structure inherited by the full subcategory of coherent sheaves.

Equations

• AlgebraicGeometry.Coh.preadditive X = { homGroup := AlgebraicGeometry.Coh.preadditive._aux_1 X, add_comp := ⋯, comp_add := ⋯ }

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Coh.abelian (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Abelian (Coh X)

Coherent sheaves on a locally noetherian scheme form an abelian category.

Built by spreading preadditive over the full subcategory's own Abelian instance, rather than by change … ; infer_instance. The two are defeq, but only at default transparency: written the second way, abelian.toPreadditive is the preadditive field of the subcategory's instance, and reaching Coh.preadditive from it needs Coh — a def — unfolded. Instance search does not do that, so every Mathlib instance asking for [Abelian C] alongside a second Preadditive-parameterised class silently fails to fire on Coh X; Variety.derivedLinear is the case that found it.

The spread pins toPreadditive to preadditive X syntactically. Abelian's other parents, IsNormalMonoCategory and IsNormalEpiCategory, are Props, so no second diamond can hide behind this one.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Coh.ι_preservesZeroMorphisms (X : Scheme) : (ι X).PreservesZeroMorphisms

The inclusion of coherent sheaves preserves zero morphisms.

instance AlgebraicGeometry.Coh.ι_additive (X : Scheme) : (ι X).Additive

The inclusion of coherent sheaves is additive.

instance AlgebraicGeometry.Coh.ι_preservesFiniteLimits (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Limits.PreservesFiniteLimits (ι X)

The inclusion of coherent sheaves preserves finite limits.

instance AlgebraicGeometry.Coh.ι_preservesFiniteColimits (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Limits.PreservesFiniteColimits (ι X)

The inclusion of coherent sheaves preserves finite colimits.

noncomputable def AlgebraicGeometry.Coh.exactInclusion (X : Scheme) [IsLocallyNoetherian X] : Coh X ⥤ₑ X.Modules

The inclusion of coherent sheaves into all module sheaves, packaged as an exact functor.

Equations

• AlgebraicGeometry.Coh.exactInclusion X = CategoryTheory.ExactFunctor.of (AlgebraicGeometry.Coh.ι X)

theorem AlgebraicGeometry.Coh.shortExact_map_ι (X : Scheme) [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) : (S.map (ι X)).ShortExact

The inclusion of coherent sheaves sends short exact sequences to short exact sequences.