The structure sheaf as a coherent sheaf

O_X is a coherent sheaf, and this file names the resulting object of Coh X. It is a two-line definition, but it needs a home: coherence of O_X is LineBundleData.isCoherent applied to LineBundleData.unit, so the fact lives in Divisors/, while the category it lands in lives in CoherentSheaf/.

The coherent derived-category owner imports this module and uses this same object as the canonical degree-zero perfect object. Keeping the coherent sheaf here avoids making ordinary coherent-sheaf consumers depend on triangulated generators or t-structures.

noncomputable def AlgebraicGeometry.Scheme.structureSheafCoh (X : Scheme) : Coh X

The structure sheaf O_X, regarded as an object of Coh X.

Coherence is Scheme.Modules.LineBundleData.isCoherent for the unit line bundle; no noetherian or finiteness hypothesis on X is needed, because an invertible sheaf is of finite presentation outright.

Equations

• X.structureSheafCoh = { obj := (AlgebraicGeometry.Scheme.Modules.LineBundleData.unit X).line, property := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.structureSheafCoh_obj (X : Scheme) : X.structureSheafCoh.obj = (Modules.LineBundleData.unit X).line

theorem AlgebraicGeometry.Scheme.structureSheafCoh_obj_eq_unit (X : Scheme) : X.structureSheafCoh.obj = SheafOfModules.unit X.ringCatSheaf

The underlying module sheaf of structureSheafCoh is the unit of the tensor product, which is what makes it the structure sheaf rather than some other invertible sheaf.

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.toPic_eq_iff {X : Scheme} (L M : LineBundleData X) : L.toPic = M.toPic ↔ Nonempty (L.line ≅ M.line)

Two line bundles have the same Picard-group element exactly when their underlying sheaves are isomorphic.

toPic_eq_of_iso is the forward direction alone. The converse is what a triviality hypothesis stated in Pic has to be unpacked through, so both are worth having; the recorded tensor inverses play no part, which is why this is an iff and not merely an implication.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.unit_toPic (X : Scheme) : (unit X).toPic = 1

The structure sheaf is the identity of the Picard group.