:: Hilbert Basis Theorem
::  by Jonathan Backer and Piotr Rudnicki
::
:: Received November 27, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, ORDINAL4,
      NAT_1, XXREAL_0, ARYTM_3, PRE_POLY, CARD_1, FUNCOP_1, PARTFUN1, SUBSET_1,
      ARYTM_1, FUNCT_4, ORDINAL1, PBOOLE, FINSET_1, ORDERS_1, VECTSP_1,
      ZFMISC_1, ALGSTR_0, POLYNOM2, GROUP_1, POLYNOM1, SUPINF_2, RLVECT_1,
      ALGSEQ_1, LATTICES, POLYNOM3, STRUCT_0, CARD_3, CARD_FIL, QUOFIELD,
      MSSUBFAM, IDEAL_1, PRELAMB, BINOP_1, FUNCT_2, HILBASIS, RECDEF_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, PBOOLE, RELAT_1, FINSET_1,
      FUNCT_1, PARTFUN1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
      RELSET_1, FUNCT_2, FUNCOP_1, FINSEQ_1, FUNCT_4, BINOP_1, XXREAL_2,
      MCART_1, FINSEQOP, FINSEQ_2, FUNCT_7, PRE_POLY, DOMAIN_1, STRUCT_0,
      ALGSTR_0, RLVECT_1, VFUNCT_1, GROUP_1, VECTSP_1, NORMSP_1, POLYNOM1,
      POLYNOM2, POLYNOM3, ALGSEQ_1, NAT_D, IDEAL_1, TOPS_2, GRCAT_1, WSIERP_1,
      ORDERS_1, GROUP_6, QUOFIELD, RECDEF_1, MATRLIN;
 constructors FINSEQOP, NAT_D, REAL_1, WSIERP_1, TOPS_2, ALGSEQ_1, GRCAT_1,
      GROUP_6, MATRIX_1, TRIANG_1, QUOFIELD, POLYNOM2, POLYNOM3, IDEAL_1,
      RECDEF_1, XXREAL_2, DOMAIN_1, BINARITH, RELSET_1, FUNCT_7, MATRLIN,
      VFUNCT_1, FUNCT_4, MOD_4, RINGCAT1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1,
      XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, CARD_5,
      PRE_CIRC, STRUCT_0, VECTSP_1, ALGSTR_1, WAYBEL_2, GCD_1, PRE_POLY,
      POLYNOM1, POLYNOM2, POLYNOM3, IDEAL_1, VALUED_0, ALGSTR_0, XXREAL_2,
      VFUNCT_1, FUNCT_2, RELSET_1, MOD_4, RINGCAT1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

theorem :: HILBASIS:1
  for A,B being FinSequence, f being Function st rng A \/ rng B c=
  dom f ex fA, fB being FinSequence st fA = f*A & fB = f*B & f*(A^B) = fA^fB;

theorem :: HILBASIS:2
  for b being bag of {} holds decomp b = <* <* {}, {} *> *>;

theorem :: HILBASIS:3
  for i,j being Nat, b being bag of j st i <= j holds (b
  |i) is Element of Bags i;

theorem :: HILBASIS:4
  for i, j being set, b1, b2 being bag of j, b19,b29 being bag of i
  st b19 = (b1|i) & b29 = (b2|i) & b1 divides b2 holds b19 divides b29;

theorem :: HILBASIS:5
  for i,j be set, b1, b2 being bag of j, b19, b29 being bag of i st
  b19=(b1|i) & b29=(b2|i) holds (b1-' b2)|i = b19-' b29 & (b1+b2)|i = b19+b29;

definition
  let n,k be Nat, b be bag of n;
  func b bag_extend k -> Element of Bags (n+1) means
:: HILBASIS:def 1

  it|n = b & it.n = k;
end;

theorem :: HILBASIS:6
  for n being Nat holds EmptyBag (n+1) = (EmptyBag n) bag_extend 0;

theorem :: HILBASIS:7
  for n be Ordinal, b, b1 be bag of n holds b1 in rng divisors b
  iff b1 divides b;

definition
  let X be set, x be Element of X;
  func UnitBag x -> Element of Bags X equals
:: HILBASIS:def 2
  (EmptyBag X)+*(x, 1);
end;

theorem :: HILBASIS:8
  for X being non empty set, x being Element of X holds support UnitBag x = {x}
;

theorem :: HILBASIS:9
  for X being non empty set, x being Element of X holds (UnitBag x)
  .x = 1 & for y being Element of X st x <> y holds (UnitBag x).y = 0;

theorem :: HILBASIS:10
  for X being non empty set, x1, x2 being Element of X st UnitBag
  x1 = UnitBag x2 holds x1 = x2;

theorem :: HILBASIS:11
  for X being non empty Ordinal, x be Element of X, L being
  well-unital non trivial doubleLoopStr, e being Function of X, L
  holds eval(UnitBag x, e) = e.x;

definition
  let X be set, x be Element of X, L be unital non empty multLoopStr_0;
  func 1_1(x,L) -> Series of X, L equals
:: HILBASIS:def 3
  0_(X,L)+*(UnitBag x,1_L);
end;

theorem :: HILBASIS:12
  for X being set, L being unital non trivial
doubleLoopStr, x be Element of X holds 1_1(x,L).UnitBag x = 1_L & for b being
  bag of X st b <> UnitBag x holds 1_1(x,L).b = 0.L;

theorem :: HILBASIS:13
  for X being set, x being Element of X, L being add-associative
right_zeroed right_complementable well-unital right-distributive
  non trivial doubleLoopStr holds Support 1_1(x,L) = {UnitBag x};

registration
  let X be Ordinal, x be Element of X, L be add-associative right_zeroed
  right_complementable well-unital right-distributive non trivial
  doubleLoopStr;
  cluster 1_1(x,L) -> finite-Support;
end;

theorem :: HILBASIS:14
  for L being add-associative right_zeroed right_complementable
  well-unital right-distributive non trivial doubleLoopStr, X being
non empty set, x1, x2 being Element of X st 1_1(x1,L) = 1_1(x2,L) holds x1 = x2
;

theorem :: HILBASIS:15
  for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, x being Element of Polynom-Ring L, p be
  sequence of L st x = p holds -x = -p;

theorem :: HILBASIS:16
  for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, x, y being Element of Polynom-Ring L, p
  , q be sequence of L st x = p & y = q holds x-y = p-q;

definition
  let L be right_zeroed add-associative right_complementable well-unital
  distributive non empty doubleLoopStr;
  let I be non empty Subset of Polynom-Ring L;
  func minlen(I) -> non empty Subset of I equals
:: HILBASIS:def 4
  { x where x is Element of I :
  for x9,y9 being Polynomial of L st x9=x & y9 in I holds len x9 <= len y9 };
end;

theorem :: HILBASIS:17
  for L be right_zeroed add-associative right_complementable
  well-unital distributive non empty doubleLoopStr, I be non empty Subset of
Polynom-Ring L, i1, i2 be Polynomial of L st i1 in minlen(I) & i2 in I holds i1
  in I & len i1 <= len i2;

definition
  let L be right_zeroed add-associative right_complementable well-unital
  distributive non empty doubleLoopStr, n be Nat, a be Element of L;
  func monomial(a,n) -> Polynomial of L means
:: HILBASIS:def 5

  for x being Nat holds (x = n implies it.x = a) & (x <> n implies it.x = 0.L);
end;

theorem :: HILBASIS:18
  for L be right_zeroed add-associative right_complementable
  well-unital distributive non empty doubleLoopStr, n be Element of NAT, a be
  Element of L holds (a <> 0.L implies len monomial(a,n) = n+1) & (a = 0.L
  implies len monomial(a,n) = 0) & len monomial (a,n) <= n+1;

theorem :: HILBASIS:19
  for L be right_zeroed add-associative right_complementable
  well-unital distributive non empty doubleLoopStr, n, x be Element of NAT, a
be Element of L, p be Polynomial of L holds (monomial(a,n)*'p).(x+n) = a * (p.x
  );

theorem :: HILBASIS:20
  for L be right_zeroed add-associative right_complementable
  well-unital distributive non empty doubleLoopStr, n, x be Element of NAT, a
be Element of L, p be Polynomial of L holds (p*'monomial(a,n)).(x+n) = (p.x) *
  a;

theorem :: HILBASIS:21
  for L be right_zeroed add-associative right_complementable
  well-unital distributive non empty doubleLoopStr, p, q be Polynomial of L
  holds len (p*'q) <= (len p)+(len q)-'1;

begin :: On Ring isomorphism

theorem :: HILBASIS:22
  for R,S being non empty doubleLoopStr, I being Ideal of R, P
  being Function of R,S st P is RingIsomorphism holds P.:I is Ideal of S;

theorem :: HILBASIS:23
  for R,S being add-associative right_zeroed right_complementable
  non empty doubleLoopStr, f being Function of R, S st f is RingHomomorphism
  holds f.(0.R) = 0.S;

theorem :: HILBASIS:24
  for R, S being add-associative right_zeroed right_complementable
  non empty doubleLoopStr, F being non empty Subset of R, G being non empty
  Subset of S, P being Function of R, S, lc being LinearCombination of F, LC
  being LinearCombination of G, E being FinSequence of [:the carrier of R, the
carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E
represents lc & (for i being set st i in dom LC
   holds LC.i = (P.((E/.i)`1_3))*(P.((E /.i)`2_3))*(P.((E/.i)`3_3)))
   holds P.(Sum lc) = Sum LC;

theorem :: HILBASIS:25
  for R, S be non empty doubleLoopStr, P be Function of R, S st P
  is RingIsomorphism holds P" is RingIsomorphism;

theorem :: HILBASIS:26
  for R,S being Abelian add-associative right_zeroed
  right_complementable associative distributive well-unital non empty
doubleLoopStr, F being non empty Subset of R, P being Function of R,S st P is
  RingIsomorphism holds P.:(F-Ideal) = (P.:F)-Ideal;

theorem :: HILBASIS:27
  for R,S being Abelian add-associative right_zeroed
  right_complementable associative distributive well-unital non empty
  doubleLoopStr, P being Function of R,S st P is RingIsomorphism & R is
  Noetherian holds S is Noetherian;

theorem :: HILBASIS:28
  for R being add-associative right_zeroed right_complementable
  associative Abelian distributive well-unital non trivial
  doubleLoopStr holds ex P being Function of R, Polynom-Ring (0,R) st P is
  RingIsomorphism;

theorem :: HILBASIS:29
  for R being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n being Nat,
   b being bag of n, p1 being Polynomial of n, R, F being FinSequence of
  the carrier of Polynom-Ring (n,R) st p1 = Sum F ex g being Function of the
carrier of Polynom-Ring (n, R), the carrier of R st (for p being Polynomial of
  n, R holds g.p = p.b) & p1.b = Sum (g*F);

definition
  let R be Abelian add-associative right_zeroed right_complementable
  associative distributive well-unital commutative non trivial
  doubleLoopStr, n be Nat;
  func upm (n,R) -> Function of Polynom-Ring (Polynom-Ring(n,R)), Polynom-Ring
  (n+1,R) means
:: HILBASIS:def 6

  for p1 being (Polynomial of Polynom-Ring (n,R)), p2 being
(Polynomial of n, R), p3 being (Polynomial of (n+1), R), b being bag of n+1 st
  p3 = it.p1 & p2 = p1.(b.n) holds p3.b = p2.(b|n);
end;

registration
  let R be Abelian add-associative right_zeroed right_complementable
  associative distributive well-unital commutative non trivial
  doubleLoopStr, n be Nat;
  cluster upm (n,R) -> additive;
  cluster upm (n,R) -> multiplicative;
  cluster upm (n,R) -> unity-preserving;
  cluster upm (n,R) -> one-to-one;
end;

definition
  let R be Abelian add-associative right_zeroed right_complementable
  associative distributive well-unital commutative non trivial
  doubleLoopStr, n be Nat;
  func mpu (n,R) -> Function of Polynom-Ring (n+1,R), Polynom-Ring
  Polynom-Ring(n,R) means
:: HILBASIS:def 7

  for p1 being (Polynomial of n+1,R), p2 being (
  Polynomial of n, R), p3 being (Polynomial of Polynom-Ring (n, R)), i being
  Element of NAT, b being bag of n st p3 = it.p1 & p2 = p3.i holds p2.b = p1.(b
  bag_extend i);
end;

theorem :: HILBASIS:30
  for R being Abelian add-associative right_zeroed
  right_complementable associative distributive well-unital commutative non
  trivial non empty doubleLoopStr, n being Nat, p being Element of
  Polynom-Ring (n+1,R) holds upm(n,R).(mpu(n,R).p) = p;

theorem :: HILBASIS:31
  for R being Abelian add-associative right_zeroed
  right_complementable associative distributive well-unital commutative non
  trivial non empty doubleLoopStr, n being Nat ex P being Function
of Polynom-Ring (Polynom-Ring(n,R)),Polynom-Ring(n+1,R) st P is RingIsomorphism
;

begin :: Hilbert basis theorem

registration
  let R be Noetherian Abelian add-associative right_zeroed
  right_complementable associative distributive well-unital commutative non
  empty doubleLoopStr;
::$N Hilbert Basis Theorem
  cluster Polynom-Ring R -> Noetherian;
end;

theorem :: HILBASIS:32
  for R being Abelian add-associative right_zeroed
  right_complementable associative distributive well-unital
commutative non trivial doubleLoopStr st R is Noetherian
  for n being Nat holds Polynom-Ring (n,R) is Noetherian;

theorem :: HILBASIS:33
  for F being Field holds F is Noetherian;

theorem :: HILBASIS:34
  for F being Field, n being Element of NAT holds Polynom-Ring (n,F) is
  Noetherian;

theorem :: HILBASIS:35
  for R being Abelian right_zeroed add-associative right_complementable
  well-unital distributive associative commutative non trivial
  doubleLoopStr, X be infinite Ordinal holds Polynom-Ring (X,R) is non
  Noetherian;