Relative-perfect and universally-gluable complexes

Pseudo-coherence, local finite Tor amplitude over a base, relative perfection and the universally-gluable refinement. These are properties of one complex over one morphism. Their objects live in the honest quasi-coherent-cohomology locus SchemeQuasicoherentDerivedCategory X, not in the derived category of all module sheaves under a different name.

They are needed before a moduli functor exists -- base change and derived operations ask for them -- so they are owned here, beside the derived category they are predicates on, and the moduli problem in Moduli/PerfectComplex/ consumes them. That subtree keeps the presheaf, restriction stability, boundedness, openness, atlas and algebraicity layer, none of which is mentioned here. This file was Moduli/PerfectComplex/Relative.lean until 2026-09-13; see docs/architecture/cutover-ledger.md, finding 11.

Stalkwise flatness of a module sheaf over a morphism is a further step down and lives with the module sheaves, in Modules/Flat.lean.

At the current Mathlib pin there is no general derived tensor product for module sheaves. Finite Tor amplitude is therefore expressed by the standard local model that can be checked without such an API: around every point the complex is represented by a bounded complex of module sheaves whose stalks are flat over the base. The bounds and the representing isomorphism are data, not an arbitrary proposition supplied by a caller.

For the same reason, a geometric fiber is computed only from an explicit globally flat model. The repository now has an interface characterizing arbitrary pullback by its left-derived universal property, but it does not yet construct that interface along arbitrary fiber inclusions. This is enough to define and inhabit the zero model and to state fiberwise negative-Ext vanishing honestly; comparison with a future K-flat construction remains a separate theorem.

def AlgebraicGeometry.schemePseudoCoherent (X : Scheme) : CategoryTheory.ObjectProperty (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X)

The locally Noetherian cohomological criterion for pseudo-coherence: bounded above with finitely presented cohomology in every degree.

SCOPE (2026-08-18 review, P2-12): on a locally Noetherian scheme this criterion is pseudo-coherence; on a general scheme the two notions diverge in both directions, and the affine family pseudofunctor instantiates this predicate over arbitrary test algebras. Any theorem that quantifies over non-Noetherian bases is therefore about THIS predicate, not about standard pseudo-coherence; the #554 preservation program must either restrict its index to the Noetherian locus or prove preservation for this criterion and say which.

Equations

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

instance AlgebraicGeometry.schemePseudoCoherent_isClosedUnderIsomorphisms (X : Scheme) : (schemePseudoCoherent X).IsClosedUnderIsomorphisms

def AlgebraicGeometry.relativeOpenBaseChange {X S : Scheme} (p : X ⟶ S) (U : X.Opens) : DerivedCategory.Families.SchemeBaseChange S

The object of Over S obtained by restricting p : X ⟶ S to an open subscheme of X.

Equations

• AlgebraicGeometry.relativeOpenBaseChange p U = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp U.ι p)

def AlgebraicGeometry.relativeOpenTo {X S : Scheme} (p : X ⟶ S) (U : X.Opens) : relativeOpenBaseChange p U ⟶ CategoryTheory.Over.mk p

The canonical open-immersion morphism from a restricted family to the original family over S.

Equations

• AlgebraicGeometry.relativeOpenTo p U = CategoryTheory.Over.homMk U.ι ⋯

@[simp]

theorem AlgebraicGeometry.relativeOpenTo_left {X S : Scheme} (p : X ⟶ S) (U : X.Opens) : CategoryTheory.Over.Hom.left (relativeOpenTo p U) = U.ι

instance AlgebraicGeometry.relativeOpenTo_isOpenImmersion {X S : Scheme} (p : X ⟶ S) (U : X.Opens) : IsOpenImmersion (CategoryTheory.Over.Hom.left (relativeOpenTo p U))

structure AlgebraicGeometry.LocalFiniteTorAmplitudeChart {X S : Scheme} (p : X ⟶ S) (E : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X) (x : ↥X) : Type (u + 1)

A bounded flat local model for one object near one point. The target of represents is the actual exact derived restriction along the open immersion; no nonexact derived pullback is used.

• openSubset : X.Opens

  An open neighbourhood on which the flat model is defined.

• mem_openSubset : x ∈ self.openSubset

  The chosen point lies in the neighbourhood.

• lower : ℤ

  Lower cohomological bound for the model.

• upper : ℤ

  Upper cohomological bound for the model.

• lower_le_upper : self.lower ≤ self.upper

  The interval of possible nonzero terms is ordered.

• model : CochainComplex (↑self.openSubset).Modules ℤ

  A complex of module sheaves on the open neighbourhood.

• strictlyGE : self.model.IsStrictlyGE self.lower

  The model has no terms below lower.

• strictlyLE : self.model.IsStrictlyLE self.upper

  The model has no terms above upper.

• flatOverBase (i : ℤ) : Scheme.Modules.IsFlatOver (CategoryTheory.CategoryStruct.comp self.openSubset.ι p) (self.model.X i)

  Every term is stalkwise flat over the base.

• represents : (DerivedCategory.SchemeDerivedCategory.Q ↑self.openSubset).obj self.model ≅ (DerivedCategory.Families.SchemeBaseChange.derivedPullback (relativeOpenTo p self.openSubset)).obj E.obj

  The model represents the exact restriction of the original object.

def AlgebraicGeometry.schemeLocallyFiniteTorAmplitudeOver {X S : Scheme} (p : X ⟶ S) : CategoryTheory.ObjectProperty (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X)

Local finite Tor amplitude over S, witnessed pointwise by bounded stalkwise-flat models on actual open neighbourhoods.

Equations

• AlgebraicGeometry.schemeLocallyFiniteTorAmplitudeOver p E = ∀ (x : ↥X), Nonempty (AlgebraicGeometry.LocalFiniteTorAmplitudeChart p E x)

instance AlgebraicGeometry.schemeLocallyFiniteTorAmplitudeOver_isClosedUnderIsomorphisms {X S : Scheme} (p : X ⟶ S) : (schemeLocallyFiniteTorAmplitudeOver p).IsClosedUnderIsomorphisms

def AlgebraicGeometry.schemeRelativePerfect {X S : Scheme} (p : X ⟶ S) : CategoryTheory.ObjectProperty (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X)

The relative-perfect predicate: schemePseudoCoherent objects with locally finite Tor amplitude over the base.

The definition takes an arbitrary morphism; the intended moduli context is a flat, locally finitely presented family, and geometric theorems state those hypotheses where they use them rather than here (see SchemeRelativePerfectCategory). The pseudo-coherence component carries the locally Noetherian scope note on schemePseudoCoherent.

Equations

• AlgebraicGeometry.schemeRelativePerfect p E = (AlgebraicGeometry.schemePseudoCoherent X E ∧ AlgebraicGeometry.schemeLocallyFiniteTorAmplitudeOver p E)

instance AlgebraicGeometry.schemeRelativePerfect_isClosedUnderIsomorphisms {X S : Scheme} (p : X ⟶ S) : (schemeRelativePerfect p).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev AlgebraicGeometry.SchemeRelativePerfectCategory {X S : Scheme} (p : X ⟶ S) : Type (u + 1)

The full category cut out by relative perfection over p. Geometric theorems about this category state flatness, finite-presentation, and Noetherian hypotheses where they are actually used rather than storing inert typeclass arguments in the category abbreviation.

Equations

• AlgebraicGeometry.SchemeRelativePerfectCategory p = (AlgebraicGeometry.schemeRelativePerfect p).FullSubcategory

theorem AlgebraicGeometry.SchemeRelativePerfectCategory.exists_boundedCoherentRepresentative {X S : Scheme} [IsLocallyNoetherian X] {p : X ⟶ S} (h : DerivedCategory.Dqc.HasBoundedCoherentDqcIdentification X) (E : SchemeRelativePerfectCategory p) (hE : DerivedCategory.Dqc.schemeBoundedCoherentCohomology X E.obj) : ∃ (F : DerivedCategory.SchemeBoundedCoherentDerivedCategory X), Nonempty (((DerivedCategory.Dqc.boundedCoherentDerivedToDqc X).obj F).obj ≅ E.obj)

A relative-perfect object with bounded coherent cohomology has a Dᵇ(Coh X) representative once the bounded-coherent Dqc identification is supplied explicitly.

theorem AlgebraicGeometry.SchemeRelativePerfectCategory.perfect_iff_compact {X S : Scheme} [IsLocallyNoetherian X] {p : X ⟶ S} (h : DerivedCategory.Dqc.PerfectObjectsAreCompactInDqc X) (E : SchemeRelativePerfectCategory p) : DerivedCategory.Dqc.schemePerfectInDqc X E.obj ↔ CategoryTheory.IsCompactObject E.obj

For a relative-perfect object, the explicit compact/perfect comparison identifies membership in the absolute perfect locus with compactness in Dqc(X).

structure AlgebraicGeometry.GeometricFiberModel {X S : Scheme} (p : X ⟶ S) (E : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X) (s : ↥S) : Type (u + 1)

A global stalkwise-flat model used to compute one geometric fiber. This does not inhabit the arbitrary left-derived pullback interface: it records the precise model from which the displayed fiber object is computed.

• totalModel : CochainComplex X.Modules ℤ

  A complex representing the total object.

• represents : (DerivedCategory.SchemeDerivedCategory.Q X).obj self.totalModel ≅ E.obj

  The total model represents E.

• flatOverBase (i : ℤ) : Scheme.Modules.IsFlatOver p (self.totalModel.X i)

  Every term is stalkwise flat over S.

noncomputable def AlgebraicGeometry.GeometricFiberModel.fiberComplex {X S : Scheme} {p : X ⟶ S} {E : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X} {s : ↥S} (M : GeometricFiberModel p E s) : CochainComplex (Scheme.Hom.fiber p s).Modules ℤ

The degreewise pullback of a chosen flat model to the scheme-theoretic fiber.

Equations

• M.fiberComplex = ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Scheme.Hom.fiberι p s)).mapHomologicalComplex (ComplexShape.up ℤ)).obj M.totalModel

noncomputable def AlgebraicGeometry.GeometricFiberModel.fiberObject {X S : Scheme} {p : X ⟶ S} {E : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X} {s : ↥S} (M : GeometricFiberModel p E s) : DerivedCategory.SchemeDerivedCategory (Scheme.Hom.fiber p s)

The geometric fiber object computed in the ambient derived category. No claim identifies the ambient category with Dqc; quasi-coherence of this object is a separate comparison theorem once arbitrary left-derived pullback has been constructed.

Equations

• M.fiberObject = (AlgebraicGeometry.DerivedCategory.SchemeDerivedCategory.Q (AlgebraicGeometry.Scheme.Hom.fiber p s)).obj M.fiberComplex

structure AlgebraicGeometry.UniversallyGluableData {X S : Scheme} (p : X ⟶ S) (E : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X) : Type (u + 1)

Explicit geometric fibers of a relative-perfect object together with negative self-Ext vanishing on every fiber.

• fiberModel (s : ↥S) : GeometricFiberModel p E s

  A flat model computing every geometric fiber.

• negativeExtVanishes (s : ↥S) (n : ℤ) (hn : n < 0) (f : (self.fiberModel s).fiberObject ⟶ (CategoryTheory.shiftFunctor (DerivedCategory.SchemeDerivedCategory (Scheme.Hom.fiber p s)) n).obj (self.fiberModel s).fiberObject) : f = 0

  Negative self-extensions vanish on every geometric fiber.

def AlgebraicGeometry.schemeUniversallyGluableRelativePerfect {X S : Scheme} (p : X ⟶ S) : CategoryTheory.ObjectProperty (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X)

The relative-perfect, universally-gluable locus.

Equations

• AlgebraicGeometry.schemeUniversallyGluableRelativePerfect p E = (AlgebraicGeometry.schemeRelativePerfect p E ∧ Nonempty (AlgebraicGeometry.UniversallyGluableData p E))

noncomputable def AlgebraicGeometry.UniversallyGluableData.ofIso {X S : Scheme} {p : X ⟶ S} {E F : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X} (e : E ≅ F) (h : UniversallyGluableData p E) : UniversallyGluableData p F

Transport universally-gluable fiber data along an isomorphism of total objects. The same flat models compute the fibers; only their representing isomorphisms change.

Equations

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

instance AlgebraicGeometry.schemeUniversallyGluableRelativePerfect_isClosedUnderIsomorphisms {X S : Scheme} (p : X ⟶ S) : (schemeUniversallyGluableRelativePerfect p).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev AlgebraicGeometry.SchemeUniversallyGluableCategory {X S : Scheme} (p : X ⟶ S) : Type (u + 1)

The full category of relative-perfect universally-gluable complexes.

Equations

• AlgebraicGeometry.SchemeUniversallyGluableCategory p = (AlgebraicGeometry.schemeUniversallyGluableRelativePerfect p).FullSubcategory

Concrete models for the canonical Dqc zero

noncomputable def AlgebraicGeometry.zeroModuleComplex (X : Scheme) : CochainComplex X.Modules ℤ

The zero cochain complex of module sheaves, named explicitly because the object-level 0 notation is not exported by every derived-category import.

Equations

• AlgebraicGeometry.zeroModuleComplex X = HomologicalComplex.zero

theorem AlgebraicGeometry.zeroModuleComplex_isZero (X : Scheme) : CategoryTheory.Limits.IsZero (zeroModuleComplex X)

The zero complex is a zero object.

theorem AlgebraicGeometry.schemePseudoCoherent_zero (X : Scheme) : schemePseudoCoherent X (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X)

The zero object is pseudo-coherent.

noncomputable def AlgebraicGeometry.zeroLocalFiniteTorAmplitudeChart {X S : Scheme} (p : X ⟶ S) (x : ↥X) : LocalFiniteTorAmplitudeChart p (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X) x

The zero object has a local finite-Tor-amplitude chart at every point.

Equations

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

theorem AlgebraicGeometry.schemeLocallyFiniteTorAmplitudeOver_zero {X S : Scheme} (p : X ⟶ S) : schemeLocallyFiniteTorAmplitudeOver p (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X)

The zero object has locally finite Tor amplitude over every base.

theorem AlgebraicGeometry.schemeRelativePerfect_zero {X S : Scheme} (p : X ⟶ S) : schemeRelativePerfect p (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X)

The zero object is relative perfect.

noncomputable def AlgebraicGeometry.zeroGeometricFiberModel {X S : Scheme} (p : X ⟶ S) (s : ↥S) : GeometricFiberModel p (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X) s

The zero total complex computes the zero object on every geometric fiber.

Equations

• AlgebraicGeometry.zeroGeometricFiberModel p s = { totalModel := AlgebraicGeometry.zeroModuleComplex X, represents := ⋯.iso ⋯, flatOverBase := ⋯ }

noncomputable def AlgebraicGeometry.universallyGluableDataZero {X S : Scheme} (p : X ⟶ S) : UniversallyGluableData p (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X)

The zero relative-perfect object is universally gluable.

Equations

• AlgebraicGeometry.universallyGluableDataZero p = { fiberModel := AlgebraicGeometry.zeroGeometricFiberModel p, negativeExtVanishes := ⋯ }

theorem AlgebraicGeometry.schemeUniversallyGluableRelativePerfect_zero {X S : Scheme} (p : X ⟶ S) : schemeUniversallyGluableRelativePerfect p (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory.zero X)

The relative-perfect universally-gluable locus is nonempty: it contains the zero complex for every flat locally finitely presented family.