:: 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))

end;
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;

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)

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 )

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

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)

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

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)

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

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

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

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

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

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));

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

end;
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) ) } ;

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

proof 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) ) } ;

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);

{ 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)

end;
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 ) } ;

{ 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;

:: 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 ) } ;

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 ;

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 ;

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 ;

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)

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

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

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 )

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))

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

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));

end;
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));

:: 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 );

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));

end;
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 );

( G -Ideal = I & PolyRedRel (G,T) is locally-confluent );

:: 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 ) );

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)

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))) )

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;

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;

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

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

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 )

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))

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

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

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

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

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

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;

ex b_{1} being Order of (Bags n) st

for b1, b2 being bag of n holds

( [b1,b2] in b_{1} iff b1 divides b2 )

for b_{1}, b_{2} being Order of (Bags n) st ( for b1, b2 being bag of n holds

( [b1,b2] in b_{1} iff b1 divides b2 ) ) & ( for b1, b2 being bag of n holds

( [b1,b2] in b_{2} iff b1 divides b2 ) ) holds

b_{1} = b_{2}

end;
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 for b1, b2 being bag of n holds

( [b1,b2] in it iff b1 divides b2 );

ex b

for b1, b2 being bag of n holds

( [b1,b2] in b

proof end;

uniqueness for b

( [b1,b2] in b

( [b1,b2] in b

b

proof end;

:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :

for n being Ordinal

for b_{2} being Order of (Bags n) holds

( b_{2} = DivOrder n iff for b1, b2 being bag of n holds

( [b1,b2] in b_{2} iff b1 divides b2 ) );

for n being Ordinal

for b

( b

( [b1,b2] in b

registration
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) #)

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

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 )

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;

end;
let T be connected TermOrder of n;

let L be non empty multLoopStr_0 ;

let p be Polynomial of n,L;

:: 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 );

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));

end;
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 );

for p being Polynomial of n,L st p in P holds

( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T );

:: 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 ) );

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;
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;

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

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

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 )

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

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;