:: Basic properties of objects and morphisms. In categories without
:: uniqueness of { \bf cod } and { \bf dom }
:: by Beata Madras
::
:: Received February 14, 1997
:: Copyright (c) 1997-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 ALTCAT_1, XBOOLE_0, CAT_1, RELAT_1, CAT_3, BINOP_1, RELAT_2,
FUNCT_1, FUNCOP_1, TARSKI, FUNCT_2, SUBSET_1, SETFAM_1, ZFMISC_1,
ALTCAT_3;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FUNCT_2, FUNCOP_1, STRUCT_0, ALTCAT_1;
constructors SETFAM_1, ALTCAT_1, RELSET_1;
registrations XBOOLE_0, SETFAM_1, FUNCT_1, RELSET_1, ALTCAT_1, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI;
expansions TARSKI;
theorems FUNCOP_1, RELAT_1, FUNCT_2, ZFMISC_1, ALTCAT_1, TARSKI, FUNCT_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
A * B = idm o2;
end;
notation
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;
synonym B is_right_inverse_of A for A is_left_inverse_of B;
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
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
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:19;
then (idm o) * (idm o) = idm o by ALTCAT_1:def 17;
then idm o is_left_inverse_of idm o;
hence thesis;
end;
definition
let C be category, o1, o2 be Object of C such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o1^> <> {};
let A be Morphism of o1,o2 such that
A3: 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
A4: B1 is_right_inverse_of A by A3;
take B1;
consider B2 being Morphism of o2,o1 such that
A5: B2 is_left_inverse_of A by A3;
B1 = idm o1 * B1 by A2,ALTCAT_1:20
.= B2 * A * B1 by A5
.= B2 * (A * B1) by A1,A2,ALTCAT_1:21
.= B2 * idm o2 by A4
.= B2 by A2,ALTCAT_1:def 17;
hence thesis by A4,A5;
end;
uniqueness
proof
let M1,M2 be Morphism of o2,o1 such that
A6: M1 is_left_inverse_of A and
M1 is_right_inverse_of A and
M2 is_left_inverse_of A and
A7: M2 is_right_inverse_of A;
thus M1 = M1 * idm o2 by A2,ALTCAT_1:def 17
.= M1 * (A * M2) by A7
.= M1 * A * M2 by A1,A2,ALTCAT_1:21
.= idm o1 * M2 by A6
.= M2 by A2,ALTCAT_1:20;
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 thesis;
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^> <> {} and
A2: <^o2,o1^> <> {};
let A be Morphism of o1,o2;
assume
A3: A is retraction & A is coretraction;
then A" is_left_inverse_of A by A1,A2,Def4;
then
A4: A" is retraction;
A5: A" is_right_inverse_of A by A1,A2,A3,Def4;
then A" is coretraction;
then
A6: (A")" is_right_inverse_of A" by A1,A2,A4,Def4;
thus (A")" = idm o2 * ((A")") by A1,ALTCAT_1:20
.= A * A" * (A")" by A5
.= A * (A" * (A")") by A1,A2,ALTCAT_1:21
.= A * idm o1 by A6
.= A by A1,ALTCAT_1:def 17;
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:19;
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 17
.= idm o by A2;
end;
definition
let C be category, o1, o2 be Object of C, A be Morphism of o1,o2;
attr A is iso means
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
A1: A is iso;
then A * A" = idm o2;
then A" is_right_inverse_of A;
hence A is retraction;
A" * A = idm o1 by A1;
then A" is_left_inverse_of A;
hence thesis;
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
A2: A is retraction & A is coretraction;
then A" is_right_inverse_of A by A1,Def4;
then
A3: A * A" = idm o2;
A" is_left_inverse_of A by A1,A2,Def4;
then A" * A = idm o1;
hence thesis by A3;
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 that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o1^> <> {};
assume that
A4: A is iso and
A5: B is iso;
consider A1 be Morphism of o2,o1 such that
A6: A1 = A";
A7: <^o2,o1^> <> {} by A2,A3,ALTCAT_1:def 2;
then
A8: A is retraction & A is coretraction by A1,A4,Th6;
consider B1 be Morphism of o3,o2 such that
A9: B1 = B";
A10: <^o3,o2^> <> {} by A1,A3,ALTCAT_1:def 2;
then
A11: B is retraction & B is coretraction by A2,A5,Th6;
A12: (B*A)*(A1*B1) = B*(A*(A1*B1)) by A1,A2,A3,ALTCAT_1:21
.= B*(A*A1*B1) by A1,A7,A10,ALTCAT_1:21
.= B*((idm o2)*B1) by A1,A7,A8,A6,Th2
.= B*B1 by A10,ALTCAT_1:20
.= idm o3 by A2,A10,A11,A9,Th2;
then
A13: (A1*B1) is_right_inverse_of (B*A);
then
A14: (B*A) is retraction;
A15: <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
then
A16: (A1*B1)*(B*A) = A1*(B1*(B*A)) by A7,A10,ALTCAT_1:21
.= A1*(B1*B*A) by A1,A2,A10,ALTCAT_1:21
.= A1*((idm o2)*A) by A2,A10,A11,A9,Th2
.= A1*A by A1,ALTCAT_1:20
.= idm o1 by A1,A7,A8,A6,Th2;
then
A17: (A1*B1) is_left_inverse_of (B*A);
then (B*A) is coretraction;
then A1*B1 = (B*A)" by A3,A15,A17,A13,A14,Def4;
hence thesis by A6,A9,A16,A12;
end;
definition
let C be category, o1, o2 be Object of C;
pred o1,o2 are_iso means
<^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:19;
take idm o;
set A = idm o;
A2: A"*A = A * A by Th4
.= idm o by A1,ALTCAT_1:def 17;
A*A" = A * A by Th4
.= idm o by A1,ALTCAT_1:def 17;
hence thesis by A2;
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;
thus <^o2,o1^> <> {} & <^o1,o2^> <> {} by A3;
consider A being Morphism of o1,o2 such that
A5: A is iso by A4;
take A1 = A";
A6: A is retraction & A is coretraction by A5,Th5;
then
A7: A1"*A1 = A * A" by A3,Th3
.= idm o2 by A3,A6,Th2;
A1*A1" = A" * A by A3,A6,Th3
.= idm o1 by A3,A6,Th2;
hence thesis by A7;
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,o3^> <> {} by A1,A2;
consider B being Morphism of o2,o3 such that
A4: B is iso by A2;
consider A being Morphism of o1,o2 such that
A5: A is iso by A1;
<^o2,o1^> <> {} & <^o3,o2^> <> {} by A1,A2;
hence
A6: <^o1,o3^> <> {} & <^o3,o1^> <> {} by A3,ALTCAT_1:def 2;
take B * A;
thus thesis by A3,A6,A5,A4,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
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
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 that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
let A be Morphism of o1,o2, B be Morphism of o2,o3;
assume that
A3: A is mono and
A4: B is mono;
let o be Object of C;
assume
A5: <^o,o1^> <> {};
then
A6: <^o,o2^> <> {} by A1,ALTCAT_1:def 2;
let M1,M2 be Morphism of o,o1;
assume
A7: (B*A)*M1 = (B*A)*M2;
(B*A)*M1 = B*(A*M1) & (B*A)*M2 = B*(A*M2) by A1,A2,A5,ALTCAT_1:21;
then A*M1 = A*M2 by A4,A7,A6;
hence thesis by A3,A5;
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 that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
let A be Morphism of o1,o2, B be Morphism of o2,o3;
assume that
A3: A is epi and
A4: B is epi;
let o be Object of C;
assume
A5: <^o3,o^> <> {};
then
A6: <^o2,o^> <> {} by A2,ALTCAT_1:def 2;
let M1,M2 be Morphism of o3,o;
assume
A7: M1*(B*A) = M2*(B*A);
M1*(B*A) = (M1*B)*A & M2*(B*A) = (M2*B)*A by A1,A2,A5,ALTCAT_1:21;
then M1*B = M2*B by A3,A7,A6;
hence thesis by A4,A5;
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;
(B*A)*M1 = B*(A*M1) & (B*A)*M2 = B*(A*M2) by A1,A3,ALTCAT_1:21;
hence thesis by A2,A3,A4;
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;
(M1*B)*A = M1*(B*A) & (M2*B)*A = M2*(B*A) by A1,A3,ALTCAT_1:21;
hence thesis by A2,A3,A4;
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 17
.= C by A1,A2,ALTCAT_1:def 17;
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:20
.= C by A3,A4,ALTCAT_1:20;
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
set o = o1;
assume
A4: A is mono;
assume not F is one-to-one;
then consider x1,x2 be object such that
A5: x1 in dom F and
A6: x2 in dom F and
A7: F.x1 = F.x2 and
A8: x1 <> x2 by FUNCT_1:def 4;
set C = o --> x2;
set B = o --> x1;
A9: dom C = o by FUNCOP_1:13;
A10: rng C c= o1
proof
let y be object;
assume y in rng C;
then ex x be object st x in dom C & C.x = y by FUNCT_1:def 3;
hence thesis by A3,A6,A9,FUNCOP_1:7;
end;
then
A11: dom (F * C) = o by A3,A9,RELAT_1:27;
C in Funcs(o,o1) by A9,A10,FUNCT_2:def 2;
then reconsider C1=C as Morphism of o,o1 by ALTCAT_1:def 14;
set o9 = the Element of o;
A12: <^o,o1^> <> {} by ALTCAT_1:19;
B.o9 = x1 by A3,A5,FUNCOP_1:7;
then
A13: B.o9 <> C.o9 by A3,A5,A8,FUNCOP_1:7;
A14: dom B = o by FUNCOP_1:13;
A15: rng B c= o1
proof
let y be object;
assume y in rng B;
then ex x be object st x in dom B & B.x = y by FUNCT_1:def 3;
hence thesis by A3,A5,A14,FUNCOP_1:7;
end;
then B in Funcs(o,o1) by A14,FUNCT_2:def 2;
then reconsider B1=B as Morphism of o,o1 by ALTCAT_1:def 14;
A16: dom (F * B) = o by A3,A14,A15,RELAT_1:27;
now
let z be object;
assume
A17: z in o;
hence (F * B).z = F.(B.z) by A16,FUNCT_1:12
.= F.x2 by A7,A17,FUNCOP_1:7
.= F.(C.z) by A17,FUNCOP_1:7
.= (F * C).z by A11,A17,FUNCT_1:12;
end;
then F * B = F * C by A16,A11,FUNCT_1:2;
then A * B1 = F * C by A1,A2,A12,ALTCAT_1:16
.= A * C1 by A1,A2,A12,ALTCAT_1:16;
hence contradiction by A4,A12,A13;
end;
thus F is one-to-one implies A is mono
proof
assume
A18: F is one-to-one;
let o be Object of EnsCat X;
assume
A19: <^o,o1^> <> {};
then
A20: <^o,o2^> <> {} by A1,ALTCAT_1:def 2;
let B,C be Morphism of o,o1;
A21: <^o,o1^> = Funcs(o,o1) by ALTCAT_1:def 14;
then consider B1 be Function such that
A22: B1 = B and
A23: dom B1 = o and
A24: rng B1 c= o1 by A19,FUNCT_2:def 2;
consider C1 be Function such that
A25: C1 = C and
A26: dom C1 = o and
A27: rng C1 c= o1 by A19,A21,FUNCT_2:def 2;
assume A * B = A * C;
then
A28: F * B1 = A * C by A1,A2,A19,A22,A20,ALTCAT_1:16
.= F * C1 by A1,A2,A19,A25,A20,ALTCAT_1:16;
now
let z be object;
assume
A29: z in o;
then F.(B1.z) = (F*B1).z by A23,FUNCT_1:13;
then
A30: F.(B1.z) = F.(C1.z) by A26,A28,A29,FUNCT_1:13;
B1.z in rng B1 & C1.z in rng C1 by A23,A26,A29,FUNCT_1:def 3;
hence B1.z = C1.z by A3,A18,A24,A27,A30,FUNCT_1:def 4;
end;
hence thesis by A22,A23,A25,A26,FUNCT_1:2;
end;
end;
suppose
A31: o2 = {};
then F = {};
hence A is mono implies F is one-to-one;
thus F is one-to-one implies A is mono
proof
set x = the Element of Funcs(o1,o2);
assume F is one-to-one;
let o be Object of EnsCat X;
assume
A32: <^o,o1^> <> {};
<^o1,o2^> = Funcs(o1,o2) by ALTCAT_1:def 14;
then consider f be Function such that
f = x and
A33: dom f = o1 and
A34: rng f c= o2 by A1,FUNCT_2:def 2;
let B,C be Morphism of o,o1;
A35: <^o,o1^> = Funcs(o,o1) by ALTCAT_1:def 14;
then consider B1 be Function such that
A36: B1 = B and
A37: dom B1 = o and
A38: rng B1 c= o1 by A32,FUNCT_2:def 2;
rng f = {} by A31,A34,XBOOLE_1:3;
then dom f = {} by RELAT_1:42;
then
A39: rng B1 = {} by A38,A33,XBOOLE_1:3;
then
A40: dom B1 = {} by RELAT_1:42;
assume A * B = A * C;
consider C1 be Function such that
A41: C1 = C and
A42: dom C1 = o and
rng C1 c= o1 by A32,A35,FUNCT_2:def 2;
B1 = {} by A39,RELAT_1:41
.= C1 by A37,A42,A40,RELAT_1:41;
hence thesis by A36,A41;
end;
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 = {};
then F = {};
hence thesis by A4,FUNCT_2:def 3,RELAT_1:38;
end;
suppose
A5: o2 <> {};
A6: o1 is Element of X by ALTCAT_1:def 14;
then o1 is trivial by A3;
then consider z be object such that
A7: o1 = {z} by A6,ZFMISC_1:131;
dom F = {z} by A5,A7,FUNCT_2:def 1;
then
A8: rng F <> {} by RELAT_1:42;
o2 is Element of X by ALTCAT_1:def 14;
then o2 is trivial by A3;
then consider y be object such that
A9: o2 = {y} by A5,ZFMISC_1:131;
rng F c= {y} by A9,RELAT_1:def 19;
then rng F = {y} by A8,ZFMISC_1:33;
hence thesis by A9,FUNCT_2:def 3;
end;
end;
hence thesis;
end;
thus F is onto implies A is epi
proof
assume
A10: F is onto;
let o be Object of EnsCat X;
assume
A11: <^o2,o^> <> {};
then
A12: <^o1,o^> <> {} by A1,ALTCAT_1:def 2;
let B,C be Morphism of o2,o;
A13: <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 14;
then consider B1 be Function such that
A14: B1 = B and
A15: dom B1 = o2 and
rng B1 c= o by A11,FUNCT_2:def 2;
consider C1 be Function such that
A16: C1 = C and
A17: dom C1 = o2 and
rng C1 c= o by A11,A13,FUNCT_2:def 2;
assume B * A = C * A;
then
A18: B1 * F = C * A by A1,A2,A11,A14,A12,ALTCAT_1:16
.= C1 * F by A1,A2,A11,A16,A12,ALTCAT_1:16;
now
assume B1 <> C1;
then consider z be object such that
A19: z in o2 and
A20: B1.z <> C1.z by A15,A17,FUNCT_1:2;
z in rng F by A10,A19,FUNCT_2:def 3;
then consider x be object such that
A21: x in dom F and
A22: F.x = z by FUNCT_1:def 3;
B1.(F.x) = (B1*F).x by A21,FUNCT_1:13;
hence contradiction by A18,A20,A21,A22,FUNCT_1:13;
end;
hence thesis by A14,A16;
end;
end;
suppose
A23: ex x be set st x in X & x is non trivial;
now
per cases;
suppose
A24: o2 <> {};
consider o be set such that
A25: o in X and
A26: o is non trivial by A23;
reconsider o as Object of EnsCat X by A25,ALTCAT_1:def 14;
A27: dom F = o1 by A24,FUNCT_2:def 1;
thus A is epi implies F is onto
proof
set k = the Element of o;
A28: rng F c= o2 by RELAT_1:def 19;
reconsider ok = (o\{k}) as non empty set by A26,ZFMISC_1:139;
assume that
A29: A is epi and
A30: not F is onto;
rng F <> o2 by A30,FUNCT_2:def 3;
then not o2 c= rng F by A28,XBOOLE_0:def 10;
then consider y be object such that
A31: y in o2 and
A32: not y in rng F;
set C = o2 --> k;
A33: dom C = o2 by FUNCOP_1:13;
A34: o <> {} by A25;
then
A35: k in o;
rng C c= o
proof
let y be object;
assume y in rng C;
then ex x be object st x in dom C & C.x = y by FUNCT_1:def 3;
hence thesis by A35,A33,FUNCOP_1:7;
end;
then C in Funcs(o2,o) by A33,FUNCT_2:def 2;
then reconsider C1=C as Morphism of o2,o by ALTCAT_1:def 14;
set l = the Element of ok;
A36: not l in {k} by XBOOLE_0:def 5;
reconsider l as Element of o by XBOOLE_0:def 5;
A37: k <> l by A36,TARSKI:def 1;
deffunc G(object) = IFEQ($1,y,l,k);
consider B be Function such that
A38: dom B = o2 and
A39: for x be object st x in o2 holds B.x = G(x) from FUNCT_1:sch 3;
A40: dom (B*F) = o1 by A27,A28,A38,RELAT_1:27;
A41: rng B c= o
proof
let y1 be object;
assume y1 in rng B;
then consider x be object such that
A42: x in dom B & B.x = y1 by FUNCT_1:def 3;
per cases;
suppose
A43: x = y;
y1 = IFEQ(x,y,l,k) by A38,A39,A42
.= l by A43,FUNCOP_1:def 8;
hence thesis by A34;
end;
suppose
A44: x <> y;
y1 = IFEQ(x,y,l,k) by A38,A39,A42
.= k by A44,FUNCOP_1:def 8;
hence thesis by A34;
end;
end;
then
A45: B in Funcs(o2,o) by A38,FUNCT_2:def 2;
then
A46: B in <^o2,o^> by ALTCAT_1:def 14;
reconsider B1=B as Morphism of o2,o by A45,ALTCAT_1:def 14;
for z be object holds z in rng(B*F) implies z in rng B
by FUNCT_1:14;
then rng (B*F) c= rng B;
then rng (B*F) c= o by A41;
then (B*F) in Funcs(o1,o) by A40,FUNCT_2:def 2;
then
A47: (B*F) in <^o1,o^> by ALTCAT_1:def 14;
B.y = IFEQ(y,y,l,k) by A31,A39
.= l by FUNCOP_1:def 8;
then
A48: not B = C by A31,A37,FUNCOP_1:7;
A49: dom (C*F) = o1 by A27,A28,A33,RELAT_1:27;
now
let z be object;
assume
A50: z in o1;
then
A51: F.z in rng F by A27,FUNCT_1:def 3;
then
A52: B.(F.z) = IFEQ((F.z),y,l,k) by A28,A39
.= k by A32,A51,FUNCOP_1:def 8;
thus (B * F).z = B.(F.z) by A40,A50,FUNCT_1:12
.= C.(F.z) by A28,A51,A52,FUNCOP_1:7
.= (C * F).z by A49,A50,FUNCT_1:12;
end;
then B * F = C * F by A40,A49,FUNCT_1:2;
then B1 * A = C * F by A1,A2,A46,A47,ALTCAT_1:16
.= C1 * A by A1,A2,A46,A47,ALTCAT_1:16;
hence contradiction by A29,A48,A46;
end;
thus F is onto implies A is epi
proof
assume
A53: F is onto;
let o be Object of EnsCat X;
assume
A54: <^o2,o^> <> {};
then
A55: <^o1,o^> <> {} by A1,ALTCAT_1:def 2;
let B,C be Morphism of o2,o;
A56: <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 14;
then consider B1 be Function such that
A57: B1 = B and
A58: dom B1 = o2 and
rng B1 c= o by A54,FUNCT_2:def 2;
consider C1 be Function such that
A59: C1 = C and
A60: dom C1 = o2 and
rng C1 c= o by A54,A56,FUNCT_2:def 2;
assume B * A = C * A;
then
A61: B1 * F = C * A by A1,A2,A54,A57,A55,ALTCAT_1:16
.= C1 * F by A1,A2,A54,A59,A55,ALTCAT_1:16;
now
assume B1 <> C1;
then consider z be object such that
A62: z in o2 and
A63: B1.z <> C1.z by A58,A60,FUNCT_1:2;
z in rng F by A53,A62,FUNCT_2:def 3;
then consider x be object such that
A64: x in dom F and
A65: F.x = z by FUNCT_1:def 3;
B1.(F.x) = (B1*F).x by A64,FUNCT_1:13;
hence contradiction by A61,A63,A64,A65,FUNCT_1:13;
end;
hence thesis by A57,A59;
end;
end;
suppose
A66: o2 = {};
then F = {};
hence A is epi implies F is onto by A66,FUNCT_2:def 3,RELAT_1:38;
thus F is onto implies A is epi
proof
assume F is onto;
let o be Object of EnsCat X;
assume
A67: <^o2,o^> <> {};
let B,C be Morphism of o2,o;
A68: <^o2,o^> = Funcs(o2,o) by ALTCAT_1:def 14;
then consider B1 be Function such that
A69: B1 = B and
A70: dom B1 = o2 and
rng B1 c= o by A67,FUNCT_2:def 2;
A71: ex C1 be Function st C1 = C & dom C1 = o2 & rng C1 c= o by A67,A68,
FUNCT_2:def 2;
assume B * A = C * A;
B1 = {} by A66,A70,RELAT_1:41;
hence thesis by A66,A69,A71,RELAT_1:41;
end;
end;
end;
hence thesis;
end;
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;
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 17
.= B * (A * R) by A2
.= C * A * R by A1,A3,A4,ALTCAT_1:21
.= C * (A * R) by A1,A3,ALTCAT_1:21
.= C * idm o2 by A2
.= C by A3,ALTCAT_1:def 17;
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;
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:20
.= R * A * B by A2
.= R * (A * C) by A1,A3,A4,ALTCAT_1:21
.= R * A * C by A1,A3,ALTCAT_1:21
.= idm o1 * C by A2
.= C by A3,ALTCAT_1:20;
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 <^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
A4: <^o2,o^> <> {};
let B, C be Morphism of o2, o;
assume B * A = C * A;
then B * (A * A") = (C * A) * A" by A1,A4,ALTCAT_1:21;
then B * idm o2 = (C * A) * A" by A1,A2,Th2;
then B * idm o2 = C * (A * A") by A1,A4,ALTCAT_1:21;
then B * idm o2 = C * idm o2 by A1,A2,Th2;
then B = C * idm o2 by A4,ALTCAT_1:def 17;
hence thesis by A4,ALTCAT_1:def 17;
end;
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
A5: <^o,o1^> <> {};
let B, C be Morphism of o, o1;
assume A * B = A * C;
then (A" * A) * B = A" * (A * C) by A1,A5,ALTCAT_1:21;
then idm o1 * B = A" * (A * C) by A1,A2,Th2;
then idm o1 * B = (A" * A) * C by A1,A5,ALTCAT_1:21;
then idm o1 * B = idm o1 * C by A1,A2,Th2;
then B = idm o1 * C by A5,ALTCAT_1:20;
hence thesis by A5,ALTCAT_1:20;
end;
hence thesis by A3;
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 that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o1^> <> {};
A4: <^o2,o1^> <> {} by A2,A3,ALTCAT_1:def 2;
A5: <^o3,o2^> <> {} by A1,A3,ALTCAT_1:def 2;
let A be Morphism of o1,o2, B be Morphism of o2,o3;
assume that
A6: A is retraction and
A7: B is retraction;
consider A1 being Morphism of o2,o1 such that
A8: A1 is_right_inverse_of A by A6;
consider B1 being Morphism of o3,o2 such that
A9: B1 is_right_inverse_of B by A7;
consider G being Morphism of o3,o1 such that
A10: G = A1 * B1;
take G;
(B * A) * G = B * (A * (A1 * B1)) by A1,A2,A3,A10,ALTCAT_1:21
.= B * ((A * A1) * B1) by A1,A4,A5,ALTCAT_1:21
.= B * (idm o2 * B1) by A8
.= B * B1 by A5,ALTCAT_1:20
.= idm o3 by A9;
hence thesis;
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 that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o1^> <> {};
A4: <^o2,o1^> <> {} by A2,A3,ALTCAT_1:def 2;
A5: <^o3,o2^> <> {} by A1,A3,ALTCAT_1:def 2;
let A be Morphism of o1,o2, B be Morphism of o2,o3;
assume that
A6: A is coretraction and
A7: B is coretraction;
consider A1 being Morphism of o2,o1 such that
A8: A1 is_left_inverse_of A by A6;
consider B1 being Morphism of o3,o2 such that
A9: B1 is_left_inverse_of B by A7;
consider G being Morphism of o3,o1 such that
A10: G = A1 * B1;
take G;
A11: <^o2,o2^> <> {} by ALTCAT_1:19;
G * (B * A) = ((A1 * B1) * B) * A by A1,A2,A3,A10,ALTCAT_1:21
.= (A1 * (B1 * B)) * A by A2,A4,A5,ALTCAT_1:21
.= (A1 * idm o2) * A by A9
.= A1 * (idm o2 *A) by A1,A4,A11,ALTCAT_1:21
.= A1 * A by A1,ALTCAT_1:20
.= idm o1 by A8;
hence thesis;
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 and
A2: A is mono and
A3: <^o1,o2^> <> {} and
A4: <^o2,o1^> <> {};
consider B being Morphism of o2,o1 such that
A5: B is_right_inverse_of A by A1;
A * B * A = (idm o2) * A by A5;
then A * (B * A) = (idm o2) * A by A3,A4,ALTCAT_1:21;
then A * (B * A) = A by A3,ALTCAT_1:20;
then
A6: <^o1,o1^> <> {} & A * (B * A) = A * idm o1 by A3,ALTCAT_1:19,def 17;
then B * A = idm o1 by A2;
then
A7: B is_left_inverse_of A;
then
A8: A is coretraction;
then
A9: A*A" = A * B by A1,A3,A4,A5,A7,Def4
.= idm o2 by A5;
A"*A = B * A by A1,A3,A4,A5,A7,A8,Def4
.= idm o1 by A2,A6;
hence thesis by A9;
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 and
A2: A is epi and
A3: <^o1,o2^> <> {} and
A4: <^o2,o1^> <> {};
consider B being Morphism of o2,o1 such that
A5: B is_left_inverse_of A by A1;
A * (B * A) = A * (idm o1) by A5;
then A * (B * A) = A by A3,ALTCAT_1:def 17;
then A * (B * A) = idm o2 * A by A3,ALTCAT_1:20;
then
A6: <^o2,o2^> <> {} & (A * B) * A = idm o2 * A by A3,A4,ALTCAT_1:19,21;
then A * B = idm o2 by A2;
then
A7: B is_right_inverse_of A;
then
A8: A is retraction;
then
A9: A"*A = B * A by A1,A3,A4,A5,A7,Def4
.= idm o1 by A5;
A*A" = A * B by A1,A3,A4,A5,A7,A8,Def4
.= idm o2 by A2,A6;
hence thesis by A9;
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);
(B * A) * G = idm o3 by A2;
then B * (A * G) = idm o3 by A1,ALTCAT_1:21;
then A * G is_right_inverse_of B;
hence thesis;
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);
A3: (G * B) * A = G * (B * A) by A1,ALTCAT_1:21;
G * (B * A) = idm o1 by A2;
then G * B is_left_inverse_of A by A3;
hence thesis;
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 that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
A4: A is retraction by A1;
A is coretraction
proof
consider A1 be Morphism of b,a such that
A5: A1 is_right_inverse_of A by A4;
A1 * (A * A1) =A1 * idm b by A5;
then A1 * (A * A1) =A1 by A3,ALTCAT_1:def 17;
then (A1 * A) * A1 =A1 by A2,A3,ALTCAT_1:21;
then
A6: (A1 * A) * A1 =idm a * A1 by A3,ALTCAT_1:20;
A1 is epi & <^a,a^> <> {} by A1,A2,A3,Th15,ALTCAT_1:19;
then (A1 * A) =idm a by A6;
then A1 is_left_inverse_of A;
hence thesis;
end;
hence thesis by A2,A3,A4,Th6;
end;
end;
registration
let C be with_units non empty AltCatStr, o be Object of C;
cluster mono epi retraction coretraction for Morphism of o,o;
existence
proof
take idm o;
thus thesis by Lm1,Th1;
end;
end;
registration
let C be category, o be Object of C;
cluster mono epi iso retraction coretraction for Morphism of o,o;
existence
proof
take I = idm o;
<^o,o^> <> {} & I is retraction coretraction by Th1,ALTCAT_1:19;
hence thesis by Th15,Th16,Th20;
end;
end;
registration
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:19;
hence thesis by Th9;
end;
end;
registration
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:19;
hence thesis by Th10;
end;
end;
registration
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:19;
hence thesis by Th7;
end;
end;
registration
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:19;
hence thesis by Th18;
end;
end;
registration
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:19;
hence thesis by Th19;
end;
end;
definition
let C be AltGraph, o be Object of C;
attr o is initial means
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^> and
A3: <^o,o1^> is trivial by A1;
ex i be object st <^o,o1^> = { i } by A2,A3,ZFMISC_1:131;
then <^o,o1^> = {M} by 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 object;
assume
A8: x in <^o,o1^>;
then reconsider M1 = x as Morphism of o,o1;
M1 = M by A6,A8;
hence thesis by TARSKI:def 1;
end;
{M} c= <^o,o1^>
by A5,TARSKI:def 1;
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;
ex N being Morphism of o2,o2 st N in <^o2,o2^> & <^o2,o2^> is trivial by A2;
then consider y being object such that
A3: <^o2,o2^> = {y} by ZFMISC_1:131;
consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> and
<^o2,o1^> is trivial by A2;
consider M1 being Morphism of o1,o2 such that
A5: M1 in <^o1,o2^> and
<^o1,o2^> is trivial by A1;
thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A5,A4;
M1 * M2 = y & idm o2 = y by A3,TARSKI:def 1;
then M2 is_right_inverse_of M1;
then
A6: M1 is retraction;
ex M being Morphism of o1,o1 st M in <^o1,o1^> & <^o1,o1^> is trivial by A1;
then consider x being object such that
A7: <^o1,o1^> = {x} by ZFMISC_1:131;
M2 * M1 = x & idm o1 = x by A7,TARSKI:def 1;
then M2 is_left_inverse_of M1;
then M1 is coretraction;
then M1 is iso by A5,A4,A6,Th6;
hence thesis;
end;
definition
let C be AltGraph, o be Object of C;
attr o is terminal means
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^> and
A3: <^o1,o^> is trivial by A1;
ex i be object st <^o1,o^> = { i } by A2,A3,ZFMISC_1:131;
then <^o1,o^> = {M} by 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 object;
assume
A8: x in <^o1,o^>;
then reconsider M1 = x as Morphism of o1,o;
M1 = M by A6,A8;
hence thesis by TARSKI:def 1;
end;
{M} c= <^o1,o^>
by A5,TARSKI:def 1;
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;
ex M being Morphism of o1,o1 st M in <^o1,o1^> & <^o1,o1^> is trivial by A1;
then consider x being object such that
A3: <^o1,o1^> = {x} by ZFMISC_1:131;
consider M2 being Morphism of o2,o1 such that
A4: M2 in <^o2,o1^> and
<^o2,o1^> is trivial by A1;
consider M1 being Morphism of o1,o2 such that
A5: M1 in <^o1,o2^> and
<^o1,o2^> is trivial by A2;
thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A5,A4;
M2 * M1 = x by A3,TARSKI:def 1;
then M2 * M1 = idm o1 by A3,TARSKI:def 1;
then M2 is_left_inverse_of M1;
then
A6: M1 is coretraction;
ex N being Morphism of o2,o2 st N in <^o2,o2^> & <^o2,o2^> is trivial by A2;
then consider y being object such that
A7: <^o2,o2^> = {y} by ZFMISC_1:131;
M1 * M2 = y by A7,TARSKI:def 1;
then M1 * M2 = idm o2 by A7,TARSKI:def 1;
then M2 is_right_inverse_of M1;
then M1 is retraction;
then M1 is iso by A5,A4,A6,Th6;
hence thesis;
end;
definition
let C be AltGraph, o be Object of C;
attr o is _zero means
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
by Th26;
definition
let C be non empty AltCatStr, o1, o2 be Object of C, M be Morphism of o1,o2;
attr M is _zero means
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;
then consider B1 being Morphism of o,o2 such that
A5: B1 in <^o,o2^> and
<^o,o2^> is trivial;
let A be Morphism of o1,o, B be Morphism of o,o3;
consider B2 being Morphism of o,o3 such that
A6: B2 in <^o,o3^> and
A7: <^o,o3^> is trivial by A4;
consider y being object such that
A8: <^o,o3^> = {y} by A6,A7,ZFMISC_1:131;
A9: o is terminal by A3;
then consider A1 being Morphism of o1,o such that
A10: A1 in <^o1,o^> and
A11: <^o1,o^> is trivial;
consider x being object such that
A12: <^o1,o^> = {x} by A10,A11,ZFMISC_1:131;
ex M being Morphism of o,o st M in <^o,o^> & <^o,o^> is trivial by A9;
then consider z being object such that
A13: <^o,o^> = {z} by ZFMISC_1:131;
consider A2 being Morphism of o2,o such that
A14: A2 in <^o2,o^> and
<^o2,o^> is trivial by A9;
A15: idm o = z & A2 * B1 = z by A13,TARSKI:def 1;
A16: B = y & B2 = y by A8,TARSKI:def 1;
A17: A = x & A1 = x by A12,TARSKI:def 1;
A18: <^o2,o3^> <> {} by A6,A14,ALTCAT_1:def 2;
M2 = B2 * A2 by A2,A3;
hence M2 * M1 = (B2*A2) * (B1*A1) by A1,A3
.= B2*A2 * B1*A1 by A5,A10,A18,ALTCAT_1:21
.= B*(idm o)*A by A5,A6,A14,A17,A16,A15,ALTCAT_1:21
.= B*A by A6,ALTCAT_1:def 17;
end;