Grace/Cumulus/Algebra/HornerRelations.g17

Open in Workbench Download source

Imports

Polynomial.HornerNormalization

Declarations

Source

1-- Normalizing polynomial relations over a coefficient homomorphism (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.HornerRelations8import Polynomial.HornerNormalization910theorem monicValue.mapped_coefficients (A B plus times f leading x : Set) (cs : List(A))11  requires function : f : A → B12  shows monicValue{A}(f, plus, times, leading, x, cs) = hornerAt{B}(plus, times, leading, x, listMap{A}(f, cs))13proof14  induction cs15  | List.nil =>16    rw [listMap, monicValue, hornerAt.nil]17    rfl18  | List.cons(c, tail) using ih =>19    have coefficient : c ∈ A by assumption20    have mapped := listMap.closed with *21    have image := FunctionBetween.apply_closed with function, coefficient22    rw [listMap, monicValue, hornerAt.cons, ih]23    rfl2425theorem monicValue.change_coefficients (A B plus times f g h leading x : Set) (cs : List(A))26  requires function : f : A → B27  requires agreement : ∀ a ∈ A, h(a) = g(f(a))28  shows monicValue{A}(h, plus, times, leading, x, cs) = monicValue{B}(g, plus, times, leading, x, listMap{A}(f, cs))29proof30  induction cs31  | List.nil => simp [listMap, monicValue]32  | List.cons(c, tail) using ih =>33    have coefficient : c ∈ A by assumption34    have image := FunctionBetween.apply_closed with function, coefficient35    have equal := agreement with c, coefficient36    simp [listMap, monicValue, ih, equal]3738section Rings39variable (A add z neg mul one B plus o minus times unit f x : Set)40notation ring R := (A, add, z, neg, mul, one)41notation ring S := (B, plus, o, minus, times, unit)42hypothesis source : IsCommRing(R)43hypothesis target : IsCommRing(S)44hypothesis hom : IsRingHom(f, R, S)45hypothesis element : x ∈ S4647theorem monicValue.zero_coefficients (cs : List(A))48  requires coefficients : ∀ n, Nat(n) → listCoefficient{A}(z, cs, n) = z49  shows monicValue{A}(f, plus, times, o, x, cs) = o50proof51  have function := IsRingHom.function with hom52  have zero := IsRingHom.zero with hom53  have zeroIn : R[0] ∈ R by typecheck54  have values : ∀ n, Nat(n) → listCoefficient{B}(o, listMap{A}(f, cs), n) = o55    intros n natural56    have value := listCoefficient.map at A, B, f, z, cs, n with *57    rw zero at value58    have original := coefficients with n, natural59    cc60  have zeros := hornerAt.zero_coefficients at B, plus, o, minus, times, unit, listMap{A}(f, cs) with *61  have vanishes := zeros with x, element62  have mappedValue := monicValue.mapped_coefficients at A, B, plus, times, f, o, x, cs with *63  cc6465theorem monicValue.normalize (cs : List(A))66  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z67  shows ∃ leading ∈ R, leading ≠ z ∧ (∃ lower, List(A, lower) ∧68    monicValue{A}(f, plus, times, o, x, cs) = polynomialHorner{A}(f, plus, times, x, leading, lower))69proof70  induction cs71  | List.nil =>72    intro nonzero73    obtain ⟨n, natural, different⟩ := nonzero74    have value := listCoefficient.nil at A, z, n with *75    exfalso76    exact different with value77  | List.cons(c, tail) using ih =>78    intro nonzero79    have coefficient : c ∈ R by assumption80    have alternatives : (∃ n, Nat(n) ∧ listCoefficient{A}(z, tail, n) ≠ z) ∨ ¬(∃ n, Nat(n) ∧ listCoefficient{A}(z, tail, n) ≠ z)81      tauto82    cases alternatives with tailNonzero | tailZero83    . obtain ⟨leading, initial, different, lower, list, equal⟩ := ih with tailNonzero84      have consList : List(A, c :: lower) by typecheck85      refine ⟨leading, initial, different, c :: lower, consList, ?_⟩86      unfold polynomialHorner at equal87      unfold polynomialHorner88      rw [monicValue, monicValue, equal]89      rfl90    . have zeros : ∀ n, Nat(n) → listCoefficient{A}(z, tail, n) = z91        intros n natural92        by_contra different93        apply tailZero94        refine ⟨n, natural, different⟩95      have different : c ≠ z96        intro headZero97        obtain ⟨n, natural, value⟩ := nonzero98        have cases := natural.zero_or_successor with natural99        cases cases with zero | successor100        . rw [zero, listCoefficient.zero] at value101          exact value with headZero102        . obtain ⟨k, kNat, shape⟩ := successor103          rw [shape, listCoefficient.succ] at value104          have tailValue := zeros with k, kNat105          exact value with tailValue106      have empty : List(A, []) by typecheck107      refine ⟨c, coefficient, different, [], empty, ?_⟩108      have tailValue := monicValue.zero_coefficients with *109      have image := IsRingHom.closed with hom, coefficient110      unfold polynomialHorner111      rw [monicValue, monicValue, tailValue]112      ring113114theorem AlgebraicOver.of_coefficient_relation (cs : List(A))115  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z116  requires relation : monicValue{A}(f, plus, times, o, x, cs) = o117  shows AlgebraicOver(f, R, S, x)118proof119  obtain ⟨leading, initial, different, lower, list, equal⟩ := monicValue.normalize at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, x, cs with *120  unfold AlgebraicOver121  refine ⟨element, leading, initial, different, lower, list, ?_⟩122  cc123124theorem IntegralOver.algebraic_of_nontrivial125  requires nontrivial : Nontrivial(R)126  requires integral : IntegralOver(f, R, S, x)127  shows AlgebraicOver(f, R, S, x)128proof129  have oneIn : R[1] ∈ R by typecheck130  have distinct := Nontrivial.distinct with nontrivial131  have nonzero : R[1] ≠ R[0]132    intro equal133    apply distinct134    cc135  have one := IsRingHom.one with hom136  obtain ⟨cs, list, relation⟩ := integral.right137  unfold AlgebraicOver138  refine ⟨element, R[1], oneIn, nonzero, cs, list, ?_⟩139  simp [polynomialHorner]140141end Rings142