Grace/Cumulus/Algebra/Polynomial/Bundled.g17

Open in Workbench Download source

Imports

Constants · Ring.Homomorphism

Declarations

Source

1-- Bundled polynomial rings: the ring value polynomialRing(R, I) over a2-- bundled coefficient ring R in the variables I, its commutative ring3-- instance, the variables X(R, I, j), the constants as the homomorphism4-- polynomialConstant(R, I) : R →+* polynomialRing(R, I), and the bridges5-- to the forms over separate pieces; everything here is ZF6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Polynomial.Bundled12import Constants13import Ring.Homomorphism1415-- The polynomial ring over R in the variables I: the finite-support16-- coefficient maps on the monomials with the convolution operations, the17-- zero map, and the constant one, built from the projections of R.18def polynomialRing (R I : Set) : Set :=19  Ring.mk(polynomials(I, R.carrier, R.zero),20    polynomialAdd(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one),21    constantFunction(monomials(I), R.carrier, R.zero),22    polynomialNeg(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one),23    polynomialMul(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one),24    polynomialConstant(I, R.carrier, R.zero, R.one))2526-- The variable X_j and the constants, the latter as one graph on R.27def X (R I j : Set) : Set := polynomialVariable(I, R.carrier, R.zero, R.one, j)28def polynomialConstant (R I : Set) : Set :=29  polynomialCoefficients(I, R.carrier, R.zero)3031theorem polynomialRing.carrierOf (R I : Set)32  shows Ring.carrier(polynomialRing(R, I)) = polynomials(I, R.carrier, R.zero)33proof34  simp [polynomialRing, Ring.mk.carrier]3536theorem polynomialRing.addOf (R I : Set)37  shows Ring.add(polynomialRing(R, I)) =38    polynomialAdd(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)39proof40  simp [polynomialRing, Ring.mk.add]4142theorem polynomialRing.zeroOf (R I : Set)43  shows Ring.zero(polynomialRing(R, I)) =44    constantFunction(monomials(I), R.carrier, R.zero)45proof46  simp [polynomialRing, Ring.mk.zero]4748theorem polynomialRing.negOf (R I : Set)49  shows Ring.neg(polynomialRing(R, I)) =50    polynomialNeg(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)51proof52  simp [polynomialRing, Ring.mk.neg]5354theorem polynomialRing.mulOf (R I : Set)55  shows Ring.mul(polynomialRing(R, I)) =56    polynomialMul(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)57proof58  simp [polynomialRing, Ring.mk.mul]5960theorem polynomialRing.oneOf (R I : Set)61  shows Ring.one(polynomialRing(R, I)) =62    polynomialConstant(I, R.carrier, R.zero, R.one)63proof64  simp [polynomialRing, Ring.mk.one]6566theorem X.value (R I j : Set)67  shows X(R, I, j) = polynomialVariable(I, R.carrier, R.zero, R.one, j)68proof69  simp [X]7071theorem polynomialConstant.graph (R I : Set)72  shows polynomialConstant(R, I) = polynomialCoefficients(I, R.carrier, R.zero)73proof74  simp [Bundled.polynomialConstant]7576-- The engine's forms at the projections of R: K is the coefficient ring77-- over separate pieces and P the polynomial ring over it.78section Engine79variable (R I : Set)80notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)81notation ring P := K[I]82hypothesis comm : CommRing(R)8384theorem polynomialRing.engine85  shows IsCommRing(P)86proof87  have parts := CommRing.parts with comm88  exact polynomials.comm_ring with parts8990instance polynomialRing.comm_ring91  shows CommRing(polynomialRing(R, I))92proof93  have engine := polynomialRing.engine at R, I with comm94  unfold polynomialRing95  exact CommRing.of_parts with engine9697theorem polynomialRing.ring98  shows Ring(polynomialRing(R, I))99proof100  exact CommRing.to_ring with (polynomialRing.comm_ring with comm)101102-- Membership in the polynomial ring is membership in the engine's carrier.103-- The instance supplies the ring the way a hypothesis does, so under104-- CommRing(R) a binder (p : polynomialRing(R, I)) is membership in its105-- carrier, p ∈ polynomialRing(R, I) is read there, the elements carry106-- p + q, p * q, and p - q, and polynomialRing(R, I)[2] is its numeral.107theorem polynomialRing.mem_iff (p : Set)108  shows p ∈ polynomialRing(R, I) ↔ p ∈ P109proof110  rw polynomialRing.carrierOf111  tauto112113instance X.mem (j : Set)114  shows X(R, I, j) ∈ polynomialRing(R, I)115proof116  have zeroIn : R[0] ∈ R := Ring.zero_mem with *117  have oneIn : R[1] ∈ R := Ring.one_mem with *118  rw [polynomialRing.carrierOf, X.value]119  exact polynomialVariable.member with *120121theorem polynomialConstant.apply (a : R)122  shows polynomialConstant(R, I)(a) =123    polynomialConstant(I, R.carrier, R.zero, a)124proof125  have zeroIn : R[0] ∈ R := Ring.zero_mem with *126  have aIn : a ∈ R by assumption127  rw polynomialConstant.graph128  exact polynomialCoefficients.value with *129130-- The constants form a homomorphism into the polynomial ring.131theorem polynomialConstant.hom132  shows polynomialConstant(R, I) : R →+* polynomialRing(R, I)133proof134  have parts := CommRing.parts with comm135  have engine := polynomialCoefficients.hom at I, R.carrier, R.add, R.zero,136    R.neg, R.mul, R.one with parts137  have shifted : IsRingHom(polynomialConstant(R, I), R.carrier, R.add, R.zero,138      R.neg, R.mul, R.one, Ring.carrier(polynomialRing(R, I)),139      Ring.add(polynomialRing(R, I)), Ring.zero(polynomialRing(R, I)),140      Ring.neg(polynomialRing(R, I)), Ring.mul(polynomialRing(R, I)),141      Ring.one(polynomialRing(R, I)))142    rw [polynomialRing.carrierOf, polynomialRing.addOf, polynomialRing.zeroOf,143      polynomialRing.negOf, polynomialRing.mulOf, polynomialRing.oneOf]144    rw polynomialConstant.graph145    exact engine146  exact RingHom.of_projections with (CommRing.to_ring with comm),147    (polynomialRing.ring with comm), shifted148149instance polynomialConstant.mem (a : R)150  shows polynomialConstant(R, I)(a) ∈ polynomialRing(R, I)151proof152  have hom := polynomialConstant.hom at R, I with comm153  exact RingHom.map_mem with *154155theorem polynomialConstant.inj (a b : R)156  requires equal : polynomialConstant(R, I)(a) = polynomialConstant(R, I)(b)157  shows a = b158proof159  have zeroIn : R[0] ∈ R := Ring.zero_mem with *160  have aIn : a ∈ R by assumption161  have bIn : b ∈ R by assumption162  rw [polynomialConstant.apply, polynomialConstant.apply] at equal163  exact polynomialConstant.injective with zeroIn, aIn, bIn, equal164165-- Ideals of the bundled polynomial ring are the engine's ideals of P.166theorem Ideal.polynomial_parts (J : Set)167  requires ideal : Ideal(polynomialRing(R, I), J)168  shows IsIdeal(P, J)169proof170  have parts := Ideal.parts with ideal171  rw [polynomialRing.carrierOf, polynomialRing.addOf, polynomialRing.zeroOf,172    polynomialRing.negOf, polynomialRing.mulOf] at parts173  exact parts174175theorem Ideal.polynomial_of_parts (J : Set)176  requires ideal : IsIdeal(P, J)177  shows Ideal(polynomialRing(R, I), J)178proof179  unfold polynomialRing180  exact Ideal.of_parts with ideal181182theorem MaximalIdeal.polynomial_parts (M : Set)183  requires maximal : MaximalIdeal(polynomialRing(R, I), M)184  shows IsMaximalIdeal(P, M)185proof186  have parts := MaximalIdeal.parts with maximal187  rw [polynomialRing.carrierOf, polynomialRing.addOf, polynomialRing.zeroOf,188    polynomialRing.negOf, polynomialRing.mulOf, polynomialRing.oneOf] at parts189  exact parts190191theorem MaximalIdeal.polynomial_of_parts (M : Set)192  requires maximal : IsMaximalIdeal(P, M)193  shows MaximalIdeal(polynomialRing(R, I), M)194proof195  unfold polynomialRing196  exact MaximalIdeal.of_parts with maximal197198end Engine199200-- Homomorphisms out of the bundled polynomial ring are the engine's201-- homomorphisms out of P, into the projections of the target.202section Homomorphisms203variable (R S I g : Set)204notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)205notation ring L := (S.carrier, S.add, S.zero, S.neg, S.mul, S.one)206notation ring P := K[I]207hypothesis comm : CommRing(R)208hypothesis target : CommRing(S)209210theorem RingHom.polynomial_parts211  requires hom : g : polynomialRing(R, I) →+* S212  shows IsRingHom(g, P, L)213proof214  have parts := RingHom.parts with hom215  rw [polynomialRing.carrierOf, polynomialRing.addOf, polynomialRing.zeroOf,216    polynomialRing.negOf, polynomialRing.mulOf, polynomialRing.oneOf] at parts217  exact parts218219theorem RingHom.polynomial_of_parts220  requires hom : IsRingHom(g, P, L)221  shows g : polynomialRing(R, I) →+* S222proof223  have shifted : IsRingHom(g, Ring.carrier(polynomialRing(R, I)),224      Ring.add(polynomialRing(R, I)), Ring.zero(polynomialRing(R, I)),225      Ring.neg(polynomialRing(R, I)), Ring.mul(polynomialRing(R, I)),226      Ring.one(polynomialRing(R, I)), S.carrier, S.add, S.zero, S.neg,227      S.mul, S.one)228    rw [polynomialRing.carrierOf, polynomialRing.addOf, polynomialRing.zeroOf,229      polynomialRing.negOf, polynomialRing.mulOf, polynomialRing.oneOf]230    exact hom231  exact RingHom.of_projections with (polynomialRing.ring with comm),232    (CommRing.to_ring with target), shifted233234end Homomorphisms235