structure CYHyp.SmoothCompleteCurve' : Type

Auxiliary record of numerical invariants of a smooth complete curve: its genus g and canonical degree degK.

• g : ℤ
• degK : ℤ

def CYHyp.mkCurve' (g : ℕ) : SmoothCompleteCurve'

Build a SmoothCompleteCurve' of genus g with canonical degree 2g - 2.

@[simp]

theorem CYHyp.mkCurve'_degK (g : ℕ) : (mkCurve' g).degK = 2 * ↑g - 2

mkCurve' g has canonical degree 2g - 2.

theorem CYHyp.mkCurve'_elliptic : (mkCurve' 1).degK = 0

An elliptic curve (genus 1) has canonical degree 0.

def CYHyp.genus_plane_curve (d : ℕ) : ℕ

Arithmetic genus of a smooth plane curve of degree d: (d-1)(d-2)/2.

theorem CYHyp.genus_plane_curve_eq_adjunction_genus (d : ℕ) (hd : 2 ≤ d) : ↑(genus_plane_curve d) = (↑d - 1) * (↑d - 2) / 2

Compatibility between the natural-number and integer formulations of the plane-curve genus.

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

Adjunction-derived identity for plane curves: with g = (d-1)(d-2)/2, one has 2g - 2 = d(d - 3).

structure SmoothProjectiveHypersurface : Type

A smooth projective hypersurface in P^n of degree d, with n, d ≥ 1.

• n : ℕ
• d : ℕ
• hn : 1 ≤ self.n
• hd : 1 ≤ self.d

def SmoothProjectiveHypersurface.canonicalTwist (Y : SmoothProjectiveHypersurface) : ℤ

Canonical twist d - n - 1 of a smooth hypersurface Y ⊂ P^n of degree d (so K_Y = O_Y(d - n - 1) by the adjunction formula).

theorem SmoothProjectiveHypersurface.adjunction_formula_hypersurface (Y : SmoothProjectiveHypersurface) : Y.canonicalTwist = ↑Y.d - ↑Y.n - 1

Adjunction formula for a hypersurface: canonicalTwist = d - n - 1.

theorem SmoothProjectiveHypersurface.canonicalTwist_from_euler (Y : SmoothProjectiveHypersurface) : Y.canonicalTwist = -(↑Y.n + 1) + ↑Y.d

Rewriting of the canonical twist using the Euler sequence: K_Y = -(n + 1) + d.

theorem SmoothProjectiveHypersurface.adjunction_formula_from_euler_and_normal (Y : SmoothProjectiveHypersurface) : Y.canonicalTwist = -(↑Y.n + 1) + ↑Y.d

Combined Euler/normal-bundle derivation of the canonical twist.

def SmoothProjectiveHypersurface.degCanonical (Y : SmoothProjectiveHypersurface) : ℤ

Degree of the canonical bundle of Y: d · (d - n - 1).

theorem SmoothProjectiveHypersurface.degCanonical_eq (Y : SmoothProjectiveHypersurface) : Y.degCanonical = ↑Y.d * (↑Y.d - ↑Y.n - 1)

Definitional unfolding of degCanonical as d · (d - n - 1).

theorem SmoothProjectiveHypersurface.degCanonical_expand (Y : SmoothProjectiveHypersurface) : Y.degCanonical = ↑Y.d ^ 2 - ↑Y.d * (↑Y.n + 1)

Expanded polynomial form of the canonical degree: d² - d(n + 1).

def SmoothProjectiveHypersurface.isCalabiYau (Y : SmoothProjectiveHypersurface) : Prop

Calabi-Yau predicate for a hypersurface: d = n + 1, equivalent to trivial canonical bundle.

theorem SmoothProjectiveHypersurface.canonicalTwist_zero_iff_calabiYau (Y : SmoothProjectiveHypersurface) : Y.canonicalTwist = 0 ↔ Y.isCalabiYau

A hypersurface has zero canonical twist iff it is Calabi-Yau.

theorem SmoothProjectiveHypersurface.degCanonical_zero_of_calabiYau (Y : SmoothProjectiveHypersurface) (h : Y.isCalabiYau) : Y.degCanonical = 0

The canonical degree vanishes on a Calabi-Yau hypersurface.

theorem SmoothProjectiveHypersurface.calabiYau_of_degCanonical_zero (Y : SmoothProjectiveHypersurface) (h : Y.degCanonical = 0) : Y.isCalabiYau

Converse: a hypersurface with vanishing canonical degree is Calabi-Yau.

def SmoothProjectiveHypersurface.ellipticCurve : SmoothProjectiveHypersurface

The smooth cubic in P² (an elliptic curve) as a SmoothProjectiveHypersurface.

def SmoothProjectiveHypersurface.K3surface : SmoothProjectiveHypersurface

A smooth quartic in P³, i.e. a K3 surface, as a SmoothProjectiveHypersurface.

def SmoothProjectiveHypersurface.CY3fold : SmoothProjectiveHypersurface

A smooth quintic in P⁴, i.e. a Calabi-Yau threefold, as a SmoothProjectiveHypersurface.

theorem SmoothProjectiveHypersurface.ellipticCurve_isCalabiYau : ellipticCurve.isCalabiYau

The elliptic curve (n, d) = (2, 3) is Calabi-Yau.

theorem SmoothProjectiveHypersurface.K3surface_isCalabiYau : K3surface.isCalabiYau

The K3 surface (n, d) = (3, 4) is Calabi-Yau.

theorem SmoothProjectiveHypersurface.CY3fold_isCalabiYau : CY3fold.isCalabiYau

The quintic threefold (n, d) = (4, 5) is Calabi-Yau.

theorem SmoothProjectiveHypersurface.ellipticCurve_canonicalTwist : ellipticCurve.canonicalTwist = 0

The canonical twist of the elliptic curve is 0.

theorem SmoothProjectiveHypersurface.ellipticCurve_degCanonical_zero : ellipticCurve.degCanonical = 0

The canonical degree of the elliptic curve is 0.

theorem SmoothProjectiveHypersurface.K3surface_degCanonical_zero : K3surface.degCanonical = 0

The canonical degree of the K3 surface is 0.

theorem SmoothProjectiveHypersurface.calabiYau_general (n : ℕ) (hn : 1 ≤ n) : have Y := { n := n, d := n + 1, hn := hn, hd := ⋯ }; Y.canonicalTwist = 0

General Calabi-Yau result: a smooth degree-(n+1) hypersurface in P^n has trivial canonical twist.

theorem SmoothProjectiveHypersurface.degCanonical_plane_curve (d : ℕ) (hd : 1 ≤ d) : have Y := { n := 2, d := d, hn := ⋯, hd := hd }; Y.degCanonical = ↑d * (↑d - 3)

Plane curve canonical degree: a smooth plane curve of degree d has deg K = d(d - 3).

theorem SmoothProjectiveHypersurface.genus_from_adjunction (d : ℕ) (hd : 1 ≤ d) (g : ℤ) (hg : 2 * g - 2 = { n := 2, d := d, hn := ⋯, hd := hd }.degCanonical) : 2 * g = (↑d - 1) * (↑d - 2)

Genus from adjunction: if 2g - 2 equals the canonical degree of a smooth plane curve of degree d, then 2g = (d - 1)(d - 2).

theorem SmoothProjectiveHypersurface.degCanonical_line : { n := 2, d := 1, hn := ⋯, hd := ⋯ }.degCanonical = -2

A line in P² has canonical degree -2.

theorem SmoothProjectiveHypersurface.degCanonical_conic : { n := 2, d := 2, hn := ⋯, hd := ⋯ }.degCanonical = -2

A smooth conic in P² has canonical degree -2.

theorem SmoothProjectiveHypersurface.degCanonical_cubic : { n := 2, d := 3, hn := ⋯, hd := ⋯ }.degCanonical = 0

A smooth cubic in P² (an elliptic curve) has canonical degree 0.

theorem SmoothProjectiveHypersurface.degCanonical_quartic : { n := 2, d := 4, hn := ⋯, hd := ⋯ }.degCanonical = 4

A smooth plane quartic has canonical degree 4.

theorem SmoothProjectiveHypersurface.elliptic_degK_consistent : ellipticCurve.degCanonical = 0 ∧ (CYHyp.mkCurve' 1).degK = 0

Consistency check: both formulations agree that the elliptic curve has degK = 0.

theorem SmoothProjectiveHypersurface.plane_curve_degK_matches (d : ℕ) (hd : 2 ≤ d) : have Y := { n := 2, d := d, hn := ⋯, hd := ⋯ }; have g := CYHyp.genus_plane_curve d; (CYHyp.mkCurve' g).degK = Y.degCanonical

The plane-curve canonical degree computed from the genus matches the hypersurface formula.

def SmoothProjectiveHypersurface.degK_hypersurface (n d : ℤ) : ℤ

Canonical degree of a smooth degree-d hypersurface in P^n as a function of (n, d).

theorem SmoothProjectiveHypersurface.degK_hypersurface_formula (n d : ℤ) : degK_hypersurface n d = d * (d - (n + 1))

Unfolding the integer-formulated degK_hypersurface.

theorem SmoothProjectiveHypersurface.degCanonical_eq_degK_hypersurface (Y : SmoothProjectiveHypersurface) : Y.degCanonical = degK_hypersurface ↑Y.n ↑Y.d

The structured canonical degree agrees with the integer-valued degK_hypersurface formula.