The congruent number curves are quadratic twists of y² = x³ − x
Lax712553.QuadraticTwist · concepts/Lax712553/QuadraticTwist.lean · lax-712553
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The congruent number curve of is . For a prime , the trace of Frobenius is the character sum , where is the quadratic character of with : each contributes points. This concept defines by that sum.
The statement is the quadratic twist formula: for every prime and every integer not divisible by ,
so every is the quadratic twist of by . The identity is exact at the level of character sums; it is the substitution , a bijection of because is invertible, together with .
Concept map
Lean source view on GitHub
| 1 | import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The congruent number curves are quadratic twists of y² = x³ − x |
| 6 | type: theorem |
| 7 | --- |
| 8 | The congruent number curve of is . For a prime , |
| 9 | the trace of Frobenius is the character |
| 10 | sum , where is the quadratic |
| 11 | character of with : each contributes |
| 12 | points. This concept defines by that sum. |
| 13 | |
| 14 | The statement is the quadratic twist formula: for every prime and every |
| 15 | integer not divisible by , |
| 16 | |
| 17 | |
| 18 | |
| 19 | so every is the quadratic twist of by . The |
| 20 | identity is exact at the level of character sums; it is the substitution |
| 21 | , a bijection of because is invertible, together with |
| 22 | . |
| 23 | -/ |
| 24 | |
| 25 | namespace Lax712553.QuadraticTwist |
| 26 | |
| 27 | /-- The trace of Frobenius of `E_n : y² = x³ − n² x` at the prime `p`, as the |
| 28 | character sum `−∑_x χ(x³ − n² x)`. -/ |
| 29 | noncomputable def a_p (n : ℤ) (p : ℕ) [Fact p.Prime] : ℤ := |
| 30 | -∑ x : ZMod p, quadraticChar (ZMod p) (x ^ 3 - (n : ZMod p) ^ 2 * x) |
| 31 | |
| 32 | /-- The quadratic twist formula `a_p(E_n) = χ(n) a_p(E_1)` for `p ∤ n`. -/ |
| 33 | axiom a_p_twist (n : ℤ) (p : ℕ) [Fact p.Prime] (hn : (n : ZMod p) ≠ 0) : |
| 34 | a_p n p = quadraticChar (ZMod p) (n : ZMod p) * a_p 1 p |
| 35 | |
| 36 | end Lax712553.QuadraticTwist |
| 37 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments