Grace/Cumulus/Algebra/Polynomial/BundledEvaluation.g17

Open in Workbench Download source

Imports

Bundled · EvaluationOver

Declarations

Source

1-- Evaluation of bundled polynomials: evaluationHom(R, S, I, f, v), the2-- homomorphism polynomialRing(R, I) →+* S sending the constants through3-- f : R →+* S and the variable X(R, I, j) to v(j), its universal property,4-- and evaluationAt(R, I, v) at a point of the coefficient ring; everything5-- here is ZF6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Polynomial.BundledEvaluation12import Bundled13import EvaluationOver1415-- Evaluation at an assignment v : I → S through a coefficient16-- homomorphism f, and at a point v : I → R of the coefficient ring itself.17def evaluationHom (R S I f v : Set) : Set :=18  polynomialAtOver(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,19    S.carrier, S.add, S.zero, S.neg, S.mul, S.one, f, v)20def evaluationAt (R I v : Set) : Set :=21  polynomialAt(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)2223theorem evaluationHom.graph (R S I f v : Set)24  shows evaluationHom(R, S, I, f, v) =25    polynomialAtOver(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one,26      S.carrier, S.add, S.zero, S.neg, S.mul, S.one, f, v)27proof28  simp [evaluationHom]2930theorem evaluationAt.graph (R I v : Set)31  shows evaluationAt(R, I, v) =32    polynomialAt(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)33proof34  simp [evaluationAt]3536section Evaluation37variable (R S I f v : Set)38notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)39notation ring L := (S.carrier, S.add, S.zero, S.neg, S.mul, S.one)40notation ring P := K[I]41hypothesis source : CommRing(R)42hypothesis target : CommRing(S)43hypothesis hom : f : R →+* S44hypothesis assignment : v : I → S.carrier4546theorem evaluationHom.hom47  shows evaluationHom(R, S, I, f, v) : polynomialRing(R, I) →+* S48proof49  have sourceParts := CommRing.parts with source50  have targetParts := CommRing.parts with target51  have homParts := RingHom.parts with hom52  have engine := polynomialAtOver.hom with sourceParts, targetParts,53    homParts, assignment54  rw evaluationHom.graph55  exact RingHom.polynomial_of_parts with source, target, engine5657instance evaluationHom.map_mem (p : polynomialRing(R, I))58  shows evaluationHom(R, S, I, f, v)(p) ∈ S59proof60  have evaluation := evaluationHom.hom at R, S, I, f, v with *61  exact RingHom.map_mem with *6263theorem evaluationHom.map_constant (a : R)64  shows evaluationHom(R, S, I, f, v)(polynomialConstant(R, I)(a)) = f(a)65proof66  have sourceParts := CommRing.parts with source67  have targetParts := CommRing.parts with target68  have homParts := RingHom.parts with hom69  have aIn : a ∈ R by assumption70  have engine := polynomialAtOver.constant with sourceParts, targetParts,71    homParts, assignment, aIn72  rw [polynomialConstant.apply, evaluationHom.graph]73  exact engine7475theorem evaluationHom.map_X (j : Set)76  requires index : j ∈ I77  shows evaluationHom(R, S, I, f, v)(X(R, I, j)) = v(j)78proof79  have sourceParts := CommRing.parts with source80  have targetParts := CommRing.parts with target81  have homParts := RingHom.parts with hom82  have engine := polynomialAtOver.variable with sourceParts, targetParts,83    homParts, assignment, index84  rw [X.value, evaluationHom.graph]85  exact engine8687-- A homomorphism agreeing with f on the constants and with v on the88-- variables is the evaluation.89theorem evaluationHom.unique (g : Set)90  requires candidate : g : polynomialRing(R, I) →+* S91  requires constants : ∀ a ∈ R, g(polynomialConstant(R, I)(a)) = f(a)92  requires variables : ∀ j ∈ I, g(X(R, I, j)) = v(j)93  shows g = evaluationHom(R, S, I, f, v)94proof95  have sourceParts := CommRing.parts with source96  have targetParts := CommRing.parts with target97  have homParts := RingHom.parts with hom98  have engineHom := RingHom.polynomial_parts with source, target, candidate99  have engineConstants : ∀ a ∈ R, g(polynomialConstant(I, K, a)) = f(a)100    intros a ha101    rw ← polynomialConstant.apply102    exact constants with a, ha103  have engineVariables : ∀ j ∈ I, g(polynomialVariable(I, K, j)) = v(j)104    intros j hj105    rw ← X.value106    exact variables with j, hj107  rw evaluationHom.graph108  exact polynomialAtOver.unique with sourceParts, targetParts, homParts,109    assignment, engineHom, engineConstants, engineVariables110111-- The universal property of the polynomial ring: exactly one homomorphism112-- extends f along the constants and sends each variable to its value.113theorem polynomialRing.universal114  shows (evaluationHom(R, S, I, f, v) : polynomialRing(R, I) →+* S) ∧115    (∀ a ∈ R,116      evaluationHom(R, S, I, f, v)(polynomialConstant(R, I)(a)) = f(a)) ∧117    (∀ j ∈ I, evaluationHom(R, S, I, f, v)(X(R, I, j)) = v(j)) ∧118    (∀ g, (g : polynomialRing(R, I) →+* S) →119      (∀ a ∈ R, g(polynomialConstant(R, I)(a)) = f(a)) →120      (∀ j ∈ I, g(X(R, I, j)) = v(j)) → g = evaluationHom(R, S, I, f, v))121proof122  have evaluation := evaluationHom.hom at R, S, I, f, v with *123  refine ⟨evaluation, ?_, ?_, ?_⟩124  . intros a ha125    exact evaluationHom.map_constant with *126  . intros j hj127    exact evaluationHom.map_X with *128  . intros g candidate constants variables129    exact evaluationHom.unique with *130131end Evaluation132133section Points134variable (R I v : Set)135notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)136notation ring P := K[I]137hypothesis comm : CommRing(R)138hypothesis assignment : v : I → R.carrier139140theorem evaluationAt.hom141  shows evaluationAt(R, I, v) : polynomialRing(R, I) →+* R142proof143  have parts := CommRing.parts with comm144  have engine := polynomialAt.hom with parts, assignment145  rw evaluationAt.graph146  exact RingHom.polynomial_of_parts with comm, comm, engine147148instance evaluationAt.map_mem (p : polynomialRing(R, I))149  shows evaluationAt(R, I, v)(p) ∈ R150proof151  have evaluation := evaluationAt.hom at R, I, v with *152  exact RingHom.map_mem with *153154theorem evaluationAt.map_constant (a : R)155  shows evaluationAt(R, I, v)(polynomialConstant(R, I)(a)) = a156proof157  have parts := CommRing.parts with comm158  have aIn : a ∈ R by assumption159  have engine := polynomialAt.constant with parts, assignment, aIn160  rw [polynomialConstant.apply, evaluationAt.graph]161  exact engine162163theorem evaluationAt.map_X (j : Set)164  requires index : j ∈ I165  shows evaluationAt(R, I, v)(X(R, I, j)) = v(j)166proof167  have parts := CommRing.parts with comm168  have engine := polynomialAt.variable with parts, assignment, index169  rw [X.value, evaluationAt.graph]170  exact engine171172theorem evaluationAt.surjective173  shows SurjectiveBetween(evaluationAt(R, I, v),174    Ring.carrier(polynomialRing(R, I)), R.carrier)175proof176  have parts := CommRing.parts with comm177  have engine := polynomialAt.surjective with parts, assignment178  rw [evaluationAt.graph, polynomialRing.carrierOf]179  exact engine180181-- Evaluation at a point is evaluation through the identity of R.182theorem evaluationAt.eq_evaluationHom183  shows evaluationAt(R, I, v) = evaluationHom(R, R, I, identity(R.carrier), v)184proof185  have parts := CommRing.parts with comm186  have engine := polynomialAtOver.identity_coefficients with parts, assignment187  rw [evaluationAt.graph, evaluationHom.graph]188  symm189  exact engine190191end Points192