:: GROEB_1 semantic presentation

definition

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

proof end;

end;

theorem Th1: :: GROEB_1:1

proof end;

theorem :: GROEB_1:2

proof end;

Lm1: for L being non empty unital associative add-associative right_zeroed right_complementable distributive add-cancelable 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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

proof end;

theorem Th5: :: GROEB_1:5

for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable 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 unital add-associative right_zeroed right_complementable distributive non trivial 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 empty unital add-associative right_zeroed right_complementable distributive non trivial 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for p being Polynomial of n,L holds PolyRedRel {p},T is locally-confluent

proof end;

theorem :: GROEB_1:11

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital add-associative right_zeroed right_complementable distributive non trivial 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

proof end;

end;

:: deftheorem defines HT GROEB_1:def 1 :

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 b' being bag of n st
( b' in S & b' divides b ) } ;
coherence

proof end;

end;

:: deftheorem defines multiples GROEB_1:def 2 :

theorem Th12: :: GROEB_1:12

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

proof end;

theorem Th13: :: GROEB_1:13

proof end;

theorem Th14: :: GROEB_1:14

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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

proof end;

Lm4: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for f being Polynomial of n,L
for g being set
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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 b' being bag of n st
( b' in HT P,T & b' divides b )

proof end;

theorem :: GROEB_1:19

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 b' being bag of n st
( b' in HT P,T & b' divides b ) ) holds
HT (P -Ideal ),T c= multiples (HT P,T)

proof end;

theorem :: GROEB_1:20

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let G be Subset of (Polynom-Ring n,L);
pred G is_Groebner_basis_wrt T means :Def3: :: GROEB_1:def 3
PolyRedRel G,T is locally-confluent;

end;

:: deftheorem Def3 defines is_Groebner_basis_wrt GROEB_1:def 3 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let G, I be Subset of (Polynom-Ring n,L);
pred G is_Groebner_basis_of I,T means :Def4: :: GROEB_1:def 4
( G -Ideal = I & PolyRedRel G,T is locally-confluent );

end;

:: deftheorem Def4 defines is_Groebner_basis_of GROEB_1:def 4 :

Lm6: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for a, b being set 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

proof end;

theorem :: GROEB_1:22

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 )

proof end;

Lm7: for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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

proof end;

theorem Th25: :: GROEB_1:25

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 b' being bag of n st
( b' in HT G,T & b' divides b )

proof end;

theorem Th28: :: GROEB_1:28

for n being Ordinal
for T being connected TermOrder of n
for L being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 b' being bag of n st
( b' in HT G,T & b' divides b ) ) holds
HT I,T c= multiples (HT G,T)

proof end;

theorem Th29: :: GROEB_1:29

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr holds {(0_ n,L)} is_Groebner_basis_of {(0_ n,L)},T

proof end;

theorem :: GROEB_1:31

proof end;

theorem :: GROEB_1:32

for T being connected admissible TermOrder of {}
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :

registration

let n be Nat;
cluster RelStr(# (Bags n),(DivOrder n) #) -> Dickson ;
coherence

proof end;

end;

theorem Th34: :: GROEB_1:34

for n being 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 unital associative add-associative right_zeroed right_complementable distributive left_zeroed doubleLoopStr
for A, B being non empty Subset of L st 0. L in A & 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 :

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let P be Subset of (Polynom-Ring n,L);
pred P is_reduced_wrt T means :Def7: :: 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 Def7 defines is_reduced_wrt GROEB_1:def 7 :

notation

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial 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 unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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 Nat
for T being connected admissible TermOrder of n
for L being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated 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;