-- Polynomial coefficient carriers, constants, and variables (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
import MonomialIdeal
import FactorTheorem
import Ring.SumExtension

-- This base module constructs the carrier, constants, and variables.
-- Polynomial.Ring builds the commutative ring using finite convolution.
def polynomials (I A z : Set) : Set := coefficientMaps(monomials(I), A, z)
def polynomialTerm (I A z a m : Set) : Set := coefficientSingle(monomials(I), A, z, a, m)
def polynomialConstant (I A z a : Set) : Set := polynomialTerm(I, A, z, a, monomialOne(I))
def polynomialVariable (I A z unit j : Set) : Set := polynomialTerm(I, A, z, unit, monomialVariable(I, j))

notation scoped polynomialVariable(I, R, j) => polynomialVariable(I, R.carrier, R.zero, R.one, j)

notation scoped polynomialConstant(I, R, a) => polynomialConstant(I, R.carrier, R.zero, a)

theorem polynomials.map (I A z p : Set)
  requires member : p ∈ polynomials(I, A, z)
  shows CoefficientMap(p, monomials(I), A, z)
proof
  unfold polynomials at member
  have data := coefficientMaps.membership.forward with member
  exact data.right

theorem polynomials.contains (I A z p : Set)
  requires map : CoefficientMap(p, monomials(I), A, z)
  shows p ∈ polynomials(I, A, z)
proof
  unfold polynomials
  exact coefficientMaps.contains with map

theorem polynomials.function (I A z p : Set)
  requires member : p ∈ polynomials(I, A, z)
  shows p : monomials(I) → A
proof
  have map := polynomials.map with member
  exact CoefficientMap.function with map

theorem polynomials.coefficient (I A z p m : Set)
  requires member : p ∈ polynomials(I, A, z)
  requires monomial : m ∈ monomials(I)
  shows p(m) ∈ A
proof
  have function := polynomials.function with member
  exact FunctionBetween.apply_closed with function, monomial

theorem polynomials.finite_support (I A z p : Set)
  requires member : p ∈ polynomials(I, A, z)
  shows Finite(functionSupport(p, monomials(I), z))
proof
  have map := polynomials.map with member
  exact CoefficientMap.finite_support with map

theorem polynomials.ext (I A z p q : Set)
  requires left : p ∈ polynomials(I, A, z)
  requires right : q ∈ polynomials(I, A, z)
  requires coefficients : ∀ m ∈ monomials(I), p(m) = q(m)
  shows p = q
proof
  have functionP := polynomials.function with left
  have functionQ := polynomials.function with right
  exact FunctionBetween.ext with functionP, functionQ, coefficients

theorem polynomialTerm.member (I A z a m : Set)
  requires zeroIn : z ∈ A
  requires coefficient : a ∈ A
  shows polynomialTerm(I, A, z, a, m) ∈ polynomials(I, A, z)
proof
  have map := CoefficientMap.single at monomials(I), A, z, a, m with *
  apply polynomials.contains
  unfold polynomialTerm
  exact map

theorem polynomialTerm.same (I A z a m : Set)
  requires zeroIn : z ∈ A
  requires coefficient : a ∈ A
  requires monomial : m ∈ monomials(I)
  shows polynomialTerm(I, A, z, a, m)(m) = a
proof
  unfold polynomialTerm
  exact coefficientSingle.same with *

theorem polynomialTerm.other (I A z a m n : Set)
  requires zeroIn : z ∈ A
  requires coefficient : a ∈ A
  requires monomial : n ∈ monomials(I)
  requires different : n ≠ m
  shows polynomialTerm(I, A, z, a, m)(n) = z
proof
  unfold polynomialTerm
  exact coefficientSingle.other with *

theorem polynomialConstant.member (I A z a : Set)
  requires zeroIn : z ∈ A
  requires coefficient : a ∈ A
  shows polynomialConstant(I, A, z, a) ∈ polynomials(I, A, z)
proof
  unfold polynomialConstant
  exact polynomialTerm.member with *

theorem polynomialConstant.coefficient (I A z a : Set)
  requires zeroIn : z ∈ A
  requires coefficient : a ∈ A
  shows polynomialConstant(I, A, z, a)(monomialOne(I)) = a
proof
  have unit := monomialOne.member at I
  unfold polynomialConstant
  exact polynomialTerm.same with *

theorem polynomialConstant.injective (I A z a b : Set)
  requires zeroIn : z ∈ A
  requires left : a ∈ A
  requires right : b ∈ A
  requires equal : polynomialConstant(I, A, z, a) = polynomialConstant(I, A, z, b)
  shows a = b
proof
  have valueA := polynomialConstant.coefficient at I, A, z, a with *
  have valueB := polynomialConstant.coefficient at I, A, z, b with *
  cc

theorem polynomialVariable.member (I A z unit j : Set)
  requires zeroIn : z ∈ A
  requires unitIn : unit ∈ A
  shows polynomialVariable(I, A, z, unit, j) ∈ polynomials(I, A, z)
proof
  unfold polynomialVariable
  exact polynomialTerm.member with *

theorem polynomialVariable.coefficient (I A z unit j : Set)
  requires zeroIn : z ∈ A
  requires unitIn : unit ∈ A
  shows polynomialVariable(I, A, z, unit, j)(monomialVariable(I, j)) = unit
proof
  have monomial := monomialVariable.member at I, j
  unfold polynomialVariable
  exact polynomialTerm.same with *

theorem polynomialTerm.index_injective (I A z a m n : Set)
  requires zeroIn : z ∈ A
  requires coefficient : a ∈ A
  requires first : m ∈ monomials(I)
  requires second : n ∈ monomials(I)
  requires nonzero : a ≠ z
  requires equal : polynomialTerm(I, A, z, a, m) = polynomialTerm(I, A, z, a, n)
  shows m = n
proof
  have alternatives : m = n ∨ m ≠ n by tauto
  cases alternatives with same | different
  . exact same
  . have valueM := polynomialTerm.same at I, A, z, a, m with *
    have valueN := polynomialTerm.other at I, A, z, a, n, m with *
    have impossible : a = z by cc
    exfalso
    exact nonzero with impossible

theorem polynomialVariable.injective (I A z unit j k : Set)
  requires zeroIn : z ∈ A
  requires unitIn : unit ∈ A
  requires nonzero : unit ≠ z
  requires first : j ∈ I
  requires second : k ∈ I
  requires equal : polynomialVariable(I, A, z, unit, j) = polynomialVariable(I, A, z, unit, k)
  shows j = k
proof
  have monomialJ := monomialVariable.member at I, j
  have monomialK := monomialVariable.member at I, k
  unfold polynomialVariable at equal
  have equalMonomials := polynomialTerm.index_injective with *
  exact monomialVariable.injective with *

section Rings
variable (I A add zero neg mul one : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)

theorem polynomials.zero
  shows constantFunction(monomials(I), A, zero) ∈ polynomials(I, A, zero)
proof
  have map := CoefficientMap.zero at monomials(I), A, add, zero, neg, mul, one with *
  exact polynomials.contains with map

theorem polynomials.add (p q : Set)
  requires left : p ∈ polynomials(I, A, zero)
  requires right : q ∈ polynomials(I, A, zero)
  shows coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) ∈ polynomials(I, A, zero)
proof
  have mapP := polynomials.map with left
  have mapQ := polynomials.map with right
  have combined := CoefficientMap.add with ring, mapP, mapQ
  exact polynomials.contains with combined

theorem polynomials.neg (p : Set)
  requires member : p ∈ polynomials(I, A, zero)
  shows coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) ∈ polynomials(I, A, zero)
proof
  have map := polynomials.map with member
  have negative := CoefficientMap.neg with ring, map
  exact polynomials.contains with negative

theorem polynomials.scale (a p : Set)
  requires scalar : a ∈ A
  requires member : p ∈ polynomials(I, A, zero)
  shows coefficientScale(monomials(I), A, add, zero, neg, mul, one, a, p) ∈ polynomials(I, A, zero)
proof
  have map := polynomials.map with member
  have scaled := CoefficientMap.scale with ring, scalar, map
  exact polynomials.contains with scaled

end Rings
-- Polynomials whose nonzero coefficients lie in a monomial ideal.
def monomialIdealPolynomials (V A z U : Set) : Set :=
  {p ∈ polynomials(V, A, z) | functionSupport(p, monomials(V), z) ⊆ U}

theorem monomialIdealPolynomials.finite_description (V A z U : Set)
  requires variables : Finite(V)
  requires ideal : MonomialIdeal(V, U)
  shows ∃ B, Finite(B) ∧ B ⊆ U ∧ (∀ p ∈ polynomials(V, A, z),
    p ∈ monomialIdealPolynomials(V, A, z, U) ↔
    (∀ m ∈ functionSupport(p, monomials(V), z), ∃ b ∈ B, MonomialDivides(V, b, m)))
proof
  obtain ⟨B, finite, included, equation⟩ := MonomialIdeal.finite_generated with variables, ideal
  refine ⟨B, finite, included, _⟩
  intros p polynomial
  constructor
  . intro member
    have data := monomialIdealPolynomials.membership.forward with member
    have bounded := data.right
    intros m hm
    have inIdeal := bounded with m, hm
    rw equation at inIdeal
    have span := monomialSpan.membership.forward with inIdeal
    exact span.right
  . intro covered
    have bounded : functionSupport(p, monomials(V), z) ⊆ U
      intros m hm
      have support := functionSupport.membership.forward with hm
      have generator := covered with m, hm
      rw equation
      apply monomialSpan.membership.backward
      constructor
      . exact support.left
      . exact generator
    exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩