:: Construction of {G}r\"obner bases. S-Polynomials and Standard
:: Representations
::  by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003-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, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, SUBSET_1,
      RELAT_1, XXREAL_0, FUNCT_1, SUPINF_2, CARD_3, ARYTM_3, TARSKI, ORDINAL4,
      PARTFUN1, CARD_1, FUNCT_7, ARYTM_1, RFINSEQ, PRE_POLY, PBOOLE, RELAT_2,
      BAGORDER, ORDERS_2, WAYBEL_4, ZFMISC_1, XCMPLX_0, ALGSTR_1, LATTICES,
      POLYNOM7, POLYNOM1, ORDINAL1, VECTSP_2, VALUED_0, VECTSP_1, BINOP_1,
      POLYRED, REWRITE1, STRUCT_0, MCART_1, TERMORD, GROEB_1, BROUWER,
      MESFUNC1, CAT_3, GROUP_1, IDEAL_1, FINSET_1, NAT_1, GROEB_2;
 notations TARSKI, RELAT_1, XBOOLE_0, SUBSET_1, RELAT_2, RELSET_1, FUNCT_1,
      ORDINAL1, XCMPLX_0, PARTFUN1, FINSET_1, XTUPLE_0, MCART_1, XXREAL_0,
      FINSEQ_1, PRE_POLY, STRUCT_0, ALGSTR_1, VECTSP_2, POLYNOM7, PBOOLE,
      ORDERS_2, REWRITE1, BAGORDER, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1,
      POLYNOM1, TERMORD, IDEAL_1, POLYRED, GROUP_1, NAT_D, NUMBERS, NAT_1,
      GROEB_1, RFINSEQ, FINSEQ_7, WAYBEL_4, RECDEF_1;
 constructors RFINSEQ, REWRITE1, FINSEQ_7, VECTSP_2, WAYBEL_4, WELLFND1,
      IDEAL_1, BAGORDER, TERMORD, POLYRED, GROEB_1, RECDEF_1, REAL_1, RELSET_1,
      PBOOLE, BINOP_2, VFUNCT_1, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, FINSEQ_1,
      REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, GCD_1, POLYNOM1,
      POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, TERMORD, POLYRED, VALUED_0,
      ALGSTR_0, PRE_POLY, CARD_1, VFUNCT_1, FUNCT_1, FUNCT_2, RELSET_1,
      XTUPLE_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

theorem :: GROEB_2:1
  for L being add-associative right_zeroed right_complementable non
  empty addLoopStr, p being FinSequence of L, n being Element of NAT st for k
being Element of NAT st k in dom p & k > n holds p.k = 0.L holds Sum p = Sum(p|
  n);

theorem :: GROEB_2:2
  for L being add-associative right_zeroed Abelian non empty addLoopStr
  , f being FinSequence of L, i,j being Element of NAT holds Sum Swap(f,i,j) =
  Sum f;

definition
  let X be set, b1,b2 be bag of X;
  assume
 b2 divides b1;
  func b1 / b2 -> bag of X means
:: GROEB_2:def 1

  b2 + it = b1;
end;

definition
  let X be set, b1,b2 be bag of X;
  func lcm(b1,b2) -> bag of X means
:: GROEB_2:def 2

  for k being object holds it.k = max(b1 .k,b2.k);
  commutativity;
  idempotence;
end;

notation
  let X be set, b1,b2 be bag of X;
  synonym b1 lcm b2 for lcm(b1,b2);
end;

:: exercise 5.45, p. 211

definition
  let X be set, b1,b2 be bag of X;
  pred b1,b2 are_disjoint means
:: GROEB_2:def 3

  for i being object holds b1.i = 0 or b2.i = 0;
end;

notation
  let X be set, b1,b2 be bag of X;
  antonym b1,b2 are_non_disjoint for b1,b2 are_disjoint;
end;

theorem :: GROEB_2:3
  for X being set, b1,b2 being bag of X holds b1 divides lcm(b1,b2)
  & b2 divides lcm(b1,b2);

:: exercise 5.45, p. 211

theorem :: GROEB_2:4
  for X being set, b1,b2,b3 be bag of X holds b1 divides b3 & b2
  divides b3 implies lcm(b1,b2) divides b3;

:: exercise 5.45, p. 211

theorem :: GROEB_2:5
  for X being set, b1,b2 being bag of X holds b1,b2 are_disjoint iff lcm
  (b1,b2) = b1 + b2;

theorem :: GROEB_2:6
  for X being set, b being bag of X holds b/b = EmptyBag X;

theorem :: GROEB_2:7
  for X being set, b1,b2 be bag of X holds b2 divides b1 iff lcm( b1,b2) = b1;

theorem :: GROEB_2:8
  for X being set, b1,b2,b3 being bag of X holds b1 divides lcm(b2,b3)
  implies lcm(b2,b1) divides lcm(b2,b3);

:: exercise 5.69 (i) ==> (ii), p. 223

theorem :: GROEB_2:9
  for X being set, b1,b2,b3 being bag of X holds lcm(b2,b1) divides lcm(
  b2,b3) implies lcm(b1,b3) divides lcm(b2,b3);

:: exercise 5.69 (ii) ==> (iii), p. 223

theorem :: GROEB_2:10
  for n being set, b1,b2,b3 being bag of n holds lcm(b1,b3) divides lcm(
  b2,b3) implies b1 divides lcm(b2,b3);

:: exercise 5.69 (iii) ==> (i), p. 223

theorem :: GROEB_2:11
  for n being Element of NAT, T being connected admissible TermOrder of
  n, P being non empty Subset of Bags n ex b being bag of n st b in P & for b9
  being bag of n st b9 in P holds b <= b9,T;

registration
  let L be add-associative right_zeroed right_complementable non trivial
  addLoopStr, a be non zero Element of L;
  cluster -a -> non zero;
end;

registration
  let X be set, L be left_zeroed right_zeroed add-cancelable distributive non
  empty doubleLoopStr, m be Monomial of X,L, a be Element of L;
  cluster a * m -> monomial-like;
end;

registration
  let n be Ordinal, L be left_zeroed right_zeroed add-cancelable distributive
domRing-like non trivial doubleLoopStr, p be non-zero Polynomial of n,L, a be
  non zero Element of L;
  cluster a * p -> non-zero;
end;

theorem :: GROEB_2:12
  for n being Ordinal, L being right_zeroed right-distributive
non empty doubleLoopStr, p,q being Series of n,L, b being bag of n holds b *'
  (p + q) = b *' p + b *' q;

theorem :: GROEB_2:13
  for n being Ordinal, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p being Series of n,L, b being bag
  of n holds b *' (-p) = -(b *' p);

theorem :: GROEB_2:14
  for n being Ordinal, L being left_zeroed right_add-cancelable
  right-distributive non empty doubleLoopStr, p being Series of n,L, b being
  bag of n, a being Element of L holds b *' (a * p) = a * (b *' p);

theorem :: GROEB_2:15
  for n being Ordinal, L being right-distributive non empty
doubleLoopStr, p,q being Series of n,L, a being Element of L holds a * (p + q)
  = a * p + a * q;

theorem :: GROEB_2:16
  for X being set, L being add-associative right_zeroed
right_complementable non empty doubleLoopStr, a being Element of L holds -(a
  |(X,L)) = (-a) |(X,L);

begin :: S-Polynomials

theorem :: GROEB_2:17
  for n being Element of NAT, T being connected admissible
  TermOrder of n, L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian almost_left_invertible
non degenerated non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L)
holds (for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P for m1
,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T) holds PolyRedRel(P,T
  ) reduces m1 *' p1 - m2 *' p2, 0_(n,L)) implies P is_Groebner_basis_wrt T;

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be
  Polynomial of n,L;
  func S-Poly(p1,p2,T) -> Polynomial of n,L equals
:: GROEB_2:def 4
  HC(p2,T) * (lcm(HT(p1,T),HT
  (p2,T))/HT(p1,T)) *' p1 - HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
end;

theorem :: GROEB_2:18
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive almost_left_invertible Abelian non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), p1,p2 being Polynomial of
  n,L st p1 in P & p2 in P holds S-Poly(p1,p2,T) in P-Ideal;

theorem :: GROEB_2:19
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, m1
  ,m2 being Monomial of n,L holds S-Poly(m1,m2,T) = 0_(n,L);

:: exercise 5.47 (i), p. 211

theorem :: GROEB_2:20
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p
being Polynomial of n,L holds S-Poly(p,0_(n,L),T) = 0_(n,L) & S-Poly(0_(n,L),p,
  T) = 0_(n,L);

theorem :: GROEB_2:21
  for n being Ordinal, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1
,p2 being Polynomial of n,L holds S-Poly(p1,p2,T) = 0_(n,L) or HT(S-Poly(p1,p2,
  T),T) < lcm(HT(p1,T),HT(p2,T)),T;

:: exercise 5.47 (ii), p. 211

theorem :: GROEB_2:22
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1
,p2 being non-zero Polynomial of n,L holds HT(p2,T) divides HT(p1,T) implies HC
  (p2,T) * p1 top_reduces_to S-Poly(p1,p2,T),p2,T;

:: exercise 5.47 (iii), p. 211

theorem :: GROEB_2:23
  for n being Element of NAT, T being connected admissible TermOrder of
  n, L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  degenerated non empty doubleLoopStr, G being Subset of Polynom-Ring(n,L)
holds G is_Groebner_basis_wrt T implies (for g1,g2,h being Polynomial of n,L st
g1 in G & g2 in G & h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T) holds
  h = 0_(n,L));

:: theorem 5.48 (i) ==> (ii), p. 211

theorem :: GROEB_2:24
  for n being Element of NAT, T being connected admissible TermOrder of
  n, L being Abelian add-associative right_complementable right_zeroed
  commutative associative well-unital distributive almost_left_invertible non
  degenerated non empty doubleLoopStr, G being Subset of Polynom-Ring(n,L)
  holds (for g1,g2,h being Polynomial of n,L st g1 in G & g2 in G & h
is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T) holds h = 0_(n,L)) implies
  (for g1,g2 being Polynomial of n,L st g1 in G & g2 in G holds PolyRedRel(G,T)
  reduces S-Poly(g1,g2,T),0_(n,L));

:: theorem 5.48 (ii) ==> (iii), p. 211

theorem :: GROEB_2:25
  for n being Element of NAT, T being admissible connected
  TermOrder of n, L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian almost_left_invertible
non degenerated non empty doubleLoopStr, G being Subset of Polynom-Ring(n,L)
  st not(0_(n,L) in G) holds (for g1,g2 being Polynomial of n,L st g1 in G & g2
  in G holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L)) implies G
  is_Groebner_basis_wrt T;

:: theorem 5.48 (iii) ==> (i), p. 211

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of
  Polynom-Ring(n,L);
  func S-Poly(P,T) -> Subset of Polynom-Ring(n,L) equals
:: GROEB_2:def 5
  { S-Poly(p1,p2,T)
  where p1,p2 is Polynomial of n,L : p1 in P & p2 in P };
end;

registration
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, P be finite
  Subset of Polynom-Ring(n,L);
  cluster S-Poly(P,T) -> finite;
end;

theorem :: GROEB_2:26
  for n being Element of NAT, T being admissible connected TermOrder of
  n, L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  degenerated non empty doubleLoopStr, G being Subset of Polynom-Ring(n,L) st
not(0_(n,L) in G) & for g being Polynomial of n,L st g in G holds g is Monomial
  of n,L holds G is_Groebner_basis_wrt T;

:: corollary 5.49, p. 212

begin :: Standard Representations

theorem :: GROEB_2:27
  for L being non empty multLoopStr, P being non empty Subset of L, A
  being LeftLinearCombination of P, i being Element of NAT holds A|i is
  LeftLinearCombination of P;

theorem :: GROEB_2:28
  for L being non empty multLoopStr, P being non empty Subset of L, A
  being LeftLinearCombination of P, i being Element of NAT holds A/^i is
  LeftLinearCombination of P;

theorem :: GROEB_2:29
  for L being non empty multLoopStr, P,Q being non empty Subset of L, A
  being LeftLinearCombination of P holds P c= Q implies A is
  LeftLinearCombination of Q;

definition
  let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, P be non empty
  Subset of Polynom-Ring(n,L), A,B be LeftLinearCombination of P;
  redefine func A^B -> LeftLinearCombination of P;
end;

definition
  let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, f be Polynomial
of n,L, P be non empty Subset of Polynom-Ring(n,L), A be LeftLinearCombination
  of P;
  pred A is_MonomialRepresentation_of f means
:: GROEB_2:def 6

  Sum A = f & for i being
Element of NAT st i in dom A ex m being Monomial of n,L, p being Polynomial of
  n,L st p in P & A/.i = m *' p;
end;

theorem :: GROEB_2:30
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
  doubleLoopStr, f being Polynomial of n,L, P being non empty Subset of
  Polynom-Ring(n,L), A being LeftLinearCombination of P st A
is_MonomialRepresentation_of f holds Support f c= union { Support(m*'p) where m
is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st i in
  dom A & A/.i = m*'p };

theorem :: GROEB_2:31
  for n being Ordinal, L being right_zeroed add-associative
  right_complementable well-unital distributive non trivial
  doubleLoopStr, f,g being Polynomial of n,L, P being non empty Subset of
  Polynom-Ring(n,L), A,B being LeftLinearCombination of P st A
  is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds (A^B)
  is_MonomialRepresentation_of f+g;

definition
  let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
  empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
  Polynom-Ring(n,L), A be LeftLinearCombination of P, b be bag of n;
  pred A is_Standard_Representation_of f,P,b,T means
:: GROEB_2:def 7

  Sum A = f & for i
being Element of NAT st i in dom A ex m being non-zero Monomial of n,L, p being
  non-zero Polynomial of n,L st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T;
end;

definition
  let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
  empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
  Polynom-Ring(n,L), A be LeftLinearCombination of P;
  pred A is_Standard_Representation_of f,P,T means
:: GROEB_2:def 8

  A is_Standard_Representation_of f,P,HT(f,T),T;
end;

definition
  let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
  empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
  Polynom-Ring(n,L), b be bag of n;
  pred f has_a_Standard_Representation_of P,b,T means
:: GROEB_2:def 9
  ex A being
  LeftLinearCombination of P st A is_Standard_Representation_of f,P,b,T;
end;

definition
  let n be Ordinal, T be connected TermOrder of n, L be right_zeroed
add-associative right_complementable well-unital distributive non trivial non
  empty doubleLoopStr, f be Polynomial of n,L, P be non empty Subset of
  Polynom-Ring(n,L);
  pred f has_a_Standard_Representation_of P,T means
:: GROEB_2:def 10

  ex A being
  LeftLinearCombination of P st A is_Standard_Representation_of f,P,T;
end;

theorem :: GROEB_2:32
  for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being Polynomial of n,L, P being non empty
Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P, b being bag of
  n holds A is_Standard_Representation_of f,P,b,T implies A
  is_MonomialRepresentation_of f;

theorem :: GROEB_2:33
  for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
  trivial non empty doubleLoopStr, f,g being Polynomial of n,L, P being non
  empty Subset of Polynom-Ring(n,L), A,B being LeftLinearCombination of P, b
  being bag of n st A is_Standard_Representation_of f,P,b,T & B
is_Standard_Representation_of g,P,b,T holds A^B is_Standard_Representation_of f
  +g,P,b,T;

theorem :: GROEB_2:34
  for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
  trivial non empty doubleLoopStr, f,g being Polynomial of n,L, P being non
  empty Subset of Polynom-Ring(n,L), A,B being LeftLinearCombination of P, b
being bag of n, i being Element of NAT st A is_Standard_Representation_of f,P,b
  ,T & B = A|i & g = Sum(A/^i) holds B is_Standard_Representation_of f-g,P,b,T;

theorem :: GROEB_2:35
  for n being Ordinal, T being connected TermOrder of n, L being Abelian
right_zeroed add-associative right_complementable well-unital distributive non
  trivial non empty doubleLoopStr, f,g being Polynomial of n,L, P being non
  empty Subset of Polynom-Ring(n,L), A,B being LeftLinearCombination of P, b
being bag of n, i being Element of NAT st A is_Standard_Representation_of f,P,b
,T & B = A/^i & g = Sum(A|i) & i <= len A holds B is_Standard_Representation_of
  f-g,P,b,T;

theorem :: GROEB_2:36
  for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being non-zero Polynomial of n,L, P being
non empty Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P st A
  is_MonomialRepresentation_of f ex i being Element of NAT, m being non-zero
Monomial of n,L, p being non-zero Polynomial of n,L st i in dom A & p in P & A.
  i = m *' p & HT(f,T) <= HT(m*'p,T),T;

theorem :: GROEB_2:37
  for n being Ordinal, T being connected TermOrder of n, L being
right_zeroed add-associative right_complementable well-unital distributive non
trivial non empty doubleLoopStr, f being non-zero Polynomial of n,L, P being
non empty Subset of Polynom-Ring(n,L), A being LeftLinearCombination of P st A
is_Standard_Representation_of f,P,T ex i being Element of NAT, m being non-zero
Monomial of n,L, p being non-zero Polynomial of n,L st p in P & i in dom A & A
  /.i = m *' p & HT(f,T) = HT(m*'p,T);

theorem :: GROEB_2:38
  for n being Ordinal, T being admissible connected TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  degenerated non empty doubleLoopStr, f being Polynomial of n,L, P being non
  empty Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,0_(n,L)
  implies f has_a_Standard_Representation_of P,T;

:: lemma 5.60, p. 218

theorem :: GROEB_2:39
  for n being Ordinal, T being admissible connected TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, f being non-zero Polynomial of n,L, P being non empty Subset of
  Polynom-Ring(n,L) holds f has_a_Standard_Representation_of P,T implies f
  is_top_reducible_wrt P,T;

:: lemma 5.61, p. 218

theorem :: GROEB_2:40
  for n being Element of NAT, T being connected admissible TermOrder of
  n, L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
degenerated non empty doubleLoopStr, G being non empty Subset of Polynom-Ring
(n,L) holds G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,
  L st f in G-Ideal holds f has_a_Standard_Representation_of G,T;
 
:: theorem 5.62, p. 219