Global sections of quasicoherent modules on an affine scheme

Mathlib's AlgebraicGeometry.tildeEquiv identifies quasicoherent modules on Spec R with R-modules. Consequently an epimorphism between quasicoherent modules is surjective on global sections, even when the epimorphism is taken in the category of all sheaves of modules.

Consequently, global sections preserve short exact sequences whose middle and right terms are quasicoherent. This is the affine exactness step used in Serre's affine acyclicity theorem; see Hartshorne, Algebraic Geometry, Chapter III, Theorem 3.5.

The file also records the base-ring action on affine global sections and extensionality of sections by restriction to basic opens.

instance TauCeti.AlgebraicGeometry.instIsRightAdjointModuleCatCarrierModulesSpecModuleSpecΓFunctor_tauCeti (R : CommRingCat) : AlgebraicGeometry.moduleSpecΓFunctor.IsRightAdjoint

The global-section functor on Spec R is right adjoint to the tilde functor.

theorem TauCeti.AlgebraicGeometry.moduleSpecΓFunctor_map_surjective_of_epi_of_isQuasicoherent {R : CommRingCat} {M N : (AlgebraicGeometry.Spec R).Modules} (f : M ⟶ N) [CategoryTheory.Epi f] [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.moduleSpecΓFunctor.map f))

An epimorphism between quasicoherent sheaves on an affine scheme is surjective on global sections.

theorem TauCeti.AlgebraicGeometry.shortExact_map_moduleSpecΓFunctor_of_isQuasicoherent {R : CommRingCat} {S : CategoryTheory.ShortComplex (AlgebraicGeometry.Spec R).Modules} (hS : S.ShortExact) [SheafOfModules.IsQuasicoherent S.X₂] [SheafOfModules.IsQuasicoherent S.X₃] : (S.map AlgebraicGeometry.moduleSpecΓFunctor).ShortExact

Taking global sections preserves a short exact sequence whose middle and right terms are quasicoherent sheaves on Spec R. The exactness hypothesis is in the ambient category of sheaves of modules.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections_Spec_apply (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] (r : R) : (AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections R (AlgebraicGeometry.Spec A)) r = (algebraMap ↑A ↑((AlgebraicGeometry.Spec A).presheaf.obj (Opposite.op ⊤))) ((algebraMap R ↑A) r)

On Spec A over Spec R, the base ring maps to global functions through A.

theorem TauCeti.AlgebraicGeometry.Scheme.baseRingToStructurePresheaf_Spec_app_apply (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] (U : (AlgebraicGeometry.Spec A).Opensᵒᵖ) (r : R) : (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R (AlgebraicGeometry.Spec A)).app U)) r = (algebraMap ↑A ↑((AlgebraicGeometry.Spec A).presheaf.obj (Opposite.op (Opposite.unop U)))) ((algebraMap R ↑A) r)

On Spec A over Spec R, the base ring maps to the functions on an open U through A.

instance TauCeti.AlgebraicGeometry.instIsScalarTowerCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecAbPresheafOpTop_tauCeti (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] (M : (AlgebraicGeometry.Spec A).Modules) : IsScalarTower R ↑A ↑(M.presheaf.obj (Opposite.op ⊤))

The base ring R acts on the global sections of a sheaf of modules on Spec A through A.

theorem TauCeti.AlgebraicGeometry.isOver_fromSpec (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] (U : ↑X.affineOpens) : AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.IsAffineOpen.fromSpec ⋯) (AlgebraicGeometry.Spec ↧R)

The canonical affine chart is a morphism over Spec R when its coordinate ring carries the algebra structure obtained by restricting the base-ring map.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.section_ext_basicOpen {A : CommRingCat} {M : (AlgebraicGeometry.Spec A).Modules} {U : (AlgebraicGeometry.Spec A).Opens} {s t : ↑(M.presheaf.obj (Opposite.op U))} (h : ∀ (f : ↑A) (hf : PrimeSpectrum.basicOpen f ≤ U), (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE hf).op)) s = (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE hf).op)) t) : s = t

Two sections over U of a sheaf of modules on Spec A agree if their restrictions to every basic open D(f) ⊆ U agree.