Comparing the repository's perfect-complex notions

The repository uses three deliberately different notions:

• schemePerfect X is the absolute thick envelope of finite locally free coherent sheaves in D(Coh X);
• schemeRelativePerfect p is pseudo-coherence plus local finite Tor amplitude over a chosen morphism p, inside Dqc(X);
• Coh.TwoTermPerfectDeterminantData F is explicit presentation data for a degree-zero coherent sheaf, restricted to a two-term finite locally free resolution.

Only the valid forgetful direction involving the presentation data is proved here: a two-term resolution gives an absolute perfect object, which then maps to the defining essential image of perfect objects in Dqc(X). Relative perfection depends on the base morphism and is not identified with absolute perfection without an additional geometric theorem.

theorem AlgebraicGeometry.schemeRelativePerfect_le_schemePseudoCoherent {X S : Scheme} (p : X ⟶ S) : schemeRelativePerfect p ≤ schemePseudoCoherent X

Relative perfection always includes pseudo-coherence. It does not, by itself, identify the object with the absolute perfect locus in Dqc(X).

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.derivedObject {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (_D : F.TwoTermPerfectDeterminantData) : DerivedCategory.SchemeCoherentDerivedCategory X

The degree-zero coherent-derived object represented by the target sheaf of a two-term finite locally free resolution.

Equations

• _D.derivedObject = (DerivedCategory.singleFunctor (AlgebraicGeometry.Coh X) 0).obj F

theorem AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.derivedObject_mem_schemePerfect {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : DerivedCategory.schemePerfect X D.derivedObject

A two-term finite locally free resolution places its degree-zero target in the absolute perfect thick envelope.

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.toSchemePerfectDerivedCategory {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : DerivedCategory.SchemePerfectDerivedCategory X

Forget two-term presentation data to the canonical absolute perfect derived category.

Equations

• D.toSchemePerfectDerivedCategory = { obj := D.derivedObject, property := ⋯ }

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.toDqc {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory X

The absolute perfect object supplied by a two-term resolution, mapped to the honest Dqc(X) locus.

Equations

• D.toDqc = (AlgebraicGeometry.DerivedCategory.Dqc.SchemeBoundedCoherentDqcCategory.ι X).obj ((AlgebraicGeometry.DerivedCategory.Dqc.perfectDerivedToDqc X).obj D.toSchemePerfectDerivedCategory)

theorem AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.toDqc_mem_schemePerfectInDqc {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : DerivedCategory.Dqc.schemePerfectInDqc X D.toDqc

The Dqc(X) object obtained from a two-term finite locally free resolution belongs to the canonical absolute-perfect essential image.