-- Polynomial homomorphisms depend only on the variables actually used (ZF).
-- 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.EvaluationSupport
import EvaluationOver
import Variables

theorem polynomialMap.variables (I A z B o f p : Set)
  requires function : f : A → B
  requires zero : f(z) = o
  requires polynomial : p ∈ polynomials(I, A, z)
  shows polynomialVariablesUsed(I, B, o, polynomialMap(I, A, z, B, o, f)(p)) ⊆ polynomialVariablesUsed(I, A, z, p)
proof
  intros i used
  obtain ⟨m, support, exponent⟩ := polynomialVariablesUsed.membership.forward with used
  obtain ⟨monomial, nonzero⟩ := functionSupport.membership.forward with support
  have value := polynomialMap.coefficient with *
  have coefficient : p(m) ≠ z
    intro vanishes
    apply nonzero
    cc
  have original : m ∈ functionSupport(p, monomials(I), z)
    exact functionSupport.membership.backward with ⟨monomial, coefficient⟩
  exact polynomialVariablesUsed.membership.backward with ⟨m, original, exponent⟩

defgraph polynomialHomVariables (I A z one B h : Set) (i ∈ I) : B := h(polynomialVariable(I, A, z, one, i))
requires zeroIn : z ∈ A
requires oneIn : one ∈ A
requires function : h : polynomials(I, A, z) → B
proof
  have variableIn := polynomialVariable.member at I, A, z, one, i with *
  exact FunctionBetween.apply_closed with function, variableIn

section Rings
variable (I A add z neg mul one B plus o minus times unit f : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring S := (B, plus, o, minus, times, unit)
notation ring P := R[I]
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)

theorem polynomialAtOver.agree_on_variables (v w p : Set)
  requires first : v : I → S
  requires second : w : I → S
  requires polynomial : p ∈ P
  requires agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), v(i) = w(i)
  shows polynomialAtOver(I, R, S, f, v)(p) = polynomialAtOver(I, R, S, f, w)(p)
proof
  have function := IsRingHom.function with hom
  have zero := IsRingHom.zero with hom
  have mapped := polynomialMap.member with *
  have variables := polynomialMap.variables with *
  have same : ∀ i ∈ polynomialVariablesUsed(I, S, polynomialMap(I, R, S, f)(p)), v(i) = w(i)
    intros i used
    have original := variables with i, used
    exact agreement with i, original
  have equal := polynomialAt.agree_on_variables at I, B, plus, o, minus, times, unit, v, w, polynomialMap(I, R, S, f)(p) with *
  have left := polynomialAtOver.value at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, p with *
  have right := polynomialAtOver.value at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, w, p with *
  cc

theorem IsRingHom.polynomial_local_ext (h g p : Set)
  requires first : IsRingHom(h, P, S)
  requires second : IsRingHom(g, P, S)
  requires polynomial : p ∈ P
  requires firstConstants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = f(a)
  requires secondConstants : ∀ a ∈ R, g(polynomialConstant(I, R, a)) = f(a)
  requires agreement : ∀ i ∈ polynomialVariablesUsed(I, R, p), h(polynomialVariable(I, R, i)) = g(polynomialVariable(I, R, i))
  shows h(p) = g(p)
proof
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have functionH := IsRingHom.function with first
  have functionG := IsRingHom.function with second
  have assignmentH := polynomialHomVariables.function at I, A, z, one, B, h with *
  have assignmentG := polynomialHomVariables.function at I, A, z, one, B, g with *
  have variablesH : ∀ i ∈ I, h(polynomialVariable(I, R, i)) = polynomialHomVariables(I, A, z, one, B, h)(i)
    intros i index
    symm
    exact polynomialHomVariables.value with *
  have variablesG : ∀ i ∈ I, g(polynomialVariable(I, R, i)) = polynomialHomVariables(I, A, z, one, B, g)(i)
    intros i index
    symm
    exact polynomialHomVariables.value with *
  have representationH := polynomialAtOver.unique at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialHomVariables(I, A, z, one, B, h), h with *
  have representationG := polynomialAtOver.unique at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, polynomialHomVariables(I, A, z, one, B, g), g with *
  have same : ∀ i ∈ polynomialVariablesUsed(I, R, p), polynomialHomVariables(I, A, z, one, B, h)(i) = polynomialHomVariables(I, A, z, one, B, g)(i)
    intros i used
    have subset := polynomialVariablesUsed.subset at I, A, z, p
    have index := subset with i, used
    have left := variablesH with i, index
    have right := variablesG with i, index
    have equal := agreement with i, used
    cc
  have equal := polynomialAtOver.agree_on_variables with *
  rwa [representationH, representationG]

end Rings