Parity of the Euler characteristic in odd dimension, and integrality for surfaces
Lax894236.Parity · concepts/Lax894236/Parity.lean · lax-894236
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Write the Euler characteristic of the smooth hypersurface in its binomial form, (the polynomial of divided by ). Its coefficients are not all even, so evenness of is not a polynomial identity; it is a parity fact.
The first statement: for every odd dimension and every integer , is even. For threefolds this is what makes the mirror-symmetry formula with an integer for every degree; the second statement is that instance.
The remaining two statements concern surfaces in , where the literature gives , and . The third statement is that is an integer for every , i.e. ; the fourth is that the three formulas satisfy the Betti relation of a simply connected surface, , as a polynomial identity in (multiplied by and with ).
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Group.Finset.Basic |
| 2 | import Mathlib.Algebra.Group.Even |
| 3 | import Mathlib.Algebra.Ring.Parity |
| 4 | import Mathlib.Data.Nat.Choose.Basic |
| 5 | import Mathlib.Order.Interval.Finset.Nat |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: Parity of the Euler characteristic in odd dimension, and integrality for surfaces |
| 10 | type: theorem |
| 11 | --- |
| 12 | Write the Euler characteristic of the smooth hypersurface in its binomial |
| 13 | form, (the polynomial |
| 14 | of `EulerCharacteristic` divided by ). Its coefficients are not all even, so |
| 15 | evenness of is not a polynomial identity; it is a parity fact. |
| 16 | |
| 17 | The first statement: for every odd dimension and every integer , |
| 18 | is even. For threefolds this is what makes the mirror-symmetry |
| 19 | formula with an integer for every |
| 20 | degree; the second statement is that instance. |
| 21 | |
| 22 | The remaining two statements concern surfaces in , where the |
| 23 | literature gives , and |
| 24 | . The third statement is that |
| 25 | is an integer for every , i.e. ; the fourth |
| 26 | is that the three formulas satisfy the Betti relation of a simply connected |
| 27 | surface, , as a polynomial identity in |
| 28 | (multiplied by and with ). |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax894236.Parity |
| 32 | |
| 33 | open 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`. -/ |
| 37 | def 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`. -/ |
| 42 | def h11Num (d : ℤ) : ℤ := 2 * d ^ 3 - 6 * d ^ 2 + 7 * d |
| 43 | |
| 44 | /-- In every odd dimension the Euler characteristic is even, for every degree. -/ |
| 45 | axiom 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. -/ |
| 48 | axiom 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. -/ |
| 51 | axiom 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 |
| 54 | the polynomial identity `3 χ = 6 + (d-1)(d-2)(d-3) + 3 h^{1,1}`. -/ |
| 55 | axiom betti_relation (d : ℤ) : |
| 56 | 3 * (d ^ 3 - 4 * d ^ 2 + 6 * d) = 6 + (d - 1) * (d - 2) * (d - 3) + h11Num d |
| 57 | |
| 58 | end Lax894236.Parity |
| 59 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments