PolynomialUniversal

Polynomial uniqueness and reconstruction of a point from its residue field (ZF)

Open in Workbench View on GitHub

1-- Polynomial uniqueness and reconstruction of a point from its residue field (ZF).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 PolynomialUniversal8import Grace.Cumulus.Algebra.Polynomial.ResidueCriterion910section Evaluation11variable (I A add zero neg mul one h : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring P := R[I]14hypothesis ring : IsCommRing(R)15hypothesis hom : IsRingHom(h, P, R)1617theorem evaluation_is_determined_by_variable_values18  requires constants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = a19  shows h = polynomialAt(I, R, polynomialValues(I, R, h))20proof21  exact IsRingHom.eq_polynomialAt with ring, hom, constants2223end Evaluation2425section Residues26variable (I A add zero neg mul one J : Set)27notation ring R := (A, add, zero, neg, mul, one)28notation ring P := R[I]29notation ring Q := P ⧸ J30hypothesis field : IsField(R)31hypothesis maximal : IsMaximalIdeal(P, J)3233theorem a_point_exists_exactly_when_coefficients_fill_the_residue_field34  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q) ↔ ∃ v, PolynomialCommonZero(I, A, add, zero, neg, mul, one, J, v)35proof36  exact polynomialResidueCoefficients.surjective_iff_common_zero at I, A, add, zero, neg, mul, one, J with *3738end Residues39