Grace/Cumulus/Algebra/Polynomial/Dickson.g17

Open in Workbench Download source

Imports

Divisibility

Declarations

Source

1-- Dickson's finite-basis theorem by classical finite-coordinate induction (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.Dickson8import Divisibility910predicate MonomialCover (C S B : Set) := ∀ m ∈ S, ∃ b ∈ B, MonomialDivides(C, b, m)11predicate FiniteMonomialBasis (C S B : Set) := Finite(B) ∧ B ⊆ S ∧ MonomialCover(C, S, B)12predicate DicksonOn (V C : Set) := ∀ S, S ⊆ monomials(V) → ∃ B, FiniteMonomialBasis(C, S, B)13def exponentSlice (S j n : Set) : Set := {m ∈ S | m(j) = n}14predicate BoundedMonomialCover (C S j n B : Set) := ∀ m ∈ S, m(j) < n → ∃ b ∈ B, MonomialDivides(insert(j, C), b, m)1516theorem exponentSlice.subset (S j n : Set)17  shows exponentSlice(S, j, n) ⊆ S18proof19  simp2021theorem listExponents.bounded (C i : Set) (xs : List(C))22  requires naturals : ∀ m ∈ C, Nat(m(i))23  shows ∃ n, Nat(n) ∧ ∀ m ∈ listSupport{C}(xs), m(i) ≤ n24proof25  induction xs26  | List.nil =>27    refine ⟨0, Naturals.constructor.zero, _⟩28    intros m member29    rw listSupport at member30    exfalso31    exact set.empty with member32  | List.cons(x, tail) using ih =>33    obtain ⟨n, nNat, bounded⟩ := ih34    have xNat := naturals with x35    have nextNat : Nat(n + x(i)) by typecheck36    refine ⟨n + x(i), nextNat, _⟩37    intros m member38    rw listSupport at member39    have alternatives := insert.membership.forward with member40    cases alternatives with equal | old41    . rw equal42      arith43    . have bound := bounded with m, old44      have subset := listSupport.subset with *45      have inC := subset with m, old46      have mNat := naturals with m, inC47      arith4849theorem Finite.exponents_bounded (V S j : Set)50  requires finite : Finite(S)51  requires subset : S ⊆ monomials(V)52  requires index : j ∈ V53  shows ∃ n, Nat(n) ∧ ∀ m ∈ S, m(j) ≤ n54proof55  obtain ⟨xs, list, covered⟩ := Finite.list_cover with finite56  have naturals : ∀ m ∈ S, Nat(m(j))57    intros m hm58    have included := subset59    have member := included with m, hm60    exact monomials.exponent with *61  obtain ⟨n, natural, bound⟩ := listExponents.bounded at S, j, xs with *62  refine ⟨n, natural, _⟩63  intros m hm64  have member := covered with m, hm65  exact bound with m, member6667theorem DicksonOn.empty (V : Set)68  shows DicksonOn(V, ∅)69proof70  intros S subset71  have casesS : (∃ m, m ∈ S) ∨ ¬(∃ m, m ∈ S) by tauto72  cases casesS with inhabited | empty73  . obtain ⟨a, member⟩ := inhabited74    witness {a}75    unfold FiniteMonomialBasis76    refine ⟨Finite.singleton at a, _, _⟩77      intros b hb78      have equal := singleton.membership.forward with hb79      rwa equal80      intros m hm81      refine ⟨a, singleton.self at a, _⟩82      intros i impossible83      exfalso84      exact set.empty with impossible85  . witness ∅86    unfold FiniteMonomialBasis87    refine ⟨Finite.empty, empty.subset at S, _⟩88    intros m hm89    have inhabited : ∃ a, a ∈ S by refine ⟨m, hm⟩90    exfalso91    exact empty with inhabited9293-- At height n, finitely many slices inherit finite bases from C.94theorem DicksonOn.bounded_slices (V C j : Set, n : Nat)95  requires index : j ∈ V96  requires previous : DicksonOn(V, C)97  shows ∀ S, S ⊆ monomials(V) → ∃ B, Finite(B) ∧ B ⊆ S ∧ BoundedMonomialCover(C, S, j, n, B)98proof99  induction n100  | zero =>101    intros S subset102    refine ⟨∅, Finite.empty, empty.subset at S, _⟩103    intros m hm below104    have member := subset with m, hm105    have mNat := monomials.exponent at V, m, j with *106    have impossible : m(j) < m(j) by arith107    exfalso108    exact Less.irreflexive with mNat, impossible109  | succ(k) using ih =>110    intros S subset111    obtain ⟨B, finiteB, subsetB, coveredB⟩ := ih with S, subset112    have sliceSubset := exponentSlice.subset at S, j, k113    have sliceBound := Subset.transitive with sliceSubset, subset114    have finiteBases := previous115    obtain ⟨D, basisD⟩ := finiteBases with exponentSlice(S, j, k), sliceBound116    rcases basisD with ⟨finiteD, subsetD, coveredD⟩117    have finite := Finite.union with finiteB, finiteD118    have subsetDS := Subset.transitive with subsetD, sliceSubset119    have included : B ∪ D ⊆ S by simp [Subset, union2.membership]120    refine ⟨B ∪ D, finite, included, _⟩121    intros m hm below122    have source := subset123    have member := source with m, hm124    have mNat := monomials.exponent at V, m, j with *125    have alternatives : m(j) < k ∨ ¬(m(j) < k) by tauto126    cases alternatives with earlier | last127      obtain ⟨b, hb, divides⟩ := coveredB with m, hm, earlier128      have inUnion : b ∈ B ∪ D129        apply union2.membership.backward130        left131        exact hb132      refine ⟨b, inUnion, divides⟩133    . have lower := LessEqual.of_not_Less at m(j), k with *134      have upper := Less.successor_upper at m(j), k with *135      have atLast := LessEqual.antisymmetric at m(j), k with *136      have inSlice : m ∈ exponentSlice(S, j, k) := exponentSlice.membership.backward with ⟨hm, atLast⟩137      obtain ⟨d, hd, sliceDivides⟩ := coveredD with m, inSlice138      have includedD := subsetD139      have bInSlice := includedD with d, hd140      have data := exponentSlice.membership.forward with bInSlice141      have coordinate : d(j) ≤ m(j)142        rw [data.right, atLast]143        exact LessEqual.reflexive at k with *144      have extended := MonomialDivides.insert with sliceDivides, coordinate145      have dInUnion : d ∈ B ∪ D146        apply union2.membership.backward147        right148        exact hd149      refine ⟨d, dInUnion, extended⟩150151theorem DicksonOn.insert (V C j : Set)152  requires index : j ∈ V153  requires previous : DicksonOn(V, C)154  shows DicksonOn(V, insert(j, C))155proof156  intros S subset157  have finiteBases := previous158  obtain ⟨B, basisB⟩ := finiteBases with S, subset159  rcases basisB with ⟨finiteB, subsetB, coveredB⟩160  have boundedB := Subset.transitive with subsetB, subset161  obtain ⟨n, natural, bound⟩ := Finite.exponents_bounded at V, B, j with *162  have slices := DicksonOn.bounded_slices at V, C, j, n with *163  obtain ⟨D, finiteD, subsetD, coveredD⟩ := slices with S, subset164  have finite := Finite.union with finiteB, finiteD165  have included : B ∪ D ⊆ S by simp [Subset, union2.membership]166  witness B ∪ D167  unfold FiniteMonomialBasis168  refine ⟨finite, included, _⟩169  intros m hm170  have source := subset171  have member := source with m, hm172  have mNat := monomials.exponent at V, m, j with *173  have alternatives : n ≤ m(j) ∨ ¬(n ≤ m(j)) by tauto174  cases alternatives with above | below175    obtain ⟨b, hb, divides⟩ := coveredB with m, hm176    have bBound := bound with b, hb177    have bSource := subsetB178    have inS := bSource with b, hb179    have bMember := source with b, inS180    have bNat := monomials.exponent at V, b, j with *181    have coordinate := LessEqual.transitive at b(j), n, m(j) with *182    have extended := MonomialDivides.insert with divides, coordinate183    have inUnion : b ∈ B ∪ D184      apply union2.membership.backward185      left186      exact hb187    refine ⟨b, inUnion, extended⟩188  . have earlier := Less.of_not_LessEqual at n, m(j) with *189    obtain ⟨d, hd, sliceDivides⟩ := coveredD with m, hm, earlier190    have dInUnion : d ∈ B ∪ D191      apply union2.membership.backward192      right193      exact hd194    refine ⟨d, dInUnion, sliceDivides⟩195196theorem Dickson.list (V : Set) (xs : List(V))197  shows DicksonOn(V, listSupport{V}(xs))198proof199  induction xs200  | List.nil =>201    rw listSupport202    exact DicksonOn.empty203  | List.cons(x, tail) using ih =>204    rw listSupport205    exact DicksonOn.insert with ih206207theorem Dickson.finite_coordinates (V : Set)208  requires finite : Finite(V)209  shows DicksonOn(V, V)210proof211  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite212  have subset := listSupport.subset with list213  have equal := Subset.antisymmetric with subset, covers214  have noetherian := Dickson.list with list215  rwa equal at noetherian216217theorem Dickson.finite_basis (V S : Set)218  requires finite : Finite(V)219  requires subset : S ⊆ monomials(V)220  shows ∃ B, FiniteMonomialBasis(V, S, B)221proof222  have noetherian := Dickson.finite_coordinates with finite223  exact noetherian with S, subset224225theorem Dickson.finite_factor_basis (V S : Set)226  requires variables : Finite(V)227  requires subset : S ⊆ monomials(V)228  shows ∃ B, Finite(B) ∧ B ⊆ S ∧ (∀ m ∈ S, ∃ b ∈ B, ∃ q ∈ monomials(V), monomialProduct(V, b, q) = m)229proof230  obtain ⟨B, basis⟩ := Dickson.finite_basis with variables, subset231  rcases basis with ⟨finite, included, covered⟩232  refine ⟨B, finite, included, _⟩233  intros m hm234  obtain ⟨b, hb, divides⟩ := covered with m, hm235  have inS := included with b, hb236  have memberB := subset with b, inS237  have memberM := subset with m, hm238  obtain ⟨q, hq, equation⟩ := MonomialDivides.iff_factor.forward at V, b, m with *239  refine ⟨b, hb, q, hq, equation⟩240