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 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
let T be 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
let L be 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
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,L)then
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:15;
then
f has_a_normal_form_wrt PolyRedRel (
P,
T)
by REWRITE1:def 14;
then consider g being
object 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 11;
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:22;
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
.=
(ff + (- gg)) + (- ff)
.=
(ff + (- ff)) + (- gg)
by RLVECT_1:def 3
.=
(0. (Polynom-Ring (n,L))) + (- gg)
by RLVECT_1:5
.=
- gg
by ALGSTR_1:def 2
;
then
- (- gg) in I
by A18, IDEAL_1:14;
then A19:
g in I
by RLVECT_1:17;
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 for a, b, c being object st [a,b] in PolyRedRel (P,T) & [a,c] in PolyRedRel (P,T) holds
b,c are_convergent_wrt PolyRedRel (P,T)let a,
b,
c be
object ;
( [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,T)consider a9,
b9 being
object 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 = b
by A26, XTUPLE_0:1;
a,
b are_convertible_wrt PolyRedRel (
P,
T)
by A23, REWRITE1:29;
then A28:
b,
a are_convertible_wrt PolyRedRel (
P,
T)
by REWRITE1:31;
consider aa,
c9 being
object 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 = c
by A30, XTUPLE_0:1;
reconsider b9 =
b9,
c9 =
c9 as
Polynomial of
n,
L by A25, A29, POLYNOM1:def 11;
reconsider bb =
b9,
cc =
c9 as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider bb =
bb,
cc =
cc as
Element of
(Polynom-Ring (n,L)) ;
a,
c are_convertible_wrt PolyRedRel (
P,
T)
by A24, REWRITE1:29;
then
bb,
cc are_congruent_mod I
by A22, A27, A31, A28, POLYRED:57, REWRITE1:30;
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; verum