:: The First Isomorphism Theorem and Other Properties of Rings
:: by Artur Korni{\l}owicz and Christoph Schwarzweller
::
:: Received November 29, 2014
:: Copyright (c) 2014-2026 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 ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, GCD_1, WELLORD1, ORDINAL4,
VECTSP_1, CARD_3, ALGSTR_0, XBOOLE_0, TARSKI, INT_1, FUNCT_2, TREES_2,
XCMPLX_0, VECTSP_2, VECTSP10, STRUCT_0, SUBSET_1, SUPINF_2, REARRAN1,
NAT_1, CARD_1, MESFUNC1, INT_3, GROUP_1, ARYTM_1, FINSEQ_1, SETFAM_1,
INT_2, YELLOW_8, QUOFIELD, MSSUBFAM, BINOP_1, GROUP_4, GROUP_6, MOD_4,
LATTICES, HURWITZ, NUMBERS, IDEAL_1, REALSET1, C0SP1, RATFUNC1, EQREL_1,
POLYNOM1, POLYNOM3, ZFMISC_1, FUNCSDOM, WAYBEL20, CARD_FIL, RING_1,
RING_2, PARTFUN1, FINSEQ_3, WAYBEL_6, FUNCOP_1, XXREAL_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, REALSET1,
FINSEQ_1, VFUNCT_1, ORDINAL1, EQREL_1, XCMPLX_0, XXREAL_0, NAT_1, INT_1,
WSIERP_1,
INT_2, INT_3, NUMBERS, VECTSP_1, VECTSP_2, QUOFIELD, STRUCT_0, ALGSTR_0,
GROUP_1, RLVECT_1, GCD_1, POLYNOM3, HURWITZ, IDEAL_1, GROUP_4, GROUP_6,
VECTSP10, MOD_4, C0SP1, RATFUNC1, RING_1;
constructors RING_1, C0SP1, BINOM, RELSET_1, GCD_1, QUOFIELD, BINOP_2,
VFUNCT_1, RATFUNC1, MOD_4, GROUP_6, REALSET1, INT_3, RINGCAT1, GROUP_4,
HURWITZ, VECTSP10, INT_2, WSIERP_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED,
FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, SUBSET_1, RELAT_1, FUNCT_2,
ALGSTR_0, RLVECT_1, QUOFIELD, REALSET1, VFUNCT_1, RATFUNC1, IDEAL_1,
MOD_4, RINGCAT1, RING_1, C0SP1, XCMPLX_0, XXREAL_0, INT_3, VALUED_0,
FUNCT_1, PARTFUN1, CARD_1, GRCAT_1, GROUP_6;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions RELAT_1, FUNCT_2, VECTSP_1, GROUP_1, GROUP_6, IDEAL_1, INT_3;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, FINSEQ_1,
VECTSP10;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, IDEAL_1, XBOOLE_0,
FUNCT_1, QUOFIELD, GROUP_6, TARSKI, GCD_1;
theorems ALGSTR_0, GROUP_1, GROUP_6, VECTSP_1, VECTSP_2, RLVECT_1, IDEAL_1,
GCD_1, SUBSET_1, FUNCT_2, TARSKI, FUNCT_1, C0SP1, POLYNOM3, RING_1,
REALSET1, HURWITZ, INT_3, RATFUNC1, ZFMISC_1, NAT_1, INT_1, INT_2, INT_5,
XBOOLE_0, FINSEQ_1, FINSEQ_2, ORDINAL1, XXREAL_0, FUNCOP_1, GROUP_4,
XREAL_1, FINSEQ_3, POLYNOM2, PARTFUN1, UPROOTS;
schemes NAT_1, FUNCT_2, RECDEF_1;
begin :: Preliminaries
definition
let R be non empty set;
let f be non empty FinSequence of R;
let x be Element of dom f;
redefine func f.x -> Element of R; :: redefines . (FUNCT_1, definition)
coherence
proof
f.x in rng f by FUNCT_1:3;
hence thesis;
end;
end;
registration
let X be set;
let F1,F2 be X-valued FinSequence;
cluster F1 ^ F2 -> X-valued;
coherence;
end;
theorem prod4:
for R being add-associative right_zeroed right_complementable
distributive well-unital non empty doubleLoopStr,
F being FinSequence of R
st ex i being Nat st i in dom F & F.i = 0.R holds Product F = 0.R
proof
let R be add-associative right_zeroed right_complementable
distributive well-unital non empty doubleLoopStr;
let m be FinSequence of R;
given i being Nat such that
A: i in dom m & m.i = 0.R;
m/.i = m.i by A,PARTFUN1:def 6;
hence thesis by A,POLYNOM2:4;
end;
theorem prod5:
for R being add-associative right_zeroed right_complementable well-unital
distributive domRing-like non degenerated doubleLoopStr,
F being FinSequence of R
holds Product F = 0.R iff ex i being Nat st i in dom F & F.i = 0.R
proof
let R be add-associative right_zeroed right_complementable well-unital
distributive domRing-like non degenerated doubleLoopStr,
F be FinSequence of R;
now assume AS: Product F = 0.R;
defpred P[Nat] means
for f being FinSequence of R st len f = $1
holds Product(f) = 0.R implies ex i being Nat st i in dom f & f.i = 0.R;
A0: P[0]
proof
let F be FinSequence of R;
assume len F = 0;
then F = <*>(the carrier of R);
then Product F = 1_R by GROUP_4:8 .= 1.R;
hence thesis;
end;
A1: for k be Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume IV: P[k];
now let F be FinSequence of R;
assume A3: len F = k+1;
then F <> {};
then consider q being FinSequence, x being object such that
B2: F = q^<*x*> by FINSEQ_1:46;
B2a: rng q c= rng F by B2,FINSEQ_1:29;
rng F c= the carrier of R;
then rng q c= the carrier of R by B2a;then
reconsider q as FinSequence of R by FINSEQ_1:def 4;
rng<*x*> = {x} by FINSEQ_1:39;
then B5: x in rng<*x*> by TARSKI:def 1;
rng<*x*> c= rng F by B2,FINSEQ_1:30;
then x in rng F by B5;
then reconsider x as Element of R;
A4: len F = len q + len<*x*> by B2,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:39;
A5: Product F = (Product q) * x by GROUP_4:6,B2;
assume A6: Product F = 0.R;
per cases by A6,A5,VECTSP_2:def 1;
suppose Product q = 0.R;
then consider j being Nat such that
C1: j in dom q & q.j = 0.R by A3,A4,IV;
C2: F.j = q.j by B2,C1,FINSEQ_1:def 7;
dom q c= dom F by B2,FINSEQ_1:26;
hence ex i being Nat st i in dom F & F.i = 0.R by C1,C2;
end;
suppose C0: x = 0.R;
dom<*x*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*x*> by TARSKI:def 1;
then C1: F.(k+1) = <*x*>.1 by B2,A4,A3,FINSEQ_1:def 7
.= x;
dom F = Seg(k+1) by A3,FINSEQ_1:def 3;
hence ex i being Nat st i in dom F & F.i = 0.R by C1,C0,FINSEQ_1:4;
end;
end;
hence thesis;
end;
A2: for k be Nat holds P[k] from NAT_1:sch 2(A0,A1);
ex n being Nat st len F = n;
hence ex i being Nat st i in dom F & F.i = 0.R by AS,A2;
end;
hence thesis by prod4;
end;
definition
let X be set;
mode Chain of X is sequence of X;
end;
definition
let X be non empty set,
C be Chain of X;
attr C is ascending means :asc:
for i being Nat holds C.i c= C.(i+1);
attr C is stagnating means
ex i being Nat
st for j being Nat st j >= i holds C.j = C.i;
end;
registration
let X be non empty set;
let x be Element of X;
cluster NAT --> x -> ascending stagnating for Chain of X;
coherence
proof
let C be Chain of X such that
A1: C = NAT --> x;
hereby
let i be Nat;
C.i = x & C.(i+1) = x by A1,FUNCOP_1:7,ORDINAL1:def 12;
hence C.i c= C.(i+1);
end;
take 0;
let j be Nat;
C.0 = x & C.j = x by A1,FUNCOP_1:7,ORDINAL1:def 12;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster ascending stagnating for Chain of X;
existence
proof
take NAT --> the Element of X;
thus thesis;
end;
end;
ch1: for X be non empty set, C be ascending Chain of X,
x be object, i,j being Nat
st (i <= j & x in C.i) holds x in C.j
proof
let X be non empty set, C be ascending Chain of X,
x be object, i,j be Nat;
assume AS: i <= j & x in C.i;
defpred P[Nat] means for j being Nat holds j = i + $1 implies x in C.j;
A: P[0] by AS;
B: now let k be Nat;
assume IV: P[k];
now let j be Nat;
assume C: j = i + (k+1);
C.(i+k) c= C.(i+k+1) by asc;
hence x in C.j by C,IV;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
ex k being Nat st j = i + k by AS,NAT_1:10;
hence x in C.j by I;
end;
theorem
for X being non empty set,
C be ascending Chain of X,
i,j being Nat st i <= j holds C.i c= C.j by ch1;
definition
let R be Ring;
func Ideals R -> Subset-Family of the carrier of R equals
the set of all I where I is Ideal of R;
coherence
proof
set C = the set of all I where I is Ideal of R;
now let x be object;
assume x in C;
then ex I being Ideal of R st x = I;
hence x in bool the carrier of R;
end;
then C c= bool the carrier of R;
hence thesis;
end;
end;
registration
let R be Ring;
cluster Ideals R -> non empty;
coherence
proof
{0.R} in Ideals(R);
hence thesis;
end;
end;
theorem id2:
for R being comRing,
I being Ideal of R,
a being Element of R holds a in I implies {a}-Ideal c= I
proof
let R be comRing, I be Ideal of R, a be Element of R;
assume AS: a in I;
now let x be Element of R;
assume A: x in {a}-Ideal;
{a}-Ideal = the set of all a*r where r is Element of R by IDEAL_1:64;
then ex r being Element of R st x = a * r by A;
hence x in I by AS,IDEAL_1:def 2;
end;
hence thesis;
end;
theorem id1:
for R being Ring,
C being ascending Chain of Ideals(R)
holds union the set of all C.i where i is Nat is Ideal of R
proof
let R be Ring, F be ascending Chain of Ideals(R);
set G = the set of all F.i where i is Nat;
set T = union G;
M: F.0 in G;
F.0 in Ideals R;
then consider I being Ideal of R such that H: I = F.0;
set x = the Element of I;
L: ex Y being set st x in Y & Y in G by M,H;
now let x be object;
assume x in T; then
consider x1 being set such that H1: x in x1 & x1 in G by TARSKI:def 4;
consider i being Nat such that H2: x1 = F.i by H1;
F.i in Ideals R;
hence x in the carrier of R by H1,H2;
end;
then T c= the carrier of R;
then reconsider T as non empty Subset of R by L,TARSKI:def 4;
now let x,y be Element of R;
assume H0: x in T & y in T; then
consider x1 being set such that H1: x in x1 & x1 in G by TARSKI:def 4;
consider i being Nat such that H2: x1 = F.i by H1;
F.i in Ideals R;
then consider Ix being Ideal of R such that H5: Ix = F.i;
consider y1 being set such that H3: y in y1 & y1 in G by H0,TARSKI:def 4;
consider j being Nat such that H4: y1 = F.j by H3;
F.j in Ideals R;
then consider Iy being Ideal of R such that H6: Iy = F.j;
now per cases;
suppose i <= j;
then x in Iy by H6,H2,H1,ch1;
hence ex Y being set st x+y in Y & Y in G by H3,H4,H6,IDEAL_1:def 1;
end;
suppose j <= i;
then y in Ix by H5,H3,H4,ch1;
hence ex Y being set st x+y in Y & Y in G by H2,H1,H5,IDEAL_1:def 1;
end;
end;
hence x + y in T by TARSKI:def 4;
end;
then A: T is add-closed;
now let p,x be Element of R;
assume x in T; then
consider x1 being set such that H1: x in x1 & x1 in G by TARSKI:def 4;
consider i being Nat such that H2: x1 = F.i by H1;
F.i in Ideals R;
then consider Ix being Ideal of R such that H5: Ix = F.i;
p * x in Ix by H1,H2,H5,IDEAL_1:def 2;
hence p * x in T by H5,H2,H1,TARSKI:def 4;
end;
then B: T is left-ideal;
now let p,x be Element of R;
assume x in T; then
consider x1 being set such that H1: x in x1 & x1 in G by TARSKI:def 4;
consider i being Nat such that H2: x1 = F.i by H1;
F.i in Ideals R;
then consider Ix being Ideal of R such that H5: Ix = F.i;
x * p in Ix by H1,H2,H5,IDEAL_1:def 3;
hence x * p in T by H1,H2,H5,TARSKI:def 4;
end;
then T is right-ideal;
hence thesis by A,B;
end;
registration
let R be non empty doubleLoopStr,
S be right_zeroed non empty doubleLoopStr;
cluster R --> 0.S -> additive;
coherence
proof
set f = R --> 0.S;
let x,y be Element of R;
thus f.(x+y) = 0.S by FUNCOP_1:7
.= 0.S + 0.S by RLVECT_1:def 4
.= 0.S + f.y by FUNCOP_1:7
.= f.x + f.y by FUNCOP_1:7;
end;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
cluster R --> 0.S -> multiplicative;
coherence
proof
set f = R --> 0.S;
let x,y be Element of R;
thus f.x * f.y = f.x * 0.S by FUNCOP_1:7
.= f.(x*y) by FUNCOP_1:7;
end;
end;
registration
let R be well-unital non empty doubleLoopStr,
S be well-unital non degenerated doubleLoopStr;
cluster R --> 0.S -> non unity-preserving;
coherence by FUNCOP_1:7;
end;
registration
let R be non empty doubleLoopStr;
cluster id R -> additive multiplicative unity-preserving;
coherence;
end;
registration
let R be non empty doubleLoopStr;
cluster id R -> monomorphism epimorphism;
coherence;
end;
registration
let R be non empty doubleLoopStr,
S be right_zeroed non empty doubleLoopStr;
cluster additive for Function of R,S;
existence
proof
take R --> 0.S;
thus thesis;
end;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
cluster multiplicative for Function of R,S;
existence
proof
take R --> 0.S;
thus thesis;
end;
end;
registration
let R,S be well-unital non empty doubleLoopStr;
cluster unity-preserving for Function of R,S;
existence
proof
deffunc F(object) = 1.S;
A: for x being object st x in the carrier of R
holds F(x) in the carrier of S;
ex f being Function of R,S
st for x being object st x in the carrier of R holds f.x = F(x)
from FUNCT_2:sch 2(A);
then consider f being Function of R,S such that
H: for x being object st x in the carrier of R holds f.x = 1.S;
take f;
thus thesis by H;
end;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
cluster additive multiplicative for Function of R,S;
existence
proof
take R --> 0.S;
thus thesis;
end;
end;
begin :: Homomorphisms, Kernel and Image
definition
let R,S be Ring;
attr S is R-homomorphic means :defhom:
ex f being Function of R,S st f is RingHomomorphism;
end;
registration
let R be Ring;
cluster R-homomorphic for Ring;
existence
proof take R,id R; thus thesis; end;
end;
registration
let R be comRing;
cluster R-homomorphic for comRing;
existence
proof take R,id R; thus thesis; end;
cluster R-homomorphic for Ring;
existence
proof take R,id R; thus thesis; end;
end;
registration
let R be Field;
cluster R-homomorphic for Field;
existence
proof take R,id R; thus thesis; end;
cluster R-homomorphic for comRing;
existence
proof take R,id R; thus thesis; end;
cluster R-homomorphic for Ring;
existence
proof take R,id R; thus thesis; end;
end;
registration
let R be Ring,
S be R-homomorphic Ring;
cluster additive multiplicative unity-preserving for Function of R,S;
existence
proof
consider f being Function of R,S such that
H: f is RingHomomorphism by defhom;
take f;
thus thesis by H;
end;
end;
definition
let R be Ring,
S be R-homomorphic Ring;
mode Homomorphism of R,S is
additive multiplicative unity-preserving Function of R,S;
end;
registration
let R,S,T be Ring;
let f be unity-preserving Function of R,S;
let g be unity-preserving Function of S,T;
cluster g * f -> unity-preserving for Function of R,T;
coherence
proof
now let x,y be Element of R;
dom f = the carrier of R by FUNCT_2:def 1;
hence (g*f).(1.R) = g.(f.(1_R)) by FUNCT_1:13
.= g.(1_S) by GROUP_1:def 13
.= 1_T by GROUP_1:def 13
.= 1.T;
end;
hence thesis;
end;
end;
registration
let R be Ring,
S be R-homomorphic Ring;
cluster -> R-homomorphic for S-homomorphic Ring;
coherence
proof
let T be S-homomorphic Ring;
set f = the Homomorphism of R,S;
set g = the Homomorphism of S,T;
g*f is Homomorphism of R,T;
hence thesis;
end;
end;
notation
let R,S be non empty doubleLoopStr;
synonym R,S are_isomorphic for R is_ringisomorph_to S;
end;
theorem hom1:
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S
holds f.(0.R) = 0.S
proof
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f be additive Function of R,S;
f.(0.R) = f.(0.R + 0.R)
.= f.(0.R) + f.(0.R) by VECTSP_1:def 20;
hence thesis by RLVECT_1:9;
end;
theorem hom4a:
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S
for x being Element of R
holds f.(-x) = - f.x
proof
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S;
let x be Element of R;
0.S = f.(0.R) by hom1
.= f.(-x + x) by RLVECT_1:5
.= f.(-x) + f.x by VECTSP_1:def 20;
hence thesis by RLVECT_1:6;
end;
theorem hom4:
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S
for x,y being Element of R holds f.(x-y) = f.x - f.y
proof
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S;
let x,y being Element of R;
thus f.(x-y) = f.x + f.(-y) by VECTSP_1:def 20
.= f.x - f.y by hom4a;
end;
theorem hom2:
for R being right_unital non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable right_unital
Abelian right-distributive domRing-like non empty doubleLoopStr,
f being multiplicative Function of R,S
holds f.(1.R) = 0.S or f.(1.R) = 1.S
proof
let R be right_unital non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable Abelian
right_unital right-distributive domRing-like non empty doubleLoopStr,
f be multiplicative Function of R,S;
A: f.(1.R) = f.(1.R * 1.R)
.= f.(1.R) * f.(1.R) by GROUP_6:def 6;
B: f.(1.R) * (1.S - f.(1.R))
= f.(1.R) * 1.S + f.(1.R) * (-f.(1.R)) by VECTSP_1:def 2
.= f.(1.R) * 1.S + -(f.(1.R) * f.(1.R)) by VECTSP_1:8
.= f.(1.R) - f.(1.R) * f.(1.R)
.= 0.S by A,RLVECT_1:15;
now assume C: f.(1.R) <> 0.S;
thus f.(1.R) = f.(1.R) + 0.S
.= f.(1.R) + (1.S + -f.(1.R)) by C,B,VECTSP_2:def 1
.= (f.(1.R) + -f.(1.R)) + 1.S by RLVECT_1:def 3
.= 0.S + 1.S by RLVECT_1:5
.= 1.S;
end;
hence thesis;
end;
hom3:
for E,F being Field,
f being additive multiplicative Function of E,F
holds (f.(1.E) = 0.F & f = E --> 0.F) or
(f.(1.E) = 1.F & f is monomorphism)
proof
let E,F be Field,
f be additive multiplicative Function of E,F;
per cases by hom2;
suppose A: f.(1.E) = 0.F;
B: dom f = the carrier of E by FUNCT_2:def 1;
now let z be object;
assume z in dom f;
then reconsider x = z as Element of E;
f.x = f.(x*1.E)
.= f.x * f.(1.E) by GROUP_6:def 6
.= 0.F by A;
hence f.z = 0.F;
end;
hence thesis by B,FUNCOP_1:11;
end;
suppose A: f.(1.E) = 1.F;
then B: f is unity-preserving;
H: now let x be Element of E;
assume x <> 0.E;
then 1.F = f.(x*x") by A,VECTSP_1:def 10
.= f.x * f.(x") by GROUP_6:def 6;
hence f.x <> 0.F;
end;
now let x,y be object;
assume D: x in the carrier of E & y in the carrier of E & f.x = f.y;
then reconsider a = x, b = y as Element of E;
G: a + (b - a)
= (a + -a) + b by RLVECT_1:def 3
.= 0.E + b by RLVECT_1:5
.= b;
then E: f.b = f.b + f.(b-a) by D,VECTSP_1:def 20;
0.F = f.b + -f.b by RLVECT_1:5
.= f.(b-a) + (f.b + -f.b) by E,RLVECT_1:def 3
.= f.(b-a) + 0.F by RLVECT_1:5
.= f.(b-a);
then b = a + 0.E by G,H .= a;
hence x = y;
end;
then f is one-to-one by FUNCT_2:19;
hence thesis by B;
end;
end;
theorem
for E,F being Field,
f being additive multiplicative Function of E,F
holds f.(1.E) = 0.F iff f = E --> 0.F
proof
let E,F be Field,
f be additive multiplicative Function of E,F;
(f.(1.E) = 0.F & f = E --> 0.F) or
(f.(1.E) = 1.F & f is monomorphism) by hom3;
hence thesis;
end;
theorem hom3a:
for E,F being Field,
f being additive multiplicative Function of E,F
holds f.(1.E) = 1.F iff f is monomorphism
proof
let E,F be Field,
f be additive multiplicative Function of E,F;
(f.(1.E) = 0.F & f = E --> 0.F) or
(f.(1.E) = 1.F & f is monomorphism) by hom3;
hence thesis;
end;
registration
let E,F be Field;
cluster additive multiplicative unity-preserving -> monomorphism
for Function of E,F;
coherence by hom3a;
end;
definition
let R be Ring,
I be Ideal of R;
func canHom I -> Function of R, R/I means :defhomI:
for a being Element of R holds it.a = Class(EqRel(R,I),a);
existence
proof
set B = R/I;
defpred P[object,object] means $2 = Class(EqRel(R,I),$1);
X: for x being object st x in the carrier of R
ex y being object st y in the carrier of B & P[x,y]
proof
let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
reconsider y = Class(EqRel(R,I),a) as Element of B by RING_1:12;
take y;
thus thesis;
end;
ex g being Function of R,B
st for x being object st x in the carrier of R holds P[x,g.x]
from FUNCT_2:sch 1(X);
then consider g being Function of R,B such that
Y: for x being object st x in the carrier of R holds
g.x = Class(EqRel(R,I),x);
take g;
thus thesis by Y;
end;
uniqueness
proof
let g1,g2 be Function of R,R/I such that
A1: for a being Element of R holds g1.a = Class(EqRel(R,I),a) and
A2: for a being Element of R holds g2.a = Class(EqRel(R,I),a);
let x be Element of R;
thus g1.x = Class(EqRel(R,I),x) by A1 .= g2.x by A2;
end;
end;
registration
let R be Ring,
I be Ideal of R;
cluster canHom I -> additive multiplicative unity-preserving;
coherence
proof
set g = canHom I, B = R/I;
now let a,b be Element of R;
reconsider x = Class(EqRel(R,I),a) as Element of B by RING_1:12;
reconsider y = Class(EqRel(R,I),b) as Element of B by RING_1:12;
H1: g.a = Class(EqRel(R,I),a) by defhomI;
H: x + y = Class(EqRel(R,I),a+b) by RING_1:13;
thus g.(a+b) = x + y by H,defhomI
.= g.a + g.b by H1,defhomI;
end;
hence g is additive;
now let a,b be Element of R;
reconsider x = Class(EqRel(R,I),a) as Element of B by RING_1:12;
reconsider y = Class(EqRel(R,I),b) as Element of B by RING_1:12;
H1: g.a = Class(EqRel(R,I),a) by defhomI;
H: x * y = Class(EqRel(R,I),a*b) by RING_1:14;
thus g.(a*b) = x * y by H,defhomI
.= g.a * g.b by H1,defhomI;
end;
hence g is multiplicative;
g.(1.R) = Class(EqRel(R,I),1.R) by defhomI .= 1.B by RING_1:15;
hence g is unity-preserving;
end;
end;
registration
let R be Ring,
I be Ideal of R;
cluster canHom I -> epimorphism;
coherence
proof
set g = canHom I, B = R/I;
now let x be object;
now assume x in the carrier of B;
then consider a being Element of R such that
H1: x = Class(EqRel(R,I),a) by RING_1:11;
H2: g.a = x by H1,defhomI;
dom g = the carrier of R by FUNCT_2:def 1;
hence x in rng g by H2,FUNCT_1:def 3;
end;
hence x in rng g iff x in the carrier of B;
end;
then g is onto by FUNCT_2:def 3,TARSKI:2;
hence thesis;
end;
end;
registration
let R be Ring,
I be Ideal of R;
cluster R/I -> R-homomorphic;
coherence
proof
canHom I is Homomorphism of R,R/I;
hence thesis;
end;
end;
registration
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let f be additive Function of R,S;
cluster ker f -> non empty;
coherence
proof
f.(0.R) = 0.S by hom1;
then 0.R in ker f;
hence ker f is non empty;
end;
end;
ker1: for R,S be non empty doubleLoopStr, f be Function of R,S,
x be Element of R st x in ker f holds f.x = 0.S
proof
let R,S be non empty doubleLoopStr, f be Function of R,S, x be Element of R;
assume x in ker f;
then ex y being Element of R st y = x & f.y = 0.S;
hence thesis;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
non empty doubleLoopStr;
let f be additive Function of R,S;
cluster ker f -> add-closed;
coherence
proof
let x,y be Element of R;
assume AS: x in ker f & y in ker f;
f.(x+y) = f.x + f.y by VECTSP_1:def 20
.= 0.S + f.y by AS,ker1
.= 0.S by AS,ker1;
hence x+y in ker f;
end;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let f be multiplicative Function of R,S;
cluster ker f -> left-ideal;
coherence
proof
let a,x be Element of R;
assume AS: x in ker f;
f.(a*x) = f.a * f.x by GROUP_6:def 6
.= f.a * 0.S by AS,ker1
.= 0.S;
hence a*x in ker f;
end;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
let f be multiplicative Function of R,S;
cluster ker f -> right-ideal;
coherence
proof
let a,x be Element of R;
assume AS: x in ker f;
f.(x*a) = f.x * f.a by GROUP_6:def 6
.= 0.S * f.a by AS,ker1
.= 0.S;
hence x*a in ker f;
end;
end;
registration
let R be well-unital non empty doubleLoopStr,
S be well-unital non degenerated doubleLoopStr;
let f be unity-preserving Function of R,S;
cluster ker f -> proper;
coherence
proof
f.(1_R) = 1_S by GROUP_1:def 13 .= 1.S;
then ker f <> the carrier of R by ker1;
hence thesis by SUBSET_1:def 6;
end;
end;
theorem ker0:
for R being Ring,
S being R-homomorphic Ring,
f being Homomorphism of R,S
holds f is monomorphism iff ker f = {0.R}
proof
let R be Ring, S be R-homomorphic Ring,
f be Homomorphism of R,S;
A: now assume B: f is monomorphism;
for x be object holds x in ker f iff x = 0.R
proof
let x be object;
C: now assume AS: x in ker f;
then reconsider a = x as Element of R;
f.a = 0.S by AS,ker1 .= f.(0.R) by hom1;
hence x = 0.R by B,FUNCT_2:19;
end;
now assume AS: x = 0.R;
then reconsider a = x as Element of R;
f.a = 0.S by AS,hom1;
hence x in ker f;
end;
hence x in ker f iff x = 0.R by C;
end;
hence ker f = {0.R} by TARSKI:def 1;
end;
now assume AS: ker f = {0.R};
now let x,y be object;
assume AS1: x in the carrier of R & y in the carrier of R & f.x = f.y;
then reconsider a = x, b = y as Element of R;
0.S = f.a - f.b by AS1,RLVECT_1:15
.= f.(a-b) by hom4;
then a - b in ker f;
then 0.R = a + -b by AS,TARSKI:def 1;
then a = -(-b) by RLVECT_1:6
.= b;
hence x = y;
end;
then f is one-to-one by FUNCT_2:19;
hence f is monomorphism;
end;
hence thesis by A;
end;
theorem kercanhomI:
for R being Ring,
I being Ideal of R holds ker(canHom I) = I
proof
let R be Ring,
I be Ideal of R;
A: now let xx be object;
assume AS: xx in ker(canHom I);
then reconsider x = xx as Element of R;
Class(EqRel(R,I),0.R) = 0.(R/I) by RING_1:def 6
.= (canHom I).x by AS,ker1
.= Class(EqRel(R,I),x) by defhomI;
then x - 0.R in I by RING_1:6;
hence xx in I;
end;
now let xx be object;
assume AS: xx in I;
then reconsider x = xx as Element of R;
x - 0.R in I by AS;
then B: Class(EqRel(R,I),x) = Class(EqRel(R,I),0.R) by RING_1:6;
(canHom I).x = Class(EqRel(R,I),x) by defhomI
.= 0.(R/I) by B,RING_1:def 6;
hence xx in ker(canHom I);
end;
hence thesis by A,TARSKI:2;
end;
theorem
for R being Ring,
I being Subset of R
holds I is Ideal of R iff
ex S being R-homomorphic Ring,
f being Homomorphism of R,S st ker f = I
proof
let R be Ring,
I be Subset of R;
now assume A: I is Ideal of R;
thus ex S being R-homomorphic Ring,
f being Homomorphism of R,S
st ker f = I
proof
reconsider I as Ideal of R by A;
take R/I,canHom I;
thus thesis by kercanhomI;
end;
end;
hence thesis;
end;
T0: for R be Ring, S be R-homomorphic Ring,
f be Homomorphism of R,S holds 0.S in rng f
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
A: f.(0.R) = 0.S by hom1;
dom f = the carrier of R by FUNCT_2:def 1;
hence 0.S in rng f by A,FUNCT_1:def 3;
end;
T1: for R be Ring, S be R-homomorphic Ring,
f be Homomorphism of R,S holds 1.S in rng f
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
A: f.(1_R) = 1_S by GROUP_1:def 13 .= 1.S;
dom f = the carrier of R by FUNCT_2:def 1;
hence 1.S in rng f by A,FUNCT_1:def 3;
end;
T3: for R being Ring, S being R-homomorphic Ring,
f being Homomorphism of R,S holds rng f is Preserv of the addF of S
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
set F = rng f; set A = the addF of S;
now let x be set;
assume x in [:F,F:];
then consider a,b being object such that
A2: a in F and
A3: b in F and
A4: x = [a,b] by ZFMISC_1:def 2;
consider a1 being Element of S such that
A5: a1 = a & a1 in rng f by A2;
consider x1 being object such that
A6: x1 in dom f & f.x1 = a1 by A5,FUNCT_1:def 3;
reconsider x1 as Element of R by A6;
consider a2 being Element of S such that
A7: a2 = b & a2 in rng f by A3;
consider x2 being object such that
A8: x2 in dom f & f.x2 = a2 by A7,FUNCT_1:def 3;
reconsider x2 as Element of R by A8;
A9: dom f = the carrier of R by FUNCT_2:def 1;
f.(x1+x2) = a1 + a2 by A8,A6,VECTSP_1:def 20
.= A.x by A4,A5,A7;
hence A.x in rng f by A9,FUNCT_1:def 3;
end;
hence thesis by REALSET1:def 1;
end;
T4: for R be Ring, S be R-homomorphic Ring,
f be Homomorphism of R,S holds rng f is Preserv of the multF of S
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
set F = rng f; set A = the multF of S;
now let x be set;
assume x in [:F,F:];
then consider a,b being object such that
A2: a in F and
A3: b in F and
A4: x = [a,b] by ZFMISC_1:def 2;
consider a1 being Element of S such that
A5: a1 = a & a1 in rng f by A2;
consider x1 being object such that
A6: x1 in dom f & f.x1 = a1 by A5,FUNCT_1:def 3;
reconsider x1 as Element of R by A6;
consider a2 being Element of S such that
A7: a2 = b & a2 in rng f by A3;
consider x2 being object such that
A8: x2 in dom f & f.x2 = a2 by A7,FUNCT_1:def 3;
reconsider x2 as Element of R by A8;
A9: dom f = the carrier of R by FUNCT_2:def 1;
f.(x1*x2) = a1 * a2 by A8,A6,GROUP_6:def 6
.= A.x by A4,A5,A7;
hence A.x in rng f by A9,FUNCT_1:def 3;
end;
hence thesis by REALSET1:def 1;
end;
definition
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
func Image f -> strict doubleLoopStr means :defim:
the carrier of it = rng f &
the addF of it = (the addF of S)||(rng f) &
the multF of it = (the multF of S)||(rng f) &
the OneF of it = 1.S &
the ZeroF of it = 0.S;
existence
proof
set A = the addF of S;
set M = the multF of S;
reconsider P = rng f as Preserv of A by T3;
reconsider R = rng f as Preserv of M by T4;
reconsider O = 1.S as Element of P by T1;
reconsider Z = 0.S as Element of P by T0;
reconsider MP = M||R as BinOp of P;
take doubleLoopStr(#P,A||P,MP,O,Z#);
thus thesis;
end;
uniqueness;
end;
T5: for R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S
for a,b be Element of (Image f), x,y be Element of S
st a = x & b = y holds a + b = x + y & a * b = x * y
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
let a,b be Element of (Image f),
x,y be Element of S;
set I = Image f;
the carrier of I = rng f by defim;
then A1: [a,b] in [:rng f,rng f:] by ZFMISC_1:def 2;
assume AS: a = x & b = y;
(the addF of I).(a,b)
= ((the addF of S)||(rng f)).(a,b) by defim
.= (the addF of S).(x,y) by AS,A1,FUNCT_1:49;
hence a + b = x + y;
(the multF of I).(a,b)
= ((the multF of S)||(rng f)).(a,b) by defim
.= (the multF of S).(x,y) by AS,A1,FUNCT_1:49;
hence a * b = x * y;
end;
T6: for R be Ring, S be R-homomorphic Ring,
f be Homomorphism of R,S
for a be Element of (Image f) ex x being Element of R st f.x = a
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
let a be Element of (Image f);
the carrier of (Image f) = rng f by defim;
then ex x being object st x in dom f & f.x = a by FUNCT_1:def 3;
hence thesis;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster Image f -> non empty;
coherence
proof
0.S in rng f by T0;
hence thesis by defim;
end;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster Image f -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
set I = Image f;
now let v,w be Element of I;
consider a being Element of R such that A1: f.a = v by T6;
consider b being Element of R such that A2: f.b = w by T6;
thus v + w = f.a + f.b by A1,A2,T5
.= w + v by A1,A2,T5;
end;
hence I is Abelian;
now let u,v,w be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
consider c being Element of R such that A3: f.c = w by T6;
A4: v + w = f.b + f.c by A2,A3,T5;
u + v = f.a + f.b by A1,A2,T5;
hence (u + v) + w = (f.a + f.b) + f.c by A3,T5
.= f.a + (f.b + f.c) by RLVECT_1:def 3
.= u + (v + w) by A1,A4,T5;
end;
hence I is add-associative;
now let v be Element of I;
consider a being Element of R such that A1: f.a = v by T6;
0.I = 0.S by defim; then
v + 0.I = f.a + 0.S by A1,T5
.= f.a;
hence v + 0.I = v by A1;
end;
hence I is right_zeroed;
now let x be Element of I;
consider a being Element of R such that A1: f.a = x by T6;
consider b being Element of R such that A2: a + b = 0.R by ALGSTR_0:def 11;
dom f = the carrier of R by FUNCT_2:def 1;
then f.b in rng f by FUNCT_1:3; then
reconsider y = f.b as Element of I by defim;
0.I = 0.S by defim
.= f.(0.R) by hom1
.= f.a + f.b by A2,VECTSP_1:def 20
.= x + y by T5,A1;
hence x is right_complementable;
end;
hence I is right_complementable;
end;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster Image f -> associative well-unital distributive;
coherence
proof
set I = Image f;
now let u,v,w be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
consider c being Element of R such that A3: f.c = w by T6;
A4: v * w = f.b * f.c by A2,A3,T5;
u * v = f.a * f.b by A1,A2,T5;
hence (u * v) * w = (f.a * f.b) * f.c by A3,T5
.= f.a * (f.b * f.c) by GROUP_1:def 3
.= u * (v * w) by A1,A4,T5;
end;
hence I is associative;
now let x be Element of I;
consider a being Element of R such that A1: f.a = x by T6;
A2: 1.S = 1.I by defim;
thus x * 1.I = f.a * 1.S by A1,A2,T5
.= x by A1;
thus 1.I * x = 1.S * f.a by A1,A2,T5
.= x by A1;
end;
hence I is well-unital;
now let u,v,w be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
consider c being Element of R such that A3: f.c = w by T6;
A4: v + w = f.b + f.c by A2,A3,T5;
A5: u * v = f.a * f.b by A1,A2,T5;
A6: u * w = f.a * f.c by A1,A3,T5;
thus u * (v + w) = f.a * (f.b + f.c) by A1,A4,T5
.= f.a * f.b + f.a * f.c by VECTSP_1:def 7
.= u * v + u * w by A5,A6,T5;
A7: v * u = f.b * f.a by A1,A2,T5;
A8: w * u = f.c * f.a by A1,A3,T5;
thus (v + w) * u = (f.b + f.c) * f.a by A1,A4,T5
.= f.b * f.a + f.c * f.a by VECTSP_1:def 7
.= v * u + w * u by A7,A8,T5;
end;
hence I is distributive;
end;
end;
registration
let R be comRing,
S be R-homomorphic comRing,
f be Homomorphism of R,S;
cluster Image f -> commutative;
coherence
proof
set I = Image f;
let u,v be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
thus u * v = f.b * f.a by A1,A2,T5
.= v * u by A1,A2,T5;
end;
end;
definition
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
redefine func Image f -> strict Subring of S; :: redefines Image (RING_2, definition)
coherence
proof
set I = Image f;
A: the carrier of I = rng f by defim;
B: the addF of I = (the addF of S)||the carrier of I by A,defim;
C: the multF of I = (the multF of S)||the carrier of I by A,defim;
D: 1.I = 1.S by defim;
0.I = 0.S by defim;
hence thesis by A,B,C,D,C0SP1:def 3;
end;
end;
definition
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
func canHom f -> Function of R/(ker f), Image f means :ch:
for a being Element of R holds it.Class(EqRel(R,ker f),a) = f.a;
existence
proof
set A = R/(ker f), B = Image f;
defpred P[object,object] means
for a being Element of R
st $1 = Class(EqRel(R,ker f),a) holds $2 = f.a;
X: for x being object st x in the carrier of A
ex y being object st y in the carrier of B & P[x,y]
proof
let x be object;
assume x in the carrier of A;
then reconsider x1 = x as Element of A;
consider b being Element of R such that
X1: x1 = Class(EqRel(R,ker f),b) by RING_1:11;
take f.b;
dom f = the carrier of R by FUNCT_2:def 1;
then f.b in rng f by FUNCT_1:3;
hence f.b in the carrier of B by defim;
now let a be Element of R;
assume x = Class(EqRel(R,ker f),a);
then 0.S = f.(a-b) by ker1,X1,RING_1:6 .= f.a - f.b by hom4;
hence f.b = f.a by RLVECT_1:21;
end;
hence thesis;
end;
ex g being Function of A,B
st for x being object st x in the carrier of A holds P[x,g.x]
from FUNCT_2:sch 1(X);
then consider g being Function of A,B such that
Y: for x being object st x in the carrier of A holds
(for a being Element of R
st x = Class(EqRel(R,ker f),a) holds g.x = f.a);
take g;
now let a be Element of R;
reconsider x = Class(EqRel(R,ker f),a) as Element of A by RING_1:12;
x in the carrier of A;
hence g.Class(EqRel(R,ker f),a) = f.a by Y;
end;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of R/(ker f), Image f such that
A1: for a being Element of R holds g1.Class(EqRel(R,ker f),a) = f.a and
A2: for a being Element of R holds g2.Class(EqRel(R,ker f),a) = f.a;
A: dom g1 = the carrier of R/(ker f) by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume x in dom g1;
then reconsider x1 = x as Element of R/(ker f);
consider b being Element of R such that
B1: x1 = Class(EqRel(R,ker f),b) by RING_1:11;
thus g1.x = f.b by B1,A1 .= g2.x by B1,A2;
end;
hence thesis by A;
end;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster canHom f -> additive multiplicative unity-preserving;
coherence
proof
set g = canHom f, A = R/(ker f), B = Image f, I = ker f;
now let x,y be Element of A;
consider a being Element of R such that
H1: x = Class(EqRel(R,I),a) by RING_1:11;
consider b being Element of R such that
H2: y = Class(EqRel(R,I),b) by RING_1:11;
H3: g.x = f.a by H1,ch;
H4: g.y = f.b by H2,ch;
x + y = Class(EqRel(R,I),a+b) by H1,H2,RING_1:13;
hence g.(x+y) = f.(a+b) by ch
.= f.a + f.b by VECTSP_1:def 20
.= g.x + g.y by H3,H4,T5;
end;
hence g is additive;
now let x,y be Element of A;
consider a being Element of R such that
H1: x = Class(EqRel(R,I),a) by RING_1:11;
consider b being Element of R such that
H2: y = Class(EqRel(R,I),b) by RING_1:11;
H3: g.x = f.a by H1,ch;
H4: g.y = f.b by H2,ch;
x * y = Class(EqRel(R,I),a*b) by H1,H2,RING_1:14;
hence g.(x*y) = f.(a*b) by ch
.= f.a * f.b by GROUP_6:def 6
.= g.x * g.y by H3,H4,T5;
end;
hence g is multiplicative;
g.(1.A) = g.Class(EqRel(R,I),1.R) by RING_1:15
.= f.(1_R) by ch
.= 1_S by GROUP_1:def 13
.= 1.B by defim;
hence g is unity-preserving;
end;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster canHom f -> monomorphism epimorphism;
coherence
proof
set g = canHom f, A = R/(ker f), B = Image f, I = ker f;
now let x,y be object;
assume D: x in the carrier of A & y in the carrier of A & g.x = g.y;
then reconsider x1=x, y1=y as Element of A;
consider a being Element of R such that
H1: x1 = Class(EqRel(R,I),a) by RING_1:11;
consider b being Element of R such that
H2: y1 = Class(EqRel(R,I),b) by RING_1:11;
H3: g.x1 = f.a by H1,ch;
f.a = f.b by D,H3,H2,ch;
then 0.S = f.a - f.b by RLVECT_1:15
.= f.(a-b) by hom4;
then a - b in I;
hence x = y by H1,H2,RING_1:6;
end;
then g is one-to-one by FUNCT_2:19;
hence g is monomorphism;
now let x be object;
Y: now assume x in rng g;
then consider y being object such that
H1: y in dom g & g.y = x by FUNCT_1:def 3;
reconsider y as Element of A by H1;
consider a being Element of R such that
H2: y = Class(EqRel(R,I),a) by RING_1:11;
H3: g.y = f.a by H2,ch;
dom f = the carrier of R by FUNCT_2:def 1;
hence x in rng f by H1,H3,FUNCT_1:3;
end;
now assume x in rng f;
then consider a being object such that
H1: a in dom f & f.a = x by FUNCT_1:def 3;
reconsider a as Element of R by H1;
H2: g.Class(EqRel(R,I),a) = f.a by ch;
H3: dom g = the carrier of A by FUNCT_2:def 1;
Class(EqRel(R,I),a) is Element of A by RING_1:12;
hence x in rng g by H3,H2,H1,FUNCT_1:3;
end;
hence x in rng g iff x in rng f by Y;
end;
then rng g = rng f by TARSKI:2;
then rng g = the carrier of B by defim;
then g is onto by FUNCT_2:def 3;
hence thesis;
end;
end;
theorem
for R being Ring,
S being R-homomorphic Ring,
f being Homomorphism of R,S holds R/(ker f), Image f are_isomorphic
proof
let R be Ring,S be R-homomorphic Ring, f be Homomorphism of R,S;
canHom f is RingIsomorphism;
hence thesis;
end;
theorem
for R being Ring,
S being R-homomorphic Ring,
f being Homomorphism of R,S
holds f is onto implies R/(ker f), S are_isomorphic
proof
let R be Ring, S be R-homomorphic Ring, f be Homomorphism of R,S;
set B = R/(ker f), I = ker f, T = Image f;
assume AS: f is onto;
then A: rng f = the carrier of S by FUNCT_2:def 3;
B: rng canHom f = the carrier of Image f by FUNCT_2:def 3
.= rng f by defim;
then reconsider g = canHom f as Function of B,S by FUNCT_2:6;
C1: now let x,y be Element of B;
thus g.(x+y)
= (canHom f).x + (canHom f).y by VECTSP_1:def 20
.= ((the addF of S)||(rng f)).((canHom f).x,(canHom f).y) by defim
.= g.x + g.y by A;
end;
C2: now let x,y be Element of B;
thus g.(x*y)
= (canHom f).x * (canHom f).y by GROUP_6:def 6
.= ((the multF of S)||(rng f)).((canHom f).x,(canHom f).y) by defim
.= g.x * g.y by A;
end;
g.(1.B) = (canHom f).(1_B)
.= 1_(Image f) by GROUP_1:def 13 .= 1.S by defim; then
C: g is additive multiplicative unity-preserving by C1,C2;
rng g = the carrier of S by B,AS,FUNCT_2:def 3;
then g is onto by FUNCT_2:def 3;
hence R/(ker f), S are_isomorphic by C;
end;
theorem
for R being Ring holds R/{0.R}, R are_isomorphic
proof
let R be Ring;
id R is RingHomomorphism;
then reconsider S = R as R-homomorphic Ring by defhom;
reconsider f = id R as Homomorphism of R,S;
A: ker f = {0.R} by ker0;
set B = R/(ker f);
B: rng canHom f = the carrier of Image f by FUNCT_2:def 3
.= rng f by defim;
then reconsider g = canHom f as Function of B,S by FUNCT_2:6;
C1: now let x,y be Element of B;
thus g.(x+y)
= (canHom f).x + (canHom f).y by VECTSP_1:def 20
.= ((the addF of S)||(rng f)).((canHom f).x,(canHom f).y) by defim
.= g.x + g.y;
end;
C2: now let x,y be Element of B;
thus g.(x*y)
= (canHom f).x * (canHom f).y by GROUP_6:def 6
.= ((the multF of S)||(rng f)).((canHom f).x,(canHom f).y) by defim
.= g.x * g.y;
end;
g.(1.B) = (canHom f).(1_B)
.= 1_(Image f) by GROUP_1:def 13 .= 1.S by defim; then
C: g is additive multiplicative unity-preserving by C1,C2;
g is onto by B,FUNCT_2:def 3;
hence thesis by A,C;
end;
registration
let R be Ring;
cluster R / [#]R -> trivial;
coherence
proof
set S = R/([#]R), I = [#]R;
now let x,y be Element of S;
consider a being Element of R such that
H1: x = Class(EqRel(R,I),a) by RING_1:11;
consider b being Element of R such that
H2: y = Class(EqRel(R,I),b) by RING_1:11;
thus x = the carrier of R by H1,RING_1:7
.= y by H2,RING_1:7;
end;
hence thesis;
end;
end;
begin :: Units and Non Units
registration
let L be right_unital non empty multLoopStr;
cluster unital for Element of L;
existence
proof
1.L = 1.L * 1.L;
hence thesis by GCD_1:def 2;
end;
end;
definition
let L be right_unital non empty multLoopStr;
mode Unit of L is unital Element of L;
end;
registration
let L be add-associative right_zeroed right_complementable
left-distributive non degenerated doubleLoopStr;
cluster non unital for Element of L;
existence
proof
for x being Element of L holds (1.L <> 0.L * x) or (1.L <> x * 0.L);
hence thesis by GCD_1:def 2;
end;
end;
definition
let L be add-associative right_zeroed right_complementable
left-distributive non degenerated doubleLoopStr;
mode NonUnit of L is non unital Element of L;
end;
registration
let L be add-associative right_zeroed right_complementable
left-distributive non degenerated doubleLoopStr;
cluster 0.L -> non unital;
coherence;
end;
registration
let L be right_unital non empty multLoopStr;
cluster 1.L -> unital;
coherence
proof
1.L = 1.L * 1.L;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable
left-distributive right_unital non degenerated doubleLoopStr;
cluster -> non zero for Unit of L;
coherence;
end;
registration
let F be Field;
cluster -> unital for non zero Element of F;
coherence
proof
let a be non zero Element of F;
a <> 0.F;
then a * a" = 1.F by VECTSP_1:def 10;
then a divides 1.F;
hence a is unital;
end;
end;
registration
let R be domRing,
u,v be unital Element of R;
cluster u * v -> unital;
coherence
proof
u divides 1.R by GCD_1:def 20;
then consider a being Element of R such that
H1: u * a = 1.R;
v divides 1.R by GCD_1:def 20;
then consider b being Element of R such that
H2: v * b = 1.R;
(b * a) * (u * v) = b * (a * (u * v)) by GROUP_1:def 3
.= b * (a * u * v) by GROUP_1:def 3
.= 1.R by H2,H1;
then (u * v) divides 1.R;
hence thesis;
end;
end;
theorem div0:
for R being comRing,
a,b being Element of R
holds a divides b iff b in {a}-Ideal
proof
let R be comRing, a,b be Element of R;
A: now assume a divides b;
then consider c being Element of R such that A1: a * c = b;
b in the set of all a*r where r is Element of R by A1;
hence b in {a}-Ideal by IDEAL_1:64;
end;
now assume b in {a}-Ideal;
then b in the set of all a*r where r is Element of R by IDEAL_1:64;
then consider c being Element of R such that A1: a * c = b;
thus a divides b by A1;
end;
hence thesis by A;
end;
theorem div1:
for R being comRing,
a,b being Element of R
holds a divides b iff {b}-Ideal c= {a}-Ideal
proof
let R be comRing, a,b be Element of R;
now assume {b}-Ideal c= {a}-Ideal;
then b in {a}-Ideal by IDEAL_1:66;
hence a divides b by div0;
end;
hence thesis by div0,IDEAL_1:67;
end;
theorem div2:
for R being comRing,
a being Element of R
holds a is Unit of R iff {a}-Ideal = [#] R
proof
let R be comRing, a be Element of R;
set A = {a}-Ideal;
B:now assume a is Unit of R;
then a divides 1.R by GCD_1:def 20;
then consider c being Element of R such that
A1: a * c = 1.R;
now let x be object;
now assume x in the carrier of R;
then reconsider x1 = x as Element of R;
x = x1 * (c * a) by A1
.= a * (x1 * c) by GROUP_1:def 3;
then x in the set of all a*r where r is Element of R;
hence x in A by IDEAL_1:64;
end;
hence x in A iff x in the carrier of R;
end;
hence A = [#]R by TARSKI:2;
end;
now assume A = [#]R;
then a is unital by div0;
hence a is Unit of R;
end;
hence thesis by B;
end;
theorem div3:
for R being comRing,
a,b being Element of R
holds a is_associated_to b iff {a}-Ideal = {b}-Ideal by div1;
begin :: Prime and Irreducible Elements
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
attr x is prime means :defprim:
x <> 0.R & not x is Unit of R &
for a,b being Element of R st x divides a * b
holds (x divides a or x divides b);
attr x is irreducible means
x <> 0.R & not x is Unit of R &
for a being Element of R st a divides x
holds (a is Unit of R or a is_associated_to x);
end;
notation
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
antonym x is reducible for x is irreducible;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster non prime for Element of R;
existence
proof
take 0.R;
thus thesis;
end;
end;
lemintr: for x,y be Integer, a,b be Element of INT.Ring
st x <> 0 & x = a & y = b
holds x divides y iff a divides b
proof
let x,y be Integer, a,b be Element of INT.Ring;
assume AS: x <> 0 & x = a & y = b;
now assume x divides y;
then consider z being Integer such that
H: x * z = y by INT_1:def 3;
reconsider c = z as Element of INT.Ring by INT_1:def 2,INT_3:def 3;
a * c = b by H,AS;
hence a divides b;
end;
hence thesis by AS,INT_1:def 3;
end;
registration
cluster prime for Element of INT.Ring;
existence
proof
set R = INT.Ring;
set t = 1.R + 1.R;
reconsider x = t as Integer;
A: t <> 0.R by INT_3:def 3;
T: not 2 divides 1 by INT_2:13;
not t divides 1.R by T,INT_3:def 3,lemintr;
then B: not t is Unit of R by GCD_1:def 20;
now let a,b be Element of R;
assume C1: t divides a * b;
reconsider y=a, z=b as Integer;
set g = x gcd y;
C2: 2 divides (y * z) by C1,INT_3:def 3,lemintr;
2 divides y or 2 divides z by C2,INT_5:7,INT_2:28;
hence (t divides a or t divides b) by INT_3:def 3,lemintr;
end;
hence thesis by A,B,defprim;
end;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster prime -> non zero non unital for Element of R;
coherence;
cluster irreducible -> non zero non unital for Element of R;
coherence;
end;
registration
let R be domRing;
cluster prime -> irreducible for Element of R;
coherence
proof
let x be Element of R;
assume A: x is prime;
now let a be Element of R;
assume C: a divides x;
then consider b being Element of R such that
D: a * b = x;
b <> 0.R by A,D;
then H: b is right_mult-cancelable by ALGSTR_0:def 37;
now per cases by A,D;
case x divides a;
hence a is_associated_to x by C;
end;
case x divides b;
then consider c being Element of R such that
F: x * c = b;
(a* c) * b = x * c by D,GROUP_1:def 3
.= 1.R * b by F;
then a divides 1.R by H;
hence a is Unit of R by GCD_1:def 20;
end;
end;
hence a is Unit of R or a is_associated_to x;
end;
hence thesis by A;
end;
end;
registration
let F be Field;
cluster -> reducible for Element of F;
coherence;
end;
definition
let R be right_unital non empty doubleLoopStr;
func IRR R -> Subset of R equals
{ x where x is Element of R : x is irreducible };
coherence
proof
set C = { x where x is Element of R : x is irreducible };
now let y be object;
assume y in C;
then ex a being Element of R st a = y & a is irreducible;
hence y in the carrier of R;
end;
then C c= the carrier of R;
hence thesis;
end;
end;
registration
let F be Field;
cluster IRR F -> empty;
coherence
proof
set y = the Element of IRR F;
assume IRR F is non empty;
then y in IRR F;
then ex a being Element of F st a = y & a is irreducible;
hence contradiction;
end;
end;
theorem ass0:
for R being domRing,
c being non zero Element of R
for b,a,d being Element of R
st a * b is_associated_to c * d & a is_associated_to c
holds b is_associated_to d
proof
let R be domRing,
c be non zero Element of R, b,a,d be Element of R;
assume AS: a * b is_associated_to c * d & a is_associated_to c;
H0: c <> 0.R;
consider u being Element of R such that
H1: u is unital & a * b * u = c * d by AS,GCD_1:18;
consider v being Element of R such that
H2: v is unital & c * v = a by AS,GCD_1:18;
H3: c * (v * b * u) = c * (v * (b * u)) by GROUP_1:def 3
.= (c * v) * (b * u) by GROUP_1:def 3
.= c * d by H1,H2,GROUP_1:def 3;
c is right_mult-cancelable by H0,ALGSTR_0:def 37;
then d = v * b * u by H3 .= (u * v) * b by GROUP_1:def 3;
hence thesis by H1,H2,GCD_1:18;
end;
theorem ass1:
for R being domRing,
a,b being Element of R
st a is irreducible & b is_associated_to a holds b is irreducible
proof
let R be domRing, a,b be Element of R;
assume AS: a is irreducible & b is_associated_to a;
then consider x being Element of R such that
H: x is unital & b * x = a by GCD_1:18;
now let c being Element of R;
assume c divides b;
then c is Unit of R or c is_associated_to a by GCD_1:2,AS;
hence c is Unit of R or c is_associated_to b by AS,GCD_1:4;
end;
hence thesis by AS,H;
end;
theorem thpr:
for R being non degenerated comRing,
a being non zero Element of R
holds a is prime iff {a}-Ideal is prime
proof
let R be non degenerated comRing, a be non zero Element of R;
set S = {a}-Ideal;
A: now assume A0: a is prime;
now let x,y be Element of R;
assume A2: x * y in S;
now per cases by A2,A0,div0;
case a divides x;
hence x in S by div0; end;
case a divides y;
hence y in S by div0; end;
end;
hence x in S or y in S;
end;
then B: S is quasi-prime by RING_1:def 1;
now assume S is non proper;
then S = the carrier of R by SUBSET_1:def 6;
then a is unital by div0;
hence contradiction by A0;
end;
hence S is prime by B;
end;
now assume A0: S is prime;
B: now let x,y being Element of R;
assume a divides x * y;
then x in S or y in S by div0,A0,RING_1:def 1;
hence a divides x or a divides y by div0;
end;
now assume a is unital;
then {1.R}-Ideal c= S by div0,IDEAL_1:67;
then the carrier of R c= S by IDEAL_1:51;
hence contradiction by A0,SUBSET_1:def 6,XBOOLE_0:def 10;
end;
hence a is prime by B;
end;
hence thesis by A;
end;
theorem maxirr:
for R being non degenerated comRing,
a being non zero Element of R
holds {a}-Ideal is maximal implies a is irreducible
proof
let R be non degenerated comRing,
a be non zero Element of R;
set S = {a}-Ideal;
assume AS: S is maximal;
B: now let x be Element of R;
assume B1: x divides a;
now per cases by div1,B1,AS,RING_1:def 3;
case S = {x}-Ideal;
hence x is_associated_to a by div1;
end;
case {x}-Ideal is non proper;
then {x}-Ideal = the carrier of R by SUBSET_1:def 6;
then x is unital by div0;
hence x is Unit of R;
end;
end;
hence x is Unit of R or x is_associated_to a;
end;
now assume a is unital;
then {1.R}-Ideal c= S by div0,IDEAL_1:67;
then the carrier of R c= S by IDEAL_1:51;
hence contradiction by AS,SUBSET_1:def 6,XBOOLE_0:def 10;
end;
hence thesis by B;
end;
begin :: Principal Ideal Domains and Factorial Rings
registration
cluster -> PID for Field;
coherence
proof
let F be Field;
let I be Ideal of F;
per cases by IDEAL_1:22;
suppose I = {0.F};
then I = {0.F}-Ideal by IDEAL_1:47;
hence thesis;
end;
suppose I = the carrier of F;
then I = {1.F}-Ideal by IDEAL_1:51;
hence thesis;
end;
end;
end;
registration
cluster PID for non empty doubleLoopStr;
existence
proof
take the Field;
thus thesis;
end;
end;
definition
mode PIDomain is PID domRing;
end;
theorem maxirr2:
for R being PIDomain,
a being non zero Element of R
holds {a}-Ideal is maximal iff a is irreducible
proof
let R be PIDomain, a be non zero Element of R;
set S = {a}-Ideal;
now assume AS: a is irreducible;
now let J be Ideal of R;
assume H0: S c= J;
J is principal by IDEAL_1:def 28;
then consider b being Element of R such that
H1: J = {b}-Ideal;
now per cases by AS,H0,H1,div1;
case b is Unit of R;
then J = [#] R by H1,div2;
hence J is non proper;
end;
case b is_associated_to a;
hence S = J by H1,div1;
end;
end;
hence J = S or J is non proper;
end;
then B: S is quasi-maximal by RING_1:def 3;
now assume S is non proper;
then S = the carrier of R by SUBSET_1:def 6;
then a is unital by div0;
hence contradiction by AS;
end;
hence S is maximal by B;
end;
hence thesis by maxirr;
end;
registration
let R be PIDomain;
cluster irreducible -> prime for Element of R;
coherence
proof
let a be Element of R;
assume AS: a is irreducible;
then {a}-Ideal is maximal by maxirr2;
hence a is prime by AS,thpr;
end;
end;
registration
cluster Euclidian -> PID for comRing;
coherence by IDEAL_1:94;
end;
registration
let R be PIDomain;
cluster ascending -> stagnating for Chain of Ideals(R);
coherence
proof
let F be Chain of Ideals(R);
set G = the set of all F.i where i is Nat;
assume AS: F is ascending; then
reconsider I = union G as Ideal of R by id1;
I is principal by IDEAL_1:def 28;
then consider a being Element of R such that
H0: I = {a}-Ideal;
a in I by H0,IDEAL_1:66; then
consider x1 being set such that H1: a in x1 & x1 in G by TARSKI:def 4;
consider i being Nat such that H2: x1 = F.i by H1;
F.i in Ideals R;
then consider Fi being Ideal of R such that H3: Fi = F.i;
Fi c= I by H1,H2,H3,TARSKI:def 4;
then B4: Fi = I by H0,H1,H2,H3,id2;
now let j be Nat;
F.j in Ideals R;
then consider Fj being Ideal of R such that H: Fj = F.j;
B5: F.j in G;
assume X: j >= i;
Fj c= I by H,B5,TARSKI:def 4;
hence F.j = F.i by B4,H,H3,H0,id2,H1,H2,ch1,AS,X;
end;
hence thesis;
end;
end;
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
let F be non empty FinSequence of R;
pred F is_a_factorization_of x means
x = Product F &
for i being Element of dom F holds F.i is irreducible;
end;
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
attr x is factorizable means
ex F being non empty FinSequence of R st F is_a_factorization_of x;
end;
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
assume AS:x is factorizable;
mode Factorization of x -> non empty FinSequence of R means :ddf:
it is_a_factorization_of x;
existence by AS;
end;
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
attr x is uniquely_factorizable means
x is factorizable &
for F,G being Factorization of x
ex B being Function of dom F, dom G
st B is bijective &
for i being Element of dom F holds G.(B.i) is_associated_to F.i;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster uniquely_factorizable -> factorizable for Element of R;
coherence;
end;
registration
let R be domRing;
cluster factorizable -> non zero non unital for Element of R;
coherence
proof
let a be Element of R;
assume a is factorizable;
then consider F being non empty FinSequence of R such that
AS: F is_a_factorization_of a;
now assume a is zero;
then consider i being Nat such that
A: i in dom F & F.i = 0.R by AS,prod5;
0.R is irreducible by A,AS;
hence contradiction;
end;
hence a is non zero;
rng F c= the carrier of R; then
reconsider f = F as Function of dom F,R by FUNCT_2:2;
now assume A1: a is unital;
consider q being FinSequence, x being object such that
A2: F = q^<*x*> by FINSEQ_1:46;
reconsider q as FinSequence of R by A2,FINSEQ_1:36;
rng<*x*> = {x} by FINSEQ_1:39;
then A5: x in rng<*x*> by TARSKI:def 1;
A6: rng<*x*> c= rng F by A2,FINSEQ_1:30;
then x in rng F by A5;
then reconsider x as Element of R;
a = (Product q) * x by GROUP_4:6,A2,AS;
then x divides a;
then A3: x is unital by A1,GCD_1:2;
consider i being Nat such that
A7: i in dom F & F.i = x by A5,A6,FINSEQ_2:10;
x is irreducible by AS,A7;
hence contradiction by A3;
end;
hence thesis;
end;
end;
fact1:
for R being right_unital non empty doubleLoopStr,
a being Element of R
holds a is irreducible iff <*a*> is_a_factorization_of a
proof
let R be right_unital non empty doubleLoopStr,
a be Element of R;
rng<*a*> c= the carrier of R; then
reconsider f = <*a*> as Function of dom <*a*>,R by FUNCT_2:2;
A: now assume AS: a is irreducible;
now let i be Element of dom <*a*>;
i in dom <*a*>;
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1,FINSEQ_1:2;
hence <*a*>.i is irreducible by AS;
end;
hence <*a*> is_a_factorization_of a by GROUP_4:9;
end;
now assume AS: <*a*> is_a_factorization_of a;
dom <*a*> = {1} by FINSEQ_1:2,FINSEQ_1:38;
then reconsider e = 1 as Element of dom<*a*> by TARSKI:def 1;
f.e = a;
hence a is irreducible by AS;
end;
hence thesis by A;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster irreducible -> factorizable for Element of R;
coherence
proof
let a be Element of R; assume a is irreducible;
then <*a*> is_a_factorization_of a by fact1;
hence thesis;
end;
end;
theorem
for R being right_unital non empty doubleLoopStr,
a being Element of R
holds a is irreducible iff <*a*> is_a_factorization_of a by fact1;
theorem fact2:
for R being well-unital associative non empty doubleLoopStr,
a,b being Element of R,
F,G being non empty FinSequence of R
st F is_a_factorization_of a & G is_a_factorization_of b
holds F^G is_a_factorization_of a * b
proof
let R be well-unital associative non empty doubleLoopStr,
a,b be Element of R,
F,G be non empty FinSequence of R;
assume AS: F is_a_factorization_of a & G is_a_factorization_of b;
reconsider FG = F^G as non empty FinSequence of R;
rng F c= the carrier of R; then
reconsider f = F as Function of dom F,R by FUNCT_2:2;
rng G c= the carrier of R; then
reconsider g = G as Function of dom G,R by FUNCT_2:2;
rng FG c= the carrier of R; then
reconsider fg = FG as Function of dom FG,R by FUNCT_2:2;
now let i be Element of dom(F^G);
now per cases by FINSEQ_1:25;
suppose B: i in dom F;
fg.i = f.i by B,FINSEQ_1:def 7;
hence (F^G).i is irreducible by B,AS;
end;
suppose ex n being Nat st n in dom G & i = len F + n;
then consider n being Nat such that B: n in dom G & i = len F + n;
fg.i = g.n by B,FINSEQ_1:def 7;
hence (F^G).i is irreducible by B,AS;
end;
end;
hence (F^G).i is irreducible;
end;
hence thesis by AS,GROUP_4:5;
end;
lemfactunique1:
for R be domRing,
a,b,x being Element of R,
F being non empty FinSequence of R
st x is prime & x divides a &
a is_associated_to b & F is_a_factorization_of b
holds ex i being Element of dom F st F.i is_associated_to x
proof
let R be domRing,
a,b,x be Element of R,
F be non empty FinSequence of R;
assume AS: x is prime & x divides a &
a is_associated_to b & F is_a_factorization_of b;
defpred P[Nat] means
for F being non empty FinSequence of R, a,b be Element of R
st len F = $1 & x divides a &
a is_associated_to b & F is_a_factorization_of b
holds ex i being Element of dom F st F.i is_associated_to x;
A0: P[0];
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume IV: P[k];
now let F be non empty FinSequence of R, a,b be Element of R;
assume A3: len F = k+1 & x divides a &
a is_associated_to b & F is_a_factorization_of b;
consider q being FinSequence, y being object such that
B2: F = q^<*y*> by FINSEQ_1:46;
B2a: rng q c= rng F by B2,FINSEQ_1:29;
rng F c= the carrier of R;
then rng q c= the carrier of R by B2a;then
reconsider q as FinSequence of R by FINSEQ_1:def 4;
rng<*y*> = {y} by FINSEQ_1:39;
then B5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng F by B2,FINSEQ_1:30;
then y in rng F by B5;
then reconsider y as Element of R;
A4: len F = len q + len<*y*> by B2,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:39;
A5: b = (Product q) * y by GROUP_4:6,B2,A3;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then A6: F.(k+1) = <*y*>.1 by B2,A4,A3,FINSEQ_1:def 7
.= y;
dom F = Seg(k+1) by A3,FINSEQ_1:def 3;
then A8: k+1 in dom F by FINSEQ_1:4;
then A7: y is irreducible by A6,A3;
consider d being Element of R such that
Z: d is unital & a * d = b by A3,GCD_1:18;
A9: x divides b by Z,A3,GCD_1:7;
per cases by A5,A9,AS;
suppose x divides y;
then x is_associated_to y by AS,A7;
hence ex i being Element of dom F st F.i is_associated_to x
by A8,A6;
end;
suppose C0: x divides (Product q);
now per cases;
suppose q = {};
then b = Product<*y*> by A3,B2,FINSEQ_1:34 .= y by GROUP_4:9;
then x is_associated_to y by AS,A7,Z,A3,GCD_1:7;
hence ex i being Element of dom F st F.i is_associated_to x
by A6,A8;
end;
suppose q <> {};
then reconsider q as non empty FinSequence of R;
now let i be Element of dom q;
dom q c= dom F by B2,FINSEQ_1:26;
then reconsider j = i as Element of dom F;
F.j is irreducible by A3;
hence q.i is irreducible by B2,FINSEQ_1:def 7;
end;
then q is_a_factorization_of (Product q);
then consider i being Element of dom q such that
C1: q.i is_associated_to x by IV,C0,A3,A4;
C3: F.i = q.i by B2,FINSEQ_1:def 7;
dom q c= dom F by B2,FINSEQ_1:26;
then i in dom F;
hence ex i being Element of dom F st F.i is_associated_to x
by C1,C3;
end;
end;
hence ex i being Element of dom F st F.i is_associated_to x;
end;
end;
hence thesis;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A0,A1);
ex n being Nat st len F = n;
hence thesis by I,AS;
end;
lemfactunique:
for R be PIDomain,
x,y being Element of R
for F,G being non empty FinSequence of R
st F is_a_factorization_of x & G is_a_factorization_of y &
x is_associated_to y
ex p being Function of dom F,dom G
st p is bijective &
for i being Element of dom F holds G.(p.i) is_associated_to F.i
proof
let R be PIDomain,
x,y being Element of R;
let F,G being non empty FinSequence of R;
assume AS: F is_a_factorization_of x & G is_a_factorization_of y &
x is_associated_to y;
defpred P[Nat] means
for x,y being Element of R
for F,G being non empty FinSequence of R
st len F = $1 & F is_a_factorization_of x & G is_a_factorization_of y &
x is_associated_to y
holds len G = $1 &
ex p being Function of dom F,dom G
st p is bijective &
for i being Element of dom F holds G.(p.i) is_associated_to F.i;
A0: P[0];
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume IV: P[k];
now let x,y being Element of R;
let F,G being non empty FinSequence of R;
assume A3: len F = k+1 & F is_a_factorization_of x &
G is_a_factorization_of y & x is_associated_to y;
consider F1 being FinSequence, a being object such that
B2: F = F1^<*a*> by FINSEQ_1:46;
B2a: rng F1 c= rng F by B2,FINSEQ_1:29;
rng F c= the carrier of R;
then rng F1 c= the carrier of R by B2a;then
reconsider F1 as FinSequence of R by FINSEQ_1:def 4;
rng<*a*> = {a} by FINSEQ_1:39;
then B5: a in rng<*a*> by TARSKI:def 1;
rng<*a*> c= rng F by B2,FINSEQ_1:30;
then a in rng F by B5;
then reconsider a as Element of R;
A4: len F = len F1 + len<*a*> by B2,FINSEQ_1:22
.= len F1 + 1 by FINSEQ_1:39;
dom<*a*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*a*> by TARSKI:def 1;
then A6: F.(k+1) = <*a*>.1 by B2,A4,A3,FINSEQ_1:def 7
.= a;
dom F = Seg(k+1) by A3,FINSEQ_1:def 3;
then A7: k+1 in dom F by FINSEQ_1:4;
then A7a: a is irreducible by A6,A3;
A10: Product F = (Product F1) * a by B2,GROUP_4:6;
consider r being FinSequence, b being object such that
G2: G = r^<*b*> by FINSEQ_1:46;
G2a: rng r c= rng G by G2,FINSEQ_1:29;
rng G c= the carrier of R;
then rng r c= the carrier of R by G2a;then
reconsider r as FinSequence of R by FINSEQ_1:def 4;
rng<*b*> = {b} by FINSEQ_1:39;
then G5: b in rng<*b*> by TARSKI:def 1;
rng<*b*> c= rng G by G2,FINSEQ_1:30;
then b in rng G by G5;
then reconsider b as Element of R;
dom<*b*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*b*> by TARSKI:def 1;
then G6: G.((len r)+1) = <*b*>.1 by G2,FINSEQ_1:def 7
.= b;
G12: len G = len r + len<*b*> by G2,FINSEQ_1:22
.= len r + 1 by FINSEQ_1:39;
then dom G = Seg((len r) + 1) by FINSEQ_1:def 3;
then (len r) + 1 in dom G by FINSEQ_1:4;
then G7: b is irreducible by G6,A3;
then G11: b is right_mult-cancelable by ALGSTR_0:def 37;
G9: Product G = (Product r) * b by G2,GROUP_4:6;
then G10: b divides y by A3;
per cases;
suppose F1 = {};
then C1: F = <*a*> by B2,FINSEQ_1:34;
then C2: len F = 1 by FINSEQ_1:40;
C5: x = a by A3,C1,GROUP_4:9;
then D1: y is irreducible by A3,A7,A6,ass1;
C3: now assume len G <> len F;
then reconsider r as non empty FinSequence of R
by G12,C1,FINSEQ_1:40;
consider u being Element of R such that
C4: u is unital & b * u = y by D1,G7,G10,GCD_1:18;
Product r is factorizable
proof
take r;
thus Product r = Product r;
let i be Element of dom r;
dom r c= dom G by G2,FINSEQ_1:26;
then reconsider j = i as Element of dom G;
G.j is irreducible by A3;
hence thesis by G2,FINSEQ_1:def 7;
end;
hence contradiction by A3,G9,C4,G11;
end;
then C7: G = <*G.1*> by C2,FINSEQ_1:40;
then C4: dom G = Seg 1 & dom F = Seg 1 by FINSEQ_1:38,C1;
then reconsider p = id(dom F) as Function of dom F,dom G;
now let i be Element of dom F;
E0: i = 1 by C4,TARSKI:def 1,FINSEQ_1:2;
then F.i = a by C1;
hence G.(p.i) is_associated_to F.i by E0,A3,C5,C7,GROUP_4:9;
end;
hence len G = k+1 & ex p being Function of dom F,dom G
st p is bijective & for i being Element of dom F
holds G.(p.i) is_associated_to F.i by A3,C4,C3;
end;
suppose F1 <> {};
then reconsider F1 as non empty FinSequence of R;
a divides Product F by A10;
then consider j being Element of dom G such that
E1: G.j is_associated_to a by lemfactunique1,A3,A7a;
rng G c= the carrier of R; then
reconsider g = G as Function of dom G,R by FUNCT_2:2;
E3: g.j = g/.j;
set G1 = Del(G,j);
consider lg1 being Nat such that
LG1: len G = lg1 + 1 & len G1 = lg1 by FINSEQ_3:104;
LG3: dom G = Seg(lg1+1) & dom G1 = Seg lg1 by LG1,FINSEQ_1:def 3; then
LG2: dom G1 c= dom G by NAT_1:11,FINSEQ_1:5;
Product G = G.j * (Product G1) by E3,RATFUNC1:3; then
a*(Product F1) is_associated_to G.j*(Product G1) by A3,B2,GROUP_4:6;
then I0: (Product F1) is_associated_to (Product G1) by A7a,E1,ass0;
now let i be Element of dom F1;
dom F1 c= dom F by B2,FINSEQ_1:26;
then reconsider j = i as Element of dom F;
F.j is irreducible by A3;
hence F1.i is irreducible by B2,FINSEQ_1:def 7;
end;
then I1: F1 is_a_factorization_of (Product F1);
now assume G1 = {};
then G1 = <*>(the carrier of R);
then Product F1 is_associated_to 1_R by I0,GROUP_4:8;
then Product F1 is unital factorizable by I1;
hence contradiction;
end;
then reconsider G1 as non empty FinSequence of R;
now let i be Element of dom G1;
i in dom G1;
then i in Seg lg1 by LG1,FINSEQ_1:def 3;
then H1: 1 <= i & i <= lg1 by FINSEQ_1:1;
per cases;
suppose G: i < j;
lg1 <= lg1 + 1 by NAT_1:11;
then i <= lg1+1 by H1,XXREAL_0:2;
then i in Seg(lg1+1) by H1;
then reconsider ii = i as Element of dom G by LG1,FINSEQ_1:def 3;
G.ii is irreducible by A3;
hence G1.i is irreducible by G,FINSEQ_3:110;
end;
suppose K: j <= i;
1 <= i+1 & i+1 <= lg1 + 1 by H1,XREAL_1:6,NAT_1:11;
then i+1 in Seg(lg1+1);
then reconsider ii = i+1 as Element of dom G by LG1,FINSEQ_1:def 3;
G.ii is irreducible by A3;
hence G1.i is irreducible by K,H1,LG1,FINSEQ_3:111;
end;
end;
then I2: G1 is_a_factorization_of (Product G1);
II: len G1 = k &
ex p being Function of dom F1,dom G1
st p is bijective &
for i being Element of dom F1 holds G1.(p.i) is_associated_to F1.i
by IV,A4,A3,I0,I1,I2;
thus III: len G = k+1 by IV,A4,A3,I0,I1,I2,LG1;
consider p being Function of dom F1,dom G1 such that
P0: p is bijective & for i being Element of dom F1
holds G1.(p.i) is_associated_to F1.i by IV,A4,A3,I0,I1,I2;
R0: p is one-to-one onto by P0;
R1: rng p = dom G1 by P0,FUNCT_2:def 3;
defpred Q[Nat,Nat] means
($2 = p.$1 & p.$1 < j & $1 <> k+1) or
($2 = (p.$1) + 1 & p.$1 >= j & $1 <> k+1) or
($2 = j & $1 = k+1);
P1: for x being Element of dom F ex y being Element of dom G st Q[x,y]
proof
let x be Element of dom F;
dom F = Seg(k+1) by A3,FINSEQ_1:def 3;
then Q0: 1 <= x & x <= k+1 by FINSEQ_1:1;
per cases;
suppose Q1: x = k+1;
take j; thus thesis by Q1;
end;
suppose Q1: x <> k+1;
then x < k+1 by Q0,XXREAL_0:1;
then x <= k by NAT_1:13;
then Q2: x in Seg k by Q0;
dom F1 = Seg k by A3,A4,FINSEQ_1:def 3;
then Q: p.x in dom G1 by Q2,R1,FUNCT_2:4;
then 1 <= p.x & p.x <= k by III,LG1,LG3,FINSEQ_1:1;
then 1 <= p.x + 1 & p.x + 1 <= k + 1 by NAT_1:11,XREAL_1:6;
then R: p.x + 1 in Seg(k+1);
now per cases;
suppose Q3: p.x < j;
reconsider px = p.x as Element of dom G by Q,LG2;
take px; (px = p.x & p.x < j & x <> k+1) by Q1,Q3;
hence thesis;
end;
suppose Q3: p.x >= j;
reconsider px1 = p.x + 1 as Element of dom G
by III,R,FINSEQ_1:def 3;
take px1; px1 = p.x + 1 & p.x >= j & x <> k+1 by Q1,Q3;
hence thesis;
end;
end;
hence thesis;
end;
end;
consider B being Function of dom F, dom G such that
P2: for x being Element of dom F holds Q[x,B.x]
from FUNCT_2:sch 3(P1);
take B;
now let x1,x2 be object;
assume S0: x1 in dom F & x2 in dom F & B.x1 = B.x2;
then reconsider x = x1, y = x2 as Element of dom F;
S1: dom F = Seg(k+1) by A3,FINSEQ_1:def 3; then
S2: 1 <= x & x <= k+1 by FINSEQ_1:1;
S3: 1 <= y & y <= k+1 by S1,FINSEQ_1:1;
per cases;
suppose S4: x = k+1;
then S5: j = B.y by S0,P2;
now assume S6: y <> k+1;
per cases;
suppose p.y < j;
hence contradiction by S5,S6,P2;
end;
suppose S7: p.y >= j;
then S9: (p.y) + 1 = B.y by S6,P2 .= j by S4,S0,P2;
consider k being Nat such that S8: p.y = j + k by S7,NAT_1:10;
p.y = j - 1 by S9;
hence contradiction by S8;
end;
end;
hence x1 = x2 by S4;
end;
suppose Q1: x <> k+1;
then x < k+1 by S2,XXREAL_0:1;
then x <= k by NAT_1:13;
then Q2: x in Seg k by S2;
Q4: x in dom F1 by Q2,A3,A4,FINSEQ_1:def 3;
Q8: now assume R0: y = k + 1;
then R1: j = B.x by P2,S0;
B.x <> j
proof
per cases;
suppose p.x < j;
hence thesis by Q1,P2;
end;
suppose Q9: p.x >= j;
then S9: (p.x) + 1 = j by R1,Q1,P2;
consider k being Nat such that
S8: p.x = j + k by Q9,NAT_1:10;
p.x = j - 1 by S9;
hence thesis by S8;
end;
end;
hence contradiction by R0,S0,P2;
end;
then y < k+1 by S3,XXREAL_0:1;
then y <= k by NAT_1:13;
then Q7: y in Seg k by S3;
dom F1 = Seg k by A3,A4,FINSEQ_1:def 3;
then Q5: y in dom p by Q7,FUNCT_2:def 1;
Q6: x in dom p by Q4,FUNCT_2:def 1;
now per cases;
suppose Q3: p.x < j;
then U1: p.x = B.y by S0,Q1,P2;
now assume U2: p.y >= j;
then (p.y) + 1 = p.x by U1,Q8,P2;
then (p.y) + 1 < p.y by Q3,U2,XXREAL_0:2;
hence contradiction by NAT_1:11;
end;
hence p.x = p.y by U1,Q8,P2;
end;
suppose Q3: p.x >= j;
then U1: (p.x) + 1 = B.y by S0,Q1,P2;
now assume U2: p.y < j;
then p.y = (p.x) + 1 by U1,Q8,P2;
then (p.x) + 1 < p.x by U2,Q3,XXREAL_0:2;
hence contradiction by NAT_1:11;
end;
then (p.y) + 1 = B.y by Q8,P2;
hence p.x = p.y by U1;
end;
end;
hence x1 = x2 by Q6,Q5,R0;
end;
end;
then T: B is one-to-one by FUNCT_2:19;
now let x be object;
now assume U0: x in dom G; then
U1: x in Seg(k+1) by III,FINSEQ_1:def 3;
U2: dom F = Seg(k+1) by A3,FINSEQ_1:def 3;
then U2a: dom F = dom G by III,FINSEQ_1:def 3;
reconsider x1=x as Element of dom F by U2,U0,III,FINSEQ_1:def 3;
U3: 1 <= x1 & x1 <= k+1 by U1,FINSEQ_1:1;
U8: dom B = dom F by FUNCT_2:def 1;
dom p = dom F1 by FUNCT_2:def 1; then
Q3: dom p = Seg k by A3,A4,FINSEQ_1:def 3
.= dom G1 by II,FINSEQ_1:def 3;
Q4: Seg k = dom G1 by II,FINSEQ_1:def 3;
per cases;
suppose U7: x1 = j;
U5: k + 1 in dom B by U8,U2,FINSEQ_1:4;
then x1 = B.(k+1) by U7,P2;
hence x in rng B by U5,FUNCT_1:def 3;
end;
suppose Q1: x1 <> j;
now per cases;
suppose QQ: x1 <= j;
then QQQ: x1 < j by Q1,XXREAL_0:1;
j <= k+1 by U2,FINSEQ_1:1,U2a;
then x1 < k + 1 by QQQ,XXREAL_0:2;
then x1 <= k by NAT_1:13;
then x1 in rng p by U3,Q4,R1;
then consider i being object such that
M: i in dom p & p.i = x1 by FUNCT_1:def 3;
reconsider i as Element of dom p by M;
i in dom G1 by Q3;
then i in Seg k by II,FINSEQ_1:def 3;
then H: 1 <= i & i <= k by FINSEQ_1:1;
N: p.i < j by M,QQ,Q1,XXREAL_0:1;
k <= k + 1 by NAT_1:11; then
i <= k + 1 by H,XXREAL_0:2; then
i in Seg(k+1) by H; then
reconsider i as Element of dom F by A3,FINSEQ_1:def 3;
i <> k+1 by H,NAT_1:19;
then B.i = x1 by M,N,P2;
hence x in rng B by U8,FUNCT_1:def 3;
end;
suppose QQ: x1 > j;
QQ1: 1 <= j & j <= k+1 by U2,FINSEQ_1:1,U2a;
QQ2: x1-1 <= (k + 1) -1 by U3,XREAL_1:9;
1 < x1 by QQ,QQ1,XXREAL_0:2; then
1 + 1 <= x1 by INT_1:7; then
(1+1)-1 <= x1-1 by XREAL_1:9;
then x1-1 in rng p by QQ2,Q4,R1,QQ;
then consider i being object such that
M: i in dom p & p.i = x1-1 by FUNCT_1:def 3;
reconsider i as Element of dom p by M;
i in dom G1 by Q3;
then i in Seg k by II,FINSEQ_1:def 3;
then H: 1 <= i & i <= k by FINSEQ_1:1;
j + 1 <= x1 by QQ,INT_1:7; then
N: (j+1)-1 <= x1-1 by XREAL_1:9;
k <= k + 1 by NAT_1:11; then
i <= k + 1 by H,XXREAL_0:2; then
i in Seg(k+1) by H; then
reconsider i as Element of dom F by A3,FINSEQ_1:def 3;
i <> k+1 by H,NAT_1:19;
then B.i = (p.i) + 1 by M,N,P2 .= x1 by M;
hence x in rng B by U8,FUNCT_1:def 3;
end;
end;
hence x in rng B;
end;
end;
hence x in dom G iff x in rng B;
end;
then B is onto by TARSKI:2,FUNCT_2:def 3;
hence B is bijective by T;
thus for i being Element of dom F holds G.(B.i) is_associated_to F.i
proof
let i be Element of dom F;
dom F = Seg(k+1) by A3,FINSEQ_1:def 3;
then Q0: 1 <= i & i <= k+1 by FINSEQ_1:1;
per cases;
suppose i = k+1;
hence thesis by P2,A6,E1;
end;
suppose Q1: i <> k+1;
then i < k+1 by Q0,XXREAL_0:1;
then i <= k by NAT_1:13;
then Q2: i in Seg k by Q0;
i in dom F1 by Q2,A3,A4,FINSEQ_1:def 3;
then p.i in dom G1 by R1,FUNCT_2:4;
then V: 1 <= p.i & p.i <= k by III,LG1,LG3,FINSEQ_1:1;
reconsider if1 = i as Element of dom F1 by Q2,A3,A4,FINSEQ_1:def 3;
now per cases;
suppose Q3: p.i < j; then
S1: G1.(p.i) = G.(p.i) by FINSEQ_3:110
.= G.(B.i) by Q1,P2,Q3;
F1.if1 = F.i by B2,FINSEQ_1:def 7;
hence thesis by S1,P0;
end;
suppose Q3: p.i >= j; then
S1: G1.(p.i) = G.((p.i)+1) by V,III,FINSEQ_3:111
.= G.(B.i) by Q1,Q3,P2;
F1.if1 = F.i by B2,FINSEQ_1:def 7;
hence thesis by S1,P0;
end;
end;
hence thesis;
end;
end;
end;
end;
hence P[k+1];
end;
I: for k be Nat holds P[k] from NAT_1:sch 2(A0,A1);
ex n being Nat st len F = n;
hence thesis by AS,I;
end;
registration
let R be PIDomain;
cluster factorizable -> uniquely_factorizable for Element of R;
coherence
proof
let a be Element of R; assume AS: a is factorizable;
hence a is factorizable;
let F,G being Factorization of a;
F is_a_factorization_of a & G is_a_factorization_of a by AS,ddf;
hence thesis by lemfactunique;
end;
end;
definition
let R be non degenerated Ring;
attr R is factorial means :df:
for a being non zero Element of R
st a is NonUnit of R holds a is uniquely_factorizable;
end;
registration
cluster factorial for non degenerated Ring;
existence
proof
take the Field;
thus thesis;
end;
end;
registration
let R be factorial non degenerated Ring;
cluster non zero non unital -> factorizable for Element of R;
coherence
proof
let a be Element of R; assume a is non zero non unital;
then a is uniquely_factorizable by df;
hence thesis;
end;
end;
definition
mode FactorialRing is factorial non degenerated Ring;
end;
registration
cluster PID -> factorial for domRing;
coherence
proof
let R be domRing;
assume Z: R is PID;
assume R is non factorial;
then consider a0 being non zero Element of R such that
XX: a0 is NonUnit of R & not a0 is uniquely_factorizable;
now assume X: not a0 is factorizable;
{a0}-Ideal in Ideals R; then
reconsider A = {a0}-Ideal as Element of Ideals R;
defpred P[set,set,set] means
for a being Element of R holds
(a <> 0.R & a is non unital & not a is factorizable & $2 = {a}-Ideal)
implies
(ex a1 being Element of R
st a1 <> 0.R & a1 is non unital & not a1 is factorizable &
$3 = {a1}-Ideal & {a}-Ideal c= {a1}-Ideal & {a}-Ideal <> {a1}-Ideal);
A: for n being Nat for x being Element of Ideals R
ex y being Element of Ideals R st P[n,x,y]
proof
let n be Nat, x be Element of Ideals R;
A1: for a being Element of R holds (a <> 0.R & a is non unital &
not a is factorizable & x = {a}-Ideal)
implies
(ex a1 being Element of R
st a1 <> 0.R & a1 is non unital & not a1 is factorizable &
x c= {a1}-Ideal & x <> {a1}-Ideal)
proof
let a be Element of R;
assume A1: a <> 0.R & a is non unital &
not a is factorizable & x = {a}-Ideal;
then a is reducible;
then consider u being Element of R such that
A3: u divides a & u is non unital & not u is_associated_to a by A1;
consider s being Element of R such that
A4: u * s = a by A3;
A5: now assume u is factorizable & s is factorizable;
then consider F,G being non empty FinSequence of R such that
H: F is_a_factorization_of u & G is_a_factorization_of s;
F^G is_a_factorization_of a by A4,H,fact2;
hence contradiction by A1;
end;
now per cases by A5;
suppose B1: not s is factorizable;
B2: s divides a by A4;
B4: s <> 0.R by A1,A4;
then H: s is right_mult-cancelable by ALGSTR_0:def 37;
B3: now assume {a}-Ideal = {s}-Ideal;
then ex e being Element of R st
e is unital & s * e = a by GCD_1:18,div3;
hence contradiction by H,A4,A3;
end;
s is non unital by A4,A3,GCD_1:18;
hence thesis by B1,B2,B3,B4,A1,div1;
end;
suppose B1: not u is factorizable;
B3: {a}-Ideal <> {u}-Ideal by A3,div1;
u <> 0.R by A4,A1;
hence thesis by B1,A3,div1,B3,A1;
end;
end;
hence thesis;
end;
now per cases;
suppose AA: ex a being Element of R st a <> 0.R & a is non unital &
not a is factorizable & x = {a}-Ideal;
consider a1 being Element of R such that
A3: a1 <> 0.R & a1 is non unital & not a1 is factorizable &
x c= {a1}-Ideal & x <> {a1}-Ideal by A1,AA;
{a1}-Ideal in Ideals R; then
reconsider A1 = {a1}-Ideal as Element of Ideals(R);
P[n,x,A1] by A3;
hence ex Y being Element of Ideals R st P[n,x,Y];
end;
suppose AA: not ex a being Element of R st a <> 0.R & a is non unital &
not a is factorizable & x = {a}-Ideal;
A1: {0.R} in Ideals R;
P[n,x,{0.R}] by AA;
hence ex y being Element of Ideals R st P[n,x,y] by A1;
end;
end;
hence ex y being Element of Ideals R st P[n,x,y];
end;
ex f being sequence of Ideals R st f.0 = A &
for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A);
then consider F being sequence of Ideals R such that
C1: F.0 = A & for n being Nat holds P[n,F.n,F.(n+1)];
B: for i being Nat holds F.i c= F.(i+1) & F.i <> F.(i+1)
proof
let i be Nat;
defpred P[Nat] means
(ex a being Element of R st a <> 0.R & a is non unital &
not a is factorizable & F.($1+1) = {a}-Ideal) &
F.$1 c= F.($1+1) & F.$1 <> F.($1+1);
A: P[0]
proof
A0: P[0,F.0,F.(0+1)] by C1;
A3: ex a1 being Element of R
st a1 <> 0.R & a1 is non unital & not a1 is factorizable &
F.1 = {a1}-Ideal & {a0}-Ideal c= {a1}-Ideal &
{a0}-Ideal <> {a1}-Ideal by A0,C1,X,XX;
thus ex a1 being Element of R
st a1 <> 0.R & a1 is non unital & not a1 is factorizable &
F.(0+1) = {a1}-Ideal by A3;
thus F.0 c= F.(0+1) & F.0 <> F.(0+1) by A3,C1;
end;
B: for k be Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume P[k];
then consider a being Element of R such that
B1: a <> 0.R & a is non unital & not a is factorizable &
F.(k+1) = {a}-Ideal & F.k c= F.(k+1) & F.k <> F.(k+1);
ex a1 being Element of R
st a1 <> 0.R & a1 is non unital & not a1 is factorizable &
F.((k+1)+1) = {a1}-Ideal & {a}-Ideal c= {a1}-Ideal &
{a}-Ideal <> {a1}-Ideal by B1,C1;
hence thesis by B1;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A,B);
hence thesis;
end;
then reconsider F as ascending Chain of Ideals R by asc;
now assume F is stagnating;
then consider i being Nat such that
D1: for j being Nat st j >= i holds F.j = F.i;
F.(i+1) = F.i by D1,NAT_1:11;
hence contradiction by B;
end;
hence contradiction by Z;
end;
hence contradiction by Z,XX;
end;
end;
begin :: Polynomial Rings over Fields
definition
let L be Field;
let p be Polynomial of L;
func deg* p -> Nat equals :S:
deg p if p <> 0_.L otherwise 0;
coherence
proof
per cases;
suppose p <> 0_.(L);
then p is non zero by UPROOTS:def 5;
hence thesis by TARSKI:1;
end;
suppose p = 0_.(L);
hence thesis;
end;
end;
consistency;
end;
definition
let L be Field;
func deg* L -> Function of Polynom-Ring L,NAT means :T:
for p being Polynomial of L holds it.p = deg* p;
existence
proof
set R = Polynom-Ring L;
defpred P[object,object] means
ex p be Polynomial of L st $1 = p & $2 = deg*(p);
A: for x being object st x in the carrier of R
ex y being object st y in NAT & P[x,y]
proof
let x be object; assume x in the carrier of R;
then reconsider p = x as Polynomial of L by POLYNOM3:def 10;
take y = deg* p;
thus thesis by ORDINAL1:def 12;
end;
ex f being Function of R,NAT
st for x being object st x in the carrier of R holds P[x,f.x]
from FUNCT_2:sch 1(A);
then consider f being Function of Polynom-Ring L,NAT such that
H: for x being object st x in the carrier of R holds P[x,f.x];
take f;
now let p be Polynomial of L;
p in the carrier of R by POLYNOM3:def 10;
then P[p,f.p] by H;
hence f.p = deg* p;
end;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of Polynom-Ring L,NAT such that
A1: for p being Polynomial of L holds g1.p = deg* p and
A2: for p being Polynomial of L holds g2.p = deg* p;
A: dom g1 = the carrier of Polynom-Ring L by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume x in dom g1;
then reconsider p = x as Polynomial of L by POLYNOM3:def 10;
thus g1.x = deg* p by A1 .= g2.x by A2;
end;
hence thesis by A;
end;
end;
theorem degA:
for L being Field
for p being Polynomial of L
for q being non zero Polynomial of L holds deg(p mod q) < deg q
proof
let L be Field;
let p be Polynomial of L;
let q be non zero Polynomial of L;
set u = p div q;
q <> 0_.(L); then
consider r being Polynomial of L such that
A: p = u *' q + r & deg r < deg q by HURWITZ:def 5;
p mod q = p - u *'q by HURWITZ:def 6
.= u *' q + r + -(u *'q) by A,POLYNOM3:def 6
.= (u *' q + -(u*' q)) + r by POLYNOM3:26
.= (u *' q - u*' q) + r by POLYNOM3:def 6
.= 0_.(L) + r by POLYNOM3:29
.= r by POLYNOM3:28;
hence thesis by A;
end;
theorem thEucl1:
for L being Field,
p being Element of Polynom-Ring L,
q being non zero Element of Polynom-Ring L
ex u,r being Element of Polynom-Ring L
st p = u * q + r &
(r = 0.(Polynom-Ring L) or (deg* L).r < (deg* L).q)
proof
let L be Field,
p be Element of Polynom-Ring L,
q be non zero Element of Polynom-Ring L;
q <> 0.(Polynom-Ring L);
then AS: q <> 0_.(L) by POLYNOM3:def 10;
then reconsider q1 = q as non zero Polynomial of L
by UPROOTS:def 5,POLYNOM3:def 10;
reconsider p1 = p as Polynomial of L by POLYNOM3:def 10;
set u = p1 div q1, r = p1 mod q1;
reconsider u,r as Element of Polynom-Ring L by POLYNOM3:def 10;
take u,r;
A: (p1 div q1) *' q1 + (p1 mod q1)
= (p1 div q1) *' q1 + (p1 - (p1 div q1) *' q1) by HURWITZ:def 6
.= (p1 div q1) *' q1 + (p1 + -((p1 div q1) *' q1)) by POLYNOM3:def 6
.= ((p1 div q1) *' q1 + -((p1 div q1) *' q1)) + p1 by POLYNOM3:26
.= ((p1 div q1) *' q1 -((p1 div q1) *' q1)) + p1 by POLYNOM3:def 6
.= 0_.(L) + p1 by POLYNOM3:29
.= p1 by POLYNOM3:28;
(p1 div q1) *' q1 = u * q by POLYNOM3:def 10;
hence p = u * q + r by A,POLYNOM3:def 10;
now assume r <> 0.(Polynom-Ring L);
then C: p1 mod q1 <> 0_.(L) by POLYNOM3:def 10;
B: (deg* L).r = deg*(p1 mod q1) by T .= deg(p1 mod q1) by C,S;
(deg* L).q = deg* q1 by T .= deg q1 by AS,S;
hence (deg* L).r < (deg* L).q by B,degA;
end;
hence thesis;
end;
thEucl2: for L being Field
ex f being Function of Polynom-Ring L,NAT
st for p,q being Element of Polynom-Ring L
st q <> 0.(Polynom-Ring L)
holds ex u,r being Element of Polynom-Ring L
st p = u * q + r & (r = 0.(Polynom-Ring L) or f.r < f.q)
proof
let L be Field; take f = deg* L;
now let p,q be Element of Polynom-Ring L;
assume q <> 0.(Polynom-Ring L);
then q is non zero;
hence ex u,r being Element of Polynom-Ring L
st p = u*q+r & (r = 0.(Polynom-Ring L) or f.r < f.q) by thEucl1;
end;
hence thesis;
end;
registration
let L be Field;
cluster Polynom-Ring L -> Euclidian;
coherence
proof
ex f being Function of Polynom-Ring(L),NAT
st for a,b being Element of Polynom-Ring(L)
st b <> 0.(Polynom-Ring(L))
ex q,r being Element of Polynom-Ring(L)
st a = q * b + r & (r = 0.(Polynom-Ring(L)) or f.r < f.b) by thEucl2;
hence thesis by INT_3:def 8;
end;
end;
definition
let L be Field;
redefine func deg* L -> DegreeFunction of Polynom-Ring L; :: redefines deg* (RING_2, definition)
coherence
proof
let a,b be Element of Polynom-Ring L;
assume b <> 0.(Polynom-Ring L);
then b is non zero;
hence thesis by thEucl1;
end;
end;