Parity of the Euler characteristic in odd dimension, and integrality for surfaces

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

proven

Loading review…

Sign in with ORCID

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

    Write the Euler characteristic of the smooth hypersurface XdnX_d^n in its binomial form, χn(d)=j=1n+1(1)j+1(n+2j+1)dj\chi_n(d) = \sum_{j=1}^{n+1} (-1)^{j+1}\binom{n+2}{j+1} d^j (the polynomial of EulerCharacteristicEulerCharacteristic divided by dd). Its coefficients are not all even, so evenness of χn(d)\chi_n(d) is not a polynomial identity; it is a parity fact.

    The first statement: for every odd dimension nn and every integer dd, χn(d)\chi_n(d) is even. For threefolds this is what makes the mirror-symmetry formula h2,1=b3/2h3,0h^{2,1} = b_3/2 - h^{3,0} with b3=4χb_3 = 4 - \chi an integer for every degree; the second statement is that instance.

    The remaining two statements concern surfaces in P3\mathbb{P}^3, where the literature gives χ=d34d2+6d\chi = d^3 - 4d^2 + 6d, h2,0=(d13)h^{2,0} = \binom{d-1}{3} and h1,1=2d332d2+7d3h^{1,1} = \tfrac{2d^3}{3} - 2d^2 + \tfrac{7d}{3}. The third statement is that h1,1h^{1,1} is an integer for every dd, i.e. 32d36d2+7d3 \mid 2d^3 - 6d^2 + 7d; the fourth is that the three formulas satisfy the Betti relation of a simply connected surface, χ=2+2h2,0+h1,1\chi = 2 + 2h^{2,0} + h^{1,1}, as a polynomial identity in dd (multiplied by 33 and with 6(d13)=(d1)(d2)(d3)6\binom{d-1}{3} = (d-1)(d-2)(d-3)).

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

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

    1 betti_relation proven

    2 three_dvd_h11Num proven

    3 two_dvd_b3 proven

    4 two_dvd_chiBinom_of_odd proven

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    2import Mathlib.Algebra.Group.Even
    3import Mathlib.Algebra.Ring.Parity
    4import Mathlib.Data.Nat.Choose.Basic
    5import Mathlib.Order.Interval.Finset.Nat
    6
    7/-!
    8---
    9title: Parity of the Euler characteristic in odd dimension, and integrality for surfaces
    10type: theorem
    11---
    12Write the Euler characteristic of the smooth hypersurface XdnX_d^n in its binomial
    13form, χn(d)=j=1n+1(1)j+1(n+2j+1)dj\chi_n(d) = \sum_{j=1}^{n+1} (-1)^{j+1}\binom{n+2}{j+1} d^j (the polynomial
    14of `EulerCharacteristic` divided by dd). Its coefficients are not all even, so
    15evenness of χn(d)\chi_n(d) is not a polynomial identity; it is a parity fact.
    16
    17The first statement: for every odd dimension nn and every integer dd,
    18χn(d)\chi_n(d) is even. For threefolds this is what makes the mirror-symmetry
    19formula h2,1=b3/2h3,0h^{2,1} = b_3/2 - h^{3,0} with b3=4χb_3 = 4 - \chi an integer for every
    20degree; the second statement is that instance.
    21
    22The remaining two statements concern surfaces in P3\mathbb{P}^3, where the
    23literature gives χ=d34d2+6d\chi = d^3 - 4d^2 + 6d, h2,0=(d13)h^{2,0} = \binom{d-1}{3} and
    24h1,1=2d332d2+7d3h^{1,1} = \tfrac{2d^3}{3} - 2d^2 + \tfrac{7d}{3}. The third statement is that
    25h1,1h^{1,1} is an integer for every dd, i.e. 32d36d2+7d3 \mid 2d^3 - 6d^2 + 7d; the fourth
    26is that the three formulas satisfy the Betti relation of a simply connected
    27surface, χ=2+2h2,0+h1,1\chi = 2 + 2h^{2,0} + h^{1,1}, as a polynomial identity in dd
    28(multiplied by 33 and with 6(d13)=(d1)(d2)(d3)6\binom{d-1}{3} = (d-1)(d-2)(d-3)).
    29-/
    30
    31namespace Lax894236.Parity
    32
    33open Finset
    34
    35/-- The Euler characteristic of `X_d^n` in binomial form,
    36`∑_{j=1}^{n+1} (-1)^(j+1) C(n+2, j+1) d^j`, as an integer polynomial in `d`. -/
    37def chiBinom (n : ℕ) (d : ℤ) : ℤ :=
    38 ∑ j ∈ Icc 1 (n + 1), (-1 : ℤ) ^ (j + 1) * ((n + 2).choose (j + 1) : ℤ) * d ^ j
    39
    40/-- Three times `h^{1,1}` of a smooth surface of degree `d` in `ℙ³`:
    41`2 d³ - 6 d² + 7 d`. -/
    42def h11Num (d : ℤ) : ℤ := 2 * d ^ 3 - 6 * d ^ 2 + 7 * d
    43
    44/-- In every odd dimension the Euler characteristic is even, for every degree. -/
    45axiom two_dvd_chiBinom_of_odd (n : ℕ) (hn : Odd n) (d : ℤ) : (2 : ℤ) ∣ chiBinom n d
    46
    47/-- For threefolds, `b₃ = 4 - χ` is even for every degree. -/
    48axiom two_dvd_b3 (d : ℤ) : (2 : ℤ) ∣ (4 - chiBinom 3 d)
    49
    50/-- `h^{1,1}` of a smooth surface in `ℙ³` is an integer for every degree. -/
    51axiom three_dvd_h11Num (d : ℤ) : (3 : ℤ) ∣ h11Num d
    52
    53/-- The Betti relation `χ = 2 + 2 h^{2,0} + h^{1,1}` holds for every degree, as
    54the polynomial identity `3 χ = 6 + (d-1)(d-2)(d-3) + 3 h^{1,1}`. -/
    55axiom betti_relation (d : ℤ) :
    56 3 * (d ^ 3 - 4 * d ^ 2 + 6 * d) = 6 + (d - 1) * (d - 2) * (d - 3) + h11Num d
    57
    58end Lax894236.Parity
    59
    Show ProofShow ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…