dickson_one_one_zmod_p — Mathlib

English

For any prime p, in ZMod p we have D_2 0 p = X^p; i.e., the p-th Dickson polynomial with k=2, a=0 agrees with X^p modulo p.

Русский

Для простого p в ZMod p имеем D_2 0 p = X^p; т.е. полином Диксона при k=2, a=0 совпадает с X^p по модулю p.

LaTeX

$$dickson\, 2\, (0 : R)\, p = X^p$$

Lean4

theorem dickson_one_one_zmod_p (p : ℕ) [Fact p.Prime] : dickson 1 (1 : ZMod p) p = X ^ p := by
  -- Recall that `dickson_one_one_eval_add_inv` characterises `dickson 1 1 p`
    -- as a polynomial that maps `x + x⁻¹` to `x ^ p + (x⁻¹) ^ p`.
    -- Since `X ^ p` also satisfies this property in characteristic `p`,
    -- we can use a variant on `Polynomial.funext` to conclude that these polynomials are equal.
    -- For this argument, we need an arbitrary infinite field of characteristic `p`.

  obtain ⟨K, _, _, H⟩ : ∃ (K : Type) (_ : Field K), ∃ _ : CharP K p, Infinite K :=
    by
    let K := FractionRing (Polynomial (ZMod p))
    let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
    have : CharP K p := by
      rw [← f.charP_iff_charP]
      infer_instance
    haveI : Infinite K :=
      Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
        (IsFractionRing.injective _ _)
    refine ⟨K, ?_, ?_, ?_⟩ <;> infer_instance
  apply map_injective (ZMod.castHom (dvd_refl p) K) (RingHom.injective _)
  rw [map_dickson, Polynomial.map_pow, map_X]
  apply eq_of_infinite_eval_eq
  apply @Set.Infinite.mono _ {x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
  · rintro _ ⟨x, rfl, hx⟩
    simp only [eval_X, eval_pow, Set.mem_setOf_eq, ZMod.cast_one', add_pow_char,
      dickson_one_one_eval_add_inv _ _ (mul_inv_cancel₀ hx), ZMod.castHom_apply]
      -- Now we need to show that the set of such `x` is infinite.
        -- If the set is finite, then we will show that `K` is also finite.

  · intro h
    rw [← Set.infinite_univ_iff] at H
    apply H
    suffices (Set.univ : Set K) = ⋃ x ∈ {x : K | ∃ y : K, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}
      by
      rw [this]
      clear this
      refine
        h.biUnion fun x _ =>
          ?_
            -- The following quadratic polynomial has as solutions the `y` for which `x = y + y⁻¹`.

      let φ : K[X] := X ^ 2 - C x * X + 1
      have hφ : φ ≠ 0 := by
        intro H
        have : φ.eval 0 = 0 := by rw [H, eval_zero]
        simpa [φ, eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul, mul_zero, sq, zero_add,
          one_ne_zero]
      classical
      convert (φ.roots ∪ {0}).toFinset.finite_toSet using 1
      ext1 y
      simp only [φ, Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union, mem_roots hφ, IsRoot,
        eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one, Multiset.mem_singleton]
      by_cases hy : y = 0
      · simp only [hy, or_true]
      apply or_congr _ Iff.rfl
      rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel₀ hy]
      apply eq_iff_eq_cancel_right.mpr
      ring
        -- Finally, we prove the claim that our finite union of finite sets covers all of `K`.

    apply (Set.eq_univ_of_forall _).symm
    intro x
    simp only [exists_prop, Set.mem_iUnion, Ne, Set.mem_setOf_eq]
    by_cases hx : x = 0
    · simp only [hx, and_true, inv_zero, or_true]
      exact ⟨_, 1, rfl, one_ne_zero⟩
    · simp only [hx, or_false, exists_eq_right]
      exact ⟨_, rfl, hx⟩

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