Copyright (c) 1997 Association of Mizar Users
environ
vocabulary ALTCAT_1, CAT_1, CAT_3, BOOLE, RELAT_1, BINOP_1, RELAT_2, FUNCT_1,
FUNCT_2, AMI_1, SGRAPH1, REALSET1, CQC_LANG, ALTCAT_3;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2,
STRUCT_0, CQC_LANG, ALTCAT_1, AMI_1;
constructors ALTCAT_1, AMI_1;
clusters FUNCT_1, AMI_1, TEX_2, ALTCAT_1, RELSET_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems CQC_LANG, RELAT_1, FUNCT_2, ZFMISC_1, ALTCAT_1, PARTFUN1, TARSKI,
FUNCT_1, REALSET1, AMI_1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_1;
begin
definition
let C be with_units (non empty AltCatStr),
o1, o2 be object of C,
A be Morphism of o1,o2,
B be Morphism of o2,o1;
pred A is_left_inverse_of B means :Def1:
A * B = idm o2;
synonym B is_right_inverse_of A;
end;
definition
let C be with_units (non empty AltCatStr),
o1, o2 be object of C,
A be Morphism of o1,o2;
attr A is retraction means :Def2:
ex B being Morphism of o2,o1 st B is_right_inverse_of A;
end;
definition
let C be with_units (non empty AltCatStr),
o1, o2 be object of C,
A be Morphism of o1,o2;
attr A is coretraction means :Def3:
ex B being Morphism of o2,o1 st B is_left_inverse_of A;
end;
theorem Th1:
for C being with_units (non empty AltCatStr), o being object of C holds
idm o is retraction & idm o is coretraction
proof
let C be with_units (non empty AltCatStr), o be object of C;
<^o,o^> <> {} by ALTCAT_1:23;
then (idm o) * (idm o) = idm o by ALTCAT_1:def 19;
then idm o is_left_inverse_of idm o & idm o is_right_inverse_of idm o by Def1
;
hence thesis by Def2,Def3;
end;
definition
let C be category,
o1, o2 be object of C such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2 such that
A2: A is retraction coretraction;
func A" -> Morphism of o2,o1 means :Def4:
it is_left_inverse_of A & it is_right_inverse_of A;
existence
proof
consider B1 being Morphism of o2,o1 such that
A3: B1 is_right_inverse_of A by A2,Def2;
consider B2 being Morphism of o2,o1 such that
A4: B2 is_left_inverse_of A by A2,Def3;
A5: B1 = idm o1 * B1 by A1,ALTCAT_1:24
.= B2 * A * B1 by A4,Def1
.= B2 * (A * B1) by A1,ALTCAT_1:25
.= B2 * idm o2 by A3,Def1
.= B2 by A1,ALTCAT_1:def 19;
take B1;
thus thesis by A3,A4,A5;
end;
uniqueness
proof
let M1,M2 be Morphism of o2,o1 such that
A6: M1 is_left_inverse_of A & M1 is_right_inverse_of A and
A7: M2 is_left_inverse_of A & M2 is_right_inverse_of A;
thus M1 = M1 * idm o2 by A1,ALTCAT_1:def 19
.= M1 * (A * M2) by A7,Def1
.= M1 * A * M2 by A1,ALTCAT_1:25
.= idm o1 * M2 by A6,Def1
.= M2 by A1,ALTCAT_1:24;
end;
end;
theorem Th2:
for C being category, o1,o2 being object of C st
<^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st
A is retraction & A is coretraction holds
A" * A = idm o1 & A * A" = idm o2
proof
let C be category,
o1,o2 be object of C such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2; assume
A is retraction & A is coretraction;
then A" is_left_inverse_of A & A" is_right_inverse_of A by A1,Def4;
hence A" * A = idm o1 & A * A" = idm o2 by Def1;
end;
theorem Th3:
for C being category, o1,o2 being object of C st
<^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is retraction & A is coretraction
holds (A")" = A
proof
let C be category,
o1,o2 be object of C such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2; assume
A is retraction & A is coretraction;
then A2: A" is_left_inverse_of A & A" is_right_inverse_of A by A1,Def4;
then A" is retraction & A" is coretraction by Def2,Def3;
then A3: (A")" is_right_inverse_of A" by A1,Def4;
thus (A")" = idm o2 * ((A")") by A1,ALTCAT_1:24
.= A * A" * (A")" by A2,Def1
.= A * (A" * (A")") by A1,ALTCAT_1:25
.= A * idm o1 by A3,Def1
.= A by A1,ALTCAT_1:def 19;
end;
theorem Th4:
for C being category, o being object of C holds
(idm o)" = idm o
proof
let C be category, o be object of C;
A1: <^o,o^> <> {} by ALTCAT_1:23;
idm o is retraction & idm o is coretraction by Th1;
then A2:(idm o)" is_left_inverse_of (idm o) by A1,Def4;
thus (idm o)" = (idm o)" * idm o by A1,ALTCAT_1:def 19
.= idm o by A2,Def1;
end;
definition
let C be category,
o1, o2 be object of C,
A be Morphism of o1,o2;
attr A is iso means :Def5:
A*A" = idm o2 & A"*A = idm o1;
end;
theorem Th5:
for C being category, o1, o2 being object of C, A being Morphism of o1,o2 st
A is iso holds A is retraction coretraction
proof
let C be category,
o1, o2 be object of C,
A be Morphism of o1,o2;
assume A is iso;
then A1: A * A" = idm o2 & A" * A = idm o1 by Def5;
then A" is_right_inverse_of A by Def1;
hence A is retraction by Def2;
A" is_left_inverse_of A by A1,Def1;
hence A is coretraction by Def3;
end;
theorem Th6:
for C being category, o1,o2 being object of C st
<^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 holds
A is iso iff A is retraction & A is coretraction
proof
let C be category,
o1,o2 be object of C such that
A1:<^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2;
thus A is iso implies A is retraction & A is coretraction by Th5;
assume that
A2: A is retraction and
A3: A is coretraction;
A" is_left_inverse_of A &
A" is_right_inverse_of A by A1,A2,A3,Def4;
then A" * A = idm o1 & A * A" = idm o2 by Def1;
hence A is iso by Def5;
end;
theorem Th7:
for C being category, o1,o2,o3 being object of C,
A being Morphism of o1,o2, B being Morphism of o2,o3 st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {}
& A is iso & B is iso holds
B * A is iso & (B * A)" = A" * B"
proof
let C be category,
o1,o2,o3 be object of C,
A be Morphism of o1,o2,
B be Morphism of o2,o3; assume
A1:<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
then A2: <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {}
by ALTCAT_1:def 4;
assume
A is iso & B is iso;
then A3: A is retraction & A is coretraction &
B is retraction & B is coretraction by A1,A2,Th6;
consider A1 be Morphism of o2,o1 such that A4: A1 = A";
consider B1 be Morphism of o3,o2 such that A5: B1 = B";
A6:(A1*B1)*(B*A) = A1*(B1*(B*A)) by A2,ALTCAT_1:25
.= A1*(B1*B*A) by A1,A2,ALTCAT_1:25
.= A1*((idm o2)*A) by A1,A2,A3,A5,Th2
.= A1*A by A1,ALTCAT_1:24
.= idm o1 by A1,A2,A3,A4,Th2;
then A7:(A1*B1) is_left_inverse_of (B*A) by Def1;
then A8:(B*A) is coretraction by Def3;
A9:(B*A)*(A1*B1) = B*(A*(A1*B1)) by A1,ALTCAT_1:25
.= B*(A*A1*B1) by A1,A2,ALTCAT_1:25
.= B*((idm o2)*B1) by A1,A2,A3,A4,Th2
.= B*B1 by A2,ALTCAT_1:24
.= idm o3 by A1,A2,A3,A5,Th2;
then A10:(A1*B1) is_right_inverse_of (B*A) by Def1;
then (B*A) is retraction by Def2;
then A1*B1 = (B*A)" by A1,A2,A7,A8,A10,Def4;
hence thesis by A4,A5,A6,A9,Def5;
end;
definition
let C be category,
o1, o2 be object of C;
pred o1,o2 are_iso means :Def6:
<^o1,o2^> <> {} & <^o2,o1^> <> {} &
ex A being Morphism of o1,o2 st A is iso;
reflexivity
proof
let o be object of C;
thus A1: <^o,o^> <> {} & <^o,o^> <> {} by ALTCAT_1:23;
take idm o;
set A = idm o;
A2: A*A" = A * A by Th4
.= idm o by A1,ALTCAT_1:def 19;
A"*A = A * A by Th4
.= idm o by A1,ALTCAT_1:def 19;
hence thesis by A2,Def5;
end;
symmetry
proof
let o1,o2 be object of C; assume that
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A4: ex A being Morphism of o1,o2 st A is iso;
consider A being Morphism of o1,o2 such that A5: A is iso by A4;
A6: A is retraction & A is coretraction by A5,Th5;
thus <^o2,o1^> <> {} & <^o1,o2^> <> {} by A3;
take A1 = A";
A7: A1*A1" = A" * A by A3,A6,Th3
.= idm o1 by A3,A6,Th2;
A1"*A1 = A * A" by A3,A6,Th3
.= idm o2 by A3,A6,Th2;
hence thesis by A7,Def5;
end;
end;
theorem
for C being category, o1,o2,o3 being object of C st
o1,o2 are_iso & o2,o3 are_iso holds o1,o3 are_iso
proof
let C be category, o1,o2,o3 be object of C such that
A1: o1,o2 are_iso and
A2: o2,o3 are_iso;
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {}
by A1,A2,Def6;
hence A4: <^o1,o3^> <> {} & <^o3,o1^> <> {} by ALTCAT_1:def 4;
consider A being Morphism of o1,o2 such that
A5: A is iso by A1,Def6;
consider B being Morphism of o2,o3 such that
A6: B is iso by A2,Def6;
take B * A;
thus thesis by A3,A4,A5,A6,Th7;
end;
definition
let C be non empty AltCatStr,
o1, o2 be object of C,
A be Morphism of o1,o2;
attr A is mono means :Def7:
for o being object of C st <^o,o1^> <> {}
for B,C being Morphism of o,o1 st A * B = A * C holds B = C;
end;
definition
let C be non empty AltCatStr,
o1, o2 be object of C,
A be Morphism of o1,o2;
attr A is epi means :Def8:
for o being object of C st <^o2,o^> <> {}
for B,C being Morphism of o2,o st B * A = C * A holds B = C;
end;
theorem Th9:
for C being associative transitive (non empty AltCatStr),
o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st
A is mono & B is mono holds
B * A is mono
proof
let C be associative transitive (non empty AltCatStr),
o1,o2,o3 be object of C; assume
A1:<^o1,o2^> <> {} & <^o2,o3^> <> {};
let A be Morphism of o1,o2,
B be Morphism of o2,o3; assume
A2: A is mono & B is mono;
let o be object of C; assume A3: <^o,o1^> <> {};
let M1,M2 be Morphism of o,o1; assume
A4:(B*A)*M1 = (B*A)*M2;
A5:(B*A)*M1 = B*(A*M1) by A1,A3,ALTCAT_1:25;
A6:(B*A)*M2 = B*(A*M2) by A1,A3,ALTCAT_1:25;
<^o,o2^> <> {} by A1,A3,ALTCAT_1:def 4;
then A*M1 = A*M2 by A2,A4,A5,A6,Def7;
hence M1 = M2 by A2,A3,Def7;
end;
theorem Th10:
for C being associative transitive (non empty AltCatStr),
o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st A is epi & B is epi
holds B * A is epi
proof
let C be associative transitive (non empty AltCatStr),
o1,o2,o3 be object of C; assume
A1:<^o1,o2^> <> {} & <^o2,o3^> <> {};
let A be Morphism of o1,o2,
B be Morphism of o2,o3; assume
A2: A is epi & B is epi;
let o be object of C; assume A3: <^o3,o^> <> {};
let M1,M2 be Morphism of o3,o; assume
A4:M1*(B*A) = M2*(B*A);
A5:M1*(B*A) = (M1*B)*A by A1,A3,ALTCAT_1:25;
A6:M2*(B*A) = (M2*B)*A by A1,A3,ALTCAT_1:25;
<^o2,o^> <> {} by A1,A3,ALTCAT_1:def 4;
then M1*B = M2*B by A2,A4,A5,A6,Def8;
hence M1 = M2 by A2,A3,Def8;
end;
theorem
for C being associative transitive (non empty AltCatStr),
o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st B * A is mono
holds A is mono
proof
let C be associative transitive (non empty AltCatStr),
o1,o2,o3 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o3^> <> {};
let A be Morphism of o1,o2,
B be Morphism of o2,o3; assume
A2: B * A is mono;
let o be object of C; assume A3: <^o,o1^> <> {};
let M1,M2 be Morphism of o,o1; assume
A4: A*M1 = A*M2;
A5:(B*A)*M1 = B*(A*M1) by A1,A3,ALTCAT_1:25;
(B*A)*M2 = B*(A*M2) by A1,A3,ALTCAT_1:25;
hence M1 = M2 by A2,A3,A4,A5,Def7;
end;
theorem
for C being associative transitive (non empty AltCatStr),
o1,o2,o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st B * A is epi
holds B is epi
proof
let C be associative transitive (non empty AltCatStr),
o1,o2,o3 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o3^> <> {};
let A be Morphism of o1,o2,
B be Morphism of o2,o3; assume
A2: B * A is epi;
let o be object of C; assume A3: <^o3,o^> <> {};
let M1,M2 be Morphism of o3,o; assume
A4: M1*B = M2*B;
A5:(M1*B)*A = M1*(B*A) by A1,A3,ALTCAT_1:25;
(M2*B)*A = M2*(B*A) by A1,A3,ALTCAT_1:25;
hence M1 = M2 by A2,A3,A4,A5,Def8;
end;
Lm1:
now
let C be with_units (non empty AltCatStr),
a be object of C;
thus idm a is epi
proof
let o be object of C such that
A1: <^a,o^> <> {};
let B, C be Morphism of a,o such that
A2: B * idm a = C * idm a;
thus B = B * idm a by A1,ALTCAT_1:def 19
.= C by A1,A2,ALTCAT_1:def 19;
end;
thus idm a is mono
proof
let o be object of C such that
A3: <^o,a^> <> {};
let B, C be Morphism of o,a such that
A4: idm a * B = idm a * C;
thus B = idm a * B by A3,ALTCAT_1:24
.= C by A3,A4,ALTCAT_1:24;
end;
end;
theorem
for X being non empty set
for o1,o2 being object of EnsCat X st <^o1,o2^> <> {}
for A being Morphism of o1,o2,
F being Function of o1,o2 st F = A holds
A is mono iff F is one-to-one
proof
let X be non empty set,
o1,o2 be object of EnsCat X; assume
A1: <^o1,o2^> <> {};
let A be Morphism of o1,o2,
F be Function of o1,o2; assume
A2: F = A;
per cases;
suppose o2 <> {};
then A3: dom F = o1 by FUNCT_2:def 1;
thus A is mono implies F is one-to-one
proof
assume
A4: A is mono;
assume not F is one-to-one;
then consider x1,x2 be set such that
A5: x1 in dom F & x2 in dom F and
A6: F.x1 = F.x2 and
A7: x1 <> x2 by FUNCT_1:def 8;
set o = o1;
A8: <^o,o1^> <> {} by ALTCAT_1:23;
deffunc G(set) = x1;
consider B be Function such that
A9: dom B = o and
A10: for x be set st x in o holds B.x = G(x) from Lambda;
deffunc H(set) = x2;
consider C be Function such that
A11: dom C = o and
A12: for x be set st x in o holds C.x = H(x) from Lambda;
consider o' be Element of o;
B.o' = x1 by A3,A5,A10;
then A13: B.o' <> C.o' by A3,A5,A7,A12;
A14: rng B c= o1
proof
let y be set; assume y in rng B;
then consider x be set such that
A15: x in dom B & B.x = y by FUNCT_1:def 5;
thus y in o1 by A3,A5,A9,A10,A15;
end;
then B in Funcs(o,o1) by A9,FUNCT_2:def 2;
then B in <^o,o1^> by ALTCAT_1:def 16;
then reconsider B1=B as Morphism of o,o1;
A16: rng C c= o1
proof
let y be set; assume y in rng C;
then consider x be set such that
A17: x in dom C & C.x = y by FUNCT_1:def 5;
thus y in o1 by A3,A5,A11,A12,A17;
end;
then C in Funcs(o,o1) by A11,FUNCT_2:def 2;
then C in <^o,o1^> by ALTCAT_1:def 16;
then reconsider C1=C as Morphism of o,o1;
A18: dom (F * B) = o by A3,A9,A14,RELAT_1:46;
A19: dom (F * C) = o by A3,A11,A16,RELAT_1:46;
now let z be set; assume A20: z in o;
hence (F * B).z = F.(B.z) by A18,FUNCT_1:22
.= F.x2 by A6,A10,A20
.= F.(C.z) by A12,A20
.= (F * C).z by A19,A20,FUNCT_1:22;
end;
then F * B = F * C by A18,A19,FUNCT_1:9;
then A * B1 = F * C by A1,A2,A8,ALTCAT_1:18
.= A * C1 by A1,A2,A8,ALTCAT_1:18;
hence contradiction by A4,A8,A13,Def7;
end;
thus F is one-to-one implies A is mono
proof
assume A21: F is one-to-one;
let o be object of EnsCat X; assume
A22: <^o,o1^> <> {};
let B,C be Morphism of o,o1; assume
A23: A * B = A * C;
A24: <^o,o1^> = Funcs(o,o1) by ALTCAT_1:def 16;
then consider B1 be Function such that
A25: B1 = B & dom B1 = o & rng B1 c= o1 by A22,FUNCT_2:def 2;
consider C1 be Function such that
A26: C1 = C & dom C1 = o & rng C1 c= o1 by A22,A24,FUNCT_2:def 2;
A27: <^o,o2^> <> {} by A1,A22,ALTCAT_1:def 4;
then A28: F * B1 = A * C by A1,A2,A22,A23,A25,ALTCAT_1:18
.= F * C1 by A1,A2,A22,A26,A27,ALTCAT_1:18;
now let z be set; assume A29: z in o;
then A30: B1.z in rng B1 & C1.z in rng C1 by A25,A26,FUNCT_1:def 5;
F.(B1.z) = (F*B1).z by A25,A29,FUNCT_1:23;
then F.(B1.z) = F.(C1.z) by A26,A28,A29,FUNCT_1:23;
hence B1.z = C1.z by A3,A21,A25,A26,A30,FUNCT_1:def 8;
end;
hence B = C by A25,A26,FUNCT_1:9;
end;
suppose A31: o2 = {};
A32: now per cases;
suppose o1 = {};
hence F = {} by PARTFUN1:57;
suppose o1 <> {};
hence F = {} by A31,FUNCT_2:def 1;
end;
thus A is mono implies F is one-to-one
proof
assume A is mono;
reconsider F1 = F as Function of {},(rng F) by A32,FUNCT_2:55,RELAT_1:60;
F1 is one-to-one by PARTFUN1:59;
hence thesis;
end;
thus F is one-to-one implies A is mono
proof
assume F is one-to-one;
let o be object of EnsCat X; assume
A33: <^o,o1^> <> {};
let B,C be Morphism of o,o1; assume
A * B = A * C;
A34: <^o,o1^> = Funcs(o,o1) by ALTCAT_1:def 16;
then consider B1 be Function such that
A35: B1 = B & dom B1 = o & rng B1 c= o1 by A33,FUNCT_2:def 2;
consider C1 be Function such that
A36: C1 = C & dom C1 = o & rng C1 c= o1 by A33,A34,FUNCT_2:def 2;
A37: <^o1,o2^> = Funcs(o1,o2) by ALTCAT_1:def 16;
consider x be Element of Funcs(o1,o2);
consider f be Function such that
A38: f = x & dom f = o1 & rng f c= o2 by A1,A37,FUNCT_2:def 2;
rng f = {} by A31,A38,XBOOLE_1:3;
then dom f = {} by RELAT_1:65;
then A39: rng B1 = {} by A35,A38,XBOOLE_1:3;
then A40: dom B1 = {} by RELAT_1:65;
B1 = {} by A39,RELAT_1:64
.= C1 by A35,A36,A40,RELAT_1:64;
hence thesis by A35,A36;
end;
end;
theorem
for X being non empty with_non-empty_elements set
for o1,o2 being object of EnsCat X st <^o1,o2^> <> {}
for A being Morphism of o1,o2,
F being Function of o1,o2 st F = A holds
A is epi iff F is onto
proof
let X be non empty with_non-empty_elements set,
o1,o2 be object of EnsCat X; assume
A1: <^o1,o2^> <> {};
let A be Morphism of o1,o2,
F be Function of o1,o2; assume
A2: F = A;
per cases;
suppose A3: for x be set st x in X holds x is trivial;
thus A is epi implies F is onto
proof
assume A is epi;
now per cases;
suppose A4: o2 = {};
now per cases;
suppose o1 = {};
hence F = {} by PARTFUN1:57;
suppose o1 <> {};
hence F = {} by A4,FUNCT_2:def 1;
end;
hence F is onto by A4,FUNCT_2:def 3,PARTFUN1:10;
suppose A5: o2 <> {};
o2 is Element of X by ALTCAT_1:def 16;
then o2 is trivial by A3;
then consider y be set such that
A6: o2 = {y} by A5,REALSET1:def 12;
A7: rng F c= {y} by A6,RELSET_1:12;
A8: o1 is Element of X by ALTCAT_1:def 16;
then A9: o1 <> {} by AMI_1:def 1;
o1 is trivial by A3,A8;
then consider z be set such that
A10: o1 = {z} by A9,REALSET1:def 12;
dom F = {z} by A5,A10,FUNCT_2:def 1;
then rng F <> {} by RELAT_1:65;
then rng F = {y} by A7,ZFMISC_1:39;
hence F is onto by A6,FUNCT_2:def 3;
end;
hence thesis;
end;
thus F is onto implies A is epi
proof assume
A11: F is onto;
let o be object of EnsCat X; assume A12: <^o2,o^> <> {};
let B,C be Morphism of o2,o; assume A13: B * A = C * A;
A14: <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 16;
then consider B1 be Function such that
A15: B1 = B & dom B1 = o2 & rng B1 c= o by A12,FUNCT_2:def 2;
consider C1 be Function such that
A16: C1 = C & dom C1 = o2 & rng C1 c= o by A12,A14,FUNCT_2:def 2;
A17: <^o1,o^> <> {} by A1,A12,ALTCAT_1:def 4;
then A18: B1 * F = C * A by A1,A2,A12,A13,A15,ALTCAT_1:18
.= C1 * F by A1,A2,A12,A16,A17,ALTCAT_1:18;
now assume B1 <> C1;
then consider z be set such that
A19: z in o2 & B1.z <> C1.z by A15,A16,FUNCT_1:9;
z in rng F by A11,A19,FUNCT_2:def 3;
then consider x be set such that
A20: x in dom F & F.x = z by FUNCT_1:def 5;
B1.(F.x) = (B1*F).x by A20,FUNCT_1:23;
hence contradiction by A18,A19,A20,FUNCT_1:23;
end;
hence thesis by A15,A16;
end;
suppose A21: ex x be set st x in X & x is non trivial;
now per cases;
suppose o2 <> {};
then A22: dom F = o1 by FUNCT_2:def 1;
consider o be set such that
A23: o in X and
A24: o is non trivial by A21;
o in the carrier of EnsCat X by A23,ALTCAT_1:def 16;
then reconsider o as object of EnsCat X;
thus A is epi implies F is onto
proof
assume that
A25: A is epi and
A26: not F is onto;
A27: rng F c= o2 by RELSET_1:12;
rng F <> o2 by A26,FUNCT_2:def 3;
then not o2 c= rng F by A27,XBOOLE_0:def 10;
then consider y be set such that
A28: y in o2 & not y in rng F by TARSKI:def 3;
A29: o <> {} by A23,AMI_1:def 1;
consider k be Element of o;
reconsider ok = (o\{k}) as non empty set by A24,A29,REALSET1:32;
consider l be Element of ok;
A30: l in o & not l in {k} by XBOOLE_0:def 4;
reconsider l as Element of o by XBOOLE_0:def 4;
A31: k <> l by A30,TARSKI:def 1;
A32: k in o & l in o by A29;
deffunc G(set) = IFEQ($1,y,l,k);
consider B be Function such that
A33: dom B = o2 and
A34: for x be set st x in o2 holds B.x = G(x) from Lambda;
deffunc G(set) = k;
consider C be Function such that
A35: dom C = o2 and
A36: for x be set st x in o2 holds C.x = G(x) from Lambda;
B.y = IFEQ(y,y,l,k) by A28,A34
.= l by CQC_LANG:def 1;
then A37: not B = C by A28,A31,A36;
A38: rng B c= o
proof
let y1 be set; assume y1 in rng B;
then consider x be set such that A39: x in dom B & B.x = y1 by FUNCT_1:
def 5;
per cases;
suppose A40: x = y;
y1 = IFEQ(x,y,l,k) by A33,A34,A39
.= l by A40,CQC_LANG:def 1;
hence y1 in o by A29;
suppose A41: x <> y;
y1 = IFEQ(x,y,l,k) by A33,A34,A39
.= k by A41,CQC_LANG:def 1;
hence y1 in o by A29;
end;
then B in Funcs(o2,o) by A33,FUNCT_2:def 2;
then A42: B in <^o2,o^> by ALTCAT_1:def 16;
then reconsider B1=B as Morphism of o2,o;
rng C c= o
proof
let y be set; assume y in rng C;
then consider x be set such that
A43: x in dom C & C.x = y by FUNCT_1:def 5;
thus y in o by A32,A35,A36,A43;
end;
then C in Funcs(o2,o) by A35,FUNCT_2:def 2;
then C in <^o2,o^> by ALTCAT_1:def 16;
then reconsider C1=C as Morphism of o2,o;
A44: dom (B*F) = o1 by A22,A27,A33,RELAT_1:46;
for z be set holds z in rng(B*F) implies z in rng B by FUNCT_1:25;
then rng (B*F) c= rng B by TARSKI:def 3;
then rng (B*F) c= o by A38,XBOOLE_1:1;
then (B*F) in Funcs(o1,o) by A44,FUNCT_2:def 2;
then A45: (B*F) in <^o1,o^> by ALTCAT_1:def 16;
A46: dom (C*F) = o1 by A22,A27,A35,RELAT_1:46;
now let z be set; assume A47: z in o1;
then A48: F.z in rng F by A22,FUNCT_1:def 5;
then A49: B.(F.z) = IFEQ((F.z),y,l,k) by A27,A34
.= k by A28,A48,CQC_LANG:def 1;
thus (B * F).z = B.(F.z) by A44,A47,FUNCT_1:22
.= C.(F.z) by A27,A36,A48,A49
.= (C * F).z by A46,A47,FUNCT_1:22;
end;
then B * F = C * F by A44,A46,FUNCT_1:9;
then B1 * A = C * F by A1,A2,A42,A45,ALTCAT_1:18
.= C1 * A by A1,A2,A42,A45,ALTCAT_1:18;
hence contradiction by A25,A37,A42,Def8;
end;
thus F is onto implies A is epi
proof
assume A50: F is onto;
let o be object of EnsCat X; assume A51: <^o2,o^> <> {};
let B,C be Morphism of o2,o; assume A52: B * A = C * A;
A53: <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 16;
then consider B1 be Function such that
A54: B1 = B & dom B1 = o2 & rng B1 c= o by A51,FUNCT_2:def 2;
consider C1 be Function such that
A55: C1 = C & dom C1 = o2 & rng C1 c= o by A51,A53,FUNCT_2:def 2;
A56: <^o1,o^> <> {} by A1,A51,ALTCAT_1:def 4;
then A57: B1 * F = C * A by A1,A2,A51,A52,A54,ALTCAT_1:18
.= C1 * F by A1,A2,A51,A55,A56,ALTCAT_1:18;
now assume B1 <> C1;
then consider z be set such that
A58: z in o2 & B1.z <> C1.z by A54,A55,FUNCT_1:9;
z in rng F by A50,A58,FUNCT_2:def 3;
then consider x be set such that
A59: x in dom F & F.x = z by FUNCT_1:def 5;
B1.(F.x) = (B1*F).x by A59,FUNCT_1:23;
hence contradiction by A57,A58,A59,FUNCT_1:23;
end;
hence thesis by A54,A55;
end;
suppose A60: o2 = {};
now per cases;
suppose o1 = {};
hence F = {} by PARTFUN1:57;
suppose o1 <> {};
hence F = {} by A60,FUNCT_2:def 1;
end;
hence A is epi implies F is onto by A60,FUNCT_2:def 3,PARTFUN1:10;
thus F is onto implies A is epi
proof
assume F is onto;
let o be object of EnsCat X; assume
A61: <^o2,o^> <> {};
let B,C be Morphism of o2,o; assume
B * A = C * A;
A62: <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 16;
then consider B1 be Function such that
A63: B1 = B & dom B1 = o2 & rng B1 c= o by A61,FUNCT_2:def 2;
consider C1 be Function such that
A64: C1 = C & dom C1 = o2 & rng C1 c= o by A61,A62,FUNCT_2:def 2;
B1 = {} & C1 = {} by A60,A63,A64,RELAT_1:64;
hence thesis by A63,A64;
end;
end;
hence thesis;
end;
theorem Th15:
for C being category, o1,o2 being object of C st
<^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is retraction holds A is epi
proof
let C be category,
o1,o2 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2; assume
A is retraction;
then consider R being Morphism of o2,o1 such that
A2: R is_right_inverse_of A by Def2;
let o be object of C; assume
A3: <^o2,o^> <> {};
let B,C be Morphism of o2,o; assume
A4: B * A = C * A;
thus B = B * idm o2 by A3,ALTCAT_1:def 19
.= B * (A * R) by A2,Def1
.= C * A * R by A1,A3,A4,ALTCAT_1:25
.= C * (A * R) by A1,A3,ALTCAT_1:25
.= C * idm o2 by A2,Def1
.= C by A3,ALTCAT_1:def 19;
end;
theorem Th16:
for C being category, o1,o2 being object of C st
<^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is coretraction holds A is mono
proof
let C be category,
o1,o2 be object of C; assume
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1,o2; assume
A is coretraction;
then consider R being Morphism of o2,o1 such that
A2: R is_left_inverse_of A by Def3;
let o be object of C; assume
A3: <^o,o1^> <> {};
let B,C be Morphism of o,o1; assume
A4: A * B = A * C;
thus B = idm o1 * B by A3,ALTCAT_1:24
.= R * A * B by A2,Def1
.= R * (A * C) by A1,A3,A4,ALTCAT_1:25
.= R * A * C by A1,A3,ALTCAT_1:25
.= idm o1 * C by A2,Def1
.= C by A3,ALTCAT_1:24;
end;
theorem
for C being category, o1,o2 being object of C st
<^o1,o2^> <> {} & <^o2,o1^> <> {}
for A being Morphism of o1,o2 st A is iso holds A is mono epi
proof
let C be category;
let o1, o2 be object of C such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
let A be Morphism of o1, o2;
assume
A is iso;
then A2: A is retraction & A is coretraction by A1,Th6;
A3: for o being object of C st <^o,o1^> <> {}
for B, C being Morphism of o, o1 st A * B = A * C holds B = C
proof
let o be object of C such that
A4: <^o,o1^> <> {};
let B, C be Morphism of o, o1;
assume A * B = A * C;
then (A" * A) * B = A" * (A * C) by A1,A4,ALTCAT_1:25;
then idm o1 * B = A" * (A * C) by A1,A2,Th2;
then idm o1 * B = (A" * A) * C by A1,A4,ALTCAT_1:25;
then idm o1 * B = idm o1 * C by A1,A2,Th2;
then B = idm o1 * C by A4,ALTCAT_1:24;
hence B = C by A4,ALTCAT_1:24;
end;
for o being object of C st <^o2,o^> <> {}
for B, C being Morphism of o2, o st B * A = C * A holds B = C
proof
let o be object of C such that
A5: <^o2,o^> <> {};
let B, C be Morphism of o2, o;
assume B * A = C * A;
then B * (A * A") = (C * A) * A" by A1,A5,ALTCAT_1:25;
then B * idm o2 = (C * A) * A" by A1,A2,Th2;
then B * idm o2 = C * (A * A") by A1,A5,ALTCAT_1:25;
then B * idm o2 = C * idm o2 by A1,A2,Th2;
then B = C * idm o2 by A5,ALTCAT_1:def 19;
hence B = C by A5,ALTCAT_1:def 19;
end;
hence A is mono & A is epi by A3,Def7,Def8;
end;
theorem Th18:
for C being category, o1,o2,o3 being object of C st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st
A is retraction & B is retraction holds
B*A is retraction
proof
let C be category,
o1,o2,o3 be object of C;
assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
then A2: <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {} by ALTCAT_1:def
4;
let A be Morphism of o1,o2, B be Morphism of o2,o3;
assume A3: A is retraction & B is retraction;
then consider A1 being Morphism of o2,o1 such that
A4: A1 is_right_inverse_of A by Def2;
consider B1 being Morphism of o3,o2 such that
A5: B1 is_right_inverse_of B by A3,Def2;
consider G being Morphism of o3,o1 such that
A6: G = A1 * B1;
take G;
(B * A) * G = B * (A * (A1 * B1)) by A1,A6,ALTCAT_1:25
.= B * ((A * A1) * B1) by A1,A2,ALTCAT_1:25
.= B * (idm o2 * B1) by A4,Def1
.= B * B1 by A2,ALTCAT_1:24
.= idm o3 by A5,Def1;
hence G is_right_inverse_of B*A by Def1;
end;
theorem Th19:
for C being category, o1,o2,o3 being object of C st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {}
for A being Morphism of o1,o2, B being Morphism of o2,o3 st
A is coretraction & B is coretraction holds
B*A is coretraction
proof
let C be category,
o1,o2,o3 be object of C;
assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
then A2: <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {} by ALTCAT_1:def
4;
let A be Morphism of o1,o2, B be Morphism of o2,o3;
assume A3: A is coretraction & B is coretraction;
then consider A1 being Morphism of o2,o1 such that
A4: A1 is_left_inverse_of A by Def3;
consider B1 being Morphism of o3,o2 such that
A5: B1 is_left_inverse_of B by A3,Def3;
consider G being Morphism of o3,o1 such that
A6: G = A1 * B1;
take G;
A7: <^o2,o2^> <> {} by ALTCAT_1:23;
G * (B * A) = ((A1 * B1) * B) * A by A1,A6,ALTCAT_1:25
.= (A1 * (B1 * B)) * A by A1,A2,ALTCAT_1:25
.= (A1 * idm o2) * A by A5,Def1
.= A1 * (idm o2 *A) by A1,A2,A7,ALTCAT_1:25
.= A1 * A by A1,ALTCAT_1:24
.= idm o1 by A4,Def1;
hence G is_left_inverse_of B*A by Def1;
end;
theorem Th20:
for C being category, o1, o2 being object of C, A being Morphism of o1,o2 st
A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {}
holds A is iso
proof
let C be category,
o1, o2 be object of C,
A be Morphism of o1,o2;
assume that
A1: A is retraction & A is mono and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {};
A3: <^o1,o1^> <> {} by ALTCAT_1:23;
consider B being Morphism of o2,o1 such that
A4: B is_right_inverse_of A by A1,Def2;
A * B * A = (idm o2) * A by A4,Def1;
then A * (B * A) = (idm o2) * A by A2,ALTCAT_1:25;
then A * (B * A) = A by A2,ALTCAT_1:24;
then A5: A * (B * A) = A * idm o1 by A2,ALTCAT_1:def 19;
then B * A = idm o1 by A1,A3,Def7;
then A6: B is_left_inverse_of A by Def1;
then A7: A is coretraction by Def3;
then A8: A*A" = A * B by A1,A2,A4,A6,Def4
.= idm o2 by A4,Def1;
A"*A = B * A by A1,A2,A4,A6,A7,Def4
.= idm o1 by A1,A3,A5,Def7;
hence thesis by A8,Def5;
end;
theorem
for C being category, o1, o2 being object of C, A being Morphism of o1, o2 st
A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {}
holds A is iso
proof
let C be category,
o1, o2 be object of C,
A be Morphism of o1,o2;
assume that
A1: A is coretraction & A is epi and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {};
A3: <^o2,o2^> <> {} by ALTCAT_1:23;
consider B being Morphism of o2,o1 such that
A4: B is_left_inverse_of A by A1,Def3;
A * (B * A) = A * (idm o1) by A4,Def1;
then A * (B * A) = A by A2,ALTCAT_1:def 19;
then A * (B * A) = idm o2 * A by A2,ALTCAT_1:24;
then A5: (A * B) * A = idm o2 * A by A2,ALTCAT_1:25;
then A * B = idm o2 by A1,A3,Def8;
then A6: B is_right_inverse_of A by Def1;
then A7: A is retraction by Def2;
then A8: A*A" = A * B by A1,A2,A4,A6,Def4
.= idm o2 by A1,A3,A5,Def8;
A"*A = B * A by A1,A2,A4,A6,A7,Def4
.= idm o1 by A4,Def1;
hence thesis by A8,Def5;
end;
theorem
for C being category, o1,o2,o3 being object of C, A being Morphism of o1,o2,
B being Morphism of o2,o3 st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction
holds B is retraction
proof
let C be category,
o1,o2,o3 be object of C,
A be Morphism of o1,o2,
B be Morphism of o2,o3;
assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
assume B * A is retraction;
then consider G be Morphism of o3,o1 such that
A2: G is_right_inverse_of (B*A) by Def2;
(B * A) * G = idm o3 by A2,Def1;
then B * (A * G) = idm o3 by A1,ALTCAT_1:25;
then A * G is_right_inverse_of B by Def1;
then consider F be Morphism of o3,o2 such that A3: F = (A * G) &
F is_right_inverse_of B;
thus thesis by A3,Def2;
end;
theorem
for C being category, o1,o2,o3 being object of C, A being Morphism of o1,o2,
B being Morphism of o2,o3 st
<^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction
holds A is coretraction
proof
let C be category,
o1,o2,o3 be object of C,
A be Morphism of o1,o2,
B be Morphism of o2,o3;
assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {};
assume B * A is coretraction;
then consider G be Morphism of o3,o1 such that
A2: G is_left_inverse_of (B * A) by Def3;
A3: (G * B) * A = G * (B * A) by A1,ALTCAT_1:25;
G * (B * A) = idm o1 by A2,Def1;
then G * B is_left_inverse_of A by A3,Def1;
then consider F be Morphism of o2,o1 such that A4: F = (G * B) &
F is_left_inverse_of A;
thus thesis by A4,Def3;
end;
theorem
for C being category st
for o1,o2 being object of C, A1 being Morphism of o1,o2 holds A1 is retraction
holds
for a,b being object of C,A being Morphism of a,b
st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso
proof
let C be category;
assume A1: for o1,o2 being object of C, A1 being Morphism of o1,o2 holds
A1 is retraction;
thus for a,b being object of C, A being Morphism of a,b
st <^a,b^> <> {} & <^b,a^> <> {} holds A is iso
proof
let a,b be object of C;
let A be Morphism of a,b;
assume A2: <^a,b^> <> {} & <^b,a^> <> {};
A3: A is retraction by A1;
A is coretraction
proof
consider A1 be Morphism of b,a such that
A4: A1 is_right_inverse_of A by A3,Def2;
A1 is retraction by A1;
then A5: A1 is epi by A2,Th15;
A6: <^a,a^> <> {} by ALTCAT_1:23;
A1 * (A * A1) =A1 * idm b by A4,Def1;
then A1 * (A * A1) =A1 by A2,ALTCAT_1:def 19;
then (A1 * A) * A1 =A1 by A2,ALTCAT_1:25;
then (A1 * A) * A1 =idm a * A1 by A2,ALTCAT_1:24;
then (A1 * A) =idm a by A5,A6,Def8;
then A1 is_left_inverse_of A by Def1;
hence thesis by Def3;
end;
hence A is iso by A2,A3,Th6;
end;
end;
definition
let C be with_units (non empty AltCatStr),
o be object of C;
cluster mono epi retraction coretraction Morphism of o,o;
existence
proof
take idm o;
thus thesis by Lm1,Th1;
end;
end;
definition
let C be category,
o be object of C;
cluster mono epi iso retraction coretraction Morphism of o,o;
existence
proof
A1: <^o,o^> <> {} by ALTCAT_1:23;
take I = idm o;
A2: I is retraction coretraction by Th1;
then I is epi mono by A1,Th15,Th16;
hence thesis by A1,A2,Th20;
end;
end;
definition
let C be category,
o be object of C,
A, B be mono Morphism of o,o;
cluster A * B -> mono;
coherence
proof
<^o,o^> <> {} by ALTCAT_1:23;
hence thesis by Th9;
end;
end;
definition
let C be category,
o be object of C,
A, B be epi Morphism of o,o;
cluster A * B -> epi;
coherence
proof
<^o,o^> <> {} by ALTCAT_1:23;
hence thesis by Th10;
end;
end;
definition
let C be category,
o be object of C,
A, B be iso Morphism of o,o;
cluster A * B -> iso;
coherence
proof
<^o,o^> <> {} by ALTCAT_1:23;
hence thesis by Th7;
end;
end;
definition
let C be category,
o be object of C,
A, B be retraction Morphism of o,o;
cluster A * B -> retraction;
coherence
proof
<^o,o^> <> {} by ALTCAT_1:23;
hence thesis by Th18;
end;
end;
definition
let C be category,
o be object of C,
A, B be coretraction Morphism of o,o;
cluster A * B -> coretraction;
coherence
proof
<^o,o^> <> {} by ALTCAT_1:23;
hence thesis by Th19;
end;
end;
definition
let C be AltGraph,
o be object of C;
attr o is initial means :Def9:
for o1 being object of C holds
ex M being Morphism of o,o1 st M in <^o,o1^> & <^o,o1^> is trivial;
end;
theorem
for C being AltGraph, o being object of C holds
o is initial iff
for o1 being object of C holds
ex M being Morphism of o,o1 st M in <^o,o1^> &
(for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1)
proof
let C be AltGraph, o be object of C;
thus o is initial implies
(for o1 being object of C holds
ex M being Morphism of o,o1 st M in <^o,o1^> &
(for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1))
proof
assume A1: o is initial;
let o1 be object of C;
consider M being Morphism of o,o1 such that
A2: M in <^o,o1^> & <^o,o1^> is trivial by A1,Def9;
consider i be set such that
A3: <^o,o1^> = { i } by A2,REALSET1:def 12;
<^o,o1^> = {M} by A3,TARSKI:def 1;
then for M1 being Morphism of o,o1 st M1 in <^o,o1^>
holds M = M1 by TARSKI:def 1;
hence thesis by A2;
end;
assume A4: (for o1 being object of C holds
ex M being Morphism of o,o1 st M in <^o,o1^> &
(for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1));
let o1 be object of C;
consider M being Morphism of o,o1 such that
A5: M in <^o,o1^> and
A6: for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds M = M1 by A4;
A7: <^o,o1^> c= {M}
proof
let x be set; assume A8: x in <^o,o1^>;
then reconsider M1 = x as Morphism of o,o1;
M1 = M by A6,A8;
hence x in {M} by TARSKI:def 1;
end;
{M} c= <^o,o1^>
proof
let x be set; assume x in {M};
hence x in <^o,o1^> by A5,TARSKI:def 1;
end;
then <^o,o1^> = {M} by A7,XBOOLE_0:def 10;
hence thesis;
end;
theorem Th26:
for C being category, o1,o2 being object of C st
o1 is initial & o2 is initial holds o1,o2 are_iso
proof
let C be category, o1,o2 be object of C
such that
A1: o1 is initial and
A2: o2 is initial;
consider M1 being Morphism of o1,o2 such that
A3: M1 in <^o1,o2^> & <^o1,o2^> is trivial by A1,Def9;
consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> & <^o2,o1^> is trivial by A2,Def9;
thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A3,A4;
A5: (ex M being Morphism of o1,o1 st M in <^o1,o1^> & <^o1,o1^> is trivial) &
(ex N being Morphism of o2,o2 st N in <^o2,o2^> & <^o2,o2^> is trivial)
by A1,A2,Def9;
then consider x being set such that A6: <^o1,o1^> = {x}
by REALSET1:def 12;
consider y being set such that A7: <^o2,o2^> = {y}
by A5,REALSET1:def 12;
A8: M1 * M2 = y & M2 * M1 = x by A6,A7,TARSKI:def 1;
idm o1 = x & idm o2 = y by A6,A7,TARSKI:def 1;
then M2 is_left_inverse_of M1 & M2 is_right_inverse_of M1 by A8,Def1;
then M1 is retraction & M1 is coretraction by Def2,Def3;
then M1 is iso by A3,A4,Th6;
hence thesis;
end;
definition
let C be AltGraph,
o be object of C;
attr o is terminal means :Def10:
for o1 being object of C holds
ex M being Morphism of o1,o st M in <^o1,o^> & <^o1,o^> is trivial;
end;
theorem
for C being AltGraph, o being object of C holds
o is terminal iff
for o1 being object of C holds
ex M being Morphism of o1,o st M in <^o1,o^> &
(for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1)
proof
let C be AltGraph, o be object of C;
thus o is terminal implies
(for o1 being object of C holds
ex M being Morphism of o1,o st M in <^o1,o^> &
(for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1))
proof
assume A1: o is terminal;
let o1 be object of C;
consider M being Morphism of o1,o such that
A2: M in <^o1,o^> & <^o1,o^> is trivial by A1,Def10;
consider i be set such that
A3: <^o1,o^> = { i } by A2,REALSET1:def 12;
<^o1,o^> = {M} by A3,TARSKI:def 1;
then for M1 being Morphism of o1,o st M1 in <^o1,o^>
holds M = M1 by TARSKI:def 1;
hence thesis by A2;
end;
assume A4: for o1 being object of C holds
ex M being Morphism of o1,o st M in <^o1,o^> &
(for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1);
let o1 be object of C;
consider M being Morphism of o1,o such that
A5: M in <^o1,o^> and
A6: for M1 being Morphism of o1,o st M1 in <^o1,o^> holds M = M1 by A4;
A7: <^o1,o^> c= {M}
proof
let x be set; assume A8: x in <^o1,o^>;
then reconsider M1 = x as Morphism of o1,o;
M1 = M by A6,A8;
hence x in {M} by TARSKI:def 1;
end;
{M} c= <^o1,o^>
proof
let x be set; assume x in {M};
hence x in <^o1,o^> by A5,TARSKI:def 1;
end;
then <^o1,o^> = {M} by A7,XBOOLE_0:def 10;
hence thesis;
end;
theorem
for C being category, o1,o2 being object of C st
o1 is terminal & o2 is terminal holds o1,o2 are_iso
proof
let C be category, o1,o2 be object of C; assume that
A1: o1 is terminal and
A2: o2 is terminal;
consider M1 being Morphism of o1,o2 such that
A3: M1 in <^o1,o2^> & <^o1,o2^> is trivial by A2,Def10;
consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> & <^o2,o1^> is trivial by A1,Def10;
thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A3,A4;
A5:(ex M being Morphism of o1,o1 st M in <^o1,o1^> & <^o1,o1^> is trivial) &
(ex N being Morphism of o2,o2 st N in <^o2,o2^> & <^o2,o2^> is trivial)
by A1,A2,Def10;
then consider x being set such that A6: <^o1,o1^> = {x}
by REALSET1:def 12;
consider y being set such that A7: <^o2,o2^> = {y}
by A5,REALSET1:def 12;
M1 * M2 = y & M2 * M1 = x by A6,A7,TARSKI:def 1;
then M1 * M2 = idm o2 & M2 * M1 = idm o1 by A6,A7,TARSKI:def 1;
then M2 is_left_inverse_of M1 & M2 is_right_inverse_of M1 by Def1;
then M1 is retraction & M1 is coretraction by Def2,Def3;
then M1 is iso by A3,A4,Th6;
hence thesis;
end;
definition
let C be AltGraph,
o be object of C;
attr o is _zero means :Def11:
o is initial terminal;
end;
theorem
for C being category, o1,o2 being object of C st
o1 is _zero & o2 is _zero holds o1,o2 are_iso
proof
let C be category, o1,o2 be object of C; assume
o1 is _zero & o2 is _zero;
then o1 is initial & o2 is initial by Def11;
hence thesis by Th26;
end;
definition
let C be non empty AltCatStr,
o1, o2 be object of C,
M be Morphism of o1,o2;
attr M is _zero means :Def12:
for o being object of C st o is _zero
for A being Morphism of o1,o, B being Morphism of o,o2 holds M = B*A;
end;
theorem
for C being category, o1,o2,o3 being object of C
for M1 being Morphism of o1,o2, M2 being Morphism of o2,o3
st M1 is _zero & M2 is _zero holds M2 * M1 is _zero
proof
let C be category,
o1,o2,o3 be object of C,
M1 be Morphism of o1,o2,
M2 be Morphism of o2,o3; assume that
A1: M1 is _zero and
A2: M2 is _zero;
let o be object of C; assume
A3: o is _zero;
then A4: o is initial & o is terminal by Def11;
let A be Morphism of o1,o, B be Morphism of o,o3;
consider B1 being Morphism of o,o2 such that
A5: B1 in <^o,o2^> & <^o,o2^> is trivial by A4,Def9;
consider B2 being Morphism of o,o3 such that
A6: B2 in <^o,o3^> & <^o,o3^> is trivial by A4,Def9;
consider A1 being Morphism of o1,o such that
A7: A1 in <^o1,o^> & <^o1,o^> is trivial by A4,Def10;
consider A2 being Morphism of o2,o such that
A8: A2 in <^o2,o^> & <^o2,o^> is trivial by A4,Def10;
A9: M2 = B2 * A2 by A2,A3,Def12;
consider x being set such that
A10: <^o1,o^> = {x} by A7,REALSET1:def 12;
A11:A = x & A1 = x by A10,TARSKI:def 1;
consider y being set such that
A12: <^o,o3^> = {y} by A6,REALSET1:def 12;
A13: B = y & B2 = y by A12,TARSKI:def 1;
(ex M being Morphism of o,o st M in <^o,o^> & <^o,o^> is trivial)
by A4,Def10;
then consider z being set such that
A14: <^o,o^> = {z} by REALSET1:def 12;
A15:idm o = z & A2 * B1 = z by A14,TARSKI:def 1;
A16: <^o,o2^> <> {} & <^o2,o^> <> {} & <^o1,o^> <> {} & <^o,o3^> <> {} &
<^o,o^> <> {} & <^o2,o3^> <> {} by A5,A6,A7,A8,ALTCAT_1:def 4;
thus M2 * M1 = (B2*A2) * (B1*A1) by A1,A3,A9,Def12
.= B2*A2 * B1*A1 by A16,ALTCAT_1:25
.= B*(idm o)*A by A5,A6,A8,A11,A13,A15,ALTCAT_1:25
.= B*A by A6,ALTCAT_1:def 19;
end;