:: Construction of {G}r\"obner Bases: Avoiding S-Polynomials -- Buchberger'sFirst Criterium
:: by Christoph Schwarzweller
::
:: Received December 10, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: GROEB_3:1
for
X being
set for
b1,
b2 being
bag of
X holds
(b1 + b2) / b2 = b1
theorem Th2: :: GROEB_3:2
theorem Th3: :: GROEB_3:3
for
n being
Ordinal for
T being
TermOrder of
n for
b1,
b2,
b3 being
bag of
n st
b1 <= b2,
T &
b2 < b3,
T holds
b1 < b3,
T
theorem Th4: :: GROEB_3:4
theorem Th5: :: GROEB_3:5
theorem Th6: :: GROEB_3:6
theorem Th7: :: GROEB_3:7
theorem Th8: :: GROEB_3:8
theorem Th9: :: GROEB_3:9
theorem Th10: :: GROEB_3:10
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 Th11: :: GROEB_3:11
theorem Th12: :: GROEB_3:12
theorem Th13: :: GROEB_3:13
theorem Th14: :: GROEB_3:14
theorem Th15: :: GROEB_3:15
:: deftheorem defines | GROEB_3:def 1 :
Lm2:
for X being set
for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds Support (s | Y) c= Support s
theorem Th16: :: GROEB_3:16
theorem :: GROEB_3:17
theorem :: GROEB_3:18
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
empty right_complementable add-associative right_zeroed addLoopStr ;
let p be
Polynomial of
n,
L;
let i be
Element of
NAT ;
assume A1:
i <= card (Support p)
;
func Upper_Support p,
T,
i -> finite Subset of
(Bags n) means :
Def2:
:: GROEB_3:def 2
(
it c= Support p &
card it = i & ( for
b,
b' being
bag of
n st
b in it &
b' in Support p &
b <= b',
T holds
b' in it ) );
existence
ex b1 being finite Subset of (Bags n) st
( b1 c= Support p & card b1 = i & ( for b, b' being bag of n st b in b1 & b' in Support p & b <= b',T holds
b' in b1 ) )
uniqueness
for b1, b2 being finite Subset of (Bags n) st b1 c= Support p & card b1 = i & ( for b, b' being bag of n st b in b1 & b' in Support p & b <= b',T holds
b' in b1 ) & b2 c= Support p & card b2 = i & ( for b, b' being bag of n st b in b2 & b' in Support p & b <= b',T holds
b' in b2 ) holds
b1 = b2
end;
:: deftheorem Def2 defines Upper_Support GROEB_3:def 2 :
:: deftheorem defines Lower_Support GROEB_3:def 3 :
theorem Th19: :: GROEB_3:19
theorem Th20: :: GROEB_3:20
theorem :: GROEB_3:21
theorem Th22: :: GROEB_3:22
theorem Th23: :: GROEB_3:23
theorem Th24: :: GROEB_3:24
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
empty right_complementable add-associative right_zeroed addLoopStr for
p being
Polynomial of
n,
L for
i being
Element of
NAT st
i <= card (Support p) holds
(
Lower_Support p,
T,
i c= Support p &
card (Lower_Support p,T,i) = (card (Support p)) - i & ( for
b,
b' being
bag of
n st
b in Lower_Support p,
T,
i &
b' in Support p &
b' <= b,
T holds
b' in Lower_Support p,
T,
i ) )
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
empty right_complementable add-associative right_zeroed addLoopStr ;
let p be
Polynomial of
n,
L;
let i be
Element of
NAT ;
func Up p,
T,
i -> Polynomial of
n,
L equals :: GROEB_3:def 4
p | (Upper_Support p,T,i);
coherence
p | (Upper_Support p,T,i) is Polynomial of n,L
;
func Low p,
T,
i -> Polynomial of
n,
L equals :: GROEB_3:def 5
p | (Lower_Support p,T,i);
coherence
p | (Lower_Support p,T,i) is Polynomial of n,L
;
end;
:: deftheorem defines Up GROEB_3:def 4 :
:: deftheorem defines Low GROEB_3:def 5 :
Lm3:
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i )
theorem :: GROEB_3:25
theorem Th26: :: GROEB_3:26
theorem Th27: :: GROEB_3:27
theorem Th28: :: GROEB_3:28
theorem Th29: :: GROEB_3:29
theorem Th30: :: GROEB_3:30
theorem Th31: :: GROEB_3:31
theorem Th32: :: GROEB_3:32
theorem Th33: :: GROEB_3:33
theorem Th34: :: GROEB_3:34
theorem Th35: :: GROEB_3:35
theorem Th36: :: GROEB_3:36
registration
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr ;
let p be
non-zero Polynomial of
n,
L;
cluster Up p,
T,1
-> non-zero monomial-like ;
coherence
( Up p,T,1 is non-zero & Up p,T,1 is monomial-like )
cluster Low p,
T,
(card (Support p)) -> monomial-like ;
coherence
Low p,T,(card (Support p)) is monomial-like
end;
theorem Th37: :: GROEB_3:37
theorem Th38: :: GROEB_3:38
theorem Th39: :: GROEB_3:39
theorem Th40: :: GROEB_3:40
theorem Th41: :: GROEB_3:41
theorem Th42: :: GROEB_3:42
theorem Th43: :: GROEB_3:43
theorem Th44: :: GROEB_3:44
Lm4:
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 P being Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T
for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds
R . i is Polynomial of n,L
theorem Th45: :: GROEB_3:45
Lm5:
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 st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
theorem Th46: :: GROEB_3:46
theorem Th47: :: GROEB_3:47
theorem :: GROEB_3:48
theorem Th49: :: GROEB_3:49
theorem :: GROEB_3:50
theorem Th51: :: GROEB_3:51
theorem Th52: :: GROEB_3:52
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 st
HT p1,
T,
HT p2,
T are_disjoint holds
for
b1,
b2 being
bag of
n st
b1 in Support (Red p1,T) &
b2 in Support (Red p2,T) holds
not
(HT p1,T) + b2 = (HT p2,T) + b1
theorem Th53: :: GROEB_3:53
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 Abelian add-associative right_zeroed doubleLoopStr for
p1,
p2 being
Polynomial of
n,
L st
HT p1,
T,
HT p2,
T are_disjoint holds
S-Poly p1,
p2,
T = ((HM p2,T) *' (Red p1,T)) - ((HM p1,T) *' (Red p2,T))
theorem Th54: :: GROEB_3:54
theorem Th55: :: GROEB_3:55
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 Abelian add-associative right_zeroed doubleLoopStr for
p1,
p2 being
non-zero Polynomial of
n,
L st
HT p1,
T,
HT p2,
T are_disjoint &
Red p1,
T is
non-zero &
Red p2,
T is
non-zero holds
PolyRedRel {p1},
T reduces ((HM p2,T) *' (Red p1,T)) - ((HM p1,T) *' (Red p2,T)),
p2 *' (Red p1,T)
theorem Th56: :: GROEB_3:56
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 Abelian add-associative right_zeroed doubleLoopStr for
p1,
p2 being
Polynomial of
n,
L st
HT p1,
T,
HT p2,
T are_disjoint holds
PolyRedRel {p1,p2},
T reduces S-Poly p1,
p2,
T,
0_ n,
L
theorem :: GROEB_3:57
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
G is_Groebner_basis_wrt T holds
for
g1,
g2 being
Polynomial of
n,
L st
g1 in G &
g2 in G & not
HT g1,
T,
HT g2,
T are_disjoint holds
PolyRedRel G,
T reduces S-Poly g1,
g2,
T,
0_ n,
L
theorem :: GROEB_3:58
for
n being
Element of
NAT for
T being
connected admissible TermOrder of
n for
L being non
degenerated non
trivial 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 not
0_ n,
L in G & ( for
g1,
g2 being
Polynomial of
n,
L st
g1 in G &
g2 in G & not
HT g1,
T,
HT g2,
T are_disjoint holds
PolyRedRel G,
T reduces S-Poly g1,
g2,
T,
0_ n,
L ) holds
for
g1,
g2,
h being
Polynomial of
n,
L st
g1 in G &
g2 in G & not
HT g1,
T,
HT g2,
T are_disjoint &
h is_a_normal_form_of S-Poly g1,
g2,
T,
PolyRedRel G,
T holds
h = 0_ n,
L
theorem :: GROEB_3:59
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 not
0_ n,
L in G & ( for
g1,
g2,
h being
Polynomial of
n,
L st
g1 in G &
g2 in G & not
HT g1,
T,
HT g2,
T are_disjoint &
h is_a_normal_form_of S-Poly g1,
g2,
T,
PolyRedRel G,
T holds
h = 0_ n,
L ) holds
G is_Groebner_basis_wrt T