:: Ring Ideals
:: by Jonathan Backer , Piotr Rudnicki and Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, ALGSTR_1, XBOOLE_0, ALGSTR_0, STRUCT_0,
VECTSP_2, VECTSP_1, BINOP_1, LATTICES, ZFMISC_1, SUBSET_1, CARD_3,
FINSEQ_1, ARYTM_3, ORDINAL4, RELAT_1, CARD_FIL, SUPINF_2, TARSKI,
ARYTM_1, MESFUNC1, CARD_1, NEWTON, NAT_1, XXREAL_0, REALSET1, FUNCT_1,
FUNCT_7, GROUP_1, PARTFUN1, PRELAMB, MCART_1, SETFAM_1, RLVECT_3, GCD_1,
LATTICE3, SQUARE_1, FINSET_1, INT_3, XCMPLX_0, IDEAL_1, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
FINSEQ_1, ORDINAL1, REALSET1, INT_3, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
NAT_1, RELSET_1, PARTFUN1, FUNCT_2, ALGSTR_1, XXREAL_2, XTUPLE_0,
MCART_1, POLYNOM1, SETFAM_1, DOMAIN_1, FINSEQ_4, NEWTON, STRUCT_0,
ALGSTR_0, RLVECT_1, VECTSP_1, GROUP_1, BINOP_1, VECTSP_2, FUNCT_7, GCD_1,
BINOM;
constructors SETFAM_1, BINOP_1, REALSET2, ALGSTR_1, GCD_1, INT_3, POLYNOM1,
BINOM, XXREAL_2, RELSET_1, FUNCT_7, FVSUM_1, FINSEQ_4, XTUPLE_0, NEWTON;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, VECTSP_1,
ALGSTR_1, INT_3, VALUED_0, ALGSTR_0, XXREAL_2, CARD_1, RELSET_1,
XTUPLE_0, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
registration
cluster add-associative left_zeroed right_zeroed for non empty addLoopStr;
end;
registration
cluster Abelian left_zeroed right_zeroed add-cancelable well-unital
add-associative associative commutative distributive for non trivial
doubleLoopStr;
end;
theorem :: IDEAL_1:1
for V being add-associative left_zeroed right_zeroed non empty
addLoopStr, v,u being Element of V holds Sum <* v,u *> = v + u;
begin :: Ideals
definition
let L be non empty addLoopStr, F being Subset of L;
attr F is add-closed means
:: IDEAL_1:def 1
for x, y being Element of L st x in F & y in F holds x+y in F;
end;
definition
let L be non empty multMagma, F be Subset of L;
attr F is left-ideal means
:: IDEAL_1:def 2
for p, x being Element of L st x in F holds p*x in F;
attr F is right-ideal means
:: IDEAL_1:def 3
for p, x being Element of L st x in F holds x*p in F;
end;
registration
let L be non empty addLoopStr;
cluster add-closed for non empty Subset of L;
end;
registration
let L be non empty multMagma;
cluster left-ideal for non empty Subset of L;
cluster right-ideal for non empty Subset of L;
end;
registration
let L be non empty doubleLoopStr;
cluster add-closed left-ideal right-ideal for non empty Subset of L;
cluster add-closed right-ideal for non empty Subset of L;
cluster add-closed left-ideal for non empty Subset of L;
end;
registration
let R be commutative non empty multMagma;
cluster left-ideal -> right-ideal for non empty Subset of R;
cluster right-ideal -> left-ideal for non empty Subset of R;
end;
definition
let L be non empty doubleLoopStr;
mode Ideal of L is add-closed left-ideal right-ideal non empty Subset of L;
end;
definition
let L be non empty doubleLoopStr;
mode RightIdeal of L is add-closed right-ideal non empty Subset of L;
end;
definition
let L be non empty doubleLoopStr;
mode LeftIdeal of L is add-closed left-ideal non empty Subset of L;
end;
theorem :: IDEAL_1:2
for R being right_zeroed left_add-cancelable left-distributive
non empty doubleLoopStr, I being left-ideal non empty Subset of R holds
0.R in I;
theorem :: IDEAL_1:3
for R being left_zeroed right_add-cancelable right-distributive
non empty doubleLoopStr, I being right-ideal non empty Subset of R holds
0.R in I;
theorem :: IDEAL_1:4
for L being right_zeroed non empty addLoopStr holds {0.L} is add-closed;
theorem :: IDEAL_1:5
for L being left_zeroed right_add-cancelable right-distributive
non empty doubleLoopStr holds {0.L} is left-ideal;
theorem :: IDEAL_1:6
for L being right_zeroed left_add-cancelable left-distributive
non empty doubleLoopStr holds {0.L} is right-ideal;
registration
let L be right_zeroed non empty addLoopStr;
cluster {0.L} -> add-closed for Subset of L;
end;
registration
let L be left_zeroed right_add-cancelable right-distributive non empty
doubleLoopStr;
cluster {0.L} -> left-ideal for Subset of L;
end;
registration
let L be right_zeroed left_add-cancelable left-distributive non empty
doubleLoopStr;
cluster {0.L} -> right-ideal for Subset of L;
end;
theorem :: IDEAL_1:7
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr holds {0.L} is Ideal of L;
theorem :: IDEAL_1:8
for L being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr holds {0.L} is LeftIdeal of L;
theorem :: IDEAL_1:9
for L being add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr holds {0.L} is RightIdeal of L;
theorem :: IDEAL_1:10
for L being non empty doubleLoopStr holds the carrier of L is Ideal of L;
theorem :: IDEAL_1:11
for L being non empty doubleLoopStr holds the carrier of L is LeftIdeal of L;
theorem :: IDEAL_1:12
for L being non empty doubleLoopStr holds the carrier of L is RightIdeal of L
;
definition
let R be left_zeroed right_zeroed add-cancelable distributive non empty
doubleLoopStr, I be Ideal of R;
redefine attr I is trivial means
:: IDEAL_1:def 4
I = {0.R};
end;
registration
let R be non trivial left_zeroed right_zeroed add-cancelable distributive
non empty doubleLoopStr;
cluster proper for Ideal of R;
end;
theorem :: IDEAL_1:13
for L being add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr, I being left-ideal
non empty Subset of L, x being Element of L st x in I holds -x in I;
theorem :: IDEAL_1:14
for L being add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr, I being right-ideal
non empty Subset of L, x being Element of L st x in I holds -x in I;
theorem :: IDEAL_1:15
for L being add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr, I being LeftIdeal of L
, x,y being Element of L st x in I & y in I holds x-y in I;
theorem :: IDEAL_1:16
for L being add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr, I being RightIdeal
of L, x,y being Element of L st x in I & y in I holds x-y in I;
theorem :: IDEAL_1:17
for R being left_zeroed right_zeroed add-cancelable
add-associative distributive non empty doubleLoopStr, I being add-closed
right-ideal non empty Subset of R, a being Element of I, n being Element of
NAT holds n*a in I;
theorem :: IDEAL_1:18
for R being well-unital left_zeroed right_zeroed add-cancelable
associative distributive non empty doubleLoopStr, I being right-ideal non
empty Subset of R, a being Element of I, n being Element of NAT st n <> 0
holds a|^n in I;
definition
let R be non empty addLoopStr, I be add-closed non empty Subset of R;
func add|(I,R) -> BinOp of I equals
:: IDEAL_1:def 5
(the addF of R)||I;
end;
definition
let R be non empty multMagma, I be right-ideal non empty Subset of R;
func mult|(I,R) -> BinOp of I equals
:: IDEAL_1:def 6
(the multF of R)||I;
end;
definition
let R be non empty addLoopStr, I be add-closed non empty Subset of R;
func Gr(I,R) -> non empty addLoopStr equals
:: IDEAL_1:def 7
addLoopStr (#I,add|(I,R),In (0.R,I)#);
end;
registration
let R be left_zeroed right_zeroed add-cancelable add-associative
distributive non empty doubleLoopStr, I be add-closed non empty Subset of R;
cluster Gr(I,R) -> add-associative;
end;
registration
let R be left_zeroed right_zeroed add-cancelable add-associative
distributive non empty doubleLoopStr, I be add-closed right-ideal non empty
Subset of R;
cluster Gr(I,R) -> right_zeroed;
end;
registration
let R be Abelian non empty doubleLoopStr, I be add-closed non empty
Subset of R;
cluster Gr(I,R) -> Abelian;
end;
registration
let R be Abelian right_unital left_zeroed right_zeroed right_complementable
add-associative distributive non empty doubleLoopStr, I be add-closed
right-ideal non empty Subset of R;
cluster Gr(I,R) -> right_complementable;
end;
theorem :: IDEAL_1:19
for R being right_unital non empty doubleLoopStr, I being
left-ideal non empty Subset of R holds I is proper iff not(1.R in I);
theorem :: IDEAL_1:20
for R being left_unital right_unital non empty doubleLoopStr, I
being right-ideal non empty Subset of R holds I is proper iff for u being
Element of R st u is unital holds not(u in I);
theorem :: IDEAL_1:21
for R being right_unital non empty doubleLoopStr, I being left-ideal
right-ideal non empty Subset of R holds I is proper iff for u being Element
of R st u is unital holds not(u in I);
theorem :: IDEAL_1:22
for R being non degenerated comRing holds R is Field iff for I being
Ideal of R holds (I = {0.R} or I = the carrier of R);
begin :: Linear combinations
definition
let R be non empty multLoopStr, A be non empty Subset of R;
mode LinearCombination of A -> FinSequence of the carrier of R means
:: IDEAL_1:def 8
for i being set st i in dom it
ex u,v being Element of R, a being Element of A st it/.i = u*a*v;
mode LeftLinearCombination of A -> FinSequence of the carrier of R means
:: IDEAL_1:def 9
for i being set st i in dom it
ex u being Element of R, a being Element of A st it/.i = u*a;
mode RightLinearCombination of A -> FinSequence of the carrier of R means
:: IDEAL_1:def 10
for i being set st i in dom it
ex u being Element of R, a being Element of A st it/.i = a*u;
end;
registration
let R be non empty multLoopStr, A be non empty Subset of R;
cluster non empty for LinearCombination of A;
cluster non empty for LeftLinearCombination of A;
cluster non empty for RightLinearCombination of A;
end;
definition
let R be non empty multLoopStr, A,B be non empty Subset of R, F be
LinearCombination of A, G be LinearCombination of B;
redefine func F^G -> LinearCombination of (A \/ B);
end;
theorem :: IDEAL_1:23
for R be associative non empty multLoopStr, A be non empty
Subset of R, a be Element of R, F be LinearCombination of A holds a*F is
LinearCombination of A;
theorem :: IDEAL_1:24
for R be associative non empty multLoopStr, A be non empty
Subset of R, a be Element of R, F be LinearCombination of A holds F*a is
LinearCombination of A;
theorem :: IDEAL_1:25
for R being right_unital non empty multLoopStr, A being non
empty Subset of R, f being LeftLinearCombination of A holds f is
LinearCombination of A;
definition
let R be non empty multLoopStr, A,B be non empty Subset of R, F be
LeftLinearCombination of A, G be LeftLinearCombination of B;
redefine func F^G -> LeftLinearCombination of (A \/ B);
end;
theorem :: IDEAL_1:26
for R be associative non empty multLoopStr, A be non empty
Subset of R, a be Element of R, F be LeftLinearCombination of A holds
a*F is LeftLinearCombination of A;
theorem :: IDEAL_1:27
for R be non empty multLoopStr, A be non empty Subset of R,
a be Element of R, F be LeftLinearCombination of A holds
F*a is LinearCombination of A;
theorem :: IDEAL_1:28
for R being left_unital non empty multLoopStr, A being non
empty Subset of R, f being RightLinearCombination of A holds
f is LinearCombination of A;
definition
let R be non empty multLoopStr, A,B be non empty Subset of R, F be
RightLinearCombination of A, G be RightLinearCombination of B;
redefine func F^G -> RightLinearCombination of (A \/ B);
end;
theorem :: IDEAL_1:29
for R be associative non empty multLoopStr, A be non empty
Subset of R, a be Element of R, F be RightLinearCombination of A holds
F*a is RightLinearCombination of A;
theorem :: IDEAL_1:30
for R be associative non empty multLoopStr, A be non empty Subset of
R, a be Element of R, F be RightLinearCombination of A holds
a*F is LinearCombination of A;
theorem :: IDEAL_1:31
for R being commutative associative non empty multLoopStr, A
being non empty Subset of R, f being LinearCombination of A holds
f is LeftLinearCombination of A & f is RightLinearCombination of A;
theorem :: IDEAL_1:32
for S being non empty doubleLoopStr, F being non empty Subset of
S, lc being non empty LinearCombination of F ex p being LinearCombination of F,
e being Element of S st lc = p^<* e *> & <*e*> is LinearCombination of F;
theorem :: IDEAL_1:33
for S being non empty doubleLoopStr, F being non empty Subset of
S, lc being non empty LeftLinearCombination of F ex p being
LeftLinearCombination of F, e being Element of S st lc = p^<* e *> & <*e*> is
LeftLinearCombination of F;
theorem :: IDEAL_1:34
for S being non empty doubleLoopStr, F being non empty Subset of
S, lc being non empty RightLinearCombination of F ex p being
RightLinearCombination of F, e being Element of S st lc = p^<* e *> & <*e*> is
RightLinearCombination of F;
definition
let R be non empty multLoopStr, A be non empty Subset of R,
L be LinearCombination of A,
E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:];
pred E represents L means
:: IDEAL_1:def 11
len E = len L & for i being set st i in
dom L holds L.i = ((E/.i)`1_3)*((E/.i)`2_3)*((E/.i)`3_3) & ((E/.i)`2_3) in A;
end;
theorem :: IDEAL_1:35
for R being non empty multLoopStr, A being non empty Subset of R, L be
LinearCombination of A ex E be FinSequence of [:the carrier of R, the carrier
of R, the carrier of R:] st E represents L;
theorem :: IDEAL_1:36
for R, S being non empty multLoopStr, F being non empty Subset of R,
lc being LinearCombination of F, G being non empty Subset of S, P being
Function of the carrier of R, the carrier of S, E being FinSequence of [:the
carrier of R, the carrier of R, the carrier of R:] st P.:F c= G & E represents
lc holds ex LC being LinearCombination of G st len lc = len LC & for i being
set st i in dom LC
holds LC.i = (P.((E/.i)`1_3))*(P.((E/.i)`2_3))*(P.((E/.i)`3_3));
definition
let R be non empty multLoopStr, A be non empty Subset of R,
L be LeftLinearCombination of A,
E be FinSequence of [:the carrier of R, the carrier of R:];
pred E represents L means
:: IDEAL_1:def 12
len E = len L & for i being set st i in
dom L holds L.i = ((E/.i)`1)*((E/.i)`2) & ((E/.i)`2) in A;
end;
theorem :: IDEAL_1:37
for R being non empty multLoopStr, A being non empty Subset of R, L be
LeftLinearCombination of A ex E be FinSequence of [:the carrier of R, the
carrier of R:] st E represents L;
theorem :: IDEAL_1:38
for R, S being non empty multLoopStr, F being non empty Subset of R,
lc being LeftLinearCombination of F, G being non empty Subset of S, P being
Function of the carrier of R, the carrier of S, E being FinSequence of [:the
carrier of R, the carrier of R:] st P.:F c= G & E represents lc holds ex LC
being LeftLinearCombination of G st len lc = len LC & for i being set st i in
dom LC holds LC.i = (P.(E/.i)`1)*(P.(E/.i)`2);
definition
let R be non empty multLoopStr, A be non empty Subset of R, L be
RightLinearCombination of A, E be FinSequence of [:the carrier of R, the
carrier of R:];
pred E represents L means
:: IDEAL_1:def 13
len E = len L & for i being set st i in
dom L holds L.i = ((E/.i)`1)*((E/.i)`2) & ((E/.i)`1) in A;
end;
theorem :: IDEAL_1:39
for R being non empty multLoopStr, A being non empty Subset of R, L be
RightLinearCombination of A ex E be FinSequence of [:the carrier of R, the
carrier of R:] st E represents L;
theorem :: IDEAL_1:40
for R, S being non empty multLoopStr, F being non empty Subset of R,
lc being RightLinearCombination of F, G being non empty Subset of S, P being
Function of the carrier of R, the carrier of S, E being FinSequence of [:the
carrier of R, the carrier of R:] st P.:F c= G & E represents lc holds ex LC
being RightLinearCombination of G st len lc = len LC & for i being set st i in
dom LC holds LC.i = (P.(E/.i)`1)*(P.(E/.i)`2);
theorem :: IDEAL_1:41
for R being non empty multLoopStr, A being non empty Subset of R, l
being LinearCombination of A, n being Nat holds l|Seg n is
LinearCombination of A;
theorem :: IDEAL_1:42
for R being non empty multLoopStr, A being non empty Subset of R, l
being LeftLinearCombination of A, n being Nat holds l|Seg n is
LeftLinearCombination of A;
theorem :: IDEAL_1:43
for R being non empty multLoopStr, A being non empty Subset of R, l
being RightLinearCombination of A, n being Nat holds l|Seg n is
RightLinearCombination of A;
begin :: Generated ideals
definition
let L be non empty doubleLoopStr, F be Subset of L;
assume
F is non empty;
func F-Ideal -> Ideal of L means
:: IDEAL_1:def 14
F c= it & for I being Ideal of L st F c= I holds it c= I;
func F-LeftIdeal -> LeftIdeal of L means
:: IDEAL_1:def 15
F c= it & for I being LeftIdeal of L st F c= I holds it c= I;
func F-RightIdeal -> RightIdeal of L means
:: IDEAL_1:def 16
F c= it & for I being RightIdeal of L st F c= I holds it c= I;
end;
theorem :: IDEAL_1:44
for L being non empty doubleLoopStr, I being Ideal of L holds I -Ideal = I;
theorem :: IDEAL_1:45
for L being non empty doubleLoopStr, I being LeftIdeal of L
holds I-LeftIdeal = I;
theorem :: IDEAL_1:46
for L being non empty doubleLoopStr, I being RightIdeal of L
holds I-RightIdeal = I;
definition
let L be non empty doubleLoopStr, I be Ideal of L;
mode Basis of I -> non empty Subset of L means
:: IDEAL_1:def 17
it-Ideal = I;
end;
theorem :: IDEAL_1:47
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr holds {0.L}-Ideal = {0.L};
theorem :: IDEAL_1:48
for L being left_zeroed right_zeroed add-cancelable distributive non
empty doubleLoopStr holds {0.L}-Ideal = {0.L};
theorem :: IDEAL_1:49
for L being left_zeroed right_zeroed right_add-cancelable
right-distributive non empty doubleLoopStr holds {0.L}-LeftIdeal = {0.L};
theorem :: IDEAL_1:50
for L being right_zeroed left_add-cancelable left-distributive non
empty doubleLoopStr holds {0.L}-RightIdeal = {0.L};
theorem :: IDEAL_1:51
for L being well-unital non empty doubleLoopStr holds {1.L}-Ideal =
the carrier of L;
theorem :: IDEAL_1:52
for L being right_unital non empty doubleLoopStr holds {1.L}
-LeftIdeal = the carrier of L;
theorem :: IDEAL_1:53
for L being left_unital non empty doubleLoopStr holds {1.L}
-RightIdeal = the carrier of L;
theorem :: IDEAL_1:54
for L being non empty doubleLoopStr holds ([#] L)-Ideal = the carrier of L;
theorem :: IDEAL_1:55
for L being non empty doubleLoopStr holds ([#] L)-LeftIdeal = the
carrier of L;
theorem :: IDEAL_1:56
for L being non empty doubleLoopStr holds ([#] L)-RightIdeal = the
carrier of L;
theorem :: IDEAL_1:57
for L being non empty doubleLoopStr, A, B being non empty Subset
of L st A c= B holds A-Ideal c= B-Ideal;
theorem :: IDEAL_1:58
for L being non empty doubleLoopStr, A, B being non empty Subset of L
st A c= B holds A-LeftIdeal c= B-LeftIdeal;
theorem :: IDEAL_1:59
for L being non empty doubleLoopStr, A, B being non empty Subset of L
st A c= B holds A-RightIdeal c= B-RightIdeal;
theorem :: IDEAL_1:60
for L being add-associative left_zeroed right_zeroed
add-cancelable associative distributive well-unital non empty doubleLoopStr,
F being non empty Subset of L, x being set holds x in F-Ideal iff ex f being
LinearCombination of F st x = Sum f;
theorem :: IDEAL_1:61
for L being add-associative left_zeroed right_zeroed
add-cancelable associative distributive well-unital non empty doubleLoopStr,
F being non empty Subset of L, x being set holds x in F-LeftIdeal iff ex f
being LeftLinearCombination of F st x = Sum f;
theorem :: IDEAL_1:62
for L being add-associative left_zeroed right_zeroed
add-cancelable associative distributive well-unital non empty doubleLoopStr,
F being non empty Subset of L, x being set holds x in F-RightIdeal iff ex f
being RightLinearCombination of F st x = Sum f;
theorem :: IDEAL_1:63
for R being add-associative left_zeroed right_zeroed
add-cancelable well-unital associative commutative distributive non empty
doubleLoopStr, F being non empty Subset of R holds F-Ideal = F-LeftIdeal & F
-Ideal = F-RightIdeal;
theorem :: IDEAL_1:64
for R being add-associative left_zeroed right_zeroed
add-cancelable well-unital associative commutative distributive non empty
doubleLoopStr, a being Element of R holds {a}-Ideal = the set of all
a*r where r is Element
of R;
theorem :: IDEAL_1:65
for R being Abelian left_zeroed right_zeroed add-cancelable
well-unital add-associative associative commutative distributive non empty
doubleLoopStr, a,b being Element of R holds {a,b}-Ideal = the set of all
a*r + b*s where r,s
is Element of R;
theorem :: IDEAL_1:66
for R being non empty doubleLoopStr, a being Element of R holds
a in {a}-Ideal;
theorem :: IDEAL_1:67
for R being Abelian left_zeroed right_zeroed right_complementable
add-associative associative commutative distributive well-unital non empty
doubleLoopStr, A being non empty Subset of R, a being Element of R holds a in
A-Ideal implies {a}-Ideal c= A-Ideal;
theorem :: IDEAL_1:68
for R being non empty doubleLoopStr, a,b being Element of R holds a in
{a,b}-Ideal & b in {a,b}-Ideal;
theorem :: IDEAL_1:69
for R being non empty doubleLoopStr, a,b being Element of R holds {a}
-Ideal c= {a,b}-Ideal & {b}-Ideal c= {a,b}-Ideal;
begin :: Some Operations on Ideals
definition
let R be non empty multMagma, I be Subset of R, a be Element of R;
func a*I -> Subset of R equals
:: IDEAL_1:def 18
{a*i where i is Element of R : i in I};
end;
registration
let R be non empty multLoopStr, I be non empty Subset of R,
a be Element of R;
cluster a*I -> non empty;
end;
registration
let R be distributive non empty doubleLoopStr, I be add-closed Subset of R,
a be Element of R;
cluster a*I -> add-closed;
end;
registration
let R be associative non empty doubleLoopStr, I be right-ideal Subset of R,
a be Element of R;
cluster a*I -> right-ideal;
end;
theorem :: IDEAL_1:70
for R being right_zeroed left_add-cancelable left-distributive
non empty doubleLoopStr, I being non empty Subset of R holds 0.R*I = {0.R};
theorem :: IDEAL_1:71
for R being left_unital non empty doubleLoopStr, I being Subset of R
holds 1.R*I = I;
definition
let R be addMagma, I,J be Subset of R;
func I + J -> Subset of R equals
:: IDEAL_1:def 19
{a + b where a,b is Element of R : a in I & b in J};
end;
registration
let R be non empty addLoopStr, I,J be non empty Subset of R;
cluster I + J -> non empty;
end;
definition
let R be Abelian non empty addLoopStr, I,J be Subset of R;
redefine func I + J;
commutativity;
end;
registration
let R be Abelian add-associative non empty addLoopStr, I,J be add-closed
Subset of R;
cluster I + J -> add-closed;
end;
registration
let R be left-distributive non empty doubleLoopStr, I,J be right-ideal
Subset of R;
cluster I + J -> right-ideal;
end;
registration
let R be right-distributive non empty doubleLoopStr, I,J be left-ideal
Subset of R;
cluster I + J -> left-ideal;
end;
theorem :: IDEAL_1:72
for R being add-associative non empty addLoopStr, I,J,K being Subset
of R holds I + (J + K) = (I + J) + K;
theorem :: IDEAL_1:73
for R being left_zeroed right_zeroed right_add-cancelable
right-distributive non empty doubleLoopStr, I,J being right-ideal non empty
Subset of R holds I c= I + J;
theorem :: IDEAL_1:74
for R being left_zeroed right_add-cancelable right-distributive
non empty doubleLoopStr, I,J being right-ideal non empty Subset of R holds
J c= I + J;
theorem :: IDEAL_1:75
for R being non empty addLoopStr, I,J being Subset of R, K being
add-closed Subset of R st I c= K & J c= K holds I + J c= K;
theorem :: IDEAL_1:76
for R being Abelian left_zeroed right_zeroed add-cancelable
well-unital add-associative associative commutative distributive non empty
doubleLoopStr, a,b being Element of R holds {a,b}-Ideal = {a}-Ideal + {b}
-Ideal;
definition
let R be non empty 1-sorted, I,J be Subset of R;
redefine func I /\ J -> Subset of R equals
:: IDEAL_1:def 20
{ x where x is Element of R : x in I & x in J };
end;
registration
let R be right_zeroed left_add-cancelable left-distributive non empty
doubleLoopStr, I,J be left-ideal non empty Subset of R;
cluster I /\ J -> non empty;
end;
registration
let R be non empty addLoopStr, I,J be add-closed Subset of R;
cluster I /\ J -> add-closed for Subset of R;
end;
registration
let R be non empty multLoopStr, I,J be left-ideal Subset of R;
cluster I /\ J -> left-ideal for Subset of R;
end;
registration
let R be non empty multLoopStr, I,J be right-ideal Subset of R;
cluster I /\ J -> right-ideal for Subset of R;
end;
theorem :: IDEAL_1:77
for R being Abelian left_zeroed right_zeroed right_complementable
left_unital add-associative left-distributive non empty doubleLoopStr, I
being add-closed left-ideal non empty Subset of R, J being Subset of R, K
being non empty Subset of R st J c= I holds I /\ (J + K) = J + (I /\ K);
definition
let R be non empty doubleLoopStr, I,J be Subset of R;
func I *' J -> Subset of R equals
:: IDEAL_1:def 21
{ Sum s where s is FinSequence of the
carrier of R : for i being Element of NAT st 1 <= i & i <= len s ex a,b being
Element of R st s.i = a*b & a in I & b in J};
end;
registration
let R be non empty doubleLoopStr, I,J be Subset of R;
cluster I *' J -> non empty;
end;
definition
let R be commutative non empty doubleLoopStr, I,J be Subset of R;
redefine func I *' J;
commutativity;
end;
registration
let R be right_zeroed add-associative non empty doubleLoopStr, I,J be
Subset of R;
cluster I *' J -> add-closed;
end;
registration
let R be right_zeroed left_add-cancelable associative left-distributive non
empty doubleLoopStr, I,J be right-ideal Subset of R;
cluster I *' J -> right-ideal;
end;
registration
let R be left_zeroed right_add-cancelable associative right-distributive
non empty doubleLoopStr, I,J be left-ideal Subset of R;
cluster I *' J -> left-ideal;
end;
theorem :: IDEAL_1:78
for R being left_zeroed right_zeroed left_add-cancelable
left-distributive non empty doubleLoopStr, I being non empty Subset of R
holds {0.R} *' I = {0.R};
theorem :: IDEAL_1:79
for R being left_zeroed right_zeroed add-cancelable distributive
non empty doubleLoopStr,
I being add-closed right-ideal non empty Subset of R,
J being add-closed left-ideal non empty Subset of R holds I *' J c= I /\ J;
theorem :: IDEAL_1:80
for R being Abelian left_zeroed right_zeroed add-cancelable
add-associative associative distributive non empty doubleLoopStr, I,J,K being
right-ideal non empty Subset of R holds I *' (J + K) = (I *' J) + (I *' K);
theorem :: IDEAL_1:81
for R being Abelian left_zeroed right_zeroed add-cancelable
add-associative commutative associative distributive non empty doubleLoopStr,
I,J being right-ideal non empty Subset of R holds (I + J) *' (I /\ J) c= I *' J
;
theorem :: IDEAL_1:82
for R being right_zeroed left_add-cancelable left-distributive non
empty doubleLoopStr, I,J being add-closed left-ideal non empty Subset of R
holds (I + J) *' (I /\ J) c= I /\ J;
definition
let R be addMagma, I,J be Subset of R;
pred I,J are_co-prime means
:: IDEAL_1:def 22
I + J = the carrier of R;
end;
theorem :: IDEAL_1:83
for R being left_zeroed left_unital non empty doubleLoopStr,
I,J being non empty Subset of R st I,J are_co-prime holds
I /\ J c= (I + J) *' (I /\ J);
theorem :: IDEAL_1:84
for R being Abelian left_zeroed right_zeroed add-cancelable
add-associative left_unital commutative associative distributive non empty
doubleLoopStr, I being add-closed left-ideal right-ideal non empty Subset of
R, J being add-closed left-ideal non empty Subset of R st I,J are_co-prime
holds I *' J = I /\ J;
definition
let R be non empty multMagma, I,J be Subset of R;
func I % J -> Subset of R equals
:: IDEAL_1:def 23
{a where a is Element of R: a*J c= I};
end;
registration
let R be right_zeroed left_add-cancelable left-distributive non empty
doubleLoopStr, I,J be left-ideal non empty Subset of R;
cluster I % J -> non empty;
end;
registration
let R be right_zeroed left_add-cancelable left-distributive non empty
doubleLoopStr, I,J be add-closed left-ideal non empty Subset of R;
cluster I % J -> add-closed;
end;
registration
let R be right_zeroed left_add-cancelable left-distributive associative
commutative non empty doubleLoopStr, I,J be left-ideal non empty Subset of R;
cluster I % J -> left-ideal;
cluster I % J -> right-ideal;
end;
theorem :: IDEAL_1:85
for R being non empty multLoopStr, I being right-ideal non empty
Subset of R, J being Subset of R holds I c= I % J;
theorem :: IDEAL_1:86
for R being right_zeroed left_add-cancelable left-distributive non
empty doubleLoopStr, I being add-closed left-ideal non empty Subset of R, J
being Subset of R holds (I % J) *' J c= I;
theorem :: IDEAL_1:87
for R being left_zeroed right_add-cancelable right-distributive
non empty doubleLoopStr, I being add-closed right-ideal non empty Subset of
R, J being Subset of R holds (I % J) *' J c= I;
theorem :: IDEAL_1:88
for R being left_zeroed right_add-cancelable right-distributive
commutative associative non empty doubleLoopStr, I being add-closed
right-ideal non empty Subset of R, J,K being Subset of R holds (I % J) % K =
I % (J *' K);
theorem :: IDEAL_1:89
for R being non empty multLoopStr, I,J,K being Subset of R holds (J /\
K) % I = (J % I) /\ (K % I);
theorem :: IDEAL_1:90
for R being left_zeroed right_zeroed right_add-cancelable
right-distributive non empty doubleLoopStr, I being add-closed Subset of R, J
,K being right-ideal non empty Subset of R holds I % (J + K) = (I % J) /\ (I
% K);
definition
let R be well-unital non empty doubleLoopStr, I be Subset of R;
func sqrt I -> Subset of R equals
:: IDEAL_1:def 24
{a where a is Element of R: ex n being
Element of NAT st a|^n in I};
end;
registration
let R be well-unital non empty doubleLoopStr, I be non empty Subset of R;
cluster sqrt I -> non empty;
end;
registration
let R be Abelian add-associative left_zeroed right_zeroed commutative
associative add-cancelable distributive well-unital non empty doubleLoopStr,
I be add-closed right-ideal non empty Subset of R;
cluster sqrt I -> add-closed;
end;
registration
let R be well-unital commutative associative non empty doubleLoopStr, I be
left-ideal non empty Subset of R;
cluster sqrt I -> left-ideal;
cluster sqrt I -> right-ideal;
end;
theorem :: IDEAL_1:91
for R being well-unital associative non empty doubleLoopStr, I being
non empty Subset of R, a being Element of R holds a in sqrt I iff ex n being
Element of NAT st a|^n in sqrt I;
theorem :: IDEAL_1:92
for R being left_zeroed right_zeroed add-cancelable distributive
well-unital associative non empty doubleLoopStr, I being add-closed
right-ideal non empty Subset of R, J being add-closed left-ideal non empty
Subset of R holds sqrt (I *' J) = sqrt (I /\ J);
begin :: Noetherian ideals
definition
let L be non empty doubleLoopStr, I be Ideal of L;
attr I is finitely_generated means
:: IDEAL_1:def 25
ex F being non empty finite Subset of L st I = F-Ideal;
end;
registration
let L be non empty doubleLoopStr;
cluster finitely_generated for Ideal of L;
end;
registration
let L be non empty doubleLoopStr, F be non empty finite Subset of L;
cluster F-Ideal -> finitely_generated;
end;
definition
let L be non empty doubleLoopStr;
attr L is Noetherian means
:: IDEAL_1:def 26
for I being Ideal of L holds I is finitely_generated;
end;
registration
cluster Euclidian Abelian add-associative right_zeroed right_complementable
well-unital distributive commutative associative non degenerated for
non empty
doubleLoopStr;
end;
definition
let L be non empty doubleLoopStr;
let I be Ideal of L;
attr I is principal means
:: IDEAL_1:def 27
ex e being Element of L st I = {e}-Ideal;
end;
definition
let L be non empty doubleLoopStr;
attr L is PID means
:: IDEAL_1:def 28
for I being Ideal of L holds I is principal;
end;
theorem :: IDEAL_1:93
for L being non empty doubleLoopStr, F being non empty Subset of
L st F <> {0.L} ex x being Element of L st x <> 0.L & x in F;
theorem :: IDEAL_1:94
for R being add-associative left_zeroed right_zeroed
right_complementable distributive well-unital Euclidian non empty
doubleLoopStr holds R is PID;
theorem :: IDEAL_1:95
for L being non empty doubleLoopStr st L is PID holds L is Noetherian;
registration
cluster INT.Ring -> Noetherian;
end;
registration
cluster Noetherian Abelian add-associative right_zeroed right_complementable
well-unital distributive commutative associative non degenerated for
non empty
doubleLoopStr;
end;
theorem :: IDEAL_1:96 :: Lemma_4_5_i_ii:
for R being Noetherian add-associative left_zeroed right_zeroed
add-cancelable associative distributive well-unital non empty doubleLoopStr
for B being non empty Subset of R ex C being non empty finite Subset of R st C
c= B & C-Ideal = B-Ideal;
theorem :: IDEAL_1:97 :: Lemma_4_5_ii_iii:
for R being non empty doubleLoopStr st for B being non empty Subset
of R ex C being non empty finite Subset of R st C c= B & C-Ideal = B-Ideal for
a being sequence of R ex m being Element of NAT st a.(m+1) in (rng (a|(m+1)))
-Ideal;
registration
let X, Y be non empty set, f be Function of X, Y, A be non empty Subset of X;
cluster f|A -> non empty;
end;
theorem :: IDEAL_1:98 :: Lemma_4_5_iii_iv:
for R being non empty doubleLoopStr st for a being sequence of R ex
m being Element of NAT st a.(m+1) in (rng (a|(m+1)))-Ideal holds not ex F being
sequence of bool (the carrier of R) st (for i being Nat holds F
.i is Ideal of R) & (for j,k being Nat st j < k holds F.j c< F.k);
theorem :: IDEAL_1:99 :: Lemma_4_5_iv_i:
for R being non empty doubleLoopStr st not ex F being sequence of
bool (the carrier of R) st (for i being Element of NAT holds F.i is Ideal
of R) & (for j,k being Element of NAT st j < k holds F.j c< F.k) holds R is
Noetherian;