Serre duality: explicit derived and cohomological interfaces

For a smooth proper variety of pure dimension n, Serre duality should identify

H^i(X, F)ᵛ ≃ Ext^(n-i)(F, ω_X).

The pinned Mathlib has derived categories and Ext, but no derived global-sections functor into D(k), coherent RHom, or Grothendieck-duality theorem. Accordingly this file packages the exact remaining realization data and derives the finite-dimensional pairing and Euler-characteristic consequences.

CanonicalSheafData.dualizingComplex constructs the object ω_X[n] rather than accepting it as a field. DerivedStatement records the functors and duality isomorphism still missing upstream. Data records the cohomology-level realization against Mathlib's actual Abelian.Ext groups. LocallyFreeSpecialization identifies those Ext groups with the cohomology of Fᵛ ⊗ ω_X; from these inputs this file proves the usual dimension and Euler symmetries.

structure AlgebraicGeometry.Duality.Serre.DerivedStatement {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (K : SmoothProperVariety.CanonicalSheafData k X n) : Type (u + 2)

The derived-category form of the missing Serre-duality construction.

The functor linearDualShift is the exact derived lift of algebraic linear duality followed by the shift [-n]. It is now constructed rather than supplied as an arbitrary field. The only remaining categorical input on this side is the explicit comparison (DerivedCategory C)ᵒᵖ ≃ DerivedCategory (Cᵒᵖ), which the pinned Mathlib does not yet bundle. The dualizing object itself is the constructed K.dualizingComplex = ω_X[n].

• rGlobalSections : CategoryTheory.Functor (DerivedCategory.SchemeCoherentDerivedCategory X) (DerivedCategory (ModuleCat k))

  Derived global sections with its base-field-linear target.

• rHomDualizing : CategoryTheory.Functor (DerivedCategory.SchemeCoherentDerivedCategory X)ᵒᵖ (DerivedCategory (ModuleCat k))

  Derived Hom into the chosen dualizing object.

• oppositeDerived : CategoryTheory.DerivedCategory.OppositeComparison (ModuleCat k)

  Comparison between the opposite derived category and the derived category of the opposite module category.

• dualityIso : self.rHomDualizing ≅ self.rGlobalSections.op.comp (ModuleCat.derivedLinearDualShift k self.oppositeDerived (-↑n))

  The derived Serre-duality isomorphism.

noncomputable def AlgebraicGeometry.Duality.Serre.DerivedStatement.linearDualShift {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} (S : DerivedStatement K) : CategoryTheory.Functor (DerivedCategory (ModuleCat k))ᵒᵖ (DerivedCategory (ModuleCat k))

The constructed derived linear-dual functor followed by the dimension shift.

Equations

• S.linearDualShift = ModuleCat.derivedLinearDualShift k S.oppositeDerived (-↑n)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Duality.Serre.DerivedStatement.dualizingObject {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} : DerivedStatement K → DerivedCategory.SchemeCoherentDerivedCategory X

The dualizing object associated to a derived Serre statement is the constructed canonical complex ω_X[n].

Equations

• x✝.dualizingObject = K.dualizingComplex

noncomputable def AlgebraicGeometry.Duality.Serre.DerivedStatement.canonicalShiftIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} : DerivedStatement K → (K.dualizingComplex ≅ (DerivedCategory.singleFunctor (Coh X) ↑n).obj K.canonicalCohObject)

The canonical shift identification attached to every derived Serre statement.

Equations

• x✝.canonicalShiftIso = K.dualizingComplexIso

theorem AlgebraicGeometry.Duality.Serre.instHasExtCoh {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] : CategoryTheory.HasExt (Coh X)

structure AlgebraicGeometry.Duality.Serre.Data {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (K : SmoothProperVariety.CanonicalSheafData k X n) (D : Cohomology.FiniteCohomology k X) : Type (u + 2)

Explicit coherent Serre-duality data relative to a finite-cohomology realization.

extSpace is a linear lift of Mathlib's additive Abelian.Ext group, just as FiniteCohomology.moduleH is a linear lift of Sheaf.H. The comparison prevents the field structure from being an unrelated replacement. Perfection is carried by the linear equivalence duality; it is not asserted as a proposition with no map.

• derived : DerivedStatement K

  The derived-category statement from which this realization is intended to be extracted.

• extSpace : Coh X → ℕ → ModuleCat k

  A base-field-linear realization of Ext^j(F, ω_X).

• extComparison (F : Coh X) (j : ℕ) : (CategoryTheory.forget₂ (ModuleCat k) AddCommGrpCat).obj (self.extSpace F j) ≅ AddCommGrpCat.of (CategoryTheory.Abelian.Ext F K.canonicalCohObject j)

  Forgetting scalars recovers Mathlib's actual Ext group.

• extFinite (F : Coh X) (j : ℕ) : Module.Finite k ↑(self.extSpace F j)

  The Ext spaces are finite-dimensional.

• duality (F : Coh X) (i : ℕ) (_hi : i ≤ n) : Module.Dual k ↑((D.moduleH i).obj F) ≃ₗ[k] ↑(self.extSpace F (n - i))

  Perfect coherent Serre duality in every degree in the geometric range.

• vanishesAboveDimension (F : Coh X) (i : ℕ) : n < i → Subsingleton ↑((D.moduleH i).obj F)

  Cohomology above the relative dimension vanishes.

noncomputable def AlgebraicGeometry.Duality.Serre.Data.coherentDualityEquiv {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (F : Coh X) (i : ℕ) (hi : i ≤ n) : Module.Dual k ↑((D.moduleH i).obj F) ≃ₗ[k] ↑(S.extSpace F (n - i))

The coherent cohomology-level Serre-duality equivalence in the geometric range.

Equations

• S.coherentDualityEquiv F i hi = S.duality F i hi

def AlgebraicGeometry.Duality.Serre.Data.pairing {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (F : Coh X) (i : ℕ) (hi : i ≤ n) : ↑((D.moduleH i).obj F) →ₗ[k] ↑(S.extSpace F (n - i)) →ₗ[k] k

The perfect pairing H^i(X,F) × Ext^(n-i)(F,ω_X) → k extracted from duality.

Equations

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

@[simp]

theorem AlgebraicGeometry.Duality.Serre.Data.pairing_apply {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (F : Coh X) (i : ℕ) (hi : i ≤ n) (x : ↑((D.moduleH i).obj F)) (y : ↑(S.extSpace F (n - i))) : ((S.pairing F i hi) x) y = ((S.duality F i hi).symm y) x

instance AlgebraicGeometry.Duality.Serre.Data.pairing_isPerfPair {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (F : Coh X) (i : ℕ) (hi : i ≤ n) : (S.pairing F i hi).IsPerfPair

The displayed coherent Serre pairing is perfect in Mathlib's standard sense: both induced maps to the opposite dual space are bijective.

theorem AlgebraicGeometry.Duality.Serre.Data.dimension_eq_ext {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (F : Coh X) (i : ℕ) (hi : i ≤ n) : D.dimension F i = Module.finrank k ↑(S.extSpace F (n - i))

Perfection gives equality of the cohomology and complementary Ext dimensions.

structure AlgebraicGeometry.Duality.Serre.Data.LocallyFreeSpecialization {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (F : Coh X) : Type (u + 1)

A locally free specialization identifies Ext with the cohomology of Fᵛ ⊗ ω_X. The dual twist is explicit because the present sheaf API does not yet construct internal Hom or prove its coherence automatically.

• rank : ℕ

  A fixed finite locally free certificate for F.

• locallyFree : F.obj.FiniteLocallyFreeData self.rank
• dualCanonicalTwist : Coh X

  The coherent sheaf representing Fᵛ ⊗ ω_X.

• extToCohomology (j : ℕ) : ↑(S.extSpace F j) ≃ₗ[k] ↑((D.moduleH j).obj self.dualCanonicalTwist)

  Ext^j(F,ω_X) is the jth cohomology of the dual canonical twist.

noncomputable def AlgebraicGeometry.Duality.Serre.Data.LocallyFreeSpecialization.cohomologyDualityEquiv {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} {S : Data K D} {F : Coh X} (L : S.LocallyFreeSpecialization F) (i : ℕ) (hi : i ≤ n) : Module.Dual k ↑((D.moduleH i).obj F) ≃ₗ[k] ↑((D.moduleH (n - i)).obj L.dualCanonicalTwist)

For a finite locally-free sheaf, coherent Serre duality becomes H^i(X,F)ᵛ ≃ H^(n-i)(X,Fᵛ ⊗ ω_X).

Equations

• L.cohomologyDualityEquiv i hi = (S.coherentDualityEquiv F i hi).trans (L.extToCohomology (n - i))

theorem AlgebraicGeometry.Duality.Serre.Data.LocallyFreeSpecialization.dimension_symmetry {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} {S : Data K D} {F : Coh X} (L : S.LocallyFreeSpecialization F) (i : ℕ) (hi : i ≤ n) : D.dimension F i = D.dimension L.dualCanonicalTwist (n - i)

The cohomology dimensions of a locally free sheaf are reflected across the dimension.

theorem AlgebraicGeometry.Duality.Serre.Data.LocallyFreeSpecialization.eulerCharacteristic_eq_sum_dimension {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) (G : Coh X) : D.eulerCharacteristic G = ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(D.dimension G i)

The Euler characteristic may be summed exactly through the geometric dimension.

theorem AlgebraicGeometry.Duality.Serre.Data.LocallyFreeSpecialization.eulerCharacteristic_symmetry {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} {S : Data K D} {F : Coh X} (L : S.LocallyFreeSpecialization F) : D.eulerCharacteristic F = (-1) ^ n * D.eulerCharacteristic L.dualCanonicalTwist

Euler-characteristic symmetry for the locally free specialization: χ(F) = (-1)^n χ(Fᵛ ⊗ ω_X).

This is the sign convention needed downstream; in dimension two the sign is positive.

theorem AlgebraicGeometry.Duality.Serre.Data.LocallyFreeSpecialization.surface_eulerCharacteristic_symmetry {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} {S : Data K D} {F : Coh X} (L : S.LocallyFreeSpecialization F) (hn : n = 2) : D.eulerCharacteristic F = D.eulerCharacteristic L.dualCanonicalTwist

On a surface, Serre duality preserves Euler characteristic.

structure AlgebraicGeometry.Duality.Serre.Data.SurfacePicardSymmetry {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (I : IntersectionTheory.Number.IntersectionContext D C 2) (canonicalClass : Scheme.Modules.Pic X) : Prop

Picard-level Euler symmetry supplied by locally free Serre duality on a surface.

This small interface is the exact #40 output used by geometric surface Riemann--Roch. Its field is a theorem produced by the locally free specialization once line-bundle representatives and their dual canonical twists are identified in the Picard group.

• symmetry (L : Scheme.Modules.Pic X) : I.eulerPic L = I.eulerPic (canonicalClass * L⁻¹)

structure AlgebraicGeometry.Duality.Serre.Data.SurfaceLineBundleFamily {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) {C : D.LinearConnectingSystem} (I : IntersectionTheory.Number.IntersectionContext D C 2) (canonicalClass : Scheme.Modules.Pic X) : Type (u + 1)

Geometric line-bundle representatives realizing the Picard Euler function and their locally free Serre-dual twists.

• dimension_eq_two : n = 2

  The geometric relative dimension is two.

• representative : Scheme.Modules.Pic X → Coh X

  A coherent representative of each Picard class.

• specialization (L : Scheme.Modules.Pic X) : S.LocallyFreeSpecialization (self.representative L)

  Locally free Serre duality for every representative.

• representativeEuler (L : Scheme.Modules.Pic X) : D.eulerCharacteristic (self.representative L) = I.eulerPic L

  The representative realizes the intrinsic Picard Euler value.

• dualEuler (L : Scheme.Modules.Pic X) : D.eulerCharacteristic (self.specialization L).dualCanonicalTwist = I.eulerPic (canonicalClass * L⁻¹)

  Its dual canonical twist realizes K_X ⊗ L⁻¹.

theorem AlgebraicGeometry.Duality.Serre.Data.SurfaceLineBundleFamily.toSurfacePicardSymmetry {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} {K : SmoothProperVariety.CanonicalSheafData k X n} {D : Cohomology.FiniteCohomology k X} (S : Data K D) {C : D.LinearConnectingSystem} {I : IntersectionTheory.Number.IntersectionContext D C 2} {canonicalClass : Scheme.Modules.Pic X} (P : S.SurfaceLineBundleFamily I canonicalClass) : SurfacePicardSymmetry I canonicalClass

Locally free Serre duality for the chosen representatives proves Picard Euler symmetry.

theorem AlgebraicGeometry.Duality.Serre.Data.SurfacePicardSymmetry.canonical {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {I : IntersectionTheory.Number.IntersectionContext D C 2} {canonicalClass : Scheme.Modules.Pic X} (P : SurfacePicardSymmetry I canonicalClass) : I.eulerPic canonicalClass = I.eulerPic 1

The trivial line bundle and the canonical bundle have the same Euler characteristic.

theorem AlgebraicGeometry.Duality.Serre.Data.SurfacePicardSymmetry.k3 {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {I : IntersectionTheory.Number.IntersectionContext D C 2} {canonicalClass : Scheme.Modules.Pic X} (P : SurfacePicardSymmetry I canonicalClass) (hK : canonicalClass = 1) (L : Scheme.Modules.Pic X) : I.eulerPic L = I.eulerPic L⁻¹

K3 sign check: when the canonical class is trivial, χ(L) = χ(L⁻¹).