Canonical sheaf data and the duality construction boundary

For a smooth variety of pure relative dimension n, the canonical sheaf is the determinant of the relative cotangent sheaf. This file packages that construction using DerivedAlgGeo's existing fixed-rank locally-free and determinant interfaces, and exposes its Picard and Cartier-divisor classes.

CanonicalSheafData retains explicit cotangent and determinant fields so callers may package a chosen model. The companion Canonical.Differentials module constructs the relative cotangent sheaf for varieties over a field, while Canonical.Descent carries the standard-smooth chart calculation through sheafification, proves fixed-rank local freeness, constructs the determinant line and its explicit tensor inverse, and supplies CanonicalSheafData.ofSmoothRelativeDifferentials. Mathlib's general relative-differentials construction for arbitrary morphisms of ringed spaces remains outside this variety-specific API.

Canonical.Derived constructs the derived-category object ω_X[n] from this package. Likewise, DualizingSheafComparison only compares a separately constructed candidate with the canonical sheaf; it does not assert that an arbitrary module sheaf is dualizing or postulate Serre duality as an axiom.

structure AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (n : ℕ) : Type (u + 1)

Explicit canonical-sheaf construction data on a smooth proper variety of pure dimension n.

The cotangent object and determinant descent are fields because the current scheme-sheaf API does not yet construct them. The relative-dimension certificate is the genuine Mathlib morphism property, not a numerical dimension assertion.

• smoothOfRelativeDimension : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))

  The structure morphism is smooth of pure relative dimension n.

• cotangent : X.Modules

  The chosen relative cotangent module sheaf.

• cotangentDeterminant : self.cotangent.DeterminantData

  Fixed-rank and determinant data for the chosen cotangent sheaf.

• cotangent_rank : self.cotangentDeterminant.rank = n

  Its locally free rank agrees with the geometric relative dimension.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.canonicalLineBundle {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : Scheme.Modules.LineBundleData X

The canonical line bundle, defined as the determinant of the cotangent sheaf.

Equations

• C.canonicalLineBundle = C.cotangentDeterminant.topExteriorPower

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.canonicalSheaf {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : X.Modules

The underlying canonical module sheaf ω_X.

Equations

• C.canonicalSheaf = C.canonicalLineBundle.line

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.antiCanonicalLineBundle {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : Scheme.Modules.LineBundleData X

The inverse, or anticanonical, line bundle.

Equations

• C.antiCanonicalLineBundle = C.canonicalLineBundle.dual

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.canonicalClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : Scheme.Modules.Pic X

The canonical Picard class [ω_X].

Equations

• C.canonicalClass = C.canonicalLineBundle.toPic

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.canonicalClassAdd {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : Additive (Scheme.Modules.Pic X)

The canonical class in additive notation.

Equations

• C.canonicalClassAdd = Additive.ofMul C.canonicalClass

@[simp]

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.antiCanonicalClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : C.antiCanonicalLineBundle.toPic = C.canonicalClass⁻¹

The anticanonical Picard class is the inverse of the canonical class.

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.determinant_rank {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) : C.cotangentDeterminant.rank = n

The chosen cotangent determinant has the recorded pure relative dimension.

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.canonicalClass_eq_of_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) {C' : CanonicalSheafData k X n} (e : C.canonicalSheaf ≅ C'.canonicalSheaf) : C.canonicalClass = C'.canonicalClass

Two canonical-sheaf packages with isomorphic line representatives define the same class.

structure AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.CanonicalDivisorData {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (C : CanonicalSheafData k X n) : Type u

An explicit Cartier representative of a canonical-sheaf package.

Existence is kept as data because the present Cartier-to-Picard API does not prove essential surjectivity for every line bundle.

• divisor : ↥X.CartierDivisor

  A Cartier divisor representing the canonical class.

• associatedSheafIso : Scheme.CartierDivisor.associatedSheaf self.divisor ≅ C.canonicalSheaf

  Its associated invertible sheaf is the canonical sheaf.

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.CanonicalDivisorData.toPic_eq_canonicalClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (C : CanonicalSheafData k X n) (D : C.CanonicalDivisorData) : Scheme.CartierDivisor.toPic D.divisor = C.canonicalClass

The associated Cartier divisor maps to the canonical Picard class.

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.CanonicalDivisorData.canonicalDivisorClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (C : CanonicalSheafData k X n) (D : C.CanonicalDivisorData) : Scheme.CartierDivisor.ClassGroup X

The canonical Cartier divisor class.

Equations

• AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.CanonicalDivisorData.canonicalDivisorClass C D = (AlgebraicGeometry.Scheme.CartierDivisor.toClass X) D.divisor

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.CanonicalDivisorData.classToPic_eq_canonicalClass {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k X] {n : ℕ} (C : CanonicalSheafData k X n) (D : C.CanonicalDivisorData) : Scheme.CartierDivisor.classToPic (Multiplicative.ofAdd (canonicalDivisorClass C D)) = C.canonicalClass

The Cartier class-to-Picard map sends the canonical divisor class to [ω_X].

structure AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.DualizingSheafComparison {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (C : CanonicalSheafData k X n) (dualizingCandidate : X.Modules) : Type u

Comparison data between a separately constructed dualizing-sheaf candidate and ω_X.

This structure deliberately contains no field claiming that dualizingCandidate is dualizing; that property must come from a comparison with the constructed canonical complex.

• iso : dualizingCandidate ≅ C.canonicalSheaf

  On a smooth pure-dimensional target, the candidate is identified with ω_X.

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.DualizingSheafComparison.candidateClass_eq {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} {C : CanonicalSheafData k X n} {D : X.Modules} (E : C.DualizingSheafComparison D) (L : Scheme.Modules.LineBundleData X) (hL : L.line ≅ D) : L.toPic = C.canonicalClass

A dualizing-candidate comparison determines the candidate's Picard class whenever it is equipped with line-bundle data.