:: Construction of {G}r\"obner bases. S-Polynomials and StandardRepresentations
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem :: GROEB_2:1
canceled;
theorem :: GROEB_2:2
canceled;
theorem :: GROEB_2:3
theorem :: GROEB_2:4
:: deftheorem Def1 defines / GROEB_2:def 1 :
for
X being
set for
b1,
b2 being
bag of
X st
b2 divides b1 holds
for
b4 being
bag of
X holds
(
b4 = b1 / b2 iff
b2 + b4 = b1 );
definition
let X be
set ;
let b1,
b2 be
bag of
X;
func lcm b1,
b2 -> bag of
X means :
Def2:
:: GROEB_2:def 2
for
k being
set holds
it . k = max (b1 . k),
(b2 . k);
existence
ex b1 being bag of X st
for k being set holds b1 . k = max (b1 . k),(b2 . k)
uniqueness
for b1, b2 being bag of X st ( for k being set holds b1 . k = max (b1 . k),(b2 . k) ) & ( for k being set holds b2 . k = max (b1 . k),(b2 . k) ) holds
b1 = b2
commutativity
for b1, b1, b2 being bag of X st ( for k being set holds b1 . k = max (b1 . k),(b2 . k) ) holds
for k being set holds b1 . k = max (b2 . k),(b1 . k)
;
idempotence
for b1 being bag of X
for k being set holds b1 . k = max (b1 . k),(b1 . k)
;
end;
:: deftheorem Def2 defines lcm GROEB_2:def 2 :
for
X being
set for
b1,
b2,
b4 being
bag of
X holds
(
b4 = lcm b1,
b2 iff for
k being
set holds
b4 . k = max (b1 . k),
(b2 . k) );
:: deftheorem Def3 defines are_disjoint GROEB_2:def 3 :
theorem :: GROEB_2:5
canceled;
theorem :: GROEB_2:6
canceled;
theorem Th7: :: GROEB_2:7
theorem Th8: :: GROEB_2:8
theorem :: GROEB_2:9
theorem Th10: :: GROEB_2:10
theorem Th11: :: GROEB_2:11
theorem :: GROEB_2:12
theorem :: GROEB_2:13
theorem :: GROEB_2:14
theorem :: GROEB_2:15
theorem Th16: :: GROEB_2:16
theorem Th17: :: GROEB_2:17
theorem Th18: :: GROEB_2:18
theorem Th19: :: GROEB_2:19
theorem Th20: :: GROEB_2:20
Lm1:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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
theorem Th21: :: GROEB_2: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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
P being
Subset of
(Polynom-Ring n,L) st not
0_ n,
L in P & ( for
p1,
p2 being
Polynomial of
n,
L st
p1 <> p2 &
p1 in P &
p2 in P holds
for
m1,
m2 being
Monomial of
n,
L st
HM (m1 *' p1),
T = HM (m2 *' p2),
T holds
PolyRedRel P,
T reduces (m1 *' p1) - (m2 *' p2),
0_ n,
L ) holds
P is_Groebner_basis_wrt T
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p1,
p2 be
Polynomial of
n,
L;
func S-Poly p1,
p2,
T -> Polynomial of
n,
L equals :: GROEB_2:def 4
((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) - ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2));
coherence
((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) - ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)) is Polynomial of n,L
;
end;
:: deftheorem defines S-Poly GROEB_2:def 4 :
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for
p1,
p2 being
Polynomial of
n,
L holds
S-Poly p1,
p2,
T = ((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) - ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2));
Lm2:
for L being non empty add-cancelable right_complementable associative well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
Lm3:
for n being Ordinal
for T being connected 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
for f, g being Element of (Polynom-Ring n,L) st f = p & g = q holds
f - g = p - q
theorem Th22: :: GROEB_2:22
theorem :: GROEB_2:23
canceled;
theorem Th24: :: GROEB_2:24
theorem Th25: :: GROEB_2:25
theorem :: GROEB_2:26
for
n being
Ordinal for
T being
connected admissible TermOrder of
n for
L being non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for
p1,
p2 being
Polynomial of
n,
L holds
(
S-Poly p1,
p2,
T = 0_ n,
L or
HT (S-Poly p1,p2,T),
T < lcm (HT p1,T),
(HT p2,T),
T )
theorem :: GROEB_2:27
theorem :: GROEB_2:28
theorem :: GROEB_2: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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
G being
Subset of
(Polynom-Ring n,L) st ( for
g1,
g2,
h being
Polynomial of
n,
L st
g1 in G &
g2 in G &
h is_a_normal_form_of S-Poly g1,
g2,
T,
PolyRedRel G,
T holds
h = 0_ n,
L ) holds
for
g1,
g2 being
Polynomial of
n,
L st
g1 in G &
g2 in G holds
PolyRedRel G,
T reduces S-Poly g1,
g2,
T,
0_ n,
L
theorem Th30: :: GROEB_2:30
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be
Subset of
(Polynom-Ring n,L);
func S-Poly P,
T -> Subset of
(Polynom-Ring n,L) equals :: GROEB_2:def 5
{ (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;
coherence
{ (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } is Subset of (Polynom-Ring n,L)
end;
:: deftheorem defines S-Poly GROEB_2:def 5 :
theorem :: GROEB_2:31
theorem :: GROEB_2:32
theorem :: GROEB_2:33
theorem :: GROEB_2:34
:: deftheorem Def6 defines is_MonomialRepresentation_of GROEB_2:def 6 :
theorem :: GROEB_2:35
theorem :: GROEB_2:36
Lm4:
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 f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
for b being bag of n st ( for i being Element of NAT st i in dom A holds
for m being Monomial of n,L
for p being Polynomial of n,L st A . i = m *' p & p in P holds
(m *' p) . b = 0. L ) holds
f . b = 0. L
:: deftheorem Def7 defines is_Standard_Representation_of GROEB_2:def 7 :
:: deftheorem Def8 defines is_Standard_Representation_of GROEB_2:def 8 :
:: deftheorem defines has_a_Standard_Representation_of GROEB_2:def 9 :
:: deftheorem Def10 defines has_a_Standard_Representation_of GROEB_2:def 10 :
theorem Th37: :: GROEB_2:37
Lm5:
for n being Ordinal
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 f, g being Polynomial of n,L
for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' holds
for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
ex A being LeftLinearCombination of P st
( f' = g' + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) )
theorem :: GROEB_2:38
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
f,
g being
Polynomial of
n,
L for
P being non
empty Subset of
(Polynom-Ring n,L) for
A,
B being
LeftLinearCombination of
P for
b being
bag of
n st
A is_Standard_Representation_of f,
P,
b,
T &
B is_Standard_Representation_of g,
P,
b,
T holds
A ^ B is_Standard_Representation_of f + g,
P,
b,
T
theorem :: GROEB_2:39
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
f,
g being
Polynomial of
n,
L for
P being non
empty Subset of
(Polynom-Ring n,L) for
A,
B being
LeftLinearCombination of
P for
b being
bag of
n for
i being
Element of
NAT st
A is_Standard_Representation_of f,
P,
b,
T &
B = A | i &
g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,
P,
b,
T
theorem :: GROEB_2:40
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
empty non
trivial right_complementable well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
f,
g being
Polynomial of
n,
L for
P being non
empty Subset of
(Polynom-Ring n,L) for
A,
B being
LeftLinearCombination of
P for
b being
bag of
n for
i being
Element of
NAT st
A is_Standard_Representation_of f,
P,
b,
T &
B = A /^ i &
g = Sum (A | i) &
i <= len A holds
B is_Standard_Representation_of f - g,
P,
b,
T
theorem Th41: :: GROEB_2:41
theorem Th42: :: GROEB_2:42
theorem Th43: :: GROEB_2:43
theorem Th44: :: GROEB_2:44
theorem :: GROEB_2:45