Derived categories of coherent sheaves on schemes

For a locally Noetherian scheme X, this module supplies the canonical geometric specialization of Mathlib's generic derived-category construction: SchemeCoherentDerivedCategory X and its bounded subcategory SchemeBoundedCoherentDerivedCategory X = Dᵇ(Coh X).

Perfect objects are defined in D(Coh X) as the thick triangulated envelope of degree-zero finite locally free coherent sheaves. The structure sheaf gives a genuine object in that envelope. Nothing in this module depends on a family of schemes or on pullback; those consumers live under DerivedCategory/Families/.

The closing section gives every line bundle a canonical image in this category: LineBundleData.coh packages the underlying sheaf with its coherence proof, LineBundleData.derivedObject places it in degree zero of D(Coh X), and LineBundleData.boundedDerivedObject packages its proved boundedness as an object of Dᵇ(Coh X); cohIso and derivedObjectIso transport both along an isomorphism of underlying sheaves, so statements about a collection of line bundles are well-defined up to iso. This is the adapter geometric consumers use to speak about a line bundle as a derived object without re-deriving the Coh-object and singleFunctor plumbing each time.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.SchemeCoherentDerivedCategory (X : Scheme) [IsLocallyNoetherian X] : Type (u + 1)

The derived category of coherent sheaves on a locally Noetherian scheme.

Equations

• AlgebraicGeometry.DerivedCategory.SchemeCoherentDerivedCategory X = DerivedCategory (AlgebraicGeometry.Coh X)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.SchemeBoundedCoherentDerivedCategory (X : Scheme) [IsLocallyNoetherian X] : Type (u + 1)

The bounded derived category Dᵇ(Coh X) of coherent sheaves on a locally Noetherian scheme.

Equations

• AlgebraicGeometry.DerivedCategory.SchemeBoundedCoherentDerivedCategory X = DerivedCategory.Bounded (AlgebraicGeometry.Coh X)

def AlgebraicGeometry.DerivedCategory.schemeFiniteLocallyFreeGenerator (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.ObjectProperty (SchemeCoherentDerivedCategory X)

Degree-zero derived objects represented by finite locally free coherent sheaves. Shifts, finite sums, cones, and retracts are added by ObjectProperty.triangEnvelope.

Equations

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

def AlgebraicGeometry.DerivedCategory.schemePerfect (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.ObjectProperty (SchemeCoherentDerivedCategory X)

The perfect-object property on the coherent derived category: the thick triangulated envelope of finite locally free coherent sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.schemePerfect X = (AlgebraicGeometry.DerivedCategory.schemeFiniteLocallyFreeGenerator X).triangEnvelope

theorem AlgebraicGeometry.DerivedCategory.schemeFiniteLocallyFreeGenerator_le_bounded (X : Scheme) [IsLocallyNoetherian X] : schemeFiniteLocallyFreeGenerator X ≤ DerivedCategory.TStructure.t.bounded

Every finite-locally-free degree-zero generator is bounded for the canonical t-structure.

theorem AlgebraicGeometry.DerivedCategory.schemePerfect_le_bounded (X : Scheme) [IsLocallyNoetherian X] : schemePerfect X ≤ DerivedCategory.TStructure.t.bounded

Every perfect complex is bounded coherent. This is the universal-property proof from the thick-envelope definition, not an additional assumption.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory (X : Scheme) [IsLocallyNoetherian X] : Type (u + 1)

Perf(X) as the full subcategory cut out by the thick envelope of finite locally free coherent sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory X = (AlgebraicGeometry.DerivedCategory.schemePerfect X).FullSubcategory

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.ι (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Functor (SchemePerfectDerivedCategory X) (SchemeCoherentDerivedCategory X)

The inclusion of perfect objects into the coherent derived category.

Equations

• AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.ι X = (AlgebraicGeometry.DerivedCategory.schemePerfect X).ι

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.toBounded (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.Functor (SchemePerfectDerivedCategory X) (SchemeBoundedCoherentDerivedCategory X)

The fully faithful inclusion Perf(X) ⥤ Dᵇ(Coh X).

Equations

• AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.toBounded X = CategoryTheory.ObjectProperty.ιOfLE ⋯

theorem AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.structureSheaf_mem_generator (X : Scheme) [IsLocallyNoetherian X] : schemeFiniteLocallyFreeGenerator X ((DerivedCategory.singleFunctor (Coh X) 0).obj X.structureSheafCoh)

The degree-zero structure sheaf lies in the finite-locally-free generating property.

theorem AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.structureSheaf_mem (X : Scheme) [IsLocallyNoetherian X] : schemePerfect X ((DerivedCategory.singleFunctor (Coh X) 0).obj X.structureSheafCoh)

The degree-zero structure sheaf is a perfect object.

noncomputable def AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.structureSheaf (X : Scheme) [IsLocallyNoetherian X] : SchemePerfectDerivedCategory X

A canonical object of Perf(X) supplied by the structure sheaf.

Equations

• AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.structureSheaf X = { obj := (DerivedCategory.singleFunctor (AlgebraicGeometry.Coh X) 0).obj X.structureSheafCoh, property := ⋯ }

instance AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.instNonemptySchemeCoherentDerivedCategorySchemeFiniteLocallyFreeGenerator (X : Scheme) [IsLocallyNoetherian X] : (schemeFiniteLocallyFreeGenerator X).Nonempty

The finite-locally-free generating property is nonempty.

instance AlgebraicGeometry.DerivedCategory.SchemePerfectDerivedCategory.instNonemptySchemeCoherentDerivedCategorySchemePerfect (X : Scheme) [IsLocallyNoetherian X] : (schemePerfect X).Nonempty

The perfect-object property is nonempty.

Line bundles as coherent derived objects

A line bundle is coherent outright — LineBundleData.isCoherent needs no noetherian hypothesis — so it has a canonical Coh X avatar, and on a locally Noetherian scheme a canonical degree-zero derived object. The declarations live in the LineBundleData namespace for dot notation, following the precedent of LineBundleData.toPic_eq_iff in CoherentSheaf/StructureSheaf.lean.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.coh {X : Scheme} (L : LineBundleData X) : Coh X

A line bundle as an object of Coh X: the underlying sheaf paired with its coherence proof. No noetherian hypothesis enters, for the same reason as Scheme.structureSheafCoh: an invertible sheaf is of finite presentation outright.

Equations

• L.coh = { obj := L.line, property := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.coh_obj {X : Scheme} (L : LineBundleData X) : L.coh.obj = L.line

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.unit_coh (X : Scheme) : (unit X).coh = X.structureSheafCoh

The unit line bundle's Coh avatar is the structure sheaf. Both sides are the same pair by definition; this records that the two routes to O_X in Coh X cannot drift apart. X is explicit because nothing else in the statement determines it, matching unit_toPic.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.cohIso {X : Scheme} {L M : LineBundleData X} (e : L.line ≅ M.line) : L.coh ≅ M.coh

Lift an isomorphism of underlying sheaves to Coh X. The inclusion is fully faithful, so this is ObjectProperty.isoMk; it is what makes coh well-defined up to the choices a LineBundleData records.

Equations

• AlgebraicGeometry.Scheme.Modules.LineBundleData.cohIso e = X.coherent.isoMk e

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.derivedObject {X : Scheme} [IsLocallyNoetherian X] (L : LineBundleData X) : DerivedCategory.SchemeCoherentDerivedCategory X

A line bundle placed in degree zero of D(Coh X) — not Dᵇ(Coh X) and not Perf(X), which is why unit_derivedObject has to project .obj off SchemePerfectDerivedCategory.structureSheaf. This is definitionally the same singleFunctor expression schemeFiniteLocallyFreeGenerator uses inline, so derivedObject_mem_generator closes on Iso.refl.

Equations

• L.derivedObject = (DerivedCategory.singleFunctor (AlgebraicGeometry.Coh X) 0).obj L.coh

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.derivedObject_mem_generator {X : Scheme} [IsLocallyNoetherian X] (L : LineBundleData X) : DerivedCategory.schemeFiniteLocallyFreeGenerator X L.derivedObject

A line bundle satisfies the finite-locally-free generating property: its rank-one atlas finiteLocallyFree is exactly the witness the property asks for, in degree zero.

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.derivedObject_perfect {X : Scheme} [IsLocallyNoetherian X] (L : LineBundleData X) : DerivedCategory.schemePerfect X L.derivedObject

Every line bundle is a perfect object of the coherent derived category: it lies in the generating property itself, before the envelope adds shifts, sums, cones, and retracts.

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.derivedObject_bounded {X : Scheme} [IsLocallyNoetherian X] (L : LineBundleData X) : DerivedCategory.TStructure.t.bounded L.derivedObject

A line bundle is bounded for the canonical t-structure, through schemeFiniteLocallyFreeGenerator_le_bounded rather than a fresh degree computation.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.boundedDerivedObject {X : Scheme} [IsLocallyNoetherian X] (L : LineBundleData X) : DerivedCategory.SchemeBoundedCoherentDerivedCategory X

A line bundle as an object of the bounded coherent derived category. The underlying derived object is derivedObject; no second representative or comparison choice is introduced.

Equations

• L.boundedDerivedObject = { obj := L.derivedObject, property := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.boundedDerivedObject_obj {X : Scheme} [IsLocallyNoetherian X] (L : LineBundleData X) : L.boundedDerivedObject.obj = L.derivedObject

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.derivedObjectIso {X : Scheme} [IsLocallyNoetherian X] {L M : LineBundleData X} (e : L.line ≅ M.line) : L.derivedObject ≅ M.derivedObject

Lift an isomorphism of underlying sheaves to the derived objects. Needed by any collection of line bundles stated up to isomorphism: it is what makes membership statements about derivedObject transportable along a change of representative.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.unit_derivedObject (X : Scheme) [IsLocallyNoetherian X] : (unit X).derivedObject = (DerivedCategory.SchemePerfectDerivedCategory.structureSheaf X).obj

The unit line bundle's derived object is the underlying object of the canonical perfect structure sheaf. Definitional, so the two routes to O_X in D(Coh X) — through LineBundleData and through SchemePerfectDerivedCategory.structureSheaf — are identified for free.