Quasi-coherence is closed under extensions

With the kernel and cokernel closure of CoherentSheaf/Quasicoherent/Kernels.lean, this completes the weak Serre property for quasi-coherent sheaves on an arbitrary scheme — what Dqc(X) needs before it can carry a triangulated structure.

Through the five-term homology long exact sequence, closure under cones needs closure under kernels, cokernels and extensions — not under subobjects and quotients, which quasi-coherence does not have. See CategoryTheory/Abelian/SerreClass/Weak.lean; an earlier version of this paragraph claimed the stronger closure, and it is not what the argument uses.

Why cohomology, when the coherent case needed none

Abelian/Extensions.lean proves the finite-presentation analogue with a horseshoe and no cohomology at all. That route does not survive here: its simultaneousImageCover takes a Finset.univ.inf of covering sieves — a finite intersection — so finitely many generators lift on one refinement and arbitrarily many do not. Quasi-coherent presentations have arbitrary index sets. So this file takes the classical route and pays the cohomological price once.

The argument

On Spec R, for 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 with M₁ and M₃ quasi-coherent:

1. M₁ is quasi-coherent, hence H¹(Spec R, M₁) = 0 (Cohomology.modules_H_subsingleton_of_isQuasicoherent).
2. So Γ carries the sequence to a short exact sequence of R-modules — left exactness is formal, and the surjectivity is step 1 fed through Sheaf.sections_surjective_of_subsingleton_H_one.
3. tilde is exact, so it carries that back to module sheaves. Right exactness was free; left exactness is the kernel closure, since tilde factors through tildeEquiv and the quasi-coherent inclusion.
4. fromTildeΓ compares the two sequences and is iso at both ends. The short five lemma makes it iso in the middle, which is quasi-coherence of M₂.

Then isQuasicoherent_iff_restrict_affineOpenCover transports it to any scheme.

On Γ

Written affineΓ R = moduleSpecSectionsFunctor R ⊤, not moduleSpecΓFunctor. The two are defeq, but only the first has domain (Spec R).Modules, which is where the geometry lives, and an instance proved for one is not found for the other. Abelian/Kernels.lean already had this functor and kept it private; it is public as of this change. Modules/Affine/Equivalence.lean records the same wrapper problem for Scheme.Modules itself.

Main results

• AlgebraicGeometry.tilde_preservesFiniteLimits;
• AlgebraicGeometry.shortExact_map_affineΓ;
• AlgebraicGeometry.isQuasicoherent_middle_affine and isQuasicoherent_middle;
• AlgebraicGeometry.quasicoherent_isClosedUnderExtensions.

Exactness of tilde

theorem AlgebraicGeometry.qcHasFiniteProducts {R : CommRingCat} : CategoryTheory.Limits.HasFiniteProducts (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).FullSubcategory

Finite products on affine quasi-coherent sheaves, transported across the tilde equivalence rather than postulated on the full subcategory.

theorem AlgebraicGeometry.qcHasBinaryBiproducts {R : CommRingCat} : CategoryTheory.Limits.HasBinaryBiproducts (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).FullSubcategory

@[implicit_reducible]

noncomputable def AlgebraicGeometry.qcAbelian {R : CommRingCat} : CategoryTheory.Abelian (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).FullSubcategory

Quasi-coherent sheaves on an affine spectrum are abelian, by the proved tilde equivalence with modules over the coordinate ring.

Equations

• AlgebraicGeometry.qcAbelian = CategoryTheory.abelianOfEquivalence AlgebraicGeometry.tildeEquiv.inverse

instance AlgebraicGeometry.qcι_preservesKernel {R : CommRingCat} {M N : (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).FullSubcategory} (g : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).ι

The inclusion of quasi-coherent sheaves preserves kernels — this is the kernel closure of Quasicoherent/Kernels.lean, in the form limit-preservation wants it.

instance AlgebraicGeometry.quasicoherentι_preservesFiniteLimits {R : CommRingCat} : CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).ι

The inclusion of quasi-coherent sheaves into all module sheaves on an affine spectrum preserves finite limits.

instance AlgebraicGeometry.tilde_preservesFiniteLimits {R : CommRingCat} : CategoryTheory.Limits.PreservesFiniteLimits (tilde.functor R)

tilde is exact.

Right exactness is free — tilde.adjunction makes it a left adjoint. Left exactness is this: tilde factors through tildeEquiv and the inclusion of quasi-coherent sheaves, and that inclusion is left exact because quasi-coherence is closed under ambient kernels.

The affine five lemma

Global sections on an affine spectrum

Γ is written moduleSpecSectionsFunctor R ⊤ rather than moduleSpecΓFunctor. The two are defeq, but only the first has domain (Spec R).Modules, which is what a short complex of the geometry here actually lives in.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineΓ (R : CommRingCat) : CategoryTheory.Functor (Spec R).Modules (ModuleCat ↑R)

Global sections on Spec R, retyped over (Spec R).Modules.

Equations

• AlgebraicGeometry.affineΓ R = AlgebraicGeometry.moduleSpecSectionsFunctor R ⊤

theorem AlgebraicGeometry.shortExact_map_affineΓ {R : CommRingCat} {S : CategoryTheory.ShortComplex (Spec R).Modules} (hS : S.ShortExact) (h₁ : SheafOfModules.IsQuasicoherent S.X₁) : (S.map (affineΓ R)).ShortExact

Global sections of a short exact sequence of module sheaves on Spec R are short exact, as soon as the sub is quasi-coherent.

Left exactness is formal — Γ preserves finite limits. The surjectivity is the cohomological input, and the only one in this file: H¹(Spec R, M₁) = 0.

The affine five lemma

noncomputable def AlgebraicGeometry.fromTildeΓShortComplexHom {R : CommRingCat} (S : CategoryTheory.ShortComplex (Spec R).Modules) : (S.map (affineΓ R)).map (tilde.functor R) ⟶ S

The comparison Γ(−)~ ⟶ −, as a morphism of short complexes.

Equations

• AlgebraicGeometry.fromTildeΓShortComplexHom S = { τ₁ := S.X₁.fromTildeΓ, τ₂ := S.X₂.fromTildeΓ, τ₃ := S.X₃.fromTildeΓ, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[simp]

theorem AlgebraicGeometry.fromTildeΓShortComplexHom_τ₂ {R : CommRingCat} (S : CategoryTheory.ShortComplex (Spec R).Modules) : (fromTildeΓShortComplexHom S).τ₂ = S.X₂.fromTildeΓ

@[simp]

theorem AlgebraicGeometry.fromTildeΓShortComplexHom_τ₁ {R : CommRingCat} (S : CategoryTheory.ShortComplex (Spec R).Modules) : (fromTildeΓShortComplexHom S).τ₁ = S.X₁.fromTildeΓ

@[simp]

theorem AlgebraicGeometry.fromTildeΓShortComplexHom_τ₃ {R : CommRingCat} (S : CategoryTheory.ShortComplex (Spec R).Modules) : (fromTildeΓShortComplexHom S).τ₃ = S.X₃.fromTildeΓ

theorem AlgebraicGeometry.isQuasicoherent_middle_affine {R : CommRingCat} {S : CategoryTheory.ShortComplex (Spec R).Modules} (hS : S.ShortExact) (h₁ : SheafOfModules.IsQuasicoherent S.X₁) (h₃ : SheafOfModules.IsQuasicoherent S.X₃) : SheafOfModules.IsQuasicoherent S.X₂

Quasi-coherence is closed under extensions on an affine spectrum.

The four steps: H¹ of the sub vanishes, so Γ of the sequence is short exact; tilde is exact, so it carries that back to a short exact sequence of module sheaves; fromTildeΓ compares the two, and is iso at both ends because both ends are quasi-coherent; the short five lemma makes it iso in the middle, which is quasi-coherence of the middle.

Any scheme

theorem AlgebraicGeometry.isQuasicoherent_middle {X : Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (h₁ : SheafOfModules.IsQuasicoherent S.X₁) (h₃ : SheafOfModules.IsQuasicoherent S.X₃) : SheafOfModules.IsQuasicoherent S.X₂

Quasi-coherence is closed under extensions, on an arbitrary scheme.

The affine case transported along X.affineOpenCover by the affine-local criterion. Restriction along an open immersion is exact, so the restricted sequence is again short exact, and its two ends are again quasi-coherent.

instance AlgebraicGeometry.quasicoherent_isClosedUnderExtensions (X : Scheme) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsClosedUnderExtensions

Quasi-coherent module sheaves on an arbitrary scheme are closed under extensions. With quasicoherent_isClosedUnderKernels and quasicoherent_isClosedUnderCokernels, this is the weak Serre property.

instance AlgebraicGeometry.quasicoherent_containsZero (X : Scheme) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).ContainsZero

The zero sheaf is quasi-coherent.

Scheme.coherent_containsZero specializes the arbitrary-ringed-site zero theorem to X.Modules, and Mathlib turns finite presentation into quasi-coherence, so this needs no QuasicoherentData of its own.

It is the fourth ingredient of the triangulated structure and the only one that is not a closure property: ObjectProperty.IsTriangulated extends ContainsZero, and closure under kernels cannot produce a first member of the class from nothing.