Grace/Cumulus/Algebra/Polynomial/MonicProducts.g17

Open in Workbench Download source

Imports

HornerExtension · MonicVanishing

Declarations

Source

1-- Monic linear products, with explicit coefficient lists and extension laws (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.MonicProducts8import HornerExtension9import MonicVanishing1011section Lengths12variable (A add zero neg mul one a : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis source : IsCommRing(R)15hypothesis center : a ∈ R1617theorem hornerLinearProduct.length (carry : Set) (cs : List(A))18  requires constant : carry ∈ R19  shows length{A}(hornerLinearProduct{A}(add, neg, mul, a, carry, cs)) = succ(length{A}(cs))20proof21  induction cs generalizing carry22  | List.nil =>23    intros carry constant24    have empty : List(A, []) by typecheck25    have ordinary := IsCommRing.ring with source26    have negative := IsRing.neg_closed with ordinary, center27    have head := IsRing.add_closed with ordinary, constant, negative28    rw [hornerLinearProduct, length.cons, length.nil]29    rfl30  | List.cons(c, tail) using ih =>31    intros carry constant32    have empty : List(A, []) by typecheck33    have coefficient : c ∈ R by assumption34    have ordinary := IsCommRing.ring with source35    have productIn := IsRing.mul_closed with ordinary, center, coefficient36    have negative := IsRing.neg_closed with ordinary, productIn37    have head := IsRing.add_closed with ordinary, constant, negative38    have rest := hornerLinearProduct.closed at A, add, zero, neg, mul, one, a, c, tail with *39    have previous := ih with c, coefficient40    rw [hornerLinearProduct, length.cons, previous, length.cons]41    rfl4243end Lengths4445section Extensions46variable (A add zero neg mul one B plus z minus times unit f x a : Set)47notation ring R := (A, add, zero, neg, mul, one)48notation ring S := (B, plus, z, minus, times, unit)49hypothesis source : IsCommRing(R)50hypothesis target : IsCommRing(S)51hypothesis hom : IsRingHom(f, R, S)52hypothesis element : x ∈ S53hypothesis center : a ∈ R5455theorem hornerLinearProduct.map_value (carry : Set) (cs : List(A))56  requires constant : carry ∈ R57  shows monicValue(R, f, S, x, hornerLinearProduct{A}(add, neg, mul, a, carry, cs)) =58    S[f(carry) + (x - f(a)) * monicValue(R, f, S, x, cs)]59proof60  induction cs generalizing carry61  | List.nil =>62    intros carry constant63    have empty : List(A, []) by typecheck64    have ordinary := IsCommRing.ring with source65    have negative := IsRing.neg_closed with ordinary, center66    have head := IsRing.add_closed with ordinary, constant, negative67    have fa := IsRingHom.closed with hom, center68    have fc := IsRingHom.closed with hom, constant69    have difference := IsRingHom.sub at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, carry, a with *70    rw [hornerLinearProduct, monicValue, monicValue, monicValue, difference]71    ring72  | List.cons(c, tail) using ih =>73    intros carry constant74    have empty : List(A, []) by typecheck75    have coefficient : c ∈ R by assumption76    have ordinary := IsCommRing.ring with source77    have product := IsRing.mul_closed with ordinary, center, coefficient78    have productIn := IsRing.mul_closed with ordinary, center, coefficient79    have negative := IsRing.neg_closed with ordinary, productIn80    have head := IsRing.add_closed with ordinary, constant, negative81    have rest := hornerLinearProduct.closed at A, add, zero, neg, mul, one, a, c, tail with *82    have previous := ih with c, coefficient83    have tailValue := monicValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, tail with *84    have fa := IsRingHom.closed with hom, center85    have fc := IsRingHom.closed with hom, coefficient86    have fcarry := IsRingHom.closed with hom, constant87    have difference := IsRingHom.sub at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, carry, R[a * c] with *88    have mappedProduct := IsRingHom.mul with hom, center, coefficient89    have outer := hornerValue.cons at A, f, plus, times, unit, x, R[carry - a * c], hornerLinearProduct{A}(add, neg, mul, a, c, tail) with *90    have original := hornerValue.cons at A, f, plus, times, unit, x, c, tail with *91    rw [hornerLinearProduct, outer, original, previous, difference, mappedProduct]92    ring9394end Extensions9596section Polynomials97variable (I A add zero neg mul one j a carry : Set)98notation ring R := (A, add, zero, neg, mul, one)99notation ring P := R[I]100hypothesis ring : IsCommRing(R)101hypothesis center : a ∈ R102hypothesis constant : carry ∈ R103104theorem polynomialFromHorner.linear_product (cs : List(A))105  shows polynomialFromHorner(I, R, j, R[1], hornerLinearProduct{A}(add, neg, mul, a, carry, cs)) =106    P[polynomialCoefficients(I, R)(carry) + (polynomialVariable(I, R, j) - polynomialCoefficients(I, R)(a)) * polynomialFromHorner(I, R, j, R[1], cs)]107proof108  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *109  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *110  have zeroIn : R[0] ∈ R by typecheck111  have oneIn : R[1] ∈ R by typecheck112  have variable := polynomialVariable.member at I, A, zero, one, j with *113  have result := hornerLinearProduct.map_value at A, add, zero, neg, mul, one, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], polynomialCoefficients(I, R), polynomialVariable(I, R, j), a, carry, cs with *114  simp [polynomialFromHorner]115116end Polynomials117-- Lower coefficients of the monic product of (X-a), one factor per list entry.118def monicFactorCoefficients {A : Set} (add z neg mul : Set) (xs : List(A)) → Set119  | add, z, neg, mul, List.nil => []120  | add, z, neg, mul, List.cons(a, tail) => hornerLinearProduct{A}(add, neg, mul, a, z, monicFactorCoefficients(add, z, neg, mul, tail))121  descends xs122123def polynomialLinearFactors (I A add zero neg mul one j : Set) (xs : List(A)) : Set :=124  polynomialFromHorner(I, A, add, zero, neg, mul, one, j, one, monicFactorCoefficients{A}(add, zero, neg, mul, xs))125126notation scoped polynomialLinearFactors(I, R, j, xs) => polynomialLinearFactors(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, xs)127128section Coefficients129variable (A add zero neg mul one : Set)130notation ring R := (A, add, zero, neg, mul, one)131hypothesis ring : IsCommRing(R)132133theorem monicFactorCoefficients.closed (xs : List(A))134  shows List(A, monicFactorCoefficients{A}(add, zero, neg, mul, xs))135proof136  induction xs137  | List.nil =>138    rw monicFactorCoefficients139    typecheck140  | List.cons(a, tail) using ih =>141    have center : a ∈ R by assumption142    have zeroIn : R[0] ∈ R by typecheck143    rw monicFactorCoefficients144    exact hornerLinearProduct.closed with *145146theorem monicFactorCoefficients.length (xs : List(A))147  shows length{A}(monicFactorCoefficients{A}(add, zero, neg, mul, xs)) = length{A}(xs)148proof149  induction xs150  | List.nil =>151    rw monicFactorCoefficients152    rfl153  | List.cons(a, tail) using ih =>154    have center : a ∈ R by assumption155    have zeroIn : R[0] ∈ R by typecheck156    have rest := monicFactorCoefficients.closed with *157    have size := hornerLinearProduct.length at A, add, zero, neg, mul, one, a, zero, monicFactorCoefficients{A}(add, zero, neg, mul, tail) with *158    rw [monicFactorCoefficients, length.cons]159    cc160161end Coefficients162163section Factors164variable (I A add zero neg mul one j : Set)165notation ring R := (A, add, zero, neg, mul, one)166notation ring P := R[I]167hypothesis ring : IsCommRing(R)168169theorem polynomialLinearFactors.member (xs : List(A))170  shows polynomialLinearFactors(I, R, j, xs) ∈ P171proof172  have oneIn : R[1] ∈ R by typecheck173  have coefficients := monicFactorCoefficients.closed with *174  unfold polynomialLinearFactors175  exact polynomialFromHorner.member with *176177theorem polynomialLinearFactors.nil178  shows polynomialLinearFactors(I, R, j, []) = P[1]179proof180  unfold polynomialLinearFactors181  rw monicFactorCoefficients182  exact polynomialFromHorner.nil with *183184theorem polynomialLinearFactors.cons (a : Set) (xs : List(A))185  requires center : a ∈ R186  shows polynomialLinearFactors(I, R, j, a :: xs) =187    P[(polynomialVariable(I, R, j) - polynomialCoefficients(I, R)(a)) * polynomialLinearFactors(I, R, j, xs)]188proof189  have zeroIn : R[0] ∈ R by typecheck190  have oneIn : R[1] ∈ R by typecheck191  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *192  have ordinary := IsCommRing.ring with target193  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *194  have mapsZero := IsRingHom.zero with hom195  have image := IsRingHom.closed with hom, center196  have variable := polynomialVariable.member at I, A, zero, one, j with *197  have negative := IsRing.neg_closed with ordinary, image198  have difference := IsRing.add_closed with ordinary, variable, negative199  have coefficients := monicFactorCoefficients.closed with *200  have rest := polynomialFromHorner.member at I, A, add, zero, neg, mul, one, j, one, monicFactorCoefficients{A}(add, zero, neg, mul, xs) with *201  have product := IsRing.mul_closed with ordinary, difference, rest202  have identity := IsRing.add_left_identity with ordinary, product203  have equation := polynomialFromHorner.linear_product at I, A, add, zero, neg, mul, one, j, a, zero, monicFactorCoefficients{A}(add, zero, neg, mul, xs) with *204  unfold polynomialLinearFactors205  rw monicFactorCoefficients206  cc207208theorem polynomialLinearFactors.leading_coefficient (xs : List(A))209  requires index : j ∈ I210  shows polynomialLinearFactors(I, R, j, xs)(monomialShift(I, j, monomialOne(I), length{A}(xs))) = R[1]211proof212  have oneIn : R[1] ∈ R by typecheck213  have coefficients := monicFactorCoefficients.closed with *214  have size := monicFactorCoefficients.length at A, add, zero, neg, mul, one, xs with *215  have leading := polynomialFromHorner.leading_coefficient at I, A, add, zero, neg, mul, one, j, one, monicFactorCoefficients{A}(add, zero, neg, mul, xs) with *216  unfold polynomialLinearFactors217  cc218219theorem polynomialLinearFactors.nonzero (xs : List(A))220  requires index : j ∈ I221  requires nontrivial : R[1] ≠ R[0]222  shows polynomialLinearFactors(I, R, j, xs) ≠ P[0]223proof224  have oneIn : R[1] ∈ R by typecheck225  have coefficients := monicFactorCoefficients.closed with *226  have nonzero := polynomialFromHorner.nonzero_of_leading at I, A, add, zero, neg, mul, one, j, one, monicFactorCoefficients{A}(add, zero, neg, mul, xs) with *227  intro equal228  apply nonzero229  unfold polynomialLinearFactors at equal230  exact equal231232end Factors233