Grace/Cumulus/Algebra/Polynomial/EvaluationSupport.g17

Open in Workbench Download source

Imports

EvaluationOver · Variables

Declarations

Source

1-- Polynomial homomorphisms depend only on the variables actually used (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.EvaluationSupport8import EvaluationOver9import Variables1011theorem polynomialMap.variables (I A z B o f p : Set)12  requires function : f : A → B13  requires zero : f(z) = o14  requires polynomial : p ∈ polynomials(I, A, z)15  shows polynomialVariablesUsed(I, B, o, polynomialMap(I, A, z, B, o, f)(p)) ⊆ polynomialVariablesUsed(I, A, z, p)16proof17  intros i used18  obtain ⟨m, support, exponent⟩ := polynomialVariablesUsed.membership.forward with used19  obtain ⟨monomial, nonzero⟩ := functionSupport.membership.forward with support20  have value := polynomialMap.coefficient with *21  have coefficient : p(m) ≠ z22    intro vanishes23    apply nonzero24    cc25  have original : m ∈ functionSupport(p, monomials(I), z)26    exact functionSupport.membership.backward with ⟨monomial, coefficient⟩27  exact polynomialVariablesUsed.membership.backward with ⟨m, original, exponent⟩2829defgraph polynomialHomVariables (I A z one B h : Set) (i ∈ I) : B := h(polynomialVariable(I, A, z, one, i))30requires zeroIn : z ∈ A31requires oneIn : one ∈ A32requires function : h : polynomials(I, A, z) → B33proof34  have variableIn := polynomialVariable.member at I, A, z, one, i with *35  exact FunctionBetween.apply_closed with function, variableIn3637section Rings38variable (I A add z neg mul one B plus o minus times unit f : Set)39notation ring R := (A, add, z, neg, mul, one)40notation ring S := (B, plus, o, minus, times, unit)41notation ring P := R[I]42hypothesis source : IsCommRing(R)43hypothesis target : IsCommRing(S)44hypothesis hom : IsRingHom(f, R, S)4546theorem polynomialAtOver.agree_on_variables (v w p : Set)47  requires first : v : I → S48  requires second : w : I → S49  requires polynomial : p ∈ P50  requires agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), v(i) = w(i)51  shows polynomialAtOver(I, R, S, f, v)(p) = polynomialAtOver(I, R, S, f, w)(p)52proof53  have function := IsRingHom.function with hom54  have zero := IsRingHom.zero with hom55  have mapped := polynomialMap.member with *56  have variables := polynomialMap.variables with *57  have same : ∀ i ∈ polynomialVariablesUsed(I, S, polynomialMap(I, R, S, f)(p)), v(i) = w(i)58    intros i used59    have original := variables with i, used60    exact agreement with i, original61  have equal := polynomialAt.agree_on_variables at I, B, plus, o, minus, times, unit, v, w, polynomialMap(I, R, S, f)(p) with *62  have left := polynomialAtOver.value at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, p with *63  have right := polynomialAtOver.value at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, w, p with *64  cc6566theorem IsRingHom.polynomial_local_ext (h g p : Set)67  requires first : IsRingHom(h, P, S)68  requires second : IsRingHom(g, P, S)69  requires polynomial : p ∈ P70  requires firstConstants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = f(a)71  requires secondConstants : ∀ a ∈ R, g(polynomialConstant(I, R, a)) = f(a)72  requires agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), h(polynomialVariable(I, R, i)) = g(polynomialVariable(I, R, i))73  shows h(p) = g(p)74proof75  have zeroIn : R[0] ∈ R by typecheck76  have oneIn : R[1] ∈ R by typecheck77  have functionH := IsRingHom.function with first78  have functionG := IsRingHom.function with second79  have assignmentH := polynomialHomVariables.function at I, A, z, one, B, h with *80  have assignmentG := polynomialHomVariables.function at I, A, z, one, B, g with *81  have variablesH : ∀ i ∈ I, h(polynomialVariable(I, R, i)) = polynomialHomVariables(I, A, z, one, B, h)(i)82    intros i index83    symm84    exact polynomialHomVariables.value with *85  have variablesG : ∀ i ∈ I, g(polynomialVariable(I, R, i)) = polynomialHomVariables(I, A, z, one, B, g)(i)86    intros i index87    symm88    exact polynomialHomVariables.value with *89  have representationH := polynomialAtOver.unique at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialHomVariables(I, A, z, one, B, h), h with *90  have representationG := polynomialAtOver.unique at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialHomVariables(I, A, z, one, B, g), g with *91  have same : ∀ i ∈ polynomialVariablesUsed(I, R, p), polynomialHomVariables(I, A, z, one, B, h)(i) = polynomialHomVariables(I, A, z, one, B, g)(i)92    intros i used93    have subset := polynomialVariablesUsed.subset at I, A, z, p94    have index := subset with i, used95    have left := variablesH with i, index96    have right := variablesG with i, index97    have equal := agreement with i, used98    cc99  have equal := polynomialAtOver.agree_on_variables with *100  rwa [representationH, representationG]101102end Rings103