let n be Element of NAT ; :: thesis: 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) 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 )
let T be connected admissible TermOrder of n; :: thesis: 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) 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 )
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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 )
let I be non empty add-closed left-ideal Subset of (Polynom-Ring n,L); :: thesis: ( I <> {(0_ n,L)} implies ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G ) )
assume A1: I <> {(0_ n,L)} ; :: thesis: ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G )
consider G being finite Subset of (Polynom-Ring n,L) such that
A2: G is_Groebner_basis_of I,T by Th35;
A3: ( G -Ideal = I & PolyRedRel G,T is locally-confluent ) by A2, Def4;
set R = PolyRedRel G,T;
X: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;
per cases ( not 0_ n,L in G or 0_ n,L in G ) ;
suppose not 0_ n,L in G ; :: thesis: ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G )
hence ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G ) by A2; :: thesis: verum
end;
suppose A4: 0_ n,L in G ; :: thesis: ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G )
set G' = G \ {(0_ n,L)};
set R' = PolyRedRel (G \ {(0_ n,L)}),T;
A5: PolyRedRel (G \ {(0_ n,L)}),T c= PolyRedRel G,T by Th4, XBOOLE_1:36;
reconsider G' = G \ {(0_ n,L)} as finite Subset of (Polynom-Ring n,L) ;
A6: for u being set st u in PolyRedRel G,T holds
u in PolyRedRel (G \ {(0_ n,L)}),T
proof
let u be set ; :: thesis: ( u in PolyRedRel G,T implies u in PolyRedRel (G \ {(0_ n,L)}),T )
assume A7: u in PolyRedRel G,T ; :: thesis: u in PolyRedRel (G \ {(0_ n,L)}),T
then consider p, q being set such that
A8: ( p in NonZero (Polynom-Ring n,L) & q in the carrier of (Polynom-Ring n,L) & u = [p,q] ) by ZFMISC_1:def 2;
reconsider q = q as Polynomial of n,L by A8, POLYNOM1:def 27;
not p in {(0_ n,L)} by A8, X, XBOOLE_0:def 5;
then p <> 0_ n,L by TARSKI:def 1;
then reconsider p = p as non-zero Polynomial of n,L by A8, POLYNOM1:def 27, POLYNOM7:def 2;
p reduces_to q,G,T by A7, A8, POLYRED:def 13;
then consider f being Polynomial of n,L such that
A9: ( f in G & p reduces_to q,f,T ) by POLYRED:def 7;
consider b being bag of such that
A10: p reduces_to q,f,b,T by A9, POLYRED:def 6;
f <> 0_ n,L by A10, POLYRED:def 5;
then not f in {(0_ n,L)} by TARSKI:def 1;
then f in G' by A9, XBOOLE_0:def 5;
then p reduces_to q,G',T by A9, POLYRED:def 7;
hence u in PolyRedRel (G \ {(0_ n,L)}),T by A8, POLYRED:def 13; :: thesis: verum
end;
for u being set st u in PolyRedRel (G \ {(0_ n,L)}),T holds
u in PolyRedRel G,T by A5;
then A11: PolyRedRel (G \ {(0_ n,L)}),T is locally-confluent by A3, A6, TARSKI:2;
now
per cases ( G' = {} or G' <> {} ) ;
case A12: G' = {} ; :: thesis: G' -Ideal = I
now
per cases ( G = {} or G <> {} ) ;
case A13: G <> {} ; :: thesis: G' -Ideal = I
A14: now
let u be set ; :: thesis: ( u in G implies u in {(0_ n,L)} )
assume A15: u in G ; :: thesis: u in {(0_ n,L)}
G c= {(0_ n,L)} by A12, XBOOLE_1:37;
hence u in {(0_ n,L)} by A15; :: thesis: verum
end;
now
let u be set ; :: thesis: ( u in {(0_ n,L)} implies u in G )
assume u in {(0_ n,L)} ; :: thesis: u in G
then A16: u = 0_ n,L by TARSKI:def 1;
A17: G c= {(0_ n,L)} by A12, XBOOLE_1:37;
hence u in G by A13; :: thesis: verum
end;
then A18: G = {(0_ n,L)} by A14, TARSKI:2;
0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;
then G is Ideal of (Polynom-Ring n,L) by A18;
hence G' -Ideal = I by A1, A3, A18, IDEAL_1:44; :: thesis: verum
end;
end;
end;
hence G' -Ideal = I ; :: thesis: verum
end;
case G' <> {} ; :: thesis: G' -Ideal = I
then reconsider GG = G, GG' = G' as non empty Subset of (Polynom-Ring n,L) ;
A19: 0. (Polynom-Ring n,L) = 0_ n,L by POLYNOM1:def 27;
A20: now
let u be set ; :: thesis: ( u in G -Ideal implies u in G' -Ideal )
assume u in G -Ideal ; :: thesis: u in G' -Ideal
then consider f being LinearCombination of GG such that
A21: u = Sum f by IDEAL_1:60;
consider g being LinearCombination of GG' such that
A22: u = Sum g by A4, A19, A21, Lm9;
thus u in G' -Ideal by A22, IDEAL_1:60; :: thesis: verum
end;
now
let u be set ; :: thesis: ( u in G' -Ideal implies u in G -Ideal )
assume A23: u in G' -Ideal ; :: thesis: u in G -Ideal
GG' -Ideal c= GG -Ideal by IDEAL_1:57, XBOOLE_1:36;
hence u in G -Ideal by A23; :: thesis: verum
end;
hence G' -Ideal = I by A3, A20, TARSKI:2; :: thesis: verum
end;
end;
end;
then A24: G' is_Groebner_basis_of I,T by A11, Def4;
now
assume 0_ n,L in G' ; :: thesis: contradiction
then not 0_ n,L in {(0_ n,L)} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
hence ex G being finite Subset of (Polynom-Ring n,L) st
( G is_Groebner_basis_of I,T & not 0_ n,L in G ) by A24; :: thesis: verum
end;
end;