two_pow_card — Mathlib

English

For every finite field F of odd characteristic, 2^{|F|/2} = χ8(|F|) in F, where χ8 is the primitive 8th cyclotomic character.

Русский

Для любого конечного поля F нечетственной характеристикой, 2^{|F|/2} = χ8(|F|) в F, где χ8 — примитивный символ 8-й циклотимической группы.

LaTeX

$$$2^{|F|/2} = \chi_8(|F|) \quad\text{in } F$$$

Lean4

/-- For every finite field `F` of odd characteristic, we have `2^(#F/2) = χ₈ #F` in `F`. -/
theorem two_pow_card {F : Type*} [Fintype F] [Field F] (hF : ringChar F ≠ 2) :
    (2 : F) ^ (Fintype.card F / 2) = χ₈ (Fintype.card F) :=
  by
  have hp2 (n : ℕ) : (2 ^ n : F) ≠ 0 := pow_ne_zero n (Ring.two_ne_zero hF)
  obtain ⟨n, hp, hc⟩ :=
    FiniteField.card F
      (ringChar F)
        -- we work in `FF`, the eighth cyclotomic field extension of `F`

  let FF := CyclotomicField 8 F
  have hchar := Algebra.ringChar_eq F FF
  have FFp := hchar.subst hp
  have := Fact.mk FFp
  have hFF := hchar ▸ hF
  have hu : IsUnit (ringChar FF : ZMod 8) :=
    by
    rw [isUnit_iff_not_dvd_char, ringChar_zmod_n]
    rw [Ne, ← Nat.prime_dvd_prime_iff_eq FFp Nat.prime_two] at hFF
    change ¬_ ∣ 2 ^ 3
    exact mt FFp.dvd_of_dvd_pow hFF
  let ψ₈ :=
    primitiveZModChar 8 F
      (by convert hp2 3 using 1; norm_cast)
        -- We cast from `AddChar (ZMod (8 : ℕ+)) FF` to `AddChar (ZMod 8) FF`
          -- This is needed to make `simp_rw [← h₁]` below work.

  let ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
  let τ : FF := ψ₈char 1
  have τ_spec : τ ^ 4 = -1 :=
    by
    rw [show τ = ψ₈.char 1 from rfl] -- to make `rw [ψ₈.prim.zmod_char_eq_one_iff]` work

    refine (sq_eq_one_iff.1 ?_).resolve_left ?_
    · rw [← pow_mul, ← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide
    · rw [← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide
        -- we consider `χ₈` as a multiplicative character `ℤ/8ℤ → FF`

  let χ := χ₈.ringHomComp (Int.castRingHom FF)
  have hχ : χ (-1) = 1 := Int.cast_one
  have hq : IsQuadratic χ :=
    isQuadratic_χ₈.comp
      _
        -- we now show that the Gauss sum of `χ` and `ψ₈` has the relevant property

  have h₁ : (fun (a : Fin 8) ↦ ↑(χ₈ a) * τ ^ (a : ℕ)) = fun a ↦ χ a * ↑(ψ₈char a) := by ext1; congr; apply pow_one
  have hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3) :=
    by
    rw [gaussSum, ← h₁, Fin.sum_univ_eight,
      -- evaluate `χ₈`
      show χ₈ 0 = 0 from rfl, show χ₈ 1 = 1 from rfl, show χ₈ 2 = 0 from rfl, show χ₈ 3 = -1 from rfl,
      show χ₈ 4 = 0 from rfl, show χ₈ 5 = -1 from rfl, show χ₈ 6 = 0 from rfl, show χ₈ 7 = 1 from rfl,
      -- normalize exponents
      show ((3 : Fin 8) : ℕ) = 3 from rfl, show ((5 : Fin 8) : ℕ) = 5 from rfl, show ((7 : Fin 8) : ℕ) = 7 from rfl]
    simp only [Int.cast_zero, zero_mul, Int.cast_one, Fin.val_one, pow_one, one_mul, zero_add, Fin.val_two, add_zero,
      Int.reduceNeg, Int.cast_neg]
    linear_combination (τ ^ 3 - τ) * τ_spec
  have hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * Fintype.card (ZMod 8) :=
    by
    rw [hχ, one_mul, ZMod.card, Nat.cast_ofNat, hg₁]
    linear_combination (4 * τ ^ 2 - 8) * τ_spec
  have h := Char.card_pow_char_pow (R := ZMod 8) hq ψ₈char (ringChar FF) n hu hFF hg
  rw [ZMod.card, ← hchar, hχ, one_mul, ← hc, ← Nat.cast_pow (ringChar F), ← hc] at h
  convert_to (8 : F) ^ (Fintype.card F / 2) = _
  · rw [(by norm_num : (8 : F) = 2 ^ 2 * 2), mul_pow, (FiniteField.isSquare_iff hF <| hp2 2).mp ⟨2, pow_two 2⟩, one_mul]
  apply (algebraMap F FF).injective
  simpa only [map_pow, map_ofNat, map_intCast, Nat.cast_ofNat] using h

Похожие утверждения