Grace/Cumulus/Algebra/Polynomial/Ring.g17

Open in Workbench Download source

Imports

Associativity

Declarations

Source

1-- Actual polynomial operation graphs and their commutative-ring structure (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.Ring8import Associativity910defunique polynomialPairAdd (I A add zero neg mul one t : Set) (s ∈ polynomials(I, A, zero)) :=11  ∃ p ∈ polynomials(I, A, zero), ∃ q ∈ polynomials(I, A, zero), t = (p, q) ∧ s = coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)12requires ring : IsCommRing(A, add, zero, neg, mul, one)13requires pair : t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)14proof15  obtain ⟨bound, p, hp, q, hq, shape⟩ := product.membership.forward at16    polynomials(I, A, zero), polynomials(I, A, zero), t with pair17  have member := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *18  refine ⟨coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), member, p, hp, q, hq, shape, rfl⟩19uniqueness20  intros u hu first v hv second21  obtain ⟨p, hp, q, hq, shapeU, valueU⟩ := first22  obtain ⟨r, hr, s, hs, shapeV, valueV⟩ := second23  have equal : (p, q) = (r, s)24    cc25  have coordinates := orderedPair.injective at p, q, r, s with equal26  cc2728defgraph polynomialAdd (I A add zero neg mul one : Set) (t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)) : polynomials(I, A, zero) := polynomialPairAdd(I, A, add, zero, neg, mul, one, t)29requires ring : IsCommRing(A, add, zero, neg, mul, one)30proof31  have selected := polynomialPairAdd.selected at I, A, add, zero, neg, mul, one, t with *32  exact selected.left3334notation scoped polynomialAdd(I, R) => polynomialAdd(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)3536theorem polynomialAdd.apply (I A add zero neg mul one p q : Set)37  requires ring : IsCommRing(A, add, zero, neg, mul, one)38  requires memberP : p ∈ polynomials(I, A, zero)39  requires memberQ : q ∈ polynomials(I, A, zero)40  shows (polynomialAdd(I, A, add, zero, neg, mul, one))(p, q) = coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)41proof42  have pair := product.pair at p, q, polynomials(I, A, zero), polynomials(I, A, zero) with *43  have selected := polynomialPairAdd.selected at I, A, add, zero, neg, mul, one, (p, q) with *44  obtain ⟨r, hr, s, hs, shape, output⟩ := selected.right45  have coordinates := orderedPair.injective with shape46  have value := polynomialAdd.value at I, A, add, zero, neg, mul, one, (p, q) with *47  unfold call248  cc4950defunique polynomialPairMul (I A add zero neg mul one t : Set) (s ∈ polynomials(I, A, zero)) :=51  ∃ p ∈ polynomials(I, A, zero), ∃ q ∈ polynomials(I, A, zero), t = (p, q) ∧ s = polynomialProduct(I, A, add, zero, neg, mul, one, p, q)52requires ring : IsCommRing(A, add, zero, neg, mul, one)53requires pair : t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)54proof55  obtain ⟨bound, p, hp, q, hq, shape⟩ := product.membership.forward with pair56  have member := polynomialProduct.member with hp, hq57  refine ⟨polynomialProduct(I, A, add, zero, neg, mul, one, p, q), member, p, hp, q, hq, shape, rfl⟩58uniqueness59  intros u hu first v hv second60  obtain ⟨p, hp, q, hq, shapeU, valueU⟩ := first61  obtain ⟨r, hr, s, hs, shapeV, valueV⟩ := second62  have equal : (p, q) = (r, s) by cc63  have coordinates := orderedPair.injective with equal64  cc6566defgraph polynomialMul (I A add zero neg mul one : Set) (t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)) : polynomials(I, A, zero) := polynomialPairMul(I, A, add, zero, neg, mul, one, t)67requires ring : IsCommRing(A, add, zero, neg, mul, one)68proof69  have selected := polynomialPairMul.selected at I, A, add, zero, neg, mul, one, t with *70  exact selected.left7172notation scoped polynomialMul(I, R) => polynomialMul(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)7374theorem polynomialMul.apply (I A add zero neg mul one p q : Set)75  requires ring : IsCommRing(A, add, zero, neg, mul, one)76  requires memberP : p ∈ polynomials(I, A, zero)77  requires memberQ : q ∈ polynomials(I, A, zero)78  shows (polynomialMul(I, A, add, zero, neg, mul, one))(p, q) = polynomialProduct(I, A, add, zero, neg, mul, one, p, q)79proof80  have pair := product.pair at p, q, polynomials(I, A, zero), polynomials(I, A, zero) with *81  have selected := polynomialPairMul.selected at I, A, add, zero, neg, mul, one, (p, q) with *82  obtain ⟨r, hr, s, hs, shape, output⟩ := selected.right83  have coordinates := orderedPair.injective with shape84  have value := polynomialMul.value at I, A, add, zero, neg, mul, one, (p, q) with *85  unfold call286  cc8788defgraph polynomialNeg (I A add zero neg mul one : Set) (p ∈ polynomials(I, A, zero)) : polynomials(I, A, zero) := coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)89requires ring : IsCommRing(A, add, zero, neg, mul, one)90proof91  exact polynomials.neg with *9293notation scoped polynomialNeg(I, R) => polynomialNeg(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)9495theorem polynomialNeg.apply (I A add zero neg mul one p : Set)96  requires ring : IsCommRing(A, add, zero, neg, mul, one)97  requires member : p ∈ polynomials(I, A, zero)98  shows (polynomialNeg(I, A, add, zero, neg, mul, one))(p) = coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)99proof100  exact polynomialNeg.value at I, A, add, zero, neg, mul, one, p with *101102section Rings103variable (I A add zero neg mul one : Set)104hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)105notation ring P := (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))106107theorem polynomials.add_commutative (p q : Set)108  requires memberP : p ∈ polynomials(I, A, zero)109  requires memberQ : q ∈ polynomials(I, A, zero)110  shows p + q = q + p111proof112  have functionP := polynomials.function with memberP113  have functionQ := polynomials.function with memberQ114  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *115  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *116  have member1 := polynomials.add at I, A, add, zero, neg, mul, one, q, p with *117  have value1 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, q, p with *118  have law := coefficientAdd.commutative at monomials(I), A, add, zero, neg, mul, one, p, q with *119  cc120121theorem polynomials.add_associative (p q r : Set)122  requires memberP : p ∈ polynomials(I, A, zero)123  requires memberQ : q ∈ polynomials(I, A, zero)124  requires memberR : r ∈ polynomials(I, A, zero)125  shows (p + q) + r = p + (q + r)126proof127  have functionP := polynomials.function with memberP128  have functionQ := polynomials.function with memberQ129  have functionR := polynomials.function with memberR130  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *131  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *132  have member1 := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *133  have value1 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, q, r with *134  have member2 := polynomials.add at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *135  have value2 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *136  have member3 := polynomials.add at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *137  have value3 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *138  have law := coefficientAdd.associative at monomials(I), A, add, zero, neg, mul, one, p, q, r with *139  cc140141theorem polynomials.add_zero (p : Set)142  requires memberP : p ∈ polynomials(I, A, zero)143  shows p + 0 = p144proof145  have functionP := polynomials.function with memberP146  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *147  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *148  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *149  have law := coefficientAdd.zero with *150  cc151152theorem polynomials.add_inverse (p : Set)153  requires memberP : p ∈ polynomials(I, A, zero)154  shows p + (-p) = 0155proof156  have functionP := polynomials.function with memberP157  have negative := polynomials.neg with *158  have negValue := polynomialNeg.apply at I, A, add, zero, neg, mul, one, p with *159  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *160  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *161  have law := coefficientAdd.inverse with *162  cc163164theorem polynomials.mul_commutative (p q : Set)165  requires memberP : p ∈ polynomials(I, A, zero)166  requires memberQ : q ∈ polynomials(I, A, zero)167  shows p * q = q * p168proof169  have functionP := polynomials.function with memberP170  have functionQ := polynomials.function with memberQ171  have member0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *172  have value0 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *173  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, p with *174  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, p with *175  have law := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, p, q with *176  cc177178theorem polynomials.mul_associative (p q r : Set)179  requires memberP : p ∈ polynomials(I, A, zero)180  requires memberQ : q ∈ polynomials(I, A, zero)181  requires memberR : r ∈ polynomials(I, A, zero)182  shows (p * q) * r = p * (q * r)183proof184  have functionP := polynomials.function with memberP185  have functionQ := polynomials.function with memberQ186  have functionR := polynomials.function with memberR187  have member0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *188  have value0 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *189  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *190  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, r with *191  have member2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r with *192  have value2 := polynomialMul.apply at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r with *193  have member3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *194  have value3 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *195  have law := polynomialProduct.associative at I, A, add, zero, neg, mul, one, p, q, r with *196  cc197198theorem polynomials.mul_one (p : Set)199  requires memberP : p ∈ polynomials(I, A, zero)200  shows p * 1 = p201proof202  have functionP := polynomials.function with memberP203  have ordinary := IsCommRing.ring with ring204  have zeroIn := IsRing.zero_in_carrier with ordinary205  have multiplicative := IsRing.multiplicative with ordinary206  have oneIn := IsMonoid.unit_in_carrier with multiplicative207  have unitPolynomial := polynomialConstant.member at I, A, zero, one with *208  have member0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one) with *209  have value0 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one) with *210  have law := polynomialProduct.one_right at I, A, add, zero, neg, mul, one, p with *211  cc212213theorem polynomials.distribute_right (p q r : Set)214  requires memberP : p ∈ polynomials(I, A, zero)215  requires memberQ : q ∈ polynomials(I, A, zero)216  requires memberR : r ∈ polynomials(I, A, zero)217  shows p * (q + r) = p * q + p * r218proof219  have functionP := polynomials.function with memberP220  have functionQ := polynomials.function with memberQ221  have functionR := polynomials.function with memberR222  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *223  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, q, r with *224  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *225  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *226  have member2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *227  have value2 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *228  have member3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *229  have value3 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, r with *230  have member4 := polynomials.add at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *231  have value4 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *232  have law := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, q, r with *233  cc234235theorem polynomials.distribute_left (p q r : Set)236  requires memberP : p ∈ polynomials(I, A, zero)237  requires memberQ : q ∈ polynomials(I, A, zero)238  requires memberR : r ∈ polynomials(I, A, zero)239  shows (p + q) * r = p * r + q * r240proof241  have functionP := polynomials.function with memberP242  have functionQ := polynomials.function with memberQ243  have functionR := polynomials.function with memberR244  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *245  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *246  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *247  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *248  have member2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *249  have value2 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, r with *250  have member3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *251  have value3 := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, r with *252  have member4 := polynomials.add at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *253  have value4 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *254  have law := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, p, q, r with *255  cc256257instance polynomials.comm_ring258  shows IsCommRing(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))259proof260  have addition := polynomialAdd.function at I, A, add, zero, neg, mul, one with *261  have multiplication := polynomialMul.function at I, A, add, zero, neg, mul, one with *262  have negation := polynomialNeg.function at I, A, add, zero, neg, mul, one with *263  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *264  have ordinary := IsCommRing.ring with ring265  have zeroIn := IsRing.zero_in_carrier with ordinary266  have multiplicative := IsRing.multiplicative with ordinary267  have oneIn := IsMonoid.unit_in_carrier with multiplicative268  have unitPolynomial := polynomialConstant.member at I, A, zero, one with *269  have addAssoc : Associative(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one))270    intros p hp q hq r hr271    exact polynomials.add_associative with *272  have addComm : Commutative(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one))273    intros p hp q hq274    exact polynomials.add_commutative with *275  have addIdentity : Identity(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero))276    constructor277    . exact zeroPolynomial278    . intros p hp279      have right := polynomials.add_zero with hp280      have comm := polynomials.add_commutative at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p with *281      constructor282      . cc283      . exact right284  have inverses : Inverse(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))285    constructor286    . exact negation287    . intros p hp288      have negative := polynomials.neg with hp289      have value := polynomialNeg.apply with hp290      have right := polynomials.add_inverse with hp291      have comm := polynomials.add_commutative at I, A, add, zero, neg, mul, one, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p), p with *292      constructor293      . cc294      . exact right295  have mulAssoc : Associative(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one))296    intros p hp q hq r hr297    exact polynomials.mul_associative with *298  have mulComm : Commutative(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one))299    intros p hp q hq300    exact polynomials.mul_commutative with *301  have mulIdentity : Identity(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))302    constructor303    . exact unitPolynomial304    . intros p hp305      have right := polynomials.mul_one with hp306      have comm := polynomials.mul_commutative at I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, one), p with *307      constructor308      . cc309      . exact right310  have distributive : Distributive(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one))311    intros p hp q hq r hr312    constructor313    . exact polynomials.distribute_right with *314    . exact polynomials.distribute_left with *315  have additive : IsAbelianGroup(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))316    unfold IsAbelianGroup317    refine ⟨_, addComm⟩318    unfold IsGroup319    refine ⟨_, inverses⟩320    unfold IsMonoid321    refine ⟨_, addIdentity⟩322    unfold IsSemigroup323    refine ⟨_, addAssoc⟩324    exact addition325  have multiplicativePolynomial : IsMonoid(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))326    unfold IsMonoid327    refine ⟨_, mulIdentity⟩328    unfold IsSemigroup329    refine ⟨_, mulAssoc⟩330    exact multiplication331  constructor332  . unfold IsRing333    refine ⟨additive, multiplicativePolynomial, distributive⟩334  . exact mulComm335336end Rings337