:: Characterization and Existence of {G}r\"obner Bases
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

definition

let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p be Polynomial of n,L;
:: original: {
redefine func {p} -> Subset of (Polynom-Ring (n,L));
coherence
{p} is Subset of (Polynom-Ring (n,L))

proof end;

end;

theorem Th1: :: GROEB_1:1

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st g = f - (m *' p)

proof end;

theorem :: GROEB_1:2

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st
( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

proof end;

Lm1: for L being non empty add-cancelable right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal

proof end;

Lm2: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring (n,L)) st f = p & g = q holds
f - g = p - q

proof end;

Lm3: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L holds f is_irreducible_wrt 0_ (n,L),T

proof end;

theorem Th3: :: GROEB_1:3

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,Q,T

proof end;

theorem Th4: :: GROEB_1:4

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q holds
PolyRedRel (P,T) c= PolyRedRel (Q,T)

proof end;

theorem Th5: :: GROEB_1:5

for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds Support (- p) = Support p

proof end;

theorem Th6: :: GROEB_1:6

for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)

proof end;

theorem Th7: :: GROEB_1:7

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds HT ((p - q),T) <= max ((HT (p,T)),(HT (q,T)),T),T

proof end;

theorem Th8: :: GROEB_1:8

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T

proof end;

theorem Th9: :: GROEB_1:9

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT (p,T) <= HT (f,T),T

proof end;

theorem Th10: :: GROEB_1:10

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds PolyRedRel ({p},T) is locally-confluent

proof end;

theorem :: GROEB_1:11

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ex p being Polynomial of n,L st
( p in P & P -Ideal = {p} -Ideal ) holds
PolyRedRel (P,T) is locally-confluent

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be Subset of (Polynom-Ring (n,L));

func HT (P,T) -> Subset of (Bags n) equals :: GROEB_1:def 1
{ (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } ;

coherence
{ (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } is Subset of (Bags n)

proof end;

end;

:: deftheorem defines HT GROEB_1:def 1 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) holds HT (P,T) = { (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } ;

definition

let n be Ordinal;
let S be Subset of (Bags n);

func multiples S -> Subset of (Bags n) equals :: GROEB_1:def 2
{ b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } ;

coherence
{ b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } is Subset of (Bags n)

proof end;

end;

:: deftheorem defines multiples GROEB_1:def 2 :
for n being Ordinal
for S being Subset of (Bags n) holds multiples S = { b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } ;

theorem :: GROEB_1:12

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is locally-confluent holds
PolyRedRel (P,T) is confluent ;

theorem :: GROEB_1:13

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is confluent holds
PolyRedRel (P,T) is with_UN_property ;

theorem :: GROEB_1:14

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_UN_property holds
PolyRedRel (P,T) is with_Church-Rosser_property ;

Lm4: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for g being object
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
g is Polynomial of n,L

proof end;

Lm5: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )

proof end;

theorem Th15: :: GROEB_1:15

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)

proof end;

theorem Th16: :: GROEB_1:16

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T

proof end;

theorem Th17: :: GROEB_1:17

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T

proof end;

theorem Th18: :: GROEB_1:18

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )

proof end;

theorem :: GROEB_1:19

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b ) ) holds
HT ((P -Ideal),T) c= multiples (HT (P,T))

proof end;

theorem :: GROEB_1:20

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st HT ((P -Ideal),T) c= multiples (HT (P,T)) holds
PolyRedRel (P,T) is locally-confluent

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let G be Subset of (Polynom-Ring (n,L));

pred G is_Groebner_basis_wrt T means :: GROEB_1:def 3
PolyRedRel (G,T) is locally-confluent ;

end;

:: deftheorem defines is_Groebner_basis_wrt GROEB_1:def 3 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) holds
( G is_Groebner_basis_wrt T iff PolyRedRel (G,T) is locally-confluent );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let G, I be Subset of (Polynom-Ring (n,L));

pred G is_Groebner_basis_of I,T means :: GROEB_1:def 4
( G -Ideal = I & PolyRedRel (G,T) is locally-confluent );

end;

:: deftheorem defines is_Groebner_basis_of GROEB_1:def 4 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) holds
( G is_Groebner_basis_of I,T iff ( G -Ideal = I & PolyRedRel (G,T) is locally-confluent ) );

Lm6: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )

proof end;

theorem :: GROEB_1:21

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G, P being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of P,T holds
PolyRedRel (G,T) is Completion of PolyRedRel (P,T)

proof end;

theorem :: GROEB_1:22

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )

proof end;

theorem :: GROEB_1:23

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds
( f in P -Ideal iff PolyRedRel (P,T) reduces f, 0_ (n,L) ) by Th15, POLYRED:60;

Lm7: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being LeftIdeal of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I

proof end;

theorem Th24: :: GROEB_1:24

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) by Th15;

theorem Th25: :: GROEB_1:25

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T

proof end;

theorem Th26: :: GROEB_1:26

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T ) holds
for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T

proof end;

theorem Th27: :: GROEB_1:27

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T ) holds
for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )

proof end;

theorem Th28: :: GROEB_1:28

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) ) holds
HT (I,T) c= multiples (HT (G,T))

proof end;

theorem Th29: :: GROEB_1:29

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds
G is_Groebner_basis_of I,T

proof end;

theorem Th30: :: GROEB_1:30

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

proof end;

theorem :: GROEB_1:31

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds {p} is_Groebner_basis_of {p} -Ideal ,T

proof end;

theorem :: GROEB_1:32

for T being connected admissible TermOrder of {}
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring ({},L))
for P being non empty Subset of (Polynom-Ring ({},L)) st P c= I & P <> {(0_ ({},L))} holds
P is_Groebner_basis_of I,T

proof end;

theorem :: GROEB_1:33

for n being non empty Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds
not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T

proof end;

Lm8: for n being Ordinal
for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3

proof end;

definition

let n be Ordinal;

func DivOrder n -> Order of (Bags n) means :Def5: :: GROEB_1:def 5
for b1, b2 being bag of n holds
( [b1,b2] in it iff b1 divides b2 );

existence
ex b₁ being Order of (Bags n) st
for b1, b2 being bag of n holds
( [b1,b2] in b₁ iff b1 divides b2 )

proof end;

uniqueness
for b₁, b₂ being Order of (Bags n) st ( for b1, b2 being bag of n holds
( [b1,b2] in b₁ iff b1 divides b2 ) ) & ( for b1, b2 being bag of n holds
( [b1,b2] in b₂ iff b1 divides b2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :
for n being Ordinal
for b₂ being Order of (Bags n) holds
( b₂ = DivOrder n iff for b1, b2 being bag of n holds
( [b1,b2] in b₂ iff b1 divides b2 ) );

registration

let n be Element of NAT ;

cluster RelStr(# (Bags n),(DivOrder n) #) -> Dickson ;

coherence
RelStr(# (Bags n),(DivOrder n) #) is Dickson

proof end;

end;

theorem Th34: :: GROEB_1:34

for n being Element of NAT
for N being Subset of RelStr(# (Bags n),(DivOrder n) #) ex B being finite Subset of (Bags n) st B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #)

proof end;

theorem Th35: :: GROEB_1:35

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

proof end;

Lm9: for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for A, B being non empty Subset of L st B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g

proof end;

theorem :: GROEB_1:36

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & not 0_ (n,L) in G )

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty multLoopStr_0 ;
let p be Polynomial of n,L;

pred p is_monic_wrt T means :Def6: :: GROEB_1:def 6
HC (p,T) = 1. L;

end;

:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty multLoopStr_0
for p being Polynomial of n,L holds
( p is_monic_wrt T iff HC (p,T) = 1. L );

definition

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

pred P is_reduced_wrt T means :: GROEB_1:def 7
for p being Polynomial of n,L st p in P holds
( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T );

end;

:: deftheorem defines is_reduced_wrt GROEB_1:def 7 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) holds
( P is_reduced_wrt T iff for p being Polynomial of n,L st p in P holds
( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T ) );

notation

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let P be Subset of (Polynom-Ring (n,L));
synonym P is_autoreduced_wrt T for P is_reduced_wrt T;

end;

theorem Th37: :: GROEB_1:37

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g

proof end;

Lm10: for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st p in I & p <> 0_ (n,L) holds
ex q being Polynomial of n,L st
( q in I & HM (q,T) = Monom ((1. L),(HT (p,T))) & q <> 0_ (n,L) )

proof end;

theorem :: GROEB_1:38

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G being Subset of (Polynom-Ring (n,L))
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T

proof end;

theorem :: GROEB_1:39

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

proof end;

theorem :: GROEB_1:40

for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G1, G2 being non empty finite Subset of (Polynom-Ring (n,L)) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds
G1 = G2

proof end;