Grace/Cumulus/Algebra/Polynomial/Constants.g17

Open in Workbench Download source

Imports

Ring

Declarations

Source

1-- The canonical, injective coefficient-ring embedding into polynomials (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.Constants8import Ring910defgraph polynomialCoefficients (I A zero : Set) (a ∈ A) : polynomials(I, A, zero) := polynomialConstant(I, A, zero, a)11requires zeroIn : zero ∈ A12proof13  exact polynomialConstant.member at I, A, zero, a with *1415notation scoped polynomialCoefficients(I, R) => polynomialCoefficients(I, R.carrier, R.zero)1617theorem polynomialConstant.value (I A zero a m : Set)18  requires zeroIn : zero ∈ A19  requires coefficient : a ∈ A20  requires monomial : m ∈ monomials(I)21  shows polynomialConstant(I, A, zero, a)(m) = singleValue(A, zero, a, monomialOne(I), m)22proof23  unfold polynomialConstant24  unfold polynomialTerm25  exact coefficientSingle.value at monomials(I), A, zero, a, monomialOne(I), m with *2627theorem polynomialConstant.zero (I A zero : Set)28  requires zeroIn : zero ∈ A29  shows polynomialConstant(I, A, zero, zero) = constantFunction(monomials(I), A, zero)30proof31  have member := polynomialConstant.member at I, A, zero, zero with *32  have function := polynomials.function with member33  have target := constantFunction.function at monomials(I), A, zero with *34  apply FunctionBetween.ext with function, target35  intros m hm36  have value := polynomialConstant.value at I, A, zero, zero, m with *37  have selected := singleValue.zero at A, zero, monomialOne(I), m with *38  have constant := constantFunction.apply at monomials(I), A, m, zero with *39  cc4041section Rings42variable (I A add zero neg mul one : Set)43hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)44notation ring R := (A, add, zero, neg, mul, one)4546theorem polynomialConstant.add (a b : Set)47  requires coefficientA : a ∈ A48  requires coefficientB : b ∈ A49  shows polynomialConstant(I, A, zero, a + b) = coefficientAdd(monomials(I), A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a), polynomialConstant(I, A, zero, b))50proof51  have ordinary := IsCommRing.ring with ring52  have zeroIn := IsRing.zero_in_carrier with ordinary53  have sumIn := IsRing.add_closed at A, add, zero, neg, mul, one, a, b with *54  have memberA := polynomialConstant.member at I, A, zero, a with *55  have memberB := polynomialConstant.member at I, A, zero, b with *56  have memberSum := polynomialConstant.member at I, A, zero, a + b with *57  have functionA := polynomials.function with memberA58  have functionB := polynomials.function with memberB59  have functionSum := polynomials.function with memberSum60  have target := coefficientAdd.function at monomials(I), A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a), polynomialConstant(I, A, zero, b) with *61  apply FunctionBetween.ext with functionSum, target62  intros m hm63  have left := polynomialConstant.value at I, A, zero, a + b, m with *64  have valueA := polynomialConstant.value at I, A, zero, a, m with *65  have valueB := polynomialConstant.value at I, A, zero, b, m with *66  have right := coefficientAdd.value at monomials(I), A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a), polynomialConstant(I, A, zero, b), m with *67  have distribute := singleValue.add at A, add, zero, neg, mul, one, a, b, monomialOne(I), m with *68  cc6970theorem polynomialConstant.neg (a : Set)71  requires coefficient : a ∈ A72  shows polynomialConstant(I, A, zero, -a) = coefficientNeg(monomials(I), A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a))73proof74  have ordinary := IsCommRing.ring with ring75  have zeroIn := IsRing.zero_in_carrier with ordinary76  have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, a with *77  have memberA := polynomialConstant.member at I, A, zero, a with *78  have memberNeg := polynomialConstant.member at I, A, zero, -a with *79  have functionA := polynomials.function with memberA80  have functionNeg := polynomials.function with memberNeg81  have target := coefficientNeg.function at monomials(I), A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a) with *82  apply FunctionBetween.ext with functionNeg, target83  intros m hm84  have left := polynomialConstant.value at I, A, zero, -a, m with *85  have valueA := polynomialConstant.value at I, A, zero, a, m with *86  have right := coefficientNeg.value at monomials(I), A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a), m with *87  have alternatives : m = monomialOne(I) ∨ m ≠ monomialOne(I) by tauto88  cases alternatives with same | different89  . have selectA := singleValue.same at A, zero, a, monomialOne(I), m with *90    have selectNeg := singleValue.same at A, zero, -a, monomialOne(I), m with *91    cc92  . have selectA := singleValue.other at A, zero, a, monomialOne(I), m with *93    have selectNeg := singleValue.other at A, zero, -a, monomialOne(I), m with *94    have negZero : -zero = zero by ring95    cc9697theorem polynomialConstant.mul (a b : Set)98  requires coefficientA : a ∈ A99  requires coefficientB : b ∈ A100  shows polynomialConstant(I, A, zero, a * b) = polynomialProduct(I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, a), polynomialConstant(I, A, zero, b))101proof102  have unit := monomialOne.member at I103  have terms := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, b, monomialOne(I), monomialOne(I) with *104  have unitLaw := monomialProduct.one with *105  unfold polynomialConstant106  cc107108theorem polynomialCoefficients.hom109  shows IsRingHom(polynomialCoefficients(I, A, zero), A, add, zero, neg, mul, one, polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))110proof111  have ordinary := IsCommRing.ring with ring112  have zeroIn := IsRing.zero_in_carrier with ordinary113  have multiplicative := IsRing.multiplicative with ordinary114  have oneIn := IsMonoid.unit_in_carrier with multiplicative115  have function := polynomialCoefficients.function at I, A, zero with *116  have zeroValue := polynomialCoefficients.value at I, A, zero, zero with *117  have zeroLaw := polynomialConstant.zero at I, A, zero with *118  have oneValue := polynomialCoefficients.value at I, A, zero, one with *119  have preservesZero : polynomialCoefficients(I, A, zero)(zero) = constantFunction(monomials(I), A, zero) by cc120  have preservesNeg : ∀ x ∈ A, polynomialCoefficients(I, A, zero)(-x) = (polynomialNeg(I, A, add, zero, neg, mul, one))(polynomialCoefficients(I, A, zero)(x))121    intros x hx122    have negative := IsRing.neg_closed with hx123    have member := polynomialConstant.member at I, A, zero, x with *124    have source := polynomialCoefficients.value at I, A, zero, -x with *125    have value := polynomialCoefficients.value at I, A, zero, x with *126    have target := polynomialNeg.apply with *127    have law := polynomialConstant.neg at I, A, add, zero, neg, mul, one, x with *128    cc129  have preservesAdd : ∀ x ∈ A, ∀ y ∈ A, polynomialCoefficients(I, A, zero)(x + y) = (polynomialAdd(I, A, add, zero, neg, mul, one))(polynomialCoefficients(I, A, zero)(x), polynomialCoefficients(I, A, zero)(y))130    intros x hx y hy131    have closed := IsRing.add_closed with hx, hy132    have memberX := polynomialConstant.member at I, A, zero, x with *133    have memberY := polynomialConstant.member at I, A, zero, y with *134    have source := polynomialCoefficients.value at I, A, zero, x + y with *135    have valueX := polynomialCoefficients.value at I, A, zero, x with *136    have valueY := polynomialCoefficients.value at I, A, zero, y with *137    have target := polynomialAdd.apply at I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, x), polynomialConstant(I, A, zero, y) with *138    have law := polynomialConstant.add at I, A, add, zero, neg, mul, one, x, y with *139    cc140  have preservesMul : ∀ x ∈ A, ∀ y ∈ A, polynomialCoefficients(I, A, zero)(x * y) = (polynomialMul(I, A, add, zero, neg, mul, one))(polynomialCoefficients(I, A, zero)(x), polynomialCoefficients(I, A, zero)(y))141    intros x hx y hy142    have closed := IsRing.mul_closed with hx, hy143    have memberX := polynomialConstant.member at I, A, zero, x with *144    have memberY := polynomialConstant.member at I, A, zero, y with *145    have source := polynomialCoefficients.value at I, A, zero, x * y with *146    have valueX := polynomialCoefficients.value at I, A, zero, x with *147    have valueY := polynomialCoefficients.value at I, A, zero, y with *148    have target := polynomialMul.apply at I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, x), polynomialConstant(I, A, zero, y) with *149    have law := polynomialConstant.mul at I, A, add, zero, neg, mul, one, x, y with *150    cc151  unfold IsRingHom152  refine ⟨function, preservesZero, oneValue, preservesNeg, preservesAdd, preservesMul⟩153154end Rings155156theorem polynomialCoefficients.injective (I A zero : Set)157  requires zeroIn : zero ∈ A158  shows InjectiveBetween(polynomialCoefficients(I, A, zero), A, polynomials(I, A, zero))159proof160  have function := polynomialCoefficients.function at I, A, zero with *161  constructor162  . exact function163  . intros x hx y hy z hz hxz hyz164    have valueX := FunctionBetween.apply_value at polynomialCoefficients(I, A, zero), A, polynomials(I, A, zero), x, z with *165    have valueY := FunctionBetween.apply_value at polynomialCoefficients(I, A, zero), A, polynomials(I, A, zero), y, z with *166    have constantX := polynomialCoefficients.value at I, A, zero, x with *167    have constantY := polynomialCoefficients.value at I, A, zero, y with *168    have equal : polynomialConstant(I, A, zero, x) = polynomialConstant(I, A, zero, y) by cc169    exact polynomialConstant.injective at I, A, zero, x, y with *170