-- Closure of polynomial supports in monomial ideals under the ring operations.
-- 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.IdealSupport
import Ring

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

theorem monomialIdealPolynomials.zero
  shows constantFunction(monomials(I), A, zero) ∈ monomialIdealPolynomials(I, A, zero, U)
proof
  have polynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  apply monomialIdealPolynomials.membership.backward
  refine ⟨polynomial, _⟩
  intros m hm
  have data := functionSupport.membership.forward with hm
  have value := constantFunction.apply at monomials(I), A, m, zero with *
  exfalso
  exact data.right with value

theorem monomialIdealPolynomials.add (p q : Set)
  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)
  requires memberQ : q ∈ monomialIdealPolynomials(I, A, zero, U)
  shows coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)
proof
  have dataP := monomialIdealPolynomials.membership.forward with memberP
  have dataQ := monomialIdealPolynomials.membership.forward with memberQ
  have polynomial := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have functionP := polynomials.function with dataP.left
  have functionQ := polynomials.function with dataQ.left
  have support := coefficientAdd.support at monomials(I), A, add, zero, neg, mul, one, p, q with *
  have unionBound : functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero) ⊆ U
    have boundP := dataP.right
    have boundQ := dataQ.right
    simp [Subset, union2.membership]
  have bounded := Subset.transitive with support, unionBound
  exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩

theorem monomialIdealPolynomials.neg (p : Set)
  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)
  shows coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) ∈ monomialIdealPolynomials(I, A, zero, U)
proof
  have data := monomialIdealPolynomials.membership.forward with memberP
  have polynomial := polynomials.neg at I, A, add, zero, neg, mul, one, p with *
  have function := polynomials.function with data.left
  have support := coefficientNeg.support with *
  have bounded := Subset.transitive with support, data.right
  exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩

theorem monomialIdealPolynomials.mul_right (p q : Set)
  requires ideal : MonomialIdeal(I, U)
  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)
proof
  have data := monomialIdealPolynomials.membership.forward with memberP
  have polynomial := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have bounded : functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, q), monomials(I), zero) ⊆ U
    intros m hm
    obtain ⟨u, hu, v, hv, equation⟩ := polynomialProduct.support_factor at I, A, add, zero, neg, mul, one, p, q, m with *
    have supportBound := data.right
    have inIdeal := supportBound with u, hu
    have monomial := functionSupport.membership.forward with hv
    have product := ideal.right with u, inIdeal, v, monomial.left
    rwa equation
  exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩

theorem monomialIdealPolynomials.mul_left (p q : Set)
  requires ideal : MonomialIdeal(I, U)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ monomialIdealPolynomials(I, A, zero, U)
  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)
proof
  have data := monomialIdealPolynomials.membership.forward with memberQ
  have comm := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, p, q with *
  have absorbed := monomialIdealPolynomials.mul_right at I, A, add, zero, neg, mul, one, U, q, p with *
  rwa comm

theorem monomialIdealPolynomials.ideal
  requires ideal : MonomialIdeal(I, U)
  shows IsIdeal(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), monomialIdealPolynomials(I, A, zero, U))
proof
  have subset : monomialIdealPolynomials(I, A, zero, U) ⊆ polynomials(I, A, zero)
    intros p hp
    have data := monomialIdealPolynomials.membership.forward with hp
    exact data.left
  have zeroMember := monomialIdealPolynomials.zero at I, A, add, zero, neg, mul, one, U with *
  have addition : ∀ p ∈ monomialIdealPolynomials(I, A, zero, U), ∀ q ∈ monomialIdealPolynomials(I, A, zero, U), (polynomialAdd(I, A, add, zero, neg, mul, one))(p, q) ∈ monomialIdealPolynomials(I, A, zero, U)
    intros p hp q hq
    have dataP := monomialIdealPolynomials.membership.forward with hp
    have dataQ := monomialIdealPolynomials.membership.forward with hq
    have value := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *
    rw value
    exact monomialIdealPolynomials.add at I, A, add, zero, neg, mul, one, U, p, q with *
  have negation : ∀ p ∈ monomialIdealPolynomials(I, A, zero, U), (polynomialNeg(I, A, add, zero, neg, mul, one))(p) ∈ monomialIdealPolynomials(I, A, zero, U)
    intros p hp
    have data := monomialIdealPolynomials.membership.forward with hp
    have value := polynomialNeg.apply at I, A, add, zero, neg, mul, one, p with *
    rw value
    exact monomialIdealPolynomials.neg at I, A, add, zero, neg, mul, one, U, p with *
  have absorption : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ monomialIdealPolynomials(I, A, zero, U), (polynomialMul(I, A, add, zero, neg, mul, one))(p, q) ∈ monomialIdealPolynomials(I, A, zero, U) ∧ (polynomialMul(I, A, add, zero, neg, mul, one))(q, p) ∈ monomialIdealPolynomials(I, A, zero, U)
    intros p hp q hq
    have data := monomialIdealPolynomials.membership.forward with hq
    have leftValue := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *
    have rightValue := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, p with *
    constructor
    . rw leftValue
      exact monomialIdealPolynomials.mul_left at I, A, add, zero, neg, mul, one, U, p, q with *
    . rw rightValue
      exact monomialIdealPolynomials.mul_right at I, A, add, zero, neg, mul, one, U, q, p with *
  unfold IsIdeal
  refine ⟨subset, zeroMember, addition, negation, absorption⟩

end Rings