The canonical dualizing complex

For canonical-sheaf data on a smooth proper variety of pure dimension n, this file constructs the coherent canonical sheaf and places it in cohomological degree n. Thus the dualizing complex used by the Serre interface is the actual derived-category object ω_X[n]; it is no longer a field supplied by downstream data.

The construction also records the geometric hypotheses supplied automatically by a smooth proper variety over a field, integrates degreewise finite-dimensional cohomology with the finite-cohomology package, and checks the shift on the zero-dimensional smooth proper point.

This is an object construction and shift convention, not a proof of Grothendieck duality. The derived RHom functor and its Serre-duality equivalence remain explicit realization data.

noncomputable def AlgebraicGeometry.SmoothProperVariety.finiteCohomology {k : Type u} [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] (D : Cohomology.FiniteDimensionalCohomology k X) : Cohomology.FiniteCohomology k X

Degreewise finite-dimensional cohomology on a smooth proper variety has the boundedness needed by the repository's FiniteCohomology interface.

Equations

• AlgebraicGeometry.SmoothProperVariety.finiteCohomology X D = D.toFiniteCohomology

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.SmoothProperVariety.point (k : Type u) [Field k] : Scheme

The smooth proper point over k: Spec k itself. It provides the zero-dimensional shift test below. Its structure morphism is the identity, recorded as the Scheme.Over instance instOverPoint.

Equations

• AlgebraicGeometry.SmoothProperVariety.point k = AlgebraicGeometry.Spec (CommRingCat.of k)

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.SmoothProperVariety.instOverPoint (k : Type u) [Field k] : (point k).Over (point k)

The point lies over itself by the identity.

Equations

• AlgebraicGeometry.SmoothProperVariety.instOverPoint k = { hom := CategoryTheory.CategoryStruct.id (AlgebraicGeometry.SmoothProperVariety.point k) }

instance AlgebraicGeometry.SmoothProperVariety.isSmoothProperVariety_point (k : Type u) [Field k] : IsSmoothProperVariety k (point k)

The point is a smooth proper variety over k: every constituent is a property of the identity morphism or of the spectrum of a field.

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.canonicalCohObject {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (K : CanonicalSheafData k X n) : Coh X

The canonical line bundle as an object of the coherent-sheaf category. Coherence follows automatically from invertibility.

Equations

• K.canonicalCohObject = { obj := K.canonicalSheaf, property := ⋯ }

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.dualizingComplex {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (K : CanonicalSheafData k X n) : DerivedCategory.SchemeCoherentDerivedCategory X

The canonical dualizing-complex candidate ω_X[n] in the coherent derived category.

Equations

• K.dualizingComplex = (DerivedCategory.singleFunctor (AlgebraicGeometry.Coh X) ↑n).obj K.canonicalCohObject

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

The defining identification of the constructed dualizing complex with ω_X[n].

Equations

• K.dualizingComplexIso = CategoryTheory.Iso.refl K.dualizingComplex

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.pointCanonicalSheafData (k : Type u) [Field k] : CanonicalSheafData k (point k) 0

Explicit dimension-zero canonical-sheaf data on the smooth proper point. Its cotangent model is the free sheaf on no generators and its determinant is the structure line.

Equations

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

@[simp]

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.pointCanonicalSheafData_canonicalSheaf (k : Type u) [Field k] : (pointCanonicalSheafData k).canonicalSheaf = SheafOfModules.unit (point k).ringCatSheaf

On the smooth proper point, the chosen canonical sheaf is the structure sheaf.

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.pointDualizingComplexIso (k : Type u) [Field k] : (pointCanonicalSheafData k).dualizingComplex ≅ (DerivedCategory.singleFunctor (Coh (point k)) 0).obj (pointCanonicalSheafData k).canonicalCohObject

Shift sanity check: the dualizing complex of the smooth proper point is the canonical object in degree zero.

Equations

• AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.pointDualizingComplexIso k = (AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.pointCanonicalSheafData k).dualizingComplexIso