English
If two polynomials have all coefficients up to degree d equal, they are equal in the polynomial ring sense.
Русский
Если два многочлена имеют равные все коэффициенты до степени d, они равны как элементы кольца полиномов.
LaTeX
$$$A_i_0 = A_i_1$ при совпадении коэффициентов до степени d.$$
Lean4
/-- If `A` is a family of enough low-degree polynomials over a finite semiring, there is a
pair of equal elements in `A`. -/
theorem exists_eq_polynomial [Semiring Fq] {d : ℕ} {m : ℕ} (hm : Fintype.card Fq ^ d ≤ m) (b : Fq[X])
(hb : natDegree b ≤ d) (A : Fin m.succ → Fq[X]) (hA : ∀ i, degree (A i) < degree b) :
∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀ := by
-- Since there are > q^d elements of A, and only q^d choices for the highest `d` coefficients,
-- there must be two elements of A with the same coefficients at
-- `0`, ... `degree b - 1` ≤ `d - 1`.
-- In other words, the following map is not injective:
set f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff j
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
simpa using
lt_of_le_of_lt hm
(Nat.lt_succ_self m)
-- Therefore, the differences have all coefficients higher than `deg b - d` equal.
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
use i₀, i₁, i_ne
ext j
by_cases hbj : degree b ≤ j
·
rw [coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj), coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj)]
-- So we only need to look for the coefficients between `0` and `deg b`.
rw [not_le] at hbj
apply congr_fun i_eq.symm ⟨j, _⟩
exact lt_of_lt_of_le (coe_lt_degree.mp hbj) hb
