Documentation

Atlas.ArithmeticGeometry.code.FiniteFields

theorem finite_subgroup_of_field_isCyclic (k : Type u_1) [Field k] (G : Subgroup kˣ) [Finite G] :

Theorem 3.3. Any finite subgroup $G$ of the multiplicative group $k^\times$ of a field $k$ is cyclic.

theorem card_filter_quadraticChar_neg_one (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F 2) :
{a : F | (quadraticChar F) a = -1}.card = (Fintype.card F - 1) / 2

The number of non-square elements in a finite field $F$ of odd characteristic is $(|F| - 1)/2$, expressed as the cardinality of the filter of elements on which the quadratic character takes the value $-1$.

theorem phi_injective {F : Type u_1} [Field F] {α β : F} (hαβ : α β) {a₁ a₂ : F} (hβ₁ : β + a₁ 0) (hβ₂ : β + a₂ 0) (h : (α + a₁) * (β + a₁)⁻¹ = (α + a₂) * (β + a₂)⁻¹) :
a₁ = a₂

Injectivity of the Möbius-like map $a \mapsto (\alpha + a)(\beta + a)^{-1}$ on the locus where $\beta + a \neq 0$, provided $\alpha \neq \beta$.

theorem rabin_different_type_count (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F 2) (α β : F) (hαβ : α β) :
{δ : F | α + δ 0 β + δ 0 (quadraticChar F) (α + δ) (quadraticChar F) (β + δ)}.card = (Fintype.card F - 1) / 2

Theorem 3.7 (Rabin). For distinct $\alpha, \beta$ in a finite field $F$ of odd characteristic, exactly $(|F| - 1)/2$ shifts $\delta$ satisfy $\alpha + \delta, \beta + \delta \neq 0$ and the quadratic characters of these shifts disagree.

theorem eval_diagonal_quadratic_form {K : Type u_1} [Field K] (a b c : K) (v : Fin 3K) :

Evaluating the diagonal ternary quadratic form $aX_0^2 + bX_1^2 + cX_2^2$ at a point $v$ yields $a v_0^2 + b v_1^2 + c v_2^2$.

theorem conic_has_rational_point_of_finite_field (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) (a b c : K) (_ha : a 0) (_hb : b 0) (_hc : c 0) :
∃ (x : K) (y : K) (z : K), (x 0 y 0 z 0) a * x ^ 2 + b * y ^ 2 + c * z ^ 2 = 0

Theorem 3.4. Every non-degenerate diagonal ternary conic $aX^2 + bY^2 + cZ^2 = 0$ over a finite field $K$ of odd characteristic has a nonzero rational point. This is a special case of the Chevalley–Warning theorem.

noncomputable def affineSolCount (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) :

The number of affine solutions $(x, y, z) \in K^3$ to the diagonal ternary quadratic form $aX^2 + bY^2 + cZ^2 = 0$.

Instances For
    noncomputable def projConicCount (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) :

    The number of projective points on the conic $aX^2 + bY^2 + cZ^2 = 0$, obtained from the affine count by removing the origin and quotienting by the action of $K^\times$.

    Instances For
      theorem diag_binary_form_trivial_of_not_square {K : Type u_1} [Field K] (a b : K) (ha : a 0) (hb : b 0) (hnsq : ¬IsSquare (-b * a⁻¹)) {x y : K} (heq : a * x ^ 2 + b * y ^ 2 = 0) :
      x = 0 y = 0

      If $-b/a$ is not a square in a field $K$, then the only solution to the binary form $a x^2 + b y^2 = 0$ is the trivial one $x = y = 0$.

      theorem quadChar_jacobi_sum (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) :
      a : K, (quadraticChar K) (a * (a - 1)) = -1

      The Jacobi-sum identity $\sum_{a \in K} \chi(a(a-1)) = -1$, where $\chi$ is the quadratic character of a finite field of odd characteristic.

      theorem quadChar_sum_sq_add (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) (d : K) (hd : d 0) :
      t : K, (quadraticChar K) (t ^ 2 + d) = -1

      For $d \neq 0$ in a finite field $K$ of odd characteristic, $\sum_{t \in K} \chi(t^2 + d) = -1$, where $\chi$ is the quadratic character.

      theorem quadChar_sum_ec (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) (e c : K) (he : e 0) (hc : c 0) :
      z : K, (quadraticChar K) (e + c * z ^ 2) = -(quadraticChar K) c

      For nonzero $e, c$ in a finite field of odd characteristic, $\sum_{z \in K} \chi(e + c z^2) = -\chi(c)$.

      theorem fiber_card_chi (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) (a d : K) (ha : a 0) :
      (Fintype.card { x : K // a * x ^ 2 + d = 0 }) = 1 + (quadraticChar K) (-d * a⁻¹)

      The number of solutions $x \in K$ to $ax^2 + d = 0$ in a finite field of odd characteristic equals $1 + \chi(-d/a)$, where $\chi$ is the quadratic character.

      theorem double_sum_vanish (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) (b c : K) (hb : b 0) (hc : c 0) :
      y : K, z : K, (quadraticChar K) (b * y ^ 2 + c * z ^ 2) = 0

      The double character sum $\sum_{y, z \in K} \chi(b y^2 + c z^2) = 0$ for nonzero $b, c$ in a finite field of odd characteristic.

      noncomputable def fiberEquivOdd (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) :
      { v : Fin 3K // a * v 0 ^ 2 + b * v 1 ^ 2 + c * v 2 ^ 2 = 0 } (p : K × K) × { x : K // a * x ^ 2 + (b * p.1 ^ 2 + c * p.2 ^ 2) = 0 }

      Fibered description of solutions of $aX_0^2 + bX_1^2 + cX_2^2 = 0$ over the projection onto the last two coordinates: equivalent to a $\Sigma$-type indexed by $(y, z)$ of solutions to $aX^2 + (b y^2 + c z^2) = 0$.

      Instances For
        theorem affineSolCount_irred_char2 (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (a b c : K) (_ha : a 0) (hb : b 0) (_hc : c 0) :

        In characteristic 2, the number of affine solutions to a non-degenerate diagonal ternary quadratic form $aX^2 + bY^2 + cZ^2 = 0$ over a finite field $K$ equals $|K|^2$ (exploiting that Frobenius $x \mapsto x^2$ is bijective).

        theorem affineSolCount_irred_odd (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (hodd : ringChar K 2) (a b c : K) (ha : a 0) (hb : b 0) (hc : c 0) :

        In odd characteristic, the number of affine solutions to a non-degenerate diagonal ternary quadratic form $aX^2 + bY^2 + cZ^2 = 0$ over a finite field $K$ equals $|K|^2$. Established via a character-sum argument.

        theorem affineSolCount_irred (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) (ha : a 0) (hb : b 0) (hc : c 0) :

        Uniform statement (any characteristic): for a non-degenerate diagonal ternary quadratic form over a finite field $K$, the number of affine solutions is $|K|^2$.

        theorem affineSolCount_double_line_char2 (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (a b : K) (ha : a 0) (hb : b 0) :

        In characteristic 2, the "double line" conic $aX^2 + bY^2 = 0$ also has $|K|^2$ affine solutions: since the form is a perfect square, every $(y, z)$ extends uniquely to a solution.

        theorem affineSolCount_split_base (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b : K) (ha : a 0) (hb : b 0) (hsq : IsSquare (-b * a⁻¹)) (hchar : ringChar K 2) :

        For the split conic $aX^2 + bY^2 = 0$ where $-b/a$ is a square in a finite field of odd characteristic (so the form factors over $K$), the number of affine solutions equals $2|K|^2 - |K|$.

        theorem geom_irred_conic_has_q_plus_one_points (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) (ha : a 0) (hb : b 0) (hc : c 0) :

        A geometrically irreducible diagonal conic $aX^2 + bY^2 + cZ^2 = 0$ over $\mathbb{F}_q$ (with $abc \neq 0$) has exactly $q + 1$ projective points.

        theorem double_line_conic_has_q_plus_one_points_char2 (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (a b : K) (ha : a 0) (hb : b 0) :

        In characteristic 2, the degenerate "double-line" conic $aX^2 + bY^2 = 0$ over $\mathbb{F}_q$ has exactly $q + 1$ projective points.

        theorem split_base_conic_has_2q_plus_one_points (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b : K) (ha : a 0) (hb : b 0) (hsq : IsSquare (-b * a⁻¹)) (hchar : ringChar K 2) :

        A conic of the form $aX^2 + bY^2 = 0$ that splits over the base field ($-b/a$ a square in $K$) has $2q + 1$ projective points: it is a union of two lines meeting in one point.

        theorem split_ext_conic_has_one_point (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b : K) (ha : a 0) (hb : b 0) (hnsq : ¬IsSquare (-b * a⁻¹)) :
        projConicCount K a b 0 = 1

        A conic $aX^2 + bY^2 = 0$ that splits only over a quadratic extension ($-b/a$ not a square in $K$) has exactly $1$ projective $K$-point: the lone point $[0 : 0 : 1]$ visible to $K$.

        def DiagConicIsGeomIrreducible {K : Type u_1} [Field K] (_a _b c : K) :

        A diagonal conic $aX^2 + bY^2 + cZ^2 = 0$ is geometrically irreducible when $c \neq 0$.

        Instances For
          def DiagConicIsSplitOverBase {K : Type u_1} [Field K] (a b c : K) :

          A diagonal conic $aX^2 + bY^2 + cZ^2 = 0$ splits over the base field $K$ when $c = 0$ and $-b/a$ is a square in $K$.

          Instances For
            def DiagConicIsSplitOverExtension {K : Type u_1} [Field K] (a b c : K) :

            A diagonal conic $aX^2 + bY^2 + cZ^2 = 0$ splits only over a quadratic extension when $c = 0$ and $-b/a$ is not a square in $K$.

            Instances For

              Corollary 3.5 (trichotomy, odd characteristic). Over a finite field of odd characteristic, a diagonal conic $aX^2 + bY^2 + cZ^2 = 0$ (with $a, b \neq 0$) is either geometrically irreducible (with $q + 1$ points), split over $K$ (with $2q + 1$ points), or split only over a quadratic extension (with $1$ point).

              theorem conic_projective_point_count_trichotomy_all_char (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) (ha : a 0) (hb : b 0) :

              Characteristic-agnostic trichotomy: over any finite field $K$, the number of projective points on a diagonal conic with $a, b \neq 0$ is either $q + 1$, $2q + 1$, or $1$.

              theorem conic_point_count_cong_one (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) (ha : a 0) (hb : b 0) :

              The number of projective points on a diagonal conic over a finite field $\mathbb{F}_q$ is always congruent to $1$ modulo $q$.

              theorem q_dvd_projConicCount_sub_one (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (a b c : K) (ha : a 0) (hb : b 0) :

              Equivalent divisibility statement: $q = |K|$ divides $\#C(\mathbb{F}_q) - 1$ for any diagonal conic $C$ with $a, b \neq 0$.