Grace/Cumulus/Algebra/Polynomial/MapHom.g17

Open in Workbench Download source

Imports

CoefficientMap · Set.OrderTransport

Declarations

Source

1-- Multiplicativity of coefficient maps and polynomial base change (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.MapHom8import CoefficientMap9import Set.OrderTransport1011predicate PolynomialMapMultiplies (I A add z neg mul one B plus o minus times unit f p q : Set) :=12  polynomialMap(I, A, z, B, o, f)(polynomialProduct(I, A, add, z, neg, mul, one, p, q)) = polynomialProduct(I, B, plus, o, minus, times, unit, polynomialMap(I, A, z, B, o, f)(p), polynomialMap(I, A, z, B, o, f)(q))1314def polynomialMapProducts (I A add z neg mul one B plus o minus times unit f p : Set) : Set :=15  {q ∈ polynomials(I, A, z) | PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, q)}1617section Rings18variable (I A add z neg mul one B plus o minus times unit f : Set)19notation ring R := (A, add, z, neg, mul, one)20notation ring S := (B, plus, o, minus, times, unit)21notation ring P := R[I]22notation ring Q := S[I]23hypothesis source : IsCommRing(R)24hypothesis target : IsCommRing(S)25hypothesis hom : IsRingHom(f, R, S)2627theorem PolynomialMapMultiplies.zero (p : Set)28  requires memberP : p ∈ P29  shows PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, P[0])30proof31  have function := IsRingHom.function with hom32  have zero := IsRingHom.zero with hom33  have mapped := polynomialMap.member with *34  have sourceZero := polynomialProduct.zero_right at I, A, add, z, neg, mul, one, p with *35  have targetZero := polynomialProduct.zero_right at I, B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p) with *36  have mapZero := polynomialMap.zero at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f with *37  unfold PolynomialMapMultiplies38  cc3940theorem PolynomialMapMultiplies.swap (p q : Set)41  requires memberP : p ∈ P42  requires memberQ : q ∈ P43  requires equation : PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, q)44  shows PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q, p)45proof46  have function := IsRingHom.function with hom47  have zero := IsRingHom.zero with hom48  have mappedP := polynomialMap.member at I, A, z, B, o, f, p with *49  have mappedQ := polynomialMap.member at I, A, z, B, o, f, q with *50  have first := polynomialProduct.commutative at I, A, add, z, neg, mul, one, p, q with *51  have second := polynomialProduct.commutative at I, B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p), polynomialMap(I, R, S, f)(q) with *52  unfold PolynomialMapMultiplies at equation53  unfold PolynomialMapMultiplies54  cc5556theorem PolynomialMapMultiplies.add (p q r : Set)57  requires memberP : p ∈ P58  requires memberQ : q ∈ P59  requires memberR : r ∈ P60  requires first : PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, q)61  requires second : PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, r)62  shows PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, coefficientAdd(monomials(I), A, add, z, neg, mul, one, q, r))63proof64  have function := IsRingHom.function with hom65  have zero := IsRingHom.zero with hom66  have mappedP := polynomialMap.member at I, A, z, B, o, f, p with *67  have mappedQ := polynomialMap.member at I, A, z, B, o, f, q with *68  have mappedR := polynomialMap.member at I, A, z, B, o, f, r with *69  have pq := polynomialProduct.member at I, A, add, z, neg, mul, one, p, q with *70  have pr := polynomialProduct.member at I, A, add, z, neg, mul, one, p, r with *71  have sourceLaw := polynomialProduct.add_right at I, A, add, z, neg, mul, one, p, q, r with *72  have targetLaw := polynomialProduct.add_right at I, B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p), polynomialMap(I, R, S, f)(q), polynomialMap(I, R, S, f)(r) with *73  have sum := polynomialMap.coefficient_add at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q, r with *74  have products := polynomialMap.coefficient_add at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialProduct(I, A, add, z, neg, mul, one, p, q), polynomialProduct(I, A, add, z, neg, mul, one, p, r) with *75  unfold PolynomialMapMultiplies at first76  unfold PolynomialMapMultiplies at second77  unfold PolynomialMapMultiplies78  cc7980theorem PolynomialMapMultiplies.terms (a b m n : Set)81  requires coefficientA : a ∈ R82  requires coefficientB : b ∈ R83  requires monomialM : m ∈ monomials(I)84  requires monomialN : n ∈ monomials(I)85  shows PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m), polynomialTerm(I, A, z, b, n))86proof87  have ordinary := IsCommRing.ring with source88  have coefficient := IsRing.mul_closed with ordinary, coefficientA,89    coefficientB90  have imageA := IsRingHom.closed with hom, coefficientA91  have imageB := IsRingHom.closed with hom, coefficientB92  have monomial := monomialProduct.member at I, m, n with *93  have sourceLaw := polynomialProduct.terms at I, A, add, z, neg, mul, one, a, b, m, n with *94  have targetLaw := polynomialProduct.terms at I, B, plus, o, minus, times, unit, f(a), f(b), m, n with *95  have left := polynomialMap.term at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, a, m with *96  have right := polynomialMap.term at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, b, n with *97  have product := polynomialMap.term at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, R[a * b], monomialProduct(I, m, n) with *98  have preserved := IsRingHom.mul with hom, coefficientA, coefficientB99  unfold PolynomialMapMultiplies100  cc101102theorem PolynomialMapMultiplies.term (a m q : Set)103  requires coefficient : a ∈ A104  requires monomial : m ∈ monomials(I)105  requires memberQ : q ∈ polynomials(I, A, z)106  shows PolynomialMapMultiplies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m), q)107proof108  have ordinary := IsCommRing.ring with source109  have zeroIn := IsRing.zero_in_carrier with ordinary110  have zeroPolynomial := polynomials.zero at I, A, add, z, neg, mul, one with *111  have fixed := polynomialTerm.member at I, A, z, a, m with *112  have base : constantFunction(monomials(I), A, z) ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m))113    apply polynomialMapProducts.membership.backward114    constructor115    . exact zeroPolynomial116    . exact PolynomialMapMultiplies.zero with *117  have terms : ∀ b ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, z, b, n) ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m))118    intros b hb n hn119    have member := polynomialTerm.member at I, A, z, b, n with *120    apply polynomialMapProducts.membership.backward121    constructor122    . exact member123    . exact PolynomialMapMultiplies.terms with *124  have sums : ∀ u ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m)), ∀ v ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m)), coefficientAdd(monomials(I), A, add, z, neg, mul, one, u, v) ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m))125    intros u hf v hg126    have first := polynomialMapProducts.membership.forward with hf127    have second := polynomialMapProducts.membership.forward with hg128    have member := polynomials.add at I, A, add, z, neg, mul, one, u, v with *129    apply polynomialMapProducts.membership.backward130    constructor131    . exact member132    . exact PolynomialMapMultiplies.add with *133  have generated := polynomials.induction at I, A, add, z, neg, mul, one, polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialTerm(I, A, z, a, m)), q with *134  have result := polynomialMapProducts.membership.forward with generated135  exact result.right136137theorem polynomialMap.product (p q : Set)138  requires memberP : p ∈ P139  requires memberQ : q ∈ P140  shows polynomialMap(I, R, S, f)(polynomialProduct(I, A, add, z, neg, mul, one, p, q)) = polynomialProduct(I, B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p), polynomialMap(I, R, S, f)(q))141proof142  have ordinary := IsCommRing.ring with source143  have zeroIn := IsRing.zero_in_carrier with ordinary144  have zeroPolynomial := polynomials.zero at I, A, add, z, neg, mul, one with *145  have base : constantFunction(monomials(I), A, z) ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q)146    apply polynomialMapProducts.membership.backward147    constructor148    . exact zeroPolynomial149    . exact PolynomialMapMultiplies.zero with *150  have terms : ∀ b ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, z, b, n) ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q)151    intros b hb n hn152    have member := polynomialTerm.member at I, A, z, b, n with *153    apply polynomialMapProducts.membership.backward154    constructor155    . exact member156    . have forward := PolynomialMapMultiplies.term at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, b, n, q with *157      exact PolynomialMapMultiplies.swap with *158  have sums : ∀ u ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q), ∀ v ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q), coefficientAdd(monomials(I), A, add, z, neg, mul, one, u, v) ∈ polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q)159    intros u hf v hg160    have first := polynomialMapProducts.membership.forward with hf161    have second := polynomialMapProducts.membership.forward with hg162    have member := polynomials.add at I, A, add, z, neg, mul, one, u, v with *163    apply polynomialMapProducts.membership.backward164    constructor165    . exact member166    . exact PolynomialMapMultiplies.add with *167  have generated := polynomials.induction at I, A, add, z, neg, mul, one, polynomialMapProducts(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q), p with *168  have result := polynomialMapProducts.membership.forward with generated169  exact PolynomialMapMultiplies.swap at170    I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, q, p with *171172theorem polynomialMap.mul (p q : Set)173  requires left : p ∈ P174  requires right : q ∈ P175  shows polynomialMap(I, R, S, f)(P[p * q]) = Q[polynomialMap(I, R, S, f)(p) * polynomialMap(I, R, S, f)(q)]176proof177  have function := IsRingHom.function with hom178  have zero := IsRingHom.zero with hom179  have mappedLeft := polynomialMap.member at I, A, z, B, o, f, p with *180  have mappedRight := polynomialMap.member at I, A, z, B, o, f, q with *181  have first := polynomialMul.apply at I, A, add, z, neg, mul, one, p, q with *182  have second := polynomialMul.apply at I, B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p), polynomialMap(I, R, S, f)(q) with *183  have value := polynomialMap.product at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, q with *184  cc185186theorem polynomialMap.hom187  shows IsRingHom(polynomialMap(I, R, S, f), P, Q)188proof189  have function := IsRingHom.function with hom190  have zero := IsRingHom.zero with hom191  have map := polynomialMap.function at I, A, z, B, o, f with *192  have sourceRing := polynomials.comm_ring at I, A, add, z, neg, mul, one with *193  have targetRing := polynomials.comm_ring at I, B, plus, o, minus, times, unit with *194  apply IsRingHom.of_add_mul_one with sourceRing, targetRing, map195  . intros p left q right196    exact polynomialMap.add with *197  . intros p left q right198    exact polynomialMap.mul with *199  . have oneIn : R[1] ∈ R200      typecheck201    have value := polynomialMap.constant at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, one with *202    have oneValue := IsRingHom.one with hom203    cc204205theorem polynomialMap.injective206  requires injective : InjectiveBetween(f, R, S)207  shows InjectiveBetween(polynomialMap(I, R, S, f), P, Q)208proof209  have function := IsRingHom.function with hom210  have zero := IsRingHom.zero with hom211  have map := polynomialMap.function at I, A, z, B, o, f with *212  unfold InjectiveBetween213  refine ⟨map, ?_⟩214  intros p hp q hq r hr first second215  have valueP := FunctionBetween.apply_value at polynomialMap(I, R, S, f), P, Q, p, r with *216  have valueQ := FunctionBetween.apply_value at polynomialMap(I, R, S, f), P, Q, q, r with *217  apply polynomials.ext with hp, hq218  intros m hm219  have memberP := polynomials.coefficient with hp, hm220  have memberQ := polynomials.coefficient with hq, hm221  have coefficientP := polynomialMap.coefficient with hp, hm222  have coefficientQ := polynomialMap.coefficient with hq, hm223  have equal : f(p(m)) = f(q(m)) by cc224  exact Injective.apply_cancel with *225226end Rings227