-- Monomial ideals, Dickson finite generation, and finite antichains (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.MonomialIdeal
import Dickson

predicate MonomialIdeal (V U : Set) := U ⊆ monomials(V) ∧
  (∀ m ∈ U, ∀ q ∈ monomials(V), monomialProduct(V, m, q) ∈ U)
def monomialSpan (V G : Set) : Set := {m ∈ monomials(V) | ∃ b ∈ G, MonomialDivides(V, b, m)}
predicate MonomialAntichain (V S : Set) := ∀ m ∈ S, ∀ n ∈ S, MonomialDivides(V, m, n) → m = n
def minimalMonomials (V S : Set) : Set := {m ∈ S | ∀ n ∈ S, MonomialDivides(V, n, m) → n = m}

theorem MonomialIdeal.subset (V U : Set)
  requires ideal : MonomialIdeal(V, U)
  shows U ⊆ monomials(V)
proof
  exact ideal.left

theorem MonomialIdeal.upward (V U m n : Set)
  requires ideal : MonomialIdeal(V, U)
  requires member : m ∈ U
  requires monomial : n ∈ monomials(V)
  requires divides : MonomialDivides(V, m, n)
  shows n ∈ U
proof
  have subset := MonomialIdeal.subset with ideal
  have mMember := subset with m, member
  obtain ⟨q, qMember, equation⟩ := MonomialDivides.iff_factor.forward at V, m, n with *
  have product := ideal.right with m, member, q, qMember
  rwa equation at product

theorem monomialSpan.contains (V G : Set)
  requires subset : G ⊆ monomials(V)
  shows G ⊆ monomialSpan(V, G)
proof
  intros m hm
  have member := subset with m, hm
  have divides := MonomialDivides.reflexive with member
  exact monomialSpan.membership.backward with ⟨member, m, hm, divides⟩

theorem monomialSpan.ideal (V G : Set)
  requires subset : G ⊆ monomials(V)
  shows MonomialIdeal(V, monomialSpan(V, G))
proof
  constructor
  . settle with Subset, monomialSpan.membership
  . intros m hm q hq
    have data := monomialSpan.membership.forward with hm
    obtain ⟨b, hb, divides⟩ := data.right
    have included := subset
    have bMember := included with b, hb
    have product := monomialProduct.member at V, m, q with *
    have factor := MonomialDivides.product at V, m, q with *
    have trans := MonomialDivides.transitive at V, b, m, monomialProduct(V, m, q) with *
    exact monomialSpan.membership.backward with ⟨product, b, hb, trans⟩

theorem monomialSpan.least (V G U : Set)
  requires ideal : MonomialIdeal(V, U)
  requires generators : G ⊆ U
  shows monomialSpan(V, G) ⊆ U
proof
  intros m hm
  have data := monomialSpan.membership.forward with hm
  obtain ⟨b, hb, divides⟩ := data.right
  have member := generators with b, hb
  exact MonomialIdeal.upward with *

theorem MonomialIdeal.finite_generated (V U : Set)
  requires variables : Finite(V)
  requires ideal : MonomialIdeal(V, U)
  shows ∃ B, Finite(B) ∧ B ⊆ U ∧ U = monomialSpan(V, B)
proof
  have subset := MonomialIdeal.subset with ideal
  obtain ⟨B, basis⟩ := Dickson.finite_basis with variables, subset
  rcases basis with ⟨finite, included, covers⟩
  have reverse := monomialSpan.least with *
  have forward : U ⊆ monomialSpan(V, B)
    intros m hm
    have source := subset
    have member := source with m, hm
    obtain ⟨b, hb, divides⟩ := covers with m, hm
    exact monomialSpan.membership.backward with ⟨member, b, hb, divides⟩
  have equal := Subset.antisymmetric with forward, reverse
  refine ⟨B, finite, included, equal⟩

theorem Dickson.antichains_finite (V S : Set)
  requires variables : Finite(V)
  requires subset : S ⊆ monomials(V)
  requires antichain : MonomialAntichain(V, S)
  shows Finite(S)
proof
  obtain ⟨B, basis⟩ := Dickson.finite_basis with variables, subset
  rcases basis with ⟨finite, included, covers⟩
  have reverse : S ⊆ B
    intros m hm
    obtain ⟨b, hb, divides⟩ := covers with m, hm
    have inS := included with b, hb
    have equal := antichain with b, inS, m, hm, divides
    rwa ← equal
  exact Finite.subset with finite, reverse

theorem minimalMonomials.subset (V S : Set)
  shows minimalMonomials(V, S) ⊆ S
proof
  simp

theorem minimalMonomials.antichain (V S : Set)
  shows MonomialAntichain(V, minimalMonomials(V, S))
proof
  intros m hm n hn divides
  have mData := minimalMonomials.membership.forward with hm
  have nData := minimalMonomials.membership.forward with hn
  exact nData.right with m, mData.left, divides

theorem Dickson.minimal_finite (V S : Set)
  requires variables : Finite(V)
  requires subset : S ⊆ monomials(V)
  shows Finite(minimalMonomials(V, S))
proof
  have included := minimalMonomials.subset at V, S
  have bounded := Subset.transitive with included, subset
  have antichain := minimalMonomials.antichain at V, S
  exact Dickson.antichains_finite with variables, bounded, antichain