PolynomialBaseChange

Polynomial base change, evaluation, and algebraic independence

Open in Workbench View on GitHub

1-- Polynomial base change, evaluation, and algebraic independence.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialBaseChange8import Grace.Cumulus.Algebra.Polynomial.EvaluationOver910section Rings11variable (I A add z neg mul one B plus o minus times unit f v : Set)12notation ring R := (A, add, z, neg, mul, one)13notation ring S := (B, plus, o, minus, times, unit)14notation ring P := R[I]15notation ring Q := S[I]16hypothesis source : IsCommRing(R)17hypothesis target : IsCommRing(S)18hypothesis hom : IsRingHom(f, R, S)1920theorem map_is_hom21  shows IsRingHom(polynomialMap(I, R, S, f), P, Q)22proof23  exact polynomialMap.hom with *2425theorem faithful_base_change26  requires injective : InjectiveBetween(f, R, S)27  shows InjectiveBetween(polynomialMap(I, R, S, f), P, Q)28proof29  exact polynomialMap.injective with *3031theorem evaluation_is_hom32  requires assignment : v : I → S33  shows IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)34proof35  exact polynomialAtOver.hom with *3637theorem evaluate_variable (j : Set)38  requires assignment : v : I → S39  requires index : j ∈ I40  shows polynomialAtOver(I, R, S, f, v)(polynomialVariable(I, R, j)) = v(j)41proof42  exact polynomialAtOver.variable with *4344theorem no_polynomial_relation (p : Set)45  requires assignment : v : I → S46  requires independent : AlgebraicallyIndependent(I, R, S, f, v)47  requires polynomial : p ∈ P48  shows polynomialAtOver(I, R, S, f, v)(p) = S[0] ↔ p = P[0]49proof50  exact AlgebraicallyIndependent.relation_iff with *5152end Rings5354section Canonical55variable (I A add z neg mul one : Set)56notation ring R := (A, add, z, neg, mul, one)57notation ring P := R[I]58hypothesis ring : IsCommRing(R)5960theorem canonical_independence61  shows AlgebraicallyIndependent(I, R, P, polynomialCoefficients(I, R), polynomialVariables(I, R))62proof63  exact polynomialVariables.algebraically_independent with *6465end Canonical66