The Euler characteristic of a smooth hypersurface as a binomial tail
Lax894236.EulerCharacteristic · concepts/Lax894236/EulerCharacteristic.lean · lax-894236
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For a smooth hypersurface of degree and dimension , the topological Euler characteristic is the polynomial in
a consequence of the Hirzebruch–Riemann–Roch computation of the Chern classes of a hypersurface. That geometric input is taken from the literature; this concept is about the polynomial itself. Multiplying by removes the division: .
The statement is that this polynomial equals the tail of the binomial expansion of from the quadratic term on, : the constant and linear terms of the binomial cancel against and , which is why is a genuine polynomial with no constant or linear term. The familiar cases are for surfaces and for threefolds.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Group.Finset.Basic |
| 2 | import Mathlib.Data.Nat.Choose.Basic |
| 3 | import Mathlib.Data.Rat.Defs |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: The Euler characteristic of a smooth hypersurface as a binomial tail |
| 8 | type: theorem |
| 9 | --- |
| 10 | For a smooth hypersurface of degree and |
| 11 | dimension , the topological Euler characteristic is the polynomial in |
| 12 | |
| 13 | |
| 14 | |
| 15 | a consequence of the Hirzebruch–Riemann–Roch computation of the Chern classes of a |
| 16 | hypersurface. That geometric input is taken from the literature; this concept is |
| 17 | about the polynomial itself. Multiplying by removes the division: |
| 18 | `chiPoly n d = (1 - d)^(n+2) - 1 + (n+2) d`. |
| 19 | |
| 20 | The statement is that this polynomial equals the tail of the binomial expansion |
| 21 | of from the quadratic term on, |
| 22 | : the constant and linear terms of |
| 23 | the binomial cancel against and , which is why is a genuine |
| 24 | polynomial with no constant or linear term. The familiar cases are |
| 25 | for surfaces and for threefolds. |
| 26 | -/ |
| 27 | |
| 28 | namespace Lax894236.EulerCharacteristic |
| 29 | |
| 30 | open Finset |
| 31 | |
| 32 | /-- `d` times the Euler characteristic of a smooth degree-`d` hypersurface of |
| 33 | dimension `n`: the polynomial `(1 - d)^(n+2) - 1 + (n+2) d`. -/ |
| 34 | def chiPoly (n : ℕ) (d : ℚ) : ℚ := (1 - d) ^ (n + 2) - 1 + ((n : ℚ) + 2) * d |
| 35 | |
| 36 | /-- The polynomial equals the binomial tail |
| 37 | `∑_{k=0}^{n} C(n+2, k+2) (-d)^(k+2)`. -/ |
| 38 | axiom chiPoly_eq_binomial_tail (n : ℕ) (d : ℚ) : |
| 39 | chiPoly n d = ∑ k ∈ range (n + 1), ((n + 2).choose (k + 2) : ℚ) * (-d) ^ (k + 2) |
| 40 | |
| 41 | end Lax894236.EulerCharacteristic |
| 42 |
Builds on
none
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments