The Hasse Bound — Lean blueprint

1. Point counts and the Frobenius endomorphism🔗

Definition1.1
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For an elliptic curve E over a finite field K = \mathbb{F}_q whose affine point type is finite, the point count \#E(\mathbb{F}_q) is the cardinality of the finite abelian group of \mathbb{F}_q-rational nonsingular affine points together with the point at infinity. In Hasse-Weil this is \texttt{pointCount } E \;:=\; \operatorname{card} E.\mathrm{Point}.

Lean code for Definition1.1●1 definition
  • defdefined in HasseWeil/Frobenius.lean
    complete
    def HasseWeil.pointCount.{u_1} {F : Type u_1} [Field F]
  (E : WeierstrassCurve.Affine F) [Fintype E.Point] : ℕ
    def HasseWeil.pointCount.{u_1} {F : Type u_1}
  [Field F]
  (E : WeierstrassCurve.Affine F)
  [Fintype E.Point] : ℕ
    The number of rational points on an affine elliptic curve, including O.
Definition1.2
uses 0
Used by 3
Reverse dependency previews
Preview
Theorem 1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Following Silverman III.4, an isogeny \varphi : E_1 \to E_2 is modelled by its pullback \varphi^* : K(E_2) \hookrightarrow K(E_1) on function fields (an injective K-algebra map) together with its group homomorphism E_1(K) \to E_2(K) on rational points. Its degree is computed, not stored, as the field-extension degree \deg\varphi \;=\; [\,K(E_1) : \varphi^* K(E_2)\,] \;=\; \operatorname{finrank}_{K(E_2)} K(E_1). Defining the degree from the pullback is what keeps the Hasse argument non-circular.

Lean code for Definition1.2●2 definitions
  • structure(2 fields)defined in HasseWeil/Basic.lean
    complete
    structure HasseWeil.Isogeny.{u_1} {F : Type u_1} [Field F] [DecidableEq F]
  (W₁ W₂ : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂] : Type u_1
    structure HasseWeil.Isogeny.{u_1} {F : Type u_1}
  [Field F] [DecidableEq F]
  (W₁ W₂ : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂] :
  Type u_1
    An isogeny `φ : E₁ → E₂` between elliptic curves over a field `F`.

An isogeny has two components:
- The **pullback** `φ* : K(E₂) →ₐ[F] K(E₁)` on function fields.
- The **group homomorphism** `φ : E₁(F) →+ E₂(F)` on rational points.

Injectivity of the pullback is derived automatically (see `Isogeny.pullback_injective`),
since any algebra homomorphism from a field is injective.

The degree is *computed* from the pullback via `Module.finrank`, not stored.

In the full algebraic-geometric theory, these two components are derived from
a single morphism of varieties. Here we carry both as data, since constructing
one from the other requires substantial algebraic geometry not yet in mathlib.

    Fields

    pullback : W₂.FunctionField →ₐ[F] W₁.FunctionField
    The pullback `φ* : K(E₂) →ₐ[F] K(E₁)` on function fields. 
    toAddMonoidHom : W₁.Point →+ W₂.Point
    The underlying group homomorphism on rational points.
  • defdefined in HasseWeil/Basic.lean
    complete
    def HasseWeil.Isogeny.degree.{u_1} {F : Type u_1} [Field F] [DecidableEq F]
  {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂] (φ : HasseWeil.Isogeny W₁ W₂) : ℕ
    def HasseWeil.Isogeny.degree.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  {W₁ W₂ : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂]
  (φ : HasseWeil.Isogeny W₁ W₂) : ℕ
    The degree of an isogeny, defined as `[K(E₁) : K(E₂)]` where `K(E₁)` is
a `K(E₂)`-module via the pullback. This is computed, not stored.
Theorem1.3
uses 1used by 0✓L∃∀N

(Degree is multiplicative.) For composable isogenies \varphi, \psi, \deg(\psi \circ \varphi) \;=\; \deg\varphi \cdot \deg\psi (Definition 1.2), and the composite of two positive-degree isogenies again has positive degree — the fact that \operatorname{End}(E) is an integral domain (Silverman III.4.2(c)).

Lean code for Theorem1.3●2 theorems
  • theoremdefined in HasseWeil/Basic.lean
    complete
    theorem HasseWeil.Isogeny.comp_degree.{u_1} {F : Type u_1} [Field F]
  [DecidableEq F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂]
  [WeierstrassCurve.IsElliptic W₃] (ψ : HasseWeil.Isogeny W₂ W₃)
  (φ : HasseWeil.Isogeny W₁ W₂) :
  (ψ.comp φ).degree = φ.degree * ψ.degree
    theorem HasseWeil.Isogeny.comp_degree.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  {W₁ W₂ W₃ : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂]
  [WeierstrassCurve.IsElliptic W₃]
  (ψ : HasseWeil.Isogeny W₂ W₃)
  (φ : HasseWeil.Isogeny W₁ W₂) :
  (ψ.comp φ).degree = φ.degree * ψ.degree
    **Degree multiplicativity**: `deg(ψ ∘ φ) = deg(φ) · deg(ψ)`.
Follows from the tower law for field extensions.
  • theoremdefined in HasseWeil/Basic.lean
    complete
    theorem HasseWeil.Isogeny.comp_degree_pos.{u_1} {F : Type u_1} [Field F]
  [DecidableEq F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂]
  [WeierstrassCurve.IsElliptic W₃] (ψ : HasseWeil.Isogeny W₂ W₃)
  (φ : HasseWeil.Isogeny W₁ W₂) (hψ : 0 < ψ.degree)
  (hφ : 0 < φ.degree) : 0 < (ψ.comp φ).degree
    theorem HasseWeil.Isogeny.comp_degree_pos.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  {W₁ W₂ W₃ : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂]
  [WeierstrassCurve.IsElliptic W₃]
  (ψ : HasseWeil.Isogeny W₂ W₃)
  (φ : HasseWeil.Isogeny W₁ W₂)
  (hψ : 0 < ψ.degree)
  (hφ : 0 < φ.degree) :
  0 < (ψ.comp φ).degree
    **No zero divisors in End E (degree form)**: the composition of two isogenies of positive
degree has positive degree. The degree restatement of "End E is an integral domain", since
`Isogeny` carries no `Zero`/`Mul` for the `NoZeroDivisors (Isogeny E E)` formulation.
Reference: Silverman III.4.2(c).
Proof for Theorem 1.3
uses 0

Immediate from the tower law [K(E_1):K(E_3)] = [K(E_1):K(E_2)]\,[K(E_2):K(E_3)] for the nested function-field extensions cut out by the two pullbacks; positivity of the product follows from positivity of each factor.

Theorem1.4
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Degree of [n].) For each n \in \mathbb{Z} the multiplication-by-n endomorphism [n] : E \to E is an isogeny with \deg[n] \;=\; n^2 (Silverman III.4.2). In particular [n] \ne 0 for n \ne 0, so \operatorname{End}(E) is torsion-free.

Lean code for Theorem1.4●2 declarations
  • defdefined in HasseWeil/Basic.lean
    complete
    def HasseWeil.mulByInt.{u_1} {F : Type u_1} [Field F] [DecidableEq F]
  (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W]
  (n : ℤ) : HasseWeil.Isogeny W W
    def HasseWeil.mulByInt.{u_1} {F : Type u_1}
  [Field F] [DecidableEq F]
  (W : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic W]
  (n : ℤ) : HasseWeil.Isogeny W W
    The multiplication-by-n endomorphism `[n]` viewed as an isogeny.

The group homomorphism is `zsmulAddGroupHom n` (scalar multiplication on `E.Point`).

The pullback `[n]* : K(E) →ₐ[F] K(E)` is defined via division polynomials:
for `f ∈ K(E)`, `[n]*(f) = f ∘ [n]`, which can be expressed using the
division polynomial `ψ_n` and the multiplication formulas. The degree of this
pullback is `n²` (Silverman III.4.2, Sutherland Theorem 6.9).

**The `n = 0` branch is an unavoidable junk default, not a placeholder.**
The zero map `[0] : E → E` is the constant map to `O`; it is *not* an
isogeny (an isogeny is a nonconstant — hence finite, surjective —
morphism), so it has no finite function-field comorphism. Consequently
`Isogeny W W` *cannot* faithfully represent `[0]`: the struct demands a
pullback `K(E) →ₐ[F] K(E)`, but the honest comorphism of `[0]` lands in
the constant subfield `F`, giving an infinite-index image (degree `0`/`∞`)
that no single `AlgHom` of the required type encodes. Since `mulByInt` is a
total function, the `n = 0` branch returns the arbitrary total-function
default `AlgHom.id F K(E)` for the pullback (its `toAddMonoidHom` IS the
genuine zero map, kernel `⊤`). This is the standard Lean "junk value for an
out-of-domain input" idiom (cf. `x / 0 = 0`), NOT a rotten placeholder: no
theorem relies on it, because every degree theorem (`mulByInt_degree`,
`mulByInt_pullbackAlgHom`-driven equalities, `mulByInt_q_pullback_*`
consumers) carries an explicit `n ≠ 0` / `0 < n` guard, and the two `n = 0`
call sites use only the genuine point map (`IsogenyKernel`: kernel `= ⊤`).
Callers needing the zero map at the point level should use
`zsmulAddGroupHom 0` directly rather than `(mulByInt W 0).toAddMonoidHom`.
See `.mathlib-quality/isogeny-compatibility-audit.md` (recommendation 4).
  • theoremdefined in HasseWeil/Basic.lean
    complete
    theorem HasseWeil.mulByInt_degree.{u_1} {F : Type u_1} [Field F] [DecidableEq F]
  (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W]
  (n : ℤ) (hn : n ≠ 0) : (HasseWeil.mulByInt W n).degree = (n ^ 2).toNat
    theorem HasseWeil.mulByInt_degree.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (W : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic W] (n : ℤ)
  (hn : n ≠ 0) :
  (HasseWeil.mulByInt W n).degree =
    (n ^ 2).toNat
    The degree of `[n]` is `n²`. Reference: Silverman III.4.2.
Proof for Theorem 1.4
Proof uses 2
Proof dependency previews
Preview
Definition 1.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The pullback [n]^* is built from the division polynomials; the finrank computation gives \deg[n] = n^2 (Definition 1.2, Theorem 2.4).

Definition1.5
uses 1
Used by 5
Reverse dependency previews
Preview
Definition 1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The q-power Frobenius \pi : E \to E is the isogeny acting on the function field by f \mapsto f^{q} (Definition 1.1). In Hasse-Weil it is \texttt{frobeniusIsog}, and \texttt{frobeniusIsog\_pullback\_apply} records that its pullback on the function field is exactly the \#K-power map (built on FiniteField.frobeniusAlgHom). Its trace is the integer t \;=\; q + 1 - \#E(\mathbb{F}_q), so that the fixed points of \pi — the \mathbb{F}_q-rational points — are counted by \deg(1 - \pi) = \#E(\mathbb{F}_q).

Lean code for Definition1.5●2 declarations
  • defdefined in HasseWeil/Frobenius.lean
    complete
    def HasseWeil.frobeniusIsog.{u_1} {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] :
  HasseWeil.Isogeny W.toAffine W.toAffine
    def HasseWeil.frobeniusIsog.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic
      W.toAffine] :
  HasseWeil.Isogeny W.toAffine W.toAffine
    The `q`-th power Frobenius endomorphism as a `Basic.Isogeny` over `K`.

The pullback `π* : K(E) →ₐ[K] K(E)` sends `f ↦ f^q` (concrete, from
`FrobeniusIsogeny.lean`). The group homomorphism on K-rational points is
the identity (since `x^q = x` for all `x ∈ K`).

Reference: Silverman, Proposition III.4.6.
  • theoremdefined in HasseWeil/Frobenius.lean
    complete
    theorem HasseWeil.frobeniusIsog_pullback_apply.{u_1} {K : Type u_1} [Field K]
  [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (f : W.toAffine.FunctionField) :
  (HasseWeil.frobeniusIsog W).pullback f = f ^ Fintype.card K
    theorem HasseWeil.frobeniusIsog_pullback_apply.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (f : W.toAffine.FunctionField) :
  (HasseWeil.frobeniusIsog W).pullback f =
    f ^ Fintype.card K
    The Frobenius pullback sends `f ↦ f^q`.
Definition1.6
uses 1
Used by 4
Reverse dependency previews
Preview
Theorem 2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Frobenius has degree q.) The q-power Frobenius \pi (Definition 1.5) has \deg\pi \;=\; [\,K(E) : K(E)^q\,] \;=\; q \;=\; \#K (Silverman III.4.6, II.2.11(a)). The core algebraic fact is that K(E) is a degree-q extension of its subfield K(E)^q of q-th powers, which is the substance of the pure inseparability of K(E)/K(E)^q.

Lean code for Definition1.6●2 theorems
  • theoremdefined in HasseWeil/Frobenius.lean
    complete
    theorem HasseWeil.frobeniusIsog_degree.{u_1} {K : Type u_1} [Field K]
  [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] :
  (HasseWeil.frobeniusIsog W).degree = Fintype.card K
    theorem HasseWeil.frobeniusIsog_degree.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic
      W.toAffine] :
  (HasseWeil.frobeniusIsog W).degree =
    Fintype.card K
    The degree of the Frobenius isogeny is `#K`.
Uses the sorry-free proof from `FrobeniusIsogeny.frobenius_finrank_functionField`.
Reference: Silverman, Proposition III.4.6.
  • theoremdefined in HasseWeil/FrobeniusIsogeny.lean
    complete
    theorem HasseWeil.frobenius_finrank_functionField.{u_1} (K : Type u_1) [Field K]
  [Fintype K] (W : WeierstrassCurve K) :
  Module.finrank W.toAffine.FunctionField W.toAffine.FunctionField =
    Fintype.card K
    theorem HasseWeil.frobenius_finrank_functionField.{u_1}
  (K : Type u_1) [Field K] [Fintype K]
  (W : WeierstrassCurve K) :
  Module.finrank W.toAffine.FunctionField
      W.toAffine.FunctionField =
    Fintype.card K
    **Core algebraic fact**: `[K(E) : K(E)^q] = q`, where the module structure on `K(E)` over
itself is via the `q`-th power Frobenius (Silverman II.2.11(a)).
Theorem1.7
uses 0used by 1✓L∃∀N

(Frobenius fixed points are the rational points.) For a finite field K with q = \#K, an element a of the algebraic closure satisfies a^q = a if and only if a \in K; equivalently, K is exactly the root set of X^q - X (Silverman V.1). Transported to the curve, the fixed locus of \pi is precisely E(\mathbb{F}_q).

Lean code for Theorem1.7●2 theorems
  • theoremdefined in HasseWeil/Curves/FrobeniusFixedLocus.lean
    complete
    theorem HasseWeil.frobenius_fixed_iff_mem_baseField.{u_1} {K : Type u_1}
  [Field K] [Fintype K] (a : AlgebraicClosure K) :
  a ^ Fintype.card K = a ↔
    a ∈ Set.range ⇑(algebraMap K (AlgebraicClosure K))
    theorem HasseWeil.frobenius_fixed_iff_mem_baseField.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  (a : AlgebraicClosure K) :
  a ^ Fintype.card K = a ↔
    a ∈
      Set.range
        ⇑(algebraMap K
            (AlgebraicClosure K))
    **Frobenius fixed-point criterion.** For a finite field `K`, an element of the algebraic
closure is fixed by the `q`-power map (`q = Fintype.card K`) iff it lies in the image of `K`.
  • theoremdefined in HasseWeil/Curves/FrobeniusFixedLocus.lean
    complete
    theorem HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X.{u_1}
  {K : Type u_1} [Field K] [Fintype K] :
  HasseWeil.baseImageFinset✝ = HasseWeil.frobRootsFinset✝
    theorem HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X.{u_1}
  {K : Type u_1} [Field K] [Fintype K] :
  HasseWeil.baseImageFinset✝ =
    HasseWeil.frobRootsFinset✝
    **The image of `K` is exactly the root set of `X ^ q - X` in the algebraic closure.**
Proof for Theorem 1.7
uses 0

X^q - X is separable (its derivative is -1) of degree q, so it has exactly q distinct roots in the algebraic closure; the q elements of K are distinct roots, hence all of them.