:: Characterization and Existence of {G}r\"obner Bases
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: GROEB_1:1
theorem :: GROEB_1:2
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,
p,
g being
Polynomial of
n,
L st
f reduces_to g,
p,
T holds
ex
m being
Monomial of
n,
L st
(
g = f - (m *' p) & not
HT (m *' p),
T in Support g &
HT (m *' p),
T <= HT f,
T,
T )
Lm1:
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
Lm2:
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 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
Lm3:
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 holds f is_irreducible_wrt 0_ n,L,T
theorem Th3: :: GROEB_1:3
theorem Th4: :: GROEB_1:4
theorem Th5: :: GROEB_1:5
theorem Th6: :: GROEB_1:6
theorem Th7: :: GROEB_1:7
theorem Th8: :: GROEB_1:8
theorem Th9: :: GROEB_1:9
theorem Th10: :: GROEB_1:10
theorem :: GROEB_1:11
:: deftheorem defines HT GROEB_1:def 1 :
:: deftheorem defines multiples GROEB_1:def 2 :
theorem :: GROEB_1:12
theorem :: GROEB_1:13
theorem :: GROEB_1:14
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 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
Lm5:
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, g being Polynomial of n,L
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel P,T reduces h,g )
theorem Th15: :: GROEB_1:15
theorem Th16: :: GROEB_1:16
theorem Th17: :: GROEB_1:17
theorem Th18: :: GROEB_1:18
theorem :: GROEB_1:19
theorem :: GROEB_1:20
:: deftheorem Def3 defines is_Groebner_basis_wrt GROEB_1:def 3 :
:: deftheorem Def4 defines is_Groebner_basis_of GROEB_1:def 4 :
Lm6:
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 a, b being set st a <> b & PolyRedRel P,T reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
theorem :: GROEB_1:21
theorem :: GROEB_1:22
theorem :: GROEB_1:23
Lm7:
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 I being LeftIdeal of (Polynom-Ring n,L)
for G being non empty Subset of (Polynom-Ring n,L) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L ) holds
G -Ideal = I
theorem Th24: :: GROEB_1:24
theorem Th25: :: GROEB_1:25
theorem Th26: :: GROEB_1:26
theorem Th27: :: GROEB_1:27
theorem Th28: :: GROEB_1:28
theorem Th29: :: GROEB_1:29
theorem Th30: :: GROEB_1:30
theorem :: GROEB_1:31
theorem :: GROEB_1:32
theorem :: GROEB_1:33
Lm8:
for n being Ordinal
for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3
:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :
theorem Th34: :: GROEB_1:34
theorem Th35: :: GROEB_1:35
Lm9:
for L being non empty right_complementable associative well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for A, B being non empty Subset of L st 0. L in A & B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
theorem :: GROEB_1:36
:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :
:: deftheorem Def7 defines is_reduced_wrt GROEB_1:def 7 :
theorem Th37: :: GROEB_1:37
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
I being
add-closed left-ideal Subset of
(Polynom-Ring n,L) for
m being
Monomial of
n,
L for
f,
g being
Polynomial of
n,
L st
f in I &
g in I &
HM f,
T = m &
HM g,
T = m & ( for
p being
Polynomial of
n,
L holds
( not
p in I or not
p < f,
T or not
HM p,
T = m ) ) & ( for
p being
Polynomial of
n,
L holds
( not
p in I or not
p < g,
T or not
HM p,
T = m ) ) holds
f = g
Lm10:
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 Polynomial of n,L
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st p in I & p <> 0_ n,L holds
ex q being Polynomial of n,L st
( q in I & HM q,T = Monom (1. L),(HT p,T) & q <> 0_ n,L )
theorem :: GROEB_1:38
theorem :: GROEB_1:39
theorem :: GROEB_1:40