-- Polynomial homomorphisms are determined by coefficients and variable values.
-- 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.Universal
import Generation
import Assignment
import Ring.Equalizer

section Homomorphisms
variable (I A add zero neg mul one B plus z minus times unit f g : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
notation ring S := (B, plus, z, minus, times, unit)
hypothesis ring : IsCommRing(R)
hypothesis first : IsRingHom(f, P, S)
hypothesis second : IsRingHom(g, P, S)

theorem IsRingHom.polynomial_ext
  requires constants : ∀ a ∈ R, f(polynomialConstant(I, R, a)) = g(polynomialConstant(I, R, a))
  requires variables : ∀ j ∈ I, f(polynomialVariable(I, R, j)) = g(polynomialVariable(I, R, j))
  shows f = g
proof
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have subring := ringEqualizer.subring with source, first, second
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have coefficients : functionImage(polynomialCoefficients(I, R), R, P) ⊆ ringEqualizer(f, g, P)
    intros p hp
    obtain ⟨member, a, ha, shape⟩ := functionImage.membership.forward with hp
    have value := polynomialCoefficients.value at I, A, zero, a with *
    have equal := constants with a, ha
    apply ringEqualizer.membership.backward
    constructor
    . exact member
    . cc
  have subalgebra : Subalgebra(polynomialCoefficients(I, R), R, P, ringEqualizer(f, g, P))
    unfold Subalgebra
    refine ⟨subring, coefficients⟩
  have generators : ∀ j ∈ I, polynomialVariable(I, R, j) ∈ ringEqualizer(f, g, P)
    intros j hj
    have member := polynomialVariable.member at I, A, zero, one, j with *
    have equal := variables with j, hj
    exact ringEqualizer.membership.backward with ⟨member, equal⟩
  have all := polynomialSubalgebra.eq_carrier with ring, subalgebra, generators
  have functionF := IsRingHom.function with first
  have functionG := IsRingHom.function with second
  apply FunctionBetween.ext with functionF, functionG
  intros p hp
  have member : p ∈ ringEqualizer(f, g, P) by rwa all
  have data := ringEqualizer.membership.forward with member
  exact data.right

end Homomorphisms

-- The assignment induced by any homomorphism back to the coefficient ring.
defgraph polynomialValues (I A add zero neg mul one h : Set) (j ∈ I) : A := h(polynomialVariable(I, A, zero, one, j))
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires hom : IsRingHom(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 ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have variableMember := polynomialVariable.member at I, A, zero, one, j with *
  exact IsRingHom.closed with hom, variableMember

notation scoped polynomialValues(I, R, h) => polynomialValues(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, h)

section Evaluation
variable (I A add zero neg mul one h : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
hypothesis ring : IsCommRing(R)
hypothesis hom : IsRingHom(h, P, R)
hypothesis constants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = a

theorem IsRingHom.eq_polynomialAt
  shows h = polynomialAt(I, R, polynomialValues(I, A, add, zero, neg, mul, one, h))
proof
  have assignment := polynomialValues.function at I, A, add, zero, neg, mul, one, h with *
  have evaluation := polynomialAt.hom with *
  have sameConstants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = polynomialAt(I, R, polynomialValues(I, A, add, zero, neg, mul, one, h))(polynomialConstant(I, R, a))
    intros a ha
    have first := constants with a, ha
    have second := polynomialAt.constant with *
    cc
  have sameVariables : ∀ j ∈ I, h(polynomialVariable(I, R, j)) = polynomialAt(I, R, polynomialValues(I, A, add, zero, neg, mul, one, h))(polynomialVariable(I, R, j))
    intros j hj
    have first := polynomialValues.value at I, A, add, zero, neg, mul, one, h, j with *
    have second := polynomialAt.variable with *
    cc
  exact IsRingHom.polynomial_ext with ring, hom, evaluation, sameConstants, sameVariables

end Evaluation