Equation from N to ZMod p

Stream: general

[Nick_adfor]

How to prove

            have h : coeff b (∑ i, X i) = (1 : ℕ) := by
              dsimp [b]
              exact coeff_eq
            have : (coeff b (∑ i, X i) : ZMod p) = (1 : ZMod p) := by
              rw [← Nat.cast_one (R := ZMod p)]
              have : (coeff b (∑ i, X i) : ZMod p) = ((coeff b (∑ i, X i) : ℕ) : ZMod p) := by sorry
              rw [this, h]
              exact Nat.cast_one

[Aaron Liu]

Can you give a #mwe?

[Nick_adfor]

The origin code is too long and hard to extract one. So I mean that if there's some lemma to solve the problem from equality in N to equality in ZMod p

[Aaron Liu]

what is the type of b? what is the type of X?

[Aaron Liu]

is coeff just Polynomial.coeff or is it something else

[Nick_adfor]

article precise.lean
It is MvPolynomial.coeff. The whole code is here and the sorry is in line 296

[Nick_adfor]

If I try rfl it will give me

Tactic `rfl` failed: The left-hand side
  coeff b (∑ i, X i)
is not definitionally equal to the right-hand side
  ↑(coeff b (∑ i, X i))

So I'm wondering if it is really a correct one.

[Ruben Van de Velde]

Let me show you how to minimize your question without needing to think about it:

import Mathlib

open Finsupp

open scoped Finset

variable {R : Type*} [CommRing R]

open MvPolynomial

/-- Lemma 2.2 :
A multivariate polynomial that vanishes on a large product finset is the zero polynomial. -/
lemma eq_zero_of_eval_zero_at_prod_finset {σ : Type*} [Finite σ] [IsDomain R]
    (P : MvPolynomial σ R) (S : σ → Finset R)
    (Hdeg : ∀ i, P.degreeOf i < #(S i))
    (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x P = 0) :
    P = 0 := by
      exact MvPolynomial.eq_zero_of_eval_zero_at_prod_finset P S Hdeg Heval

variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

/-- Definition of elimination polynomials g_i -/
noncomputable def elimination_polynomials (A : Fin (k + 1) → Finset (ZMod p)) :
    Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p) :=
  fun i => ∏ a ∈ A i, (MvPolynomial.X i - C a)

noncomputable def reduce_polynomial_degrees (P : MvPolynomial (Fin (k + 1)) (ZMod p))
    (g : Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p))
    (c : Fin (k + 1) → ℕ) : MvPolynomial (Fin (k + 1)) (ZMod p) :=

  P.support.sum fun m =>
    let coeff := P.coeff m
    let needs_replacement : Finset (Fin (k + 1)) :=
      Finset.filter (fun i => m i > c i) Finset.univ
    if h : needs_replacement.Nonempty then
      let i : Fin (k + 1) := needs_replacement.min' h
      let new_m : (Fin (k + 1)) →₀ ℕ :=
        Finsupp.update m i (m i - (c i + 1))
      coeff • (MvPolynomial.monomial new_m 1) * g i
    else
      coeff • MvPolynomial.monomial m 1

theorem ANR_polynomial_method (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (A : Fin (k + 1) → Finset (ZMod p))
    (c : Fin (k + 1) → ℕ)
    (hA : ∀ i, (A i).card = c i + 1)
    (m : ℕ) (hm : m = (∑ i, c i) - h.totalDegree)
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0) :
    let S : Finset (ZMod p) :=
      (Fintype.piFinset A).filter (fun f => h.eval f ≠ 0) |>.image (fun f => ∑ i, f i)
    S.card ≥ m + 1 ∧ m < p := by
  -- Define the restricted sumset S
  set S : Finset (ZMod p) :=
  ((Fintype.piFinset A).filter (fun f => h.eval f ≠ 0)).image (fun f => ∑ i, f i) with hS_def

  -- Step 1: Prove |S| >= m + 1 by contradiction
  have hS_card : S.card ≥ m + 1 := by
    by_contra! H

    have hS_size : S.card ≤ m := by omega
    obtain ⟨E, hE_sub, hE_card⟩ : ∃ E : Multiset (ZMod p), S.val ⊆ E ∧ E.card = m := sorry

    -- Define the polynomial Q
    set sumX : MvPolynomial (Fin (k + 1)) (ZMod p) := ∑ i, MvPolynomial.X i with hsumX_def
    set Q : MvPolynomial (Fin (k + 1)) (ZMod p) :=
      h * (E.map (fun e => sumX - C e)).prod with hQ_def

    -- Q vanishes on prod A_i
    have hQ_total_deg : Q.totalDegree = ∑ i, c i := by
      rw [hQ_def, hsumX_def]
      have h_prod_deg : ((E.map (fun e => sumX - C e)).prod).totalDegree = m := by
        rw [hsumX_def]
        have degree_of_each : ∀ e : ZMod p, (sumX - C e).totalDegree = 1 := by
          intro e
          rw [hsumX_def]
          have : (∑ i : Fin (k + 1), X i - C e) = (∑ i, X i) + (-C e) := by rw [sub_eq_add_neg]
          rw [MvPolynomial.totalDegree]
          apply le_antisymm
          · sorry
          simp
          let b : (Fin (k + 1)) →₀ ℕ := Finsupp.single (0 : Fin (k + 1)) 1
          refine ⟨b, ?_, ?_⟩
          · have coeff_eq : coeff (Finsupp.single (0 : Fin (k + 1)) 1) (∑ i, X i) = 1 := by sorry
            rw [show b = Finsupp.single (0 : Fin (k + 1)) 1 by rfl] at *

            have : b = Finsupp.single (0 : Fin (k + 1)) 1 := rfl
            rw [← this]
            have b_ne_zero : b ≠ 0 := by sorry
            have : ¬(0 = b) := Ne.symm b_ne_zero
            simp [this]
            change coeff b (∑ i, X i) ≠ 0
            have h1 : (1 : ℕ) ≠ (0 : ZMod p) := by sorry
            have h : coeff b (∑ i, X i) = (1 : ℕ) := by sorry
            have : (coeff b (∑ i, X i) : ZMod p) = (1 : ZMod p) := by
              rw [← Nat.cast_one (R := ZMod p)]
              have : (coeff b (∑ i, X i) : ZMod p) = ((coeff b (∑ i, X i) : ℕ) : ZMod p) := by sorry -- <--
              rw [this, h]
            simp_all
          · sorry
        sorry
      sorry
    sorry

[Nick_adfor]

Okay, I've seen you sorry all the following goal and -- <-- the needed one.

[Aaron Liu]

I have rw [← Nat.coe_castRingHom, ← coeff_map, map_sum]; simp

[Ruben Van de Velde]

I ended up with

              have : (coeff b (∑ i, X i) : ZMod p) = ((coeff b (∑ i, X i) : ℕ) : ZMod p) := by
                rw [coeff_sum, coeff_sum]
                simp
                apply Finset.sum_congr rfl fun i _ => ?_
                rw [coeff_single_X]
                rw [coeff_single_X]
                simp

[Ruben Van de Velde]

Or even

              have : (coeff b (∑ i, X i) : ZMod p) = ((coeff b (∑ i, X i) : ℕ) : ZMod p) := by
                simp [coeff_sum, ‹b = _›]

[Nick_adfor]

Ruben Van de Velde said:

Or even

              have : (coeff b (∑ i, X i) : ZMod p) = ((coeff b (∑ i, X i) : ℕ) : ZMod p) := by
                simp [coeff_sum, ‹b = _›]

I've never seen things like ‹b = _›

[Nick_adfor]

Aaron Liu said:

I have rw [← Nat.coe_castRingHom, ← coeff_map, map_sum]; simp

I can understand coeff_map but I'm not familiar with coe_castRingHom :(

[Ruben Van de Velde]

Yeah, I should have just used simp [coeff_sum, b]

[Aaron Liu]

docs#Nat.coe_castRingHom the ringhom version of Nat.cast is Nat.castRingHom, this lemma says they're the same underlying function

[Ruben Van de Velde]

The "French quotes" mean "the assumption in your context that looks like this", that is, the have : b = Finsupp.single (0 : Fin (k + 1)) 1 := rfl above (because you had another hypothesis called this in between, I couldn't use it by name)

[Nick_adfor]

It's really a pity that coeff_map and coeff_sum do not have @[simp] ......