-- Multiplicative monomial values extend canonically to polynomial homomorphisms.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Polynomial.EvaluationHom
import Evaluation

predicate MonomialCharacter (I A mul one h : Set) :=
  FunctionBetween(h, monomials(I), A) ∧ h(monomialOne(I)) = one ∧
  (∀ m ∈ monomials(I), ∀ n ∈ monomials(I), h(monomialProduct(I, m, n)) = call2(mul, h(m), h(n)))

predicate EvaluationMultiplies (I A add zero neg mul one h p q : Set) :=
  polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialProduct(I, A, add, zero, neg, mul, one, p, q)) = call2(mul, polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q))

def evaluationProducts (I A add zero neg mul one h p : Set) : Set :=
  {q ∈ polynomials(I, A, zero) | EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, q)}

-- Sending every monomial to one evaluates every variable at one.
theorem MonomialCharacter.at_one (I A add zero neg mul one : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows MonomialCharacter(I, A, mul, one, constantFunction(monomials(I), A, one))
proof
  have ordinary := IsCommRing.ring with ring
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have function := constantFunction.function at monomials(I), A, one with *
  have unit := monomialOne.member at I
  have unitValue := constantFunction.apply at monomials(I), A, monomialOne(I), one with *
  unfold MonomialCharacter
  refine ⟨function, unitValue, ?_⟩
  intros m hm n hn
  have product := monomialProduct.member with hm, hn
  have left := constantFunction.apply at monomials(I), A, monomialProduct(I, m, n), one with *
  have first := constantFunction.apply at monomials(I), A, m, one with *
  have second := constantFunction.apply at monomials(I), A, n, one with *
  have identity := IsMonoid.left_identity with *
  cc

section Evaluation
variable (I A add zero neg mul one h : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
hypothesis character : MonomialCharacter(I, A, mul, one, h)
notation ring R := (A, add, zero, neg, mul, one)

theorem EvaluationMultiplies.zero (p : Set)
  requires member : p ∈ polynomials(I, A, zero)
  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, constantFunction(monomials(I), A, zero))
proof
  unfold MonomialCharacter at character
  have product := polynomialProduct.zero_right with *
  have zeroValue := polynomialEvaluate.zero at I, A, add, zero, neg, mul, one, h with *
  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *
  have annihilate : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * zero = zero by ring
  unfold EvaluationMultiplies
  cc

theorem EvaluationMultiplies.swap (p q : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires equation : EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, q)
  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, q, p)
proof
  unfold MonomialCharacter at character
  have comm := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, p, q with *
  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *
  have valueQ := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, q with *
  have commute : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p)
    ring
  unfold EvaluationMultiplies at equation
  unfold EvaluationMultiplies
  cc

theorem EvaluationMultiplies.add (p q r : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  requires first : EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, q)
  requires second : EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, r)
  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r))
proof
  unfold MonomialCharacter at character
  have pq := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have pr := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *
  have distribute := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, q, r with *
  have evaluateSum := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, q, r with *
  have evaluateProducts := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *
  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *
  have valueQ := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, q with *
  have valueR := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, r with *
  have distributeValues : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * (polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(r)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(r)
    ring
  unfold EvaluationMultiplies at first
  unfold EvaluationMultiplies at second
  unfold EvaluationMultiplies
  cc

theorem EvaluationMultiplies.terms (a b m n : Set)
  requires coefficientA : a ∈ A
  requires coefficientB : b ∈ A
  requires monomialM : m ∈ monomials(I)
  requires monomialN : n ∈ monomials(I)
  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))
proof
  have data := character
  have values := data.left
  have multiplication := data.right.right with m, monomialM, n, monomialN
  have ordinary := IsCommRing.ring with ring
  have coefficient := IsRing.mul_closed at A, add, zero, neg, mul, one, a, b with *
  have monomial := monomialProduct.member at I, m, n with *
  have product := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, b, m, n with *
  have left := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, a * b, monomialProduct(I, m, n) with *
  have valueA := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, a, m with *
  have valueB := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, b, n with *
  have imageM := FunctionBetween.apply_closed at h, monomials(I), A, m with *
  have imageN := FunctionBetween.apply_closed at h, monomials(I), A, n with *
  have rearrange : (a * b) * (h(m) * h(n)) = (a * h(m)) * (b * h(n)) by ring
  unfold EvaluationMultiplies
  cc

theorem EvaluationMultiplies.term (a m q : Set)
  requires coefficient : a ∈ A
  requires monomial : m ∈ monomials(I)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m), q)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have fixed := polynomialTerm.member at I, A, zero, a, m with *
  have base : constantFunction(monomials(I), A, zero) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m))
    apply evaluationProducts.membership.backward
    constructor
    . exact zeroPolynomial
    . exact EvaluationMultiplies.zero with *
  have terms : ∀ b ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, zero, b, n) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m))
    intros b hb n hn
    have member := polynomialTerm.member at I, A, zero, b, n with *
    apply evaluationProducts.membership.backward
    constructor
    . exact member
    . exact EvaluationMultiplies.terms with *
  have sums : ∀ f ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m)), ∀ g ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m)), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m))
    intros f hf g hg
    have first := evaluationProducts.membership.forward with hf
    have second := evaluationProducts.membership.forward with hg
    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *
    apply evaluationProducts.membership.backward
    constructor
    . exact member
    . exact EvaluationMultiplies.add with *
  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m)), q with *
  have result := evaluationProducts.membership.forward with generated
  exact result.right

theorem polynomialEvaluate.mul (p q : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialProduct(I, A, add, zero, neg, mul, one, p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have base : constantFunction(monomials(I), A, zero) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q)
    apply evaluationProducts.membership.backward
    constructor
    . exact zeroPolynomial
    . exact EvaluationMultiplies.zero with *
  have terms : ∀ b ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, zero, b, n) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q)
    intros b hb n hn
    have member := polynomialTerm.member at I, A, zero, b, n with *
    apply evaluationProducts.membership.backward
    constructor
    . exact member
    . have forward := EvaluationMultiplies.term at I, A, add, zero, neg, mul, one, h, b, n, q with *
      exact EvaluationMultiplies.swap with *
  have sums : ∀ f ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q), ∀ g ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q)
    intros f hf g hg
    have first := evaluationProducts.membership.forward with hf
    have second := evaluationProducts.membership.forward with hg
    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *
    apply evaluationProducts.membership.backward
    constructor
    . exact member
    . exact EvaluationMultiplies.add with *
  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, evaluationProducts(I, A, add, zero, neg, mul, one, h, q), p with *
  have result := evaluationProducts.membership.forward with generated
  exact EvaluationMultiplies.swap at
    I, A, add, zero, neg, mul, one, h, q, p with *

theorem polynomialEvaluate.constant (a : Set)
  requires coefficient : a ∈ A
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialConstant(I, A, zero, a)) = a
proof
  unfold MonomialCharacter at character
  have unit := monomialOne.member at I
  have term := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, a, monomialOne(I) with *
  have identity : a * one = a by ring
  unfold polynomialConstant
  cc

theorem polynomialEvaluate.hom
  shows IsRingHom(polynomialEvaluate(I, A, add, zero, neg, mul, one, h), 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), A, add, zero, neg, mul, one)
proof
  have data := character
  unfold MonomialCharacter at data
  have ordinary := IsCommRing.ring with ring
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have function := polynomialEvaluate.function at I, A, add, zero, neg, mul, one, h with *
  have preservesZero := polynomialEvaluate.zero at I, A, add, zero, neg, mul, one, h with *
  have preservesOne := polynomialEvaluate.constant with *
  have preservesNeg : ∀ p ∈ polynomials(I, A, zero), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)((polynomialNeg(I, A, add, zero, neg, mul, one))(p)) = -polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p)
    intros p hp
    have operation := polynomialNeg.apply with *
    have value := polynomialEvaluate.neg at I, A, add, zero, neg, mul, one, h, p with *
    cc
  have preservesAdd : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ polynomials(I, A, zero), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)((polynomialAdd(I, A, add, zero, neg, mul, one))(p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)
    intros p hp q hq
    have operation := polynomialAdd.apply with hp, hq
    have value := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, p, q with *
    cc
  have preservesMul : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ polynomials(I, A, zero), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)((polynomialMul(I, A, add, zero, neg, mul, one))(p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)
    intros p hp q hq
    have operation := polynomialMul.apply with hp, hq
    have value := polynomialEvaluate.mul with hp, hq
    cc
  unfold IsRingHom
  refine ⟨function, preservesZero, preservesOne, preservesNeg, preservesAdd, preservesMul⟩

end Evaluation