Grace/Cumulus/Algebra/Polynomial/EvaluationOver.g17

Open in Workbench Download source

Imports

MapHom · Universal

Declarations

Source

1-- Polynomial evaluation over a coefficient homomorphism and algebraic independence.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.EvaluationOver8import MapHom9import Universal1011def polynomialAtOver (I A add z neg mul one B plus o minus times unit f v : Set) : Set :=12  compose(polynomialAt(I, B, plus, o, minus, times, unit, v), polynomialMap(I, A, z, B, o, f), polynomials(I, A, z), polynomials(I, B, o), B)1314notation scoped polynomialAtOver(I, R, S, f, v) => polynomialAtOver(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S.carrier, S.add, S.zero, S.neg, S.mul, S.one, f, v)1516predicate AlgebraicallyIndependent (I A add z neg mul one B plus o minus times unit f v : Set) :=17  IsRingHom(f, A, add, z, neg, mul, one, B, plus, o, minus, times, unit) ∧ FunctionBetween(v, I, B) ∧ InjectiveBetween(polynomialAtOver(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v), polynomials(I, A, z), B)1819notation scoped AlgebraicallyIndependent(I, R, S, f, v) => AlgebraicallyIndependent(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S.carrier, S.add, S.zero, S.neg, S.mul, S.one, f, v)2021section Rings22variable (I A add z neg mul one B plus o minus times unit f v : Set)23notation ring R := (A, add, z, neg, mul, one)24notation ring S := (B, plus, o, minus, times, unit)25notation ring P := R[I]26notation ring Q := S[I]27hypothesis source : IsCommRing(R)28hypothesis target : IsCommRing(S)29hypothesis hom : IsRingHom(f, R, S)30hypothesis assignment : v : I → S3132theorem polynomialAtOver.hom33  shows IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)34proof35  have mapped : IsRingHom(polynomialMap(I, R, S, f), P, Q)36    exact polynomialMap.hom with *37  have evaluated := polynomialAt.hom with *38  unfold polynomialAtOver39  exact IsRingHom.compose with *4041theorem polynomialAtOver.value (p : Set)42  requires polynomial : p ∈ P43  shows polynomialAtOver(I, R, S, f, v)(p) = polynomialAt(I, S, v)(polynomialMap(I, R, S, f)(p))44proof45  have mapHom : IsRingHom(polynomialMap(I, R, S, f), P, Q)46    exact polynomialMap.hom with *47  have evaluationHom := polynomialAt.hom with *48  have map := IsRingHom.function with mapHom49  have evaluation := IsRingHom.function with evaluationHom50  unfold polynomialAtOver51  exact compose.apply with *5253theorem polynomialAtOver.constant (a : Set)54  requires coefficient : a ∈ R55  shows polynomialAtOver(I, R, S, f, v)(polynomialConstant(I, R, a)) = f(a)56proof57  have zeroIn : R[0] ∈ R by typecheck58  have member := polynomialConstant.member at I, A, z, a with *59  have image := IsRingHom.closed with hom, coefficient60  have mapped := polynomialMap.constant at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, a with *61  have evaluated := polynomialAt.constant with *62  rwa [polynomialAtOver.value, mapped]6364theorem polynomialAtOver.coefficient_image65  shows functionImage(f, R, S) ⊆ functionImage(polynomialAtOver(I, R, S, f, v), P, S)66proof67  have evaluation : IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)68    exact polynomialAtOver.hom with *69  have function := IsRingHom.function with evaluation70  have zeroIn : R[0] ∈ R by typecheck71  intros x member72  obtain ⟨inS, a, coefficient, shape⟩ := functionImage.membership.forward with member73  have constant := polynomialConstant.member at I, A, z, a with *74  have value := polynomialAtOver.constant at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, a with *75  have image := functionImage.value at polynomialAtOver(I, R, S, f, v), P, S, polynomialConstant(I, R, a) with *76  rw value at image77  rwa shape7879theorem polynomialAtOver.variable (j : Set)80  requires index : j ∈ I81  shows polynomialAtOver(I, R, S, f, v)(polynomialVariable(I, R, j)) = v(j)82proof83  have zeroIn : R[0] ∈ R by typecheck84  have oneIn : R[1] ∈ R by typecheck85  have member := polynomialVariable.member at I, A, z, one, j with *86  have mapped := polynomialMap.variable at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, j with *87  have evaluated := polynomialAt.variable with *88  rwa [polynomialAtOver.value, mapped]8990theorem polynomialAtOver.unique (h : Set)91  requires morphism : IsRingHom(h, P, S)92  requires constants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = f(a)93  requires variables : ∀ j ∈ I, h(polynomialVariable(I, R, j)) = v(j)94  shows h = polynomialAtOver(I, R, S, f, v)95proof96  have evaluation : IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)97    exact polynomialAtOver.hom with *98  have sameConstants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = polynomialAtOver(I, R, S, f, v)(polynomialConstant(I, R, a))99    intros a ha100    have first := constants with a, ha101    have second := polynomialAtOver.constant with *102    cc103  have sameVariables : ∀ j ∈ I, h(polynomialVariable(I, R, j)) = polynomialAtOver(I, R, S, f, v)(polynomialVariable(I, R, j))104    intros j hj105    have first := variables with j, hj106    have second := polynomialAtOver.variable at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, j with *107    cc108  exact IsRingHom.polynomial_ext with *109110theorem AlgebraicallyIndependent.relation_iff (p : Set)111  requires independent : AlgebraicallyIndependent(I, R, S, f, v)112  requires polynomial : p ∈ P113  shows polynomialAtOver(I, R, S, f, v)(p) = S[0] ↔ p = P[0]114proof115  have evaluation : IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)116    exact polynomialAtOver.hom with *117  have zero := IsRingHom.zero with evaluation118  have zeroMember := polynomials.zero at I, A, add, z, neg, mul, one with *119  have injective := independent.right.right120  constructor121  . intro vanishes122    have equal : polynomialAtOver(I, R, S, f, v)(p) = polynomialAtOver(I, R, S, f, v)(P[0]) by cc123    exact Injective.apply_cancel with *124  . intro equal125    rwa equal126127theorem AlgebraicallyIndependent.of_no_relation128  requires relations : ∀ p ∈ P, polynomialAtOver(I, R, S, f, v)(p) = S[0] → p = P[0]129  shows AlgebraicallyIndependent(I, R, S, f, v)130proof131  have evaluation : IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)132    exact polynomialAtOver.hom with *133  have function := IsRingHom.function with evaluation134  have sourceRing := polynomials.comm_ring at I, A, add, z, neg, mul, one with *135  have ordinary := IsCommRing.ring with sourceRing136  unfold AlgebraicallyIndependent137  refine ⟨hom, assignment, ?_⟩138  unfold InjectiveBetween139  refine ⟨function, ?_⟩140  intros p hp q hq y hy first second141  have valueP := FunctionBetween.apply_value at polynomialAtOver(I, R, S, f, v), P, S, p, y with *142  have valueQ := FunctionBetween.apply_value at polynomialAtOver(I, R, S, f, v), P, S, q, y with *143  have negative := IsRing.neg_closed with ordinary, hq144  have difference : P[p - q] ∈ P145    exact IsRing.add_closed with *146  have mapped := IsRingHom.sub with sourceRing, evaluation, hp, hq147  have zero : polynomialAtOver(I, R, S, f, v)(P[p - q]) = S[0]148    rw [mapped, valueP, valueQ]149    ring150  have vanishes := relations with P[p - q], difference, zero151  linear_combination vanishes152153end Rings154section Canonical155variable (I A add z neg mul one : Set)156notation ring R := (A, add, z, neg, mul, one)157notation ring P := R[I]158hypothesis ring : IsCommRing(R)159160theorem polynomialAtOver.identity_coefficients (v : Set)161  requires assignment : v : I → R162  shows polynomialAtOver(I, R, R, identity(R), v) = polynomialAt(I, R, v)163proof164  have hom := IsRingHom.identity with ring165  have evaluation := polynomialAt.hom with *166  have constants : ∀ a ∈ R, polynomialAt(I, R, v)(polynomialConstant(I, R, a)) = identity(R)(a)167    intros a ha168    have value := polynomialAt.constant with *169    have same := identity.apply with *170    cc171  have variables : ∀ j ∈ I, polynomialAt(I, R, v)(polynomialVariable(I, R, j)) = v(j)172    intros j hj173    exact polynomialAt.variable with *174  symm175  exact polynomialAtOver.unique with *176177theorem polynomialAtOver.canonical_variables178  shows polynomialAtOver(I, R, P, polynomialCoefficients(I, R), polynomialVariables(I, R)) = identity(P)179proof180  have target := polynomials.comm_ring at I, A, add, z, neg, mul, one with *181  have hom := polynomialCoefficients.hom at I, A, add, z, neg, mul, one with *182  have zeroIn : R[0] ∈ R by typecheck183  have oneIn : R[1] ∈ R by typecheck184  have assignment := polynomialVariables.function at I, A, z, one with *185  have identity := IsRingHom.identity with target186  have constants : ∀ a ∈ R, identity(P)(polynomialConstant(I, R, a)) = polynomialCoefficients(I, R)(a)187    intros a ha188    have member := polynomialConstant.member at I, A, z, a with *189    have value := polynomialCoefficients.value at I, A, z, a with *190    have same := identity.apply with member191    cc192  have variables : ∀ j ∈ I, identity(P)(polynomialVariable(I, R, j)) = polynomialVariables(I, R)(j)193    intros j hj194    have member := polynomialVariable.member at I, A, z, one, j with *195    have value := polynomialVariables.value at I, A, z, one, j with *196    have same := identity.apply with member197    cc198  symm199  exact polynomialAtOver.unique with *200201theorem polynomialVariables.algebraically_independent202  shows AlgebraicallyIndependent(I, R, P, polynomialCoefficients(I, R), polynomialVariables(I, R))203proof204  have hom := polynomialCoefficients.hom at I, A, add, z, neg, mul, one with *205  have zeroIn : R[0] ∈ R by typecheck206  have oneIn : R[1] ∈ R by typecheck207  have assignment := polynomialVariables.function at I, A, z, one with *208  have evaluation := polynomialAtOver.canonical_variables at I, A, add, z, neg, mul, one with *209  have injective := identity.injective at P210  unfold AlgebraicallyIndependent211  refine ⟨hom, assignment, ?_⟩212  rwa evaluation213214end Canonical215