Grace/Cumulus/Algebra/Polynomial/Transfer.g17

Open in Workbench Download source

Imports

EvaluationSupport

Declarations

Source

1-- Moving a polynomial between variable sets, preserving supported evaluations (ZF).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.Transfer8import EvaluationSupport910defgraph polynomialTransferVariables (I J A z one : Set) (i ∈ I) : polynomials(J, A, z) := polynomialVariable(J, A, z, one, i)11requires zeroIn : z ∈ A12requires oneIn : one ∈ A13proof14  exact polynomialVariable.member with *1516def polynomialTransfer (I J A add z neg mul one : Set) : Set :=17  polynomialAtOver(I, A, add, z, neg, mul, one, polynomials(J, A, z), polynomialAdd(J, A, add, z, neg, mul, one), constantFunction(monomials(J), A, z), polynomialNeg(J, A, add, z, neg, mul, one), polynomialMul(J, A, add, z, neg, mul, one), polynomialConstant(J, A, z, one), polynomialCoefficients(J, A, z), polynomialTransferVariables(I, J, A, z, one))1819notation scoped polynomialTransfer(I, J, R) => polynomialTransfer(I, J, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)2021section Rings22variable (I J A add z neg mul one : Set)23notation ring R := (A, add, z, neg, mul, one)24notation ring P := R[I]25notation ring Q := R[J]26hypothesis ring : IsCommRing(R)2728theorem polynomialTransfer.hom29  shows IsRingHom(polynomialTransfer(I, J, R), P, Q)30proof31  have target : IsCommRing(Q)32    exact polynomials.comm_ring with *33  have coefficients : IsRingHom(polynomialCoefficients(J, R), R, Q)34    exact polynomialCoefficients.hom with *35  have zeroIn : R[0] ∈ R by typecheck36  have oneIn : R[1] ∈ R by typecheck37  have assignment := polynomialTransferVariables.function at I, J, A, z, one with *38  unfold polynomialTransfer39  exact polynomialAtOver.hom with *4041theorem polynomialTransfer.constant (a : Set)42  requires coefficient : a ∈ R43  shows polynomialTransfer(I, J, R)(polynomialConstant(I, R, a)) = polynomialConstant(J, R, a)44proof45  have target : IsCommRing(Q)46    exact polynomials.comm_ring with *47  have coefficients : IsRingHom(polynomialCoefficients(J, R), R, Q)48    exact polynomialCoefficients.hom with *49  have zeroIn : R[0] ∈ R by typecheck50  have oneIn : R[1] ∈ R by typecheck51  have assignment := polynomialTransferVariables.function at I, J, A, z, one with *52  have value := polynomialCoefficients.value at J, A, z, a with *53  unfold polynomialTransfer54  rwa polynomialAtOver.constant5556theorem polynomialTransfer.variable (i : Set)57  requires index : i ∈ I58  shows polynomialTransfer(I, J, R)(polynomialVariable(I, R, i)) = polynomialVariable(J, R, i)59proof60  have target : IsCommRing(Q)61    exact polynomials.comm_ring with *62  have coefficients : IsRingHom(polynomialCoefficients(J, R), R, Q)63    exact polynomialCoefficients.hom with *64  have zeroIn : R[0] ∈ R by typecheck65  have oneIn : R[1] ∈ R by typecheck66  have assignment := polynomialTransferVariables.function at I, J, A, z, one with *67  have value := polynomialTransferVariables.value at I, J, A, z, one, i with *68  unfold polynomialTransfer69  rwa polynomialAtOver.variable7071theorem polynomialTransfer.outside_variable (i : Set)72  requires index : i ∈ I73  requires outside : ¬(i ∈ J)74  shows polynomialTransfer(I, J, R)(polynomialVariable(I, R, i)) = Q[1]75proof76  have mapped := polynomialTransfer.variable at I, J, A, add, z, neg, mul, one, i with *77  have monomial := monomialVariable.member at J, i78  have unit := monomialOne.member at J79  have same : monomialVariable(J, i) = monomialOne(J)80    apply monomials.ext with monomial, unit81    intros k member82    have distinct : k ≠ i83      intro equal84      rw equal at member85      exact outside with member86    have value := coefficientSingle.other at J, ℕ, (0:Nat), (1:Nat), i, k with *87    have zero := monomialOne.value at J, k with *88    unfold monomialVariable89    cc90  rw mapped91  simp [polynomialVariable, polynomialConstant]9293section Evaluation94variable (B plus o minus times unit f v w : Set)95notation ring S := (B, plus, o, minus, times, unit)96hypothesis target : IsCommRing(S)97hypothesis hom : IsRingHom(f, R, S)98hypothesis first : v : I → S99hypothesis second : w : J → S100101theorem polynomialTransfer.evaluate_supported (p : Set)102  requires polynomial : p ∈ P103  requires supported : polynomialVariablesUsed(I, R, p) ⊆ J104  requires agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), v(i) = w(i)105  shows polynomialAtOver(J, R, S, f, w)(polynomialTransfer(I, J, R)(p)) = polynomialAtOver(I, R, S, f, v)(p)106proof107  have transfer : IsRingHom(polynomialTransfer(I, J, R), P, Q)108    exact polynomialTransfer.hom with *109  have evaluationI : IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)110    exact polynomialAtOver.hom with *111  have evaluationJ : IsRingHom(polynomialAtOver(J, R, S, f, w), Q, S)112    exact polynomialAtOver.hom with *113  have sourceRing : IsCommRing(P)114    exact polynomials.comm_ring with *115  have combined := IsRingHom.compose with sourceRing, transfer, evaluationJ116  have functionT := IsRingHom.function with transfer117  have functionJ := IsRingHom.function with evaluationJ118  have zeroIn : R[0] ∈ R by typecheck119  have oneIn : R[1] ∈ R by typecheck120  have constants : ∀ a ∈ R, compose(polynomialAtOver(J, R, S, f, w), polynomialTransfer(I, J, R), P, Q, S)(polynomialConstant(I, R, a)) = f(a)121    intros a coefficient122    have member := polynomialConstant.member at I, A, z, a with *123    have composed := compose.apply at polynomialAtOver(J, R, S, f, w), polynomialTransfer(I, J, R), P, Q, S, polynomialConstant(I, R, a) with *124    have mapped := polynomialTransfer.constant at I, J, A, add, z, neg, mul, one, a with *125    have evaluated := polynomialAtOver.constant at J, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, w, a with *126    cc127  have originals : ∀ a ∈ R, polynomialAtOver(I, R, S, f, v)(polynomialConstant(I, R, a)) = f(a)128    intros a coefficient129    exact polynomialAtOver.constant with *130  have variables : ∀ i ∈ polynomialVariablesUsed(I, R, p), compose(polynomialAtOver(J, R, S, f, w), polynomialTransfer(I, J, R), P, Q, S)(polynomialVariable(I, R, i)) = polynomialAtOver(I, R, S, f, v)(polynomialVariable(I, R, i))131    intros i used132    have subset := polynomialVariablesUsed.subset at I, A, z, p133    have inI := subset with i, used134    have inJ := supported with i, used135    have member := polynomialVariable.member at I, A, z, one, i with *136    have composed := compose.apply at polynomialAtOver(J, R, S, f, w), polynomialTransfer(I, J, R), P, Q, S, polynomialVariable(I, R, i) with *137    have mapped := polynomialTransfer.variable at I, J, A, add, z, neg, mul, one, i with *138    have evaluated := polynomialAtOver.variable at J, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, w, i with *139    have original := polynomialAtOver.variable at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, i with *140    have same := agreement with i, used141    cc142  have equal := IsRingHom.polynomial_local_ext with *143  have value := compose.apply at polynomialAtOver(J, R, S, f, w), polynomialTransfer(I, J, R), P, Q, S, p with *144  cc145146end Evaluation147148theorem polynomialTransfer.roundtrip (p : Set)149  requires polynomial : p ∈ P150  requires supported : polynomialVariablesUsed(I, R, p) ⊆ J151  shows polynomialTransfer(J, I, R)(polynomialTransfer(I, J, R)(p)) = p152proof153  have target : IsCommRing(P)154    exact polynomials.comm_ring with *155  have coefficients : IsRingHom(polynomialCoefficients(I, R), R, P)156    exact polynomialCoefficients.hom with *157  have zeroIn : R[0] ∈ R by typecheck158  have oneIn : R[1] ∈ R by typecheck159  have first := polynomialVariables.function at I, A, z, one with *160  have second := polynomialTransferVariables.function at J, I, A, z, one with *161  have agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), polynomialVariables(I, R)(i) = polynomialTransferVariables(J, I, A, z, one)(i)162    intros i used163    have subset := polynomialVariablesUsed.subset at I, A, z, p164    have inI := subset with i, used165    have included := supported166    have inJ := included with i, used167    have left := polynomialVariables.value at I, A, z, one, i with *168    have right := polynomialTransferVariables.value at J, I, A, z, one, i with *169    cc170  have equal : polynomialAtOver(J, R, P, polynomialCoefficients(I, R), polynomialTransferVariables(J, I, A, z, one))(polynomialTransfer(I, J, R)(p)) = polynomialAtOver(I, R, P, polynomialCoefficients(I, R), polynomialVariables(I, R))(p)171    exact polynomialTransfer.evaluate_supported with *172  have canonical := polynomialAtOver.canonical_variables at I, A, add, z, neg, mul, one with *173  rw canonical at equal174  have identity := identity.apply at p, P with *175  unfold polynomialTransfer at equal176  unfold polynomialTransfer177  cc178179theorem polynomialTransfer.nonzero_supported (p : Set)180  requires polynomial : p ∈ P181  requires supported : polynomialVariablesUsed(I, R, p) ⊆ J182  requires nonzero : p ≠ P[0]183  shows polynomialTransfer(I, J, R)(p) ≠ Q[0]184proof185  have reverse : IsRingHom(polynomialTransfer(J, I, R), Q, P)186    exact polynomialTransfer.hom with *187  have zero := IsRingHom.zero with reverse188  have recovered := polynomialTransfer.roundtrip with *189  intro vanishes190  apply nonzero191  cc192193theorem polynomialTransfer.injective194  requires subset : I ⊆ J195  shows InjectiveBetween(polynomialTransfer(I, J, R), P, Q)196proof197  have hom : IsRingHom(polynomialTransfer(I, J, R), P, Q)198    exact polynomialTransfer.hom with *199  have function := IsRingHom.function with hom200  unfold InjectiveBetween201  refine ⟨function, ?_⟩202  intros p hp q hq y hy first second203  have valueP := FunctionBetween.apply_value at polynomialTransfer(I, J, R), P, Q, p, y with *204  have valueQ := FunctionBetween.apply_value at polynomialTransfer(I, J, R), P, Q, q, y with *205  have usedP := polynomialVariablesUsed.subset at I, A, z, p206  have usedQ := polynomialVariablesUsed.subset at I, A, z, q207  have supportedP := Subset.transitive with usedP, subset208  have supportedQ := Subset.transitive with usedQ, subset209  have recoveredP := polynomialTransfer.roundtrip at I, J, A, add, z, neg, mul, one, p with *210  have recoveredQ := polynomialTransfer.roundtrip at I, J, A, add, z, neg, mul, one, q with *211  cc212213end Rings214