def CanonicalSheafCurves.CurveWitness (g : ℤ) : Prop

Existence witness for a smooth complete curve of genus g: a Dedekind k-algebra A whose Kähler differential module has rank g.

theorem CanonicalSheafCurves.curveWitness_zero : CurveWitness 0

The rational numbers ℚ (as a ℚ-algebra) witness the genus-0 case of CurveWitness.

theorem CanonicalSheafCurves.curveWitness_of_nat (g : ℕ) : CurveWitness ↑g

For every natural number g, there exists a smooth complete curve of genus g.

structure CanonicalSheafCurves.SmoothCompleteCurve : Type

Numerical data of a smooth complete curve: genus g, canonical degree degK, Euler characteristic homomorphism χ : ℤ × ℤ →+ ℤ (taking (rank, degree) to χ(F)), satisfying the structure-sheaf and skyscraper normalisations plus existence of an underlying Dedekind witness.

• g : ℤ
• χ : ℤ × ℤ →+ ℤ
• degK : ℤ
• hg_nonneg : 0 ≤ self.g
• hχ_struct : self.χ (1, 0) = 1 - self.g
• hχ_sky : self.χ (0, 1) = 1
• hwf : CurveWitness self.g

theorem CanonicalSheafCurves.serre_duality_chi_canonical (C : SmoothCompleteCurve) : C.χ (1, C.degK) = C.g - 1

Serre duality at the level of Euler characteristics: χ(K_C) = g - 1.

theorem CanonicalSheafCurves.SmoothCompleteCurve.hχ_canonical (C : SmoothCompleteCurve) : C.χ (1, C.degK) = C.g - 1

Convenience projection: the canonical-sheaf Euler characteristic of C is g - 1.

def CanonicalSheafCurves.canonicalSheafClass (C : SmoothCompleteCurve) : ℤ × ℤ

Class of the canonical sheaf of C in the Picard-style invariant ℤ × ℤ of (rank, degree): K_C is a line bundle (rank 1) of degree degK.

def CanonicalSheafCurves.curveGenusOfSmooth (C : SmoothCompleteCurve) : ℤ

Genus of the smooth complete curve C, as an integer.

def CanonicalSheafCurves.canonicalDeg (C : SmoothCompleteCurve) : ℤ

Degree of the canonical divisor of C.

theorem CanonicalSheafCurves.chi_eq_rr (C : SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d) = d - r * (C.g - 1)

Riemann-Roch on C: χ(F) = d - r(g - 1) for a sheaf of rank r and degree d.

theorem CanonicalSheafCurves.chi_canonical_by_rr (C : SmoothCompleteCurve) : C.χ (1, C.degK) = C.degK + 1 - C.g

Specialisation of Riemann-Roch to the canonical class: χ(K_C) = deg K_C + 1 - g.

theorem CanonicalSheafCurves.SmoothCompleteCurve.serre_duality (C : SmoothCompleteCurve) : C.χ (1, C.degK) = C.g - 1

Serre duality on C in the form χ(K_C) = g - 1.

theorem CanonicalSheafCurves.serre_duality_chi (C : SmoothCompleteCurve) : C.χ (1, 0) + C.χ (1, C.degK) = 0

Euler-characteristic form of Serre duality: χ(O_C) + χ(K_C) = 0.

theorem CanonicalSheafCurves.chi_canonical (C : SmoothCompleteCurve) : C.χ (1, C.degK) = C.g - 1

Restatement of Serre duality: χ(K_C) = g - 1.

theorem CanonicalSheafCurves.deg_canonical_eq_2g_sub_2 (C : SmoothCompleteCurve) : C.degK = 2 * C.g - 2

Degree of the canonical divisor: deg K_C = 2g - 2 (combining Riemann-Roch and Serre duality).

theorem CanonicalSheafCurves.deg_canonical_eq_2_mul_g_sub_1 (C : SmoothCompleteCurve) : C.degK = 2 * (C.g - 1)

Factored form of the canonical degree: deg K_C = 2(g - 1).

theorem CanonicalSheafCurves.deg_canonical_eq_neg2_chi_O (C : SmoothCompleteCurve) : C.degK = -2 * C.χ (1, 0)

Expression of the canonical degree via the structure-sheaf Euler characteristic: deg K_C = -2 χ(O_C).

theorem CanonicalSheafCurves.deg_canonical_P1_from_formula (C : SmoothCompleteCurve) : C.g = 0 → C.degK = -2

Specialisation to genus 0 (P^1): deg K_{P^1} = -2.

theorem CanonicalSheafCurves.deg_canonical_P1_check : 2 * 0 - 2 = -2

Numerical sanity check: 2·0 - 2 = -2.

theorem CanonicalSheafCurves.deg_canonical_elliptic (C : SmoothCompleteCurve) : C.g = 1 → C.degK = 0

Specialisation to genus 1 (elliptic curves): deg K_E = 0.

theorem CanonicalSheafCurves.deg_canonical_elliptic_check : 2 * 1 - 2 = 0

Numerical sanity check: 2·1 - 2 = 0.

theorem CanonicalSheafCurves.deg_canonical_genus2 (C : SmoothCompleteCurve) : C.g = 2 → C.degK = 2

Specialisation to genus 2: deg K_C = 2.

theorem CanonicalSheafCurves.deg_canonical_genus2_check : 2 * 2 - 2 = 2

Numerical sanity check: 2·2 - 2 = 2.

theorem CanonicalSheafCurves.chi_canonical_from_degree (C : SmoothCompleteCurve) : C.degK + 1 - C.g = C.g - 1

Identity deg K_C + 1 - g = g - 1, equivalent to Serre duality at the level of degrees.

theorem CanonicalSheafCurves.chi_symmetry (C : SmoothCompleteCurve) : 1 - C.g + (C.g - 1) = 0

Algebraic symmetry (1 - g) + (g - 1) = 0 reflecting Serre duality on Euler characteristics.

theorem CanonicalSheafCurves.canonical_positive_degree (C : SmoothCompleteCurve) (hg : C.g ≥ 2) : C.degK > 0

Positivity of the canonical degree for genus g ≥ 2.

theorem CanonicalSheafCurves.canonical_negative_degree_P1 (C : SmoothCompleteCurve) (hg : C.g = 0) : C.degK < 0

Negativity of the canonical degree for genus 0 curves (i.e. P^1).

theorem CanonicalSheafCurves.canonical_zero_degree_elliptic (C : SmoothCompleteCurve) (hg : C.g = 1) : C.degK = 0

Vanishing of the canonical degree for elliptic curves (g = 1).

def CanonicalSheafCurves.mkCurve (g : ℕ) (hwf : CurveWitness ↑g := ⋯) : SmoothCompleteCurve

Construct a SmoothCompleteCurve of genus g : ℕ using the Riemann-Roch Euler characteristic homomorphism and the canonical degree formula 2g - 2.

@[simp]

theorem CanonicalSheafCurves.mkCurve_degK (g : ℕ) : (mkCurve g).degK = 2 * ↑g - 2

The canonical degree of mkCurve g is 2g - 2 by definition.

@[simp]

theorem CanonicalSheafCurves.mkCurve_genus (g : ℕ) : (mkCurve g).g = ↑g

The genus of mkCurve g is g by definition.

theorem CanonicalSheafCurves.mkCurve_P1 : (mkCurve 0).degK = -2

Canonical degree for mkCurve 0 (the projective line): -2.

theorem CanonicalSheafCurves.mkCurve_elliptic : (mkCurve 1).degK = 0

Canonical degree for mkCurve 1 (elliptic curves): 0.

theorem CanonicalSheafCurves.mkCurve_genus2 : (mkCurve 2).degK = 2

Canonical degree for mkCurve 2 (genus-2 curves): 2.

theorem CanonicalSheafCurves.genus_eq_dim_kahler (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (C : SmoothCompleteCurve) (hg : C.g = ↑(RiemannRochCurves.curveGenus k A)) : C.degK = 2 * ↑(RiemannRochCurves.curveGenus k A) - 2

If the abstract genus of C equals the Dedekind-domain genus curveGenus k A, then the canonical degree formula 2g - 2 agrees with the algebraic invariant.

theorem CanonicalSheafCurves.adjunction_genus_plane_curve (d : ℤ) : d * (d - 3) + 2 = (d - 1) * (d - 2)

Adjunction identity for a plane curve of degree d: d(d - 3) + 2 = (d - 1)(d - 2). This encodes 2g - 2 = d(d - 3) and g = (d - 1)(d - 2)/2.

theorem CanonicalSheafCurves.adjunction_genus_plane_curve_degK (d : ℤ) (_hd : 0 ≤ d) : have g := (d - 1) * (d - 2) / 2; 2 * g - 2 = d * (d - 3)

Canonical-degree form of the adjunction formula on a plane curve of degree d: 2g - 2 = d(d - 3), where g = (d - 1)(d - 2)/2.

theorem CanonicalSheafCurves.canonical_P1_consistent_euler : (mkCurve 0).degK = -(1 + 1)

Consistency with the Euler-sequence calculation on P^1: deg K_{P^1} = -(1 + 1) = -2.

theorem CanonicalSheafCurves.elliptic_from_adjunction : (mkCurve 1).degK = 3 * (3 - 3)

Adjunction-formula consistency for the smooth plane cubic (d = 3): deg K = 3·(3 - 3) = 0, matching mkCurve 1.