Grace/Cumulus/Algebra/Polynomial/MonomialIdeal.g17

Open in Workbench Download source

Imports

Dickson

Declarations

• MonomialIdeal predicate
• monomialSpan def
• MonomialAntichain predicate
• minimalMonomials def
• MonomialIdeal.subset theorem derivation
• MonomialIdeal.upward theorem derivation
• monomialSpan.contains theorem derivation
• monomialSpan.ideal theorem derivation
• monomialSpan.least theorem derivation
• MonomialIdeal.finite_generated theorem derivation
• Dickson.antichains_finite theorem derivation
• minimalMonomials.subset theorem derivation
• minimalMonomials.antichain theorem derivation
• Dickson.minimal_finite theorem derivation

Source

1-- Monomial ideals, Dickson finite generation, and finite antichains (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.MonomialIdeal8import Dickson910predicate MonomialIdeal (V U : Set) := U ⊆ monomials(V) ∧11  (∀ m ∈ U, ∀ q ∈ monomials(V), monomialProduct(V, m, q) ∈ U)12def monomialSpan (V G : Set) : Set := {m ∈ monomials(V) | ∃ b ∈ G, MonomialDivides(V, b, m)}13predicate MonomialAntichain (V S : Set) := ∀ m ∈ S, ∀ n ∈ S, MonomialDivides(V, m, n) → m = n14def minimalMonomials (V S : Set) : Set := {m ∈ S | ∀ n ∈ S, MonomialDivides(V, n, m) → n = m}1516theorem MonomialIdeal.subset (V U : Set)17  requires ideal : MonomialIdeal(V, U)18  shows U ⊆ monomials(V)19proof20  exact ideal.left2122theorem MonomialIdeal.upward (V U m n : Set)23  requires ideal : MonomialIdeal(V, U)24  requires member : m ∈ U25  requires monomial : n ∈ monomials(V)26  requires divides : MonomialDivides(V, m, n)27  shows n ∈ U28proof29  have subset := MonomialIdeal.subset with ideal30  have mMember := subset with m, member31  obtain ⟨q, qMember, equation⟩ := MonomialDivides.iff_factor.forward at V, m, n with *32  have product := ideal.right with m, member, q, qMember33  rwa equation at product3435theorem monomialSpan.contains (V G : Set)36  requires subset : G ⊆ monomials(V)37  shows G ⊆ monomialSpan(V, G)38proof39  intros m hm40  have member := subset with m, hm41  have divides := MonomialDivides.reflexive with member42  exact monomialSpan.membership.backward with ⟨member, m, hm, divides⟩4344theorem monomialSpan.ideal (V G : Set)45  requires subset : G ⊆ monomials(V)46  shows MonomialIdeal(V, monomialSpan(V, G))47proof48  constructor49  . settle with Subset, monomialSpan.membership50  . intros m hm q hq51    have data := monomialSpan.membership.forward with hm52    obtain ⟨b, hb, divides⟩ := data.right53    have included := subset54    have bMember := included with b, hb55    have product := monomialProduct.member at V, m, q with *56    have factor := MonomialDivides.product at V, m, q with *57    have trans := MonomialDivides.transitive at V, b, m, monomialProduct(V, m, q) with *58    exact monomialSpan.membership.backward with ⟨product, b, hb, trans⟩5960theorem monomialSpan.least (V G U : Set)61  requires ideal : MonomialIdeal(V, U)62  requires generators : G ⊆ U63  shows monomialSpan(V, G) ⊆ U64proof65  intros m hm66  have data := monomialSpan.membership.forward with hm67  obtain ⟨b, hb, divides⟩ := data.right68  have member := generators with b, hb69  exact MonomialIdeal.upward with *7071theorem MonomialIdeal.finite_generated (V U : Set)72  requires variables : Finite(V)73  requires ideal : MonomialIdeal(V, U)74  shows ∃ B, Finite(B) ∧ B ⊆ U ∧ U = monomialSpan(V, B)75proof76  have subset := MonomialIdeal.subset with ideal77  obtain ⟨B, basis⟩ := Dickson.finite_basis with variables, subset78  rcases basis with ⟨finite, included, covers⟩79  have reverse := monomialSpan.least with *80  have forward : U ⊆ monomialSpan(V, B)81    intros m hm82    have source := subset83    have member := source with m, hm84    obtain ⟨b, hb, divides⟩ := covers with m, hm85    exact monomialSpan.membership.backward with ⟨member, b, hb, divides⟩86  have equal := Subset.antisymmetric with forward, reverse87  refine ⟨B, finite, included, equal⟩8889theorem Dickson.antichains_finite (V S : Set)90  requires variables : Finite(V)91  requires subset : S ⊆ monomials(V)92  requires antichain : MonomialAntichain(V, S)93  shows Finite(S)94proof95  obtain ⟨B, basis⟩ := Dickson.finite_basis with variables, subset96  rcases basis with ⟨finite, included, covers⟩97  have reverse : S ⊆ B98    intros m hm99    obtain ⟨b, hb, divides⟩ := covers with m, hm100    have inS := included with b, hb101    have equal := antichain with b, inS, m, hm, divides102    rwa ← equal103  exact Finite.subset with finite, reverse104105theorem minimalMonomials.subset (V S : Set)106  shows minimalMonomials(V, S) ⊆ S107proof108  simp109110theorem minimalMonomials.antichain (V S : Set)111  shows MonomialAntichain(V, minimalMonomials(V, S))112proof113  intros m hm n hn divides114  have mData := minimalMonomials.membership.forward with hm115  have nData := minimalMonomials.membership.forward with hn116  exact nData.right with m, mData.left, divides117118theorem Dickson.minimal_finite (V S : Set)119  requires variables : Finite(V)120  requires subset : S ⊆ monomials(V)121  shows Finite(minimalMonomials(V, S))122proof123  have included := minimalMonomials.subset at V, S124  have bounded := Subset.transitive with included, subset125  have antichain := minimalMonomials.antichain at V, S126  exact Dickson.antichains_finite with variables, bounded, antichain127