BundledPolynomials
Bundled polynomial rings: the ring polynomialRing(R, I) over a bundled
1-- Bundled polynomial rings: the ring polynomialRing(R, I) over a bundled2-- coefficient ring, ring arithmetic on its elements, evaluation at a point3-- through the homomorphism laws, the point ideal over a field, and the4-- factor theorem in Horner form.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module BundledPolynomials11import Grace.Cumulus.Algebra.Polynomial.BundledIdeals12import Grace.Cumulus.Algebra.Polynomial.BundledRoots1314-- Under CommRing(R) the instance polynomialRing.comm_ring makes15-- polynomialRing(R, I) a commutative ring, and the instance supplies the16-- ring the way a hypothesis does: a binder (p : polynomialRing(R, I)) is17-- membership in its carrier, its elements carry the ring notation, and18-- `ring` proves identities between polynomials.19section Polynomials20variable (R I : Set)21hypothesis comm : CommRing(R)2223theorem difference_of_squares (p q : polynomialRing(R, I))24 shows (p + q) * (p - q) = p * p - q * q25proof26 ring2728-- Evaluation at a point v : I → R is a homomorphism sending X_j to v(j)29-- and a constant to itself.30theorem evaluate_square_plus (v j : Set) (a : R)31 requires assignment : v : I → R.carrier32 requires index : j ∈ I33 shows evaluationAt(R, I, v)(X(R, I, j) * X(R, I, j) +34 polynomialConstant(R, I)(a)) = v(j) * v(j) + a35proof36 have evaluation := evaluationAt.hom with comm, assignment37 rw [RingHom.map_add, RingHom.map_mul, evaluationAt.map_X,38 evaluationAt.map_constant]39 rfl40end Polynomials4142-- Over a field the point ideal is maximal, and X - a divides a Horner43-- polynomial vanishing at a.44section Fields45variable (R : Set)46hypothesis field : Field(R)4748theorem point_ideal_maximal (I v : Set)49 requires assignment : v : I → R.carrier50 shows MaximalIdeal(polynomialRing(R, I), pointIdeal(R, I, v))51proof52 exact MaximalIdeal.point with *5354theorem factor (leading a x c : R) (cs : List(R.carrier))55 requires root : horner(R, leading, a, c :: cs) = R[0]56 shows horner(R, leading, x, c :: cs) =57 (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))58proof59 have comm := Field.to_comm_ring with field60 exact horner.factor with *61end Fields62