let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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
let I be 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
let P be non empty Subset of (Polynom-Ring n,L); ( P c= I & HT I,T c= multiples (HT P,T) implies P is_Groebner_basis_of I,T )
assume A1:
P c= I
; ( not HT I,T c= multiples (HT P,T) or P is_Groebner_basis_of I,T )
set R = PolyRedRel P,T;
assume A2:
HT I,T c= multiples (HT P,T)
; P is_Groebner_basis_of I,T
A3:
for f being Polynomial of n,L st f in I & f <> 0_ n,L holds
f is_reducible_wrt P,T
proof
let f be
Polynomial of
n,
L;
( f in I & f <> 0_ n,L implies f is_reducible_wrt P,T )
assume that A4:
f in I
and A5:
f <> 0_ n,
L
;
f is_reducible_wrt P,T
HT f,
T in { (HT p,T) where p is Polynomial of n,L : ( p in I & p <> 0_ n,L ) }
by A4, A5;
then
HT f,
T in multiples (HT P,T)
by A2;
then
ex
b being
Element of
Bags n st
(
b = HT f,
T & ex
b9 being
bag of
n st
(
b9 in HT P,
T &
b9 divides b ) )
;
then consider b9 being
bag of
n such that A6:
b9 in HT P,
T
and A7:
b9 divides HT f,
T
;
consider p being
Polynomial of
n,
L such that A8:
b9 = HT p,
T
and A9:
p in P
and A10:
p <> 0_ n,
L
by A6;
consider s being
bag of
n such that A11:
b9 + s = HT f,
T
by A7, TERMORD:1;
set g =
f - (((f . (HT f,T)) / (HC p,T)) * (s *' p));
Support f <> {}
by A5, POLYNOM7:1;
then
HT f,
T in Support f
by TERMORD:def 6;
then
f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),
p,
HT f,
T,
T
by A5, A8, A10, A11, POLYRED:def 5;
then
f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),
p,
T
by POLYRED:def 6;
then
f reduces_to f - (((f . (HT f,T)) / (HC p,T)) * (s *' p)),
P,
T
by A9, POLYRED:def 7;
hence
f is_reducible_wrt P,
T
by POLYRED:def 9;
verum
end;
A12:
PolyRedRel P,T c= PolyRedRel I,T
by A1, Th4;
A13:
for f being Polynomial of n,L st f in I holds
PolyRedRel P,T reduces f, 0_ n,L
proof
let f be
Polynomial of
n,
L;
( f in I implies PolyRedRel P,T reduces f, 0_ n,L )
assume A14:
f in I
;
PolyRedRel P,T reduces f, 0_ n,L
per cases
( f = 0_ n,L or f <> 0_ n,L )
;
suppose
f <> 0_ n,
L
;
PolyRedRel P,T reduces f, 0_ n,Lthen
f is_reducible_wrt P,
T
by A3, A14;
then consider v being
Polynomial of
n,
L such that A15:
f reduces_to v,
P,
T
by POLYRED:def 9;
[f,v] in PolyRedRel P,
T
by A15, POLYRED:def 13;
then
f in field (PolyRedRel P,T)
by RELAT_1:30;
then
f has_a_normal_form_wrt PolyRedRel P,
T
by REWRITE1:def 14;
then consider g being
set such that A16:
g is_a_normal_form_of f,
PolyRedRel P,
T
by REWRITE1:def 11;
A17:
PolyRedRel P,
T reduces f,
g
by A16, REWRITE1:def 6;
then reconsider g9 =
g as
Polynomial of
n,
L by Lm4;
reconsider ff =
f,
gg =
g9 as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider ff =
ff,
gg =
gg as
Element of
(Polynom-Ring n,L) ;
f - g9 = ff - gg
by Lm2;
then
ff - gg in I -Ideal
by A12, A17, POLYRED:59, REWRITE1:23;
then
ff - gg in I
by IDEAL_1:44;
then A18:
(ff - gg) - ff in I
by A14, IDEAL_1:16;
(ff - gg) - ff =
(ff + (- gg)) - ff
by RLVECT_1:def 14
.=
(ff + (- gg)) + (- ff)
by RLVECT_1:def 14
.=
(ff + (- ff)) + (- gg)
by RLVECT_1:def 6
.=
(0. (Polynom-Ring n,L)) + (- gg)
by RLVECT_1:16
.=
- gg
by ALGSTR_1:def 5
;
then
- (- gg) in I
by A18, IDEAL_1:14;
then A19:
g in I
by RLVECT_1:30;
assume
not
PolyRedRel P,
T reduces f,
0_ n,
L
;
contradictionthen
g <> 0_ n,
L
by A16, REWRITE1:def 6;
then
g9 is_reducible_wrt P,
T
by A3, A19;
then consider u being
Polynomial of
n,
L such that A20:
g9 reduces_to u,
P,
T
by POLYRED:def 9;
A21:
[g9,u] in PolyRedRel P,
T
by A20, POLYRED:def 13;
g is_a_normal_form_wrt PolyRedRel P,
T
by A16, REWRITE1:def 6;
hence
contradiction
by A21, REWRITE1:def 5;
verum end;
end;
then A22:
P -Ideal = I
by A1, Lm7;
now let a,
b,
c be
set ;
( [a,b] in PolyRedRel P,T & [a,c] in PolyRedRel P,T implies b,c are_convergent_wrt PolyRedRel P,T )assume that A23:
[a,b] in PolyRedRel P,
T
and A24:
[a,c] in PolyRedRel P,
T
;
b,c are_convergent_wrt PolyRedRel P,Tconsider a9,
b9 being
set such that
a9 in NonZero (Polynom-Ring n,L)
and A25:
b9 in the
carrier of
(Polynom-Ring n,L)
and A26:
[a,b] = [a9,b9]
by A23, ZFMISC_1:def 2;
A27:
b9 =
[a,b] `2
by A26, MCART_1:def 2
.=
b
by MCART_1:def 2
;
a,
b are_convertible_wrt PolyRedRel P,
T
by A23, REWRITE1:30;
then A28:
b,
a are_convertible_wrt PolyRedRel P,
T
by REWRITE1:32;
consider aa,
c9 being
set such that
aa in NonZero (Polynom-Ring n,L)
and A29:
c9 in the
carrier of
(Polynom-Ring n,L)
and A30:
[a,c] = [aa,c9]
by A24, ZFMISC_1:def 2;
A31:
c9 =
[a,c] `2
by A30, MCART_1:def 2
.=
c
by MCART_1:def 2
;
reconsider b9 =
b9,
c9 =
c9 as
Polynomial of
n,
L by A25, A29, POLYNOM1:def 27;
reconsider bb =
b9,
cc =
c9 as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider bb =
bb,
cc =
cc as
Element of
(Polynom-Ring n,L) ;
a,
c are_convertible_wrt PolyRedRel P,
T
by A24, REWRITE1:30;
then
bb,
cc are_congruent_mod I
by A22, A27, A31, A28, POLYRED:57, REWRITE1:31;
then A32:
bb - cc in I
by POLYRED:def 14;
b9 - c9 = bb - cc
by Lm2;
hence
b,
c are_convergent_wrt PolyRedRel P,
T
by A13, A27, A31, A32, POLYRED:50;
verum end;
then
PolyRedRel P,T is locally-confluent
by REWRITE1:def 24;
hence
P is_Groebner_basis_of I,T
by A22, Def4; verum