The arithmetic obstruction to a linear subspace class being a multiple of the hyperplane power
Lax894236.LinearSubspaceClass · concepts/Lax894236/LinearSubspaceClass.lean · lax-894236
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be a smooth hypersurface of degree and even dimension containing a linear subspace , and let be the hyperplane class. Two intersection numbers are standard: and . If the class of were a rational multiple , then and would be an integer, since intersection numbers of algebraic cycles are integers.
This concept isolates the arithmetic step: for every integer there is no rational with and an integer. Hence is not a rational multiple of for any , in every even dimension.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.Rat.Defs |
| 2 | import Mathlib.Data.Int.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: The arithmetic obstruction to a linear subspace class being a multiple of the hyperplane power |
| 7 | type: theorem |
| 8 | --- |
| 9 | Let be a smooth hypersurface of degree and even |
| 10 | dimension containing a linear subspace , and let |
| 11 | be the hyperplane class. Two intersection numbers are standard: |
| 12 | and . If the class of were a rational multiple |
| 13 | , then and would be an integer, since |
| 14 | intersection numbers of algebraic cycles are integers. |
| 15 | |
| 16 | This concept isolates the arithmetic step: for every integer there is |
| 17 | no rational with and an integer. Hence is not a |
| 18 | rational multiple of for any , in every even dimension. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax894236.LinearSubspaceClass |
| 22 | |
| 23 | /-- For `d ≥ 2` there is no rational `c` with `c d = 1` and `c² d` an integer. -/ |
| 24 | axiom no_rational_multiple (d : ℤ) (hd : 2 ≤ d) : |
| 25 | ¬ ∃ c : ℚ, c * (d : ℚ) = 1 ∧ ∃ n : ℤ, c ^ 2 * (d : ℚ) = (n : ℚ) |
| 26 | |
| 27 | end Lax894236.LinearSubspaceClass |
| 28 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments