Lax Lean Archive

The Kodaira trichotomy of a hypersurface as a statement about binomial coefficients

Lax894236.GeometricGenus · concepts/Lax894236/GeometricGenus.lean · lax-894236

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    By Griffiths' description of the Hodge numbers of hypersurfaces, the geometric genus of a smooth hypersurface of degree dd and dimension nn is hn,0(Xdn)=(d−1n+1)h^{n,0}(X_d^n) = \binom{d-1}{n+1}. Writing m=d−1m = d - 1, this concept defines pgmn=C(m,n+1)pg m n = C(m, n+1) and states the classification by the sign of the canonical bundle as facts about binomial coefficients:

    • Fano: hn,0=0h^{n,0} = 0 if and only if d≤n+1d \le n+1;
    • Calabi–Yau: hn,0=1h^{n,0} = 1 if and only if d=n+2d = n+2;
    • general type: d≥n+3d \ge n+3 implies hn,0≥2h^{n,0} \ge 2.

    For plane curves (n=1n = 1) the same formula is the genus–degree formula g=(d−12)=(d−1)(d−2)2g = \binom{d-1}{2} = \tfrac{(d-1)(d-2)}{2}, which is the last statement.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 genus_degree proven

    2 pg_eq_one_iff proven

    3 pg_eq_zero_iff proven

    4 two_le_pg proven

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Choose.Basic
    2
    3/-!
    4---
    5title: The Kodaira trichotomy of a hypersurface as a statement about binomial coefficients
    6type: theorem
    7---
    8By Griffiths' description of the Hodge numbers of hypersurfaces, the geometric
    9genus of a smooth hypersurface of degree dd and dimension nn is
    10hn,0(Xdn)=(d−1n+1)h^{n,0}(X_d^n) = \binom{d-1}{n+1}. Writing m=d−1m = d - 1, this concept defines
    11`pg m n = C(m, n+1)` and states the classification by the sign of the canonical
    12bundle as facts about binomial coefficients:
    13
    14- Fano: hn,0=0h^{n,0} = 0 if and only if d≤n+1d \le n+1;
    15- Calabi–Yau: hn,0=1h^{n,0} = 1 if and only if d=n+2d = n+2;
    16- general type: d≥n+3d \ge n+3 implies hn,0≥2h^{n,0} \ge 2.
    17
    18For plane curves (n=1n = 1) the same formula is the genus–degree formula
    19g=(d−12)=(d−1)(d−2)2g = \binom{d-1}{2} = \tfrac{(d-1)(d-2)}{2}, which is the last statement.
    20-/
    21
    22namespace Lax894236.GeometricGenus
    23
    24/-- The geometric genus `h^{n,0}` of a smooth hypersurface of degree `m + 1` and
    25dimension `n`, by Griffiths' formula: `C(m, n+1)`. -/
    26def pg (m n : ℕ) : ℕ := m.choose (n + 1)
    27
    28/-- Fano: the geometric genus vanishes if and only if `d ≤ n + 1`. -/
    29axiom pg_eq_zero_iff (m n : ℕ) : pg m n = 0 ↔ m < n + 1
    30
    31/-- Calabi–Yau: the geometric genus is `1` if and only if `d = n + 2`. -/
    32axiom pg_eq_one_iff (m n : ℕ) : pg m n = 1 ↔ m = n + 1
    33
    34/-- General type: for `d ≥ n + 3` the geometric genus is at least `2`. -/
    35axiom two_le_pg (m n : ℕ) (h : n + 2 ≤ m) : 2 ≤ pg m n
    36
    37/-- The genus–degree formula for smooth plane curves of degree `m + 1`. -/
    38axiom genus_degree (m : ℕ) : pg m 1 = m * (m - 1) / 2
    39
    40end Lax894236.GeometricGenus
    41
    Show ProofShow ProofShow ProofShow Proof
    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…