Grace/Cumulus/Algebra/Polynomial/Nonvanishing.g17

Open in Workbench Download source

Imports

HornerReconstruction · HornerNormalization

Declarations

Source

1-- Nonvanishing of sparse multivariate polynomials over infinite fields (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.Nonvanishing8import HornerReconstruction9import HornerNormalization1011theorem polynomialVariablesUsed.empty_constant (I A z p : Set)12  requires zeroIn : z ∈ A13  requires polynomial : p ∈ polynomials(I, A, z)14  requires unused : polynomialVariablesUsed(I, A, z, p) ⊆ ∅15  shows p = polynomialConstant(I, A, z, p(monomialOne(I)))16proof17  have unit := monomialOne.member at I18  have coefficient := polynomials.coefficient with *19  have constant := polynomialConstant.member at I, A, z, p(monomialOne(I)) with *20  apply polynomials.ext with polynomial, constant21  intros m monomial22  have alternatives : m = monomialOne(I) ∨ m ≠ monomialOne(I) by tauto23  cases alternatives with same | different24  . rw same25    symm26    exact polynomialConstant.coefficient with *27  . have vanishes : p(m) = z28      by_contra nonzero29      have supported : m ∈ functionSupport(p, monomials(I), z)30        exact functionSupport.membership.backward with ⟨monomial, nonzero⟩31      have exponents : ∀ i ∈ I, m(i) = monomialOne(I)(i)32        intros i index33        have zero := monomialOne.value with index34        rw zero35        by_contra present36        have inSupport : i ∈ functionSupport(m, I, 0) := functionSupport.membership.backward with ⟨index, present⟩37        have used : i ∈ polynomialVariablesUsed(I, A, z, p)38          exact polynomialVariablesUsed.membership.backward with ⟨m, supported, inSupport⟩39        have impossible := unused with i, used40        exact set.empty with impossible41      have equal := monomials.ext with *42      exact different with equal43    have value := polynomialConstant.value at I, A, z, p(monomialOne(I)), m with *44    have selected := singleValue.other at A, z, p(monomialOne(I)), monomialOne(I), m with *45    cc4647section Fields48variable (I A add z neg mul one : Set)49notation ring R := (A, add, z, neg, mul, one)50notation ring P := R[I]51hypothesis field : IsField(R)52hypothesis infinite : ¬Finite(R)5354theorem polynomialAt.nonvanishing_from_coefficient (p j v : Set, n : Nat)55  requires polynomial : p ∈ P56  requires index : j ∈ I57  requires assignment : v : I → R58  requires nonzero : polynomialAt(I, R, v)(polynomialVariableCoefficient(I, R, p, j, n)) ≠ z59  shows ∃ w, FunctionBetween(w, I, R) ∧ polynomialAt(I, R, w)(p) ≠ z60proof61  have ring := IsField.comm_ring with field62  have zeroIn : z ∈ R by typecheck63  have polynomialRing := polynomials.comm_ring at I, A, add, z, neg, mul, one with *64  have zeroMember : P[0] ∈ P by typecheck65  obtain ⟨cs, list, coefficients⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *66  have hom := polynomialAt.hom with *67  have function := IsRingHom.function with hom68  have zeroValue := IsRingHom.zero with hom69  have lookup := listCoefficient.map at P, A, polynomialAt(I, R, v), P[0], cs, n with *70  have value := coefficients with n71  have scalarNonzero : ∃ k, Nat(k) ∧ listCoefficient{A}(z, listMap{P}(polynomialAt(I, R, v), cs), k) ≠ z72    refine ⟨n, assumption, ?_⟩73    rw [zeroValue, value] at lookup74    rwa lookup75  obtain ⟨a, element, avoids⟩ := hornerAt.exists_nonzero_of_coefficient at A, add, z, neg, mul, one, listMap{P}(polynomialAt(I, R, v), cs) with *76  have updated := coefficientErase.function at I, A, a, v, j with *77  have coordinate := coefficientErase.same at I, A, a, v, j with *78  have away : ∀ i ∈ I, i ≠ j → v(i) = coefficientErase(I, A, a, v, j)(i)79    intros i hi different80    symm81    exact coefficientErase.other with *82  have same : ∀ k, Nat(k) → polynomialAt(I, R, v)(listCoefficient{P}(P[0], cs, k)) = polynomialAt(I, R, coefficientErase(I, A, a, v, j))(listCoefficient{P}(P[0], cs, k))83    intros k natural84    have coefficient := coefficients with k, natural85    rw coefficient86    exact polynomialVariableCoefficient.agree_away with *87  have maps := listMap.congr_coefficients with *88  have evaluation := polynomialAt.reconstruction at I, A, add, z, neg, mul, one, p, j, coefficientErase(I, A, a, v, j), cs with *89  refine ⟨coefficientErase(I, A, a, v, j), updated, ?_⟩90  rwa [evaluation, coordinate, ← maps]9192theorem polynomialAt.nonvanishing_on_list (p : Set) (xs : List(I))93  requires polynomial : p ∈ P94  requires nonzero : p ≠ P[0]95  requires variables : polynomialVariablesUsed(I, A, z, p) ⊆ listSupport{I}(xs)96  shows ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(p) ≠ z97proof98  induction xs generalizing p99  | List.nil =>100    intros p polynomial nonzero variables101    have ring := IsField.comm_ring with field102    have zeroIn : z ∈ R by typecheck103    rw listSupport at variables104    have constant := polynomialVariablesUsed.empty_constant with *105    have unit := monomialOne.member at I106    have coefficient := polynomials.coefficient with *107    have different : p(monomialOne(I)) ≠ z108      intro equal109      have zero := polynomialConstant.zero at I, A, z with *110      apply nonzero111      rwa [constant, equal]112    have assignment := constantFunction.function at I, A, z with *113    have evaluation := polynomialAt.constant with coefficient114    refine ⟨constantFunction(I, A, z), assignment, ?_⟩115    rwa [constant, evaluation]116  | List.cons(j, tail) using ih =>117    intros p polynomial nonzero variables118    have index : j ∈ I by assumption119    have ring := IsField.comm_ring with field120    have zeroIn : z ∈ R by typecheck121    obtain ⟨n, nIn, coefficientNonzero⟩ := polynomialVariableCoefficient.exists_nonzero at I, A, z, p, j with *122    have natural := nat.omega.backward with nIn123    have coefficient := polynomialVariableCoefficient.member at I, A, z, p, j, n with *124    have smaller := polynomialVariableCoefficient.variables at I, A, z, p, j, n with *125    have bounded : polynomialVariablesUsed(I, A, z, polynomialVariableCoefficient(I, R, p, j, n)) ⊆ listSupport{I}(tail)126      intros i hi127      have reduced := smaller with i, hi128      obtain ⟨used, absent⟩ := difference.membership.forward with reduced129      have member := variables with i, used130      rw listSupport at member131      have alternatives := insert.membership.forward with member132      cases alternatives with same | old133      . exfalso134        apply absent135        exact singleton.membership.backward with same136      . exact old137    obtain ⟨v, assignment, value⟩ := ih with polynomialVariableCoefficient(I, R, p, j, n), coefficient, coefficientNonzero, bounded138    exact polynomialAt.nonvanishing_from_coefficient with *139140theorem polynomialAt.exists_nonzero (p : Set)141  requires polynomial : p ∈ P142  requires nonzero : p ≠ P[0]143  shows ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(p) ≠ z144proof145  have finite := polynomialVariablesUsed.finite with *146  have subset := polynomialVariablesUsed.subset at I, A, z, p147  obtain ⟨xs, list, covers⟩ := Finite.cover_in at polynomialVariablesUsed(I, A, z, p), I with *148  exact polynomialAt.nonvanishing_on_list with *149150theorem polynomialAt.ext (p q : Set)151  requires left : p ∈ P152  requires right : q ∈ P153  requires agreement : ∀ v, FunctionBetween(v, I, R) → polynomialAt(I, R, v)(p) = polynomialAt(I, R, v)(q)154  shows p = q155proof156  have ring := IsField.comm_ring with field157  have source := polynomials.comm_ring at I, A, add, z, neg, mul, one with *158  have ordinary := IsCommRing.ring with source159  have negative := IsRing.neg_closed with ordinary, right160  have difference : P[p - q] ∈ P161    exact IsRing.add_closed with *162  by_contra different163  have nonzero : P[p - q] ≠ P[0]164    intro vanishes165    apply different166    linear_combination vanishes167  obtain ⟨v, assignment, value⟩ := polynomialAt.exists_nonzero at I, A, add, z, neg, mul, one, P[p - q] with *168  have hom := polynomialAt.hom with *169  have mapped := IsRingHom.sub with source, hom, left, right170  have same := agreement with v, assignment171  have inQ := IsRingHom.closed with hom, right172  apply value173  rw [mapped, same]174  ring175176end Fields177