Grace/Cumulus/Algebra/Polynomial/HornerHom.g17

Open in Workbench Download source

Imports

Horner · CoefficientLists

Declarations

Source

1-- Horner evaluation commutes with a ring homomorphism, coefficient by coefficient.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.HornerHom8import Horner9import CoefficientLists1011section Homomorphisms12variable (A add zero neg mul one B plus z minus times unit h leading x : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15hypothesis ring : IsCommRing(R)16hypothesis hom : IsRingHom(h, R, S)17hypothesis initial : leading ∈ R18hypothesis element : x ∈ R1920theorem hornerAt.map (cs : List(A))21  shows h(hornerAt{A}(add, mul, leading, x, cs)) = hornerAt{B}(plus, times, h(leading), h(x), listMap{A}(h, cs))22proof23  induction cs24  | List.nil =>25    rw [listMap, hornerAt.nil, hornerAt.nil]26    rfl27  | List.cons(c, tail) using ih =>28    have coefficient : c ∈ R by assumption29    have function := IsRingHom.function with hom30    have image := IsRingHom.closed with hom, coefficient31    have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, tail with *32    have ordinary := IsCommRing.ring with ring33    have product := IsRing.mul_closed with ordinary, element, value34    have sumMap := IsRingHom.add with hom, coefficient, product35    have productMap := IsRingHom.mul with hom, element, value36    have source := hornerAt.cons at A, add, mul, leading, x, c, tail with *37    have target := hornerAt.cons at B, plus, times, h(leading), h(x), h(c), listMap{A}(h, tail) with *38    rw [listMap, source, target]39    cc4041end Homomorphisms42theorem hornerValue.cons (A f plus times leading x c : Set) (cs : List(A))43  requires coefficient : c ∈ A44  shows monicValue{A}(f, plus, times, leading, x, c :: cs) = plus(f(c), times(x, monicValue{A}(f, plus, times, leading, x, cs)))45proof46  rw monicValue47  rfl4849section Rings50variable (A add zero neg mul one B plus z minus times unit f leading a : Set)51notation ring R := (A, add, zero, neg, mul, one)52notation ring S := (B, plus, z, minus, times, unit)53hypothesis source : IsCommRing(R)54hypothesis target : IsCommRing(S)55hypothesis hom : IsRingHom(f, R, S)56hypothesis initial : leading ∈ R57hypothesis center : a ∈ R5859theorem hornerAt.map_cons (c : Set) (cs : List(A))60  requires coefficient : c ∈ R61  shows f(hornerAt{A}(add, mul, leading, a, c :: cs)) = S[f(c) + f(a) * f(hornerAt{A}(add, mul, leading, a, cs))]62proof63  have ordinary := IsCommRing.ring with source64  have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, cs with *65  have product := IsRing.mul_closed with ordinary, center, value66  have mappedProduct := IsRingHom.mul with hom, center, value67  have mappedSum := IsRingHom.add with hom, coefficient, product68  rw [hornerAt.cons, mappedSum, mappedProduct]69  rfl7071-- Evaluation at an arbitrary extension element; no injectivity is required.72theorem hornerValue.synthetic_division (x c : Set) (cs : List(A))73  requires element : x ∈ S74  requires coefficient : c ∈ R75  shows monicValue{A}(f, plus, times, f(leading), x, c :: cs) = S[f(hornerAt{A}(add, mul, leading, a, c :: cs)) + (x - f(a)) * monicValue{A}(f, plus, times, f(leading), x, hornerQuotient{A}(add, mul, leading, a, cs))]76proof77  induction cs generalizing c78  | List.nil =>79    intros c coefficient80    have imageC := IsRingHom.closed with hom, coefficient81    have imageA := IsRingHom.closed with hom, center82    have imageLeading := IsRingHom.closed with hom, initial83    have mapped := hornerAt.map_cons at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, leading, a, c, [] with *84    rw [mapped, hornerAt.nil, hornerQuotient, monicValue, monicValue, monicValue]85    ring86  | List.cons(d, tail) using ih =>87    intros c coefficient88    have dIn : d ∈ R by assumption89    have imageC := IsRingHom.closed with hom, coefficient90    have imageA := IsRingHom.closed with hom, center91    have imageLeading := IsRingHom.closed with hom, initial92    have baseValue := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, d :: tail with *93    have imageValue := IsRingHom.closed with hom, baseValue94    have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, tail with *95    have valueQ := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(leading), hornerQuotient{A}(add, mul, leading, a, tail) with *96    have previous := ih with d, dIn97    have mapped := hornerAt.map_cons at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, leading, a, c, d :: tail with *98    have outer := hornerValue.cons at A, f, plus, times, f(leading), x, c, d :: tail with *99    have quotientValue := hornerValue.cons at A, f, plus, times, f(leading), x, hornerAt{A}(add, mul, leading, a, d :: tail), hornerQuotient{A}(add, mul, leading, a, tail) with *100    rw [mapped, hornerQuotient, outer, quotientValue, previous]101    ring102103end Rings104