Dickson

Classical Dickson finite bases and monomial ideals, in arbitrary finite dimension

Open in Workbench View on GitHub

1-- Classical Dickson finite bases and monomial ideals, in arbitrary finite dimension.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module DicksonExamples8import Grace.Cumulus.Algebra.Polynomial910theorem finite_basis (V S : Set)11  requires variables : Finite(V)12  requires monomials : S ⊆ monomials(V)13  shows ∃ B, Finite(B) ∧ B ⊆ S ∧ (∀ m ∈ S, ∃ b ∈ B, ∃ q ∈ monomials(V), monomialProduct(V, b, q) = m)14proof15  exact Dickson.finite_factor_basis at V, S with *1617theorem finite_generators (V U : Set)18  requires variables : Finite(V)19  requires ideal : MonomialIdeal(V, U)20  shows ∃ B, Finite(B) ∧ B ⊆ U ∧ U = monomialSpan(V, B)21proof22  exact MonomialIdeal.finite_generated with variables, ideal2324theorem finite_antichains (V S : Set)25  requires variables : Finite(V)26  requires monomials : S ⊆ monomials(V)27  requires antichain : MonomialAntichain(V, S)28  shows Finite(S)29proof30  exact Dickson.antichains_finite with variables, monomials, antichain3132theorem finitely_many_minimal_elements (V S : Set)33  requires variables : Finite(V)34  requires monomials : S ⊆ monomials(V)35  shows Finite(minimalMonomials(V, S))36proof37  exact Dickson.minimal_finite with variables, monomials3839theorem two_variables (x y U : Set)40  requires ideal : MonomialIdeal(insert(y, {x}), U)41  shows ∃ B, Finite(B) ∧ B ⊆ U ∧ U = monomialSpan(insert(y, {x}), B)42proof43  have singleton := Finite.singleton at x44  have variables := Finite.insert at {x}, y with singleton45  exact MonomialIdeal.finite_generated with variables, ideal46