Copyright (c) 1989 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCOP_1, PARTFUN1, TARSKI, WELLORD1,
CAT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FUNCOP_1;
constructors FUNCOP_1, WELLORD2, MEMBERED, PARTFUN1, XBOOLE_0;
clusters FUNCT_1, RELSET_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2,
XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, PARTFUN1, FUNCOP_1, SUBSET_1,
WELLORD2, RELAT_1, RELSET_1, XBOOLE_1;
schemes FUNCT_2;
begin :: Auxiliary theorems
reserve a,b,c,o,m for set;
canceled 3;
theorem Th4:
for X,Y,Z being set, D being non empty set, f being Function of X,D
st Y c= X & f.:Y c= Z holds f|Y is Function of Y,Z
proof let X,Y,Z be set, D be non empty set, f be Function of X,D;
assume that
A1: Y c= X and
A2: f.:Y c= Z;
dom f = X by FUNCT_2:def 1;
then A3: dom(f|Y) = Y by A1,RELAT_1:91;
A4: rng(f|Y) c= Z by A2,RELAT_1:148;
now assume Z = {}; then rng(f|Y) = {} by A4,XBOOLE_1:3;
hence Y = {} by A3,RELAT_1:65;
end;
hence f|Y is Function of Y,Z by A3,A4,FUNCT_2:def 1,RELSET_1:11;
end;
definition let A be non empty set,b;
redefine func A --> b -> Function of A,{b};
coherence
proof {b} <> {} &
dom(A --> b) = A & rng(A --> b) c= {b} by FUNCOP_1:19;
hence thesis by FUNCT_2:def 1,RELSET_1:11;
end;
end;
definition let a,b,c;
func (a,b).-->c -> PartFunc of [:{a},{b}:],{c} equals
:Def1: {[a,b]} --> c;
correctness
proof [:{a},{b}:] = {[a,b]} by ZFMISC_1:35;
hence thesis;
end;
end;
canceled 2;
theorem Th7:
dom (a,b).-->c = {[a,b]} & dom (a,b).-->c = [:{a},{b}:]
proof (a,b).-->c = {[a,b]} --> c by Def1;
hence dom (a,b).-->c = {[a,b]} by FUNCT_2:def 1;
hence dom (a,b).-->c = [:{a},{b}:] by ZFMISC_1:35;
end;
theorem Th8:
((a,b).-->c).[a,b] = c
proof [:{a},{b}:] = {[a,b]} & [a,b] in {[a,b]} & (a,b).-->c = {[a,b]} --> c
by Def1,TARSKI:def 1,ZFMISC_1:35;
hence thesis by FUNCT_2:65;
end;
theorem Th9:
for x being Element of {a} for y being Element of {b}
holds ((a,b).-->c).[x,y] = c
proof let x be Element of {a}; let y be Element of {b};
x = a & y = b by TARSKI:def 1; hence thesis by Th8;
end;
:: Structure of a Category
definition
struct CatStr
(# Objects,Morphisms -> non empty set,
Dom,Cod -> Function of the Morphisms, the Objects,
Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
Id -> Function of the Objects, the Morphisms
#);
end;
reserve C for CatStr;
definition let C;
mode Object of C is Element of the Objects of C;
mode Morphism of C is Element of the Morphisms of C;
end;
reserve a,b,c,d for Object of C;
reserve f,g for Morphism of C;
:: Domain and Codomain of a Morphism
definition let C,f;
func dom(f) -> Object of C equals
:Def2: (the Dom of C).f;
correctness;
func cod(f) -> Object of C equals
:Def3: (the Cod of C).f;
correctness;
end;
definition let C,f,g;
assume A1: [g,f] in dom(the Comp of C);
func g*f -> Morphism of C equals
:Def4: ( the Comp of C ).[g,f];
coherence by A1,PARTFUN1:27;
end;
definition let C,a;
func id (a) -> Morphism of C equals
:Def5: ( the Id of C ).a;
correctness;
end;
definition let C,a,b;
func Hom(a,b) -> Subset of the Morphisms of C equals
:Def6: { f : dom(f)=a & cod(f)=b };
correctness
proof set M = { f : dom(f)=a & cod(f)=b };
M c= the Morphisms of C
proof let x be set; assume x in M;
then ex f st x = f & dom(f)=a & cod(f)=b;
hence thesis;
end;
hence thesis;
end;
end;
canceled 8;
theorem Th18:
f in Hom(a,b) iff dom(f)=a & cod(f)=b
proof
A1: Hom(a,b) = { g : dom(g)=a & cod(g)=b } by Def6;
thus f in Hom(a,b) implies dom(f) = a & cod(f) = b
proof assume f in Hom(a,b);
then ex g st f = g & dom(g) = a & cod(g) = b by A1;
hence thesis;
end;
thus thesis by A1;
end;
theorem
Hom(dom(f),cod(f)) <> {} by Th18;
definition let C,a,b;
assume A1: Hom(a,b)<>{};
mode Morphism of a,b -> Morphism of C means
:Def7: it in Hom(a,b);
existence by A1,SUBSET_1:10;
end;
canceled;
theorem
for f being set st f in Hom(a,b) holds f is Morphism of a,b by Def7;
theorem Th22:
for f being Morphism of C holds f is Morphism of dom(f),cod(f)
proof let f be Morphism of C; f in Hom(dom(f),cod(f)) by Th18;
hence f is Morphism of dom(f),cod(f) by Def7;
end;
theorem Th23:
for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b
proof let f be Morphism of a,b;
assume Hom(a,b) <> {}; then f in Hom(a,b) by Def7;
hence dom(f) = a & cod(f) = b by Th18;
end;
theorem
for f being Morphism of a,b for h being Morphism of c,d
st Hom(a,b) <> {} & Hom(c,d) <> {} & f = h holds a = c & b = d
proof let f be Morphism of a,b; let h be Morphism of c,d;
assume Hom(a,b) <> {} & Hom(c,d) <> {};
then dom(f) = a & cod(f) = b & dom(h) = c & cod(h) = d by Th23;
hence thesis;
end;
theorem Th25:
for f being Morphism of a,b st Hom(a,b) = {f}
for g being Morphism of a,b holds f = g
proof let f be Morphism of a,b such that
A1: Hom(a,b) = {f};
let g be Morphism of a,b;
g in {f} by A1,Def7; hence thesis by TARSKI:def 1;
end;
theorem Th26:
for f being Morphism of a,b
st Hom(a,b) <> {} & for g being Morphism of a,b holds f = g
holds Hom(a,b) = {f}
proof let f be Morphism of a,b such that
A1: Hom(a,b) <> {} and
A2: for g being Morphism of a,b holds f = g;
for x being set holds x in Hom(a,b) iff x = f
proof let x be set;
thus x in Hom(a,b) implies x = f
proof
A3: Hom(a,b) = { g: dom(g)=a & cod(g)=b } by Def6;
assume x in Hom(a,b);
then consider g being Morphism of C such that
A4: x = g and
A5: dom(g)=a & cod(g)=b by A3;
g is Morphism of a,b by A5,Th22;
hence thesis by A2,A4;
end;
thus thesis by A1,Def7;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for f being Morphism of a,b st Hom(a,b),Hom(c,d) are_equipotent &
Hom(a,b) = {f}
holds ex h being Morphism of c,d st Hom(c,d) = {h}
proof let f be Morphism of a,b;
assume Hom(a,b),Hom(c,d) are_equipotent;
then consider F being Function such that F is one-to-one and
A1: dom F = Hom(a,b) & rng F = Hom(c,d) by WELLORD2:def 4;
assume Hom(a,b) = {f};
then A2: Hom(c,d) = {F.f} by A1,FUNCT_1:14;
then F.f in Hom(c,d) by TARSKI:def 1; then F.f is Morphism of c,d by Def7;
hence thesis by A2;
end;
Lm1:
now let o,m be set; let C be CatStr such that
A1: C = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #);
set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C,
CI = the Id of C;
thus for f,g being Element of the Morphisms of C holds
[g,f] in dom CP iff CD.g=CC.f
proof let f,g be Element of the Morphisms of C;
f = m & g = m & dom CP = {[m,m]} by A1,Th7,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
thus for f,g being Element of the Morphisms of C
st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g
proof let f,g be Element of the Morphisms of C;
CP.[g,f] = m by A1,Th9;
then reconsider gf = CP.[g,f] as Element of the Morphisms of C by A1,
TARSKI:def 1;
CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65;
hence thesis;
end;
thus for f,g,h being Element of the Morphisms of C
st CD.h = CC.g & CD.g = CC.f
holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f]
proof let f,g,h be Element of the Morphisms of C;
CP.[g,f] = m & CP.[h,g] = m by A1,Th9;
then reconsider gf = CP.[g,f],hg = CP.[h,g] as Element of the Morphisms of
C
by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,Th9;
hence thesis;
end;
let b be Element of the Objects of C;
b = o by A1,TARSKI:def 1;
hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65;
thus for f being Element of the Morphisms of C st CC.f = b
holds CP.[CI.b,f] = f
proof let f be Element of the Morphisms of C; f = m by A1,TARSKI:def 1;
hence thesis by A1,Th9;
end;
let g be Element of the Morphisms of C;
g = m by A1,TARSKI:def 1; hence CP.[g,CI.b] = g by A1,Th9;
end;
:: Category
definition let C be CatStr;
attr C is Category-like means
:Def8:
(for f,g being Element of the Morphisms of C holds
[g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f)
& (for f,g being Element of the Morphisms of C
st (the Dom of C).g=(the Cod of C).f holds
(the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f &
(the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g)
& (for f,g,h being Element of the Morphisms of C
st (the Dom of C).h = (the Cod of C).g &
(the Dom of C).g = (the Cod of C).f
holds (the Comp of C).[h,(the Comp of C).[g,f]]
= (the Comp of C).[(the Comp of C).[h,g],f] )
& (for b being Element of the Objects of C holds
(the Dom of C).((the Id of C).b) = b &
(the Cod of C).((the Id of C).b) = b &
(for f being Element of the Morphisms of C st (the Cod of C).f = b
holds (the Comp of C).[(the Id of C).b,f] = f ) &
(for g being Element of the Morphisms of C st (the Dom of C).g = b
holds (the Comp of C).[g,(the Id of C).b] = g ) );
end;
definition
cluster Category-like CatStr;
existence
proof take C = CatStr(# {0},{1},{1}-->0,{1}-->0,(1,1).-->1,{0}-->1 #);
thus (for f,g being Element of the Morphisms of C holds
[g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f)
& (for f,g being Element of the Morphisms of C
st (the Dom of C).g=(the Cod of C).f holds
(the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f &
(the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g)
& (for f,g,h being Element of the Morphisms of C
st (the Dom of C).h = (the Cod of C).g &
(the Dom of C).g = (the Cod of C).f
holds (the Comp of C).[h,(the Comp of C).[g,f]]
= (the Comp of C).[(the Comp of C).[h,g],f] )
& (for b being Element of the Objects of C holds
(the Dom of C).((the Id of C).b) = b &
(the Cod of C).((the Id of C).b) = b &
(for f being Element of the Morphisms of C st (the Cod of C).f = b
holds (the Comp of C).[(the Id of C).b,f] = f ) &
(for g being Element of the Morphisms of C st (the Dom of C).g = b
holds (the Comp of C).[g,(the Id of C).b] = g ) ) by Lm1;
end;
end;
definition
mode Category is Category-like CatStr;
end;
definition
cluster strict Category;
existence
proof
set C = CatStr(# {0},{1},{1}-->0,{1}-->0,(1,1).-->1,{0}-->1 #);
(for f,g being Element of the Morphisms of C holds
[g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f)
& (for f,g being Element of the Morphisms of C
st (the Dom of C).g=(the Cod of C).f holds
(the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f &
(the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g)
& (for f,g,h being Element of the Morphisms of C
st (the Dom of C).h = (the Cod of C).g &
(the Dom of C).g = (the Cod of C).f
holds (the Comp of C).[h,(the Comp of C).[g,f]]
= (the Comp of C).[(the Comp of C).[h,g],f] )
& (for b being Element of the Objects of C holds
(the Dom of C).((the Id of C).b) = b &
(the Cod of C).((the Id of C).b) = b &
(for f being Element of the Morphisms of C st (the Cod of C).f = b
holds (the Comp of C).[(the Id of C).b,f] = f ) &
(for g being Element of the Morphisms of C st (the Dom of C).g = b
holds (the Comp of C).[g,(the Id of C).b] = g ) ) by Lm1;
then C is Category by Def8;
hence thesis;
end;
end;
canceled;
theorem
for C being CatStr
st ( for f,g being Morphism of C
holds [g,f] in dom(the Comp of C) iff dom g = cod f )
& ( for f,g being Morphism of C st dom g = cod f
holds dom(g*f) = dom f & cod (g*f) = cod g )
& ( for f,g,h being Morphism of C st dom h = cod g & dom g = cod f
holds h*(g*f) = (h*g)*f )
& ( for b being Object of C
holds dom id b = b & cod id b = b &
(for f being Morphism of C st cod f = b holds (id b)*f = f) &
(for g being Morphism of C st dom g = b holds g*(id b) = g) )
holds C is Category-like
proof let C be CatStr;
set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C,
CI = the Id of C;
assume that
A1: for f,g being Morphism of C
holds [g,f] in dom CP iff dom g = cod f and
A2: for f,g being Morphism of C st dom g = cod f
holds dom(g*f) = dom f & cod (g*f) = cod g and
A3: for f,g,h being Morphism of C st dom h = cod g & dom g = cod f
holds h*(g*f) = (h*g)*f and
A4: for b being Object of C
holds dom id b = b & cod id b = b &
(for f being Morphism of C st cod f = b holds (id b)*f = f) &
(for g being Morphism of C st dom g = b holds g*(id b) = g);
thus
A5: for f,g being Element of the Morphisms of C
holds [g,f] in dom CP iff CD.g=CC.f
proof let f,g be Element of the Morphisms of C;
CD.g = dom g & CC.f = cod f by Def2,Def3;
hence thesis by A1;
end;
thus
A6: for f,g being Element of the Morphisms of C st CD.g=CC.f
holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g
proof let f,g be Element of the Morphisms of C such that
A7: CD.g=CC.f;
CD.g = dom g & CC.f = cod f by Def2,Def3;
then dom(g*f)=dom f & cod(g*f)=cod g & [g,f] in dom CP &
CD.(g*f) = dom(g*f) & CC.(g*f) = cod(g*f)
by A2,A5,A7,Def2,Def3;
then CD.(CP.[g,f]) = dom f & CC.(CP.[g,f]) = cod g by Def4;
hence thesis by Def2,Def3;
end;
thus for f,g,h being Element of the Morphisms of C
st CD.h = CC.g & CD.g = CC.f
holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f]
proof let f,g,h be Element of the Morphisms of C such that
A8: CD.h = CC.g & CD.g = CC.f;
A9: CD.h = dom h & CC.g = cod g & CD.g = dom g & CC.f = cod f
by Def2,Def3;
[g,f] in dom CP & [h,g] in dom CP by A5,A8;
then A10: g*f = CP.[g,f] & h*g = CP.[h,g] by Def4;
CD.(CP.[h,g]) = CD.g & CC.(CP.[g,f]) = CC.g by A6,A8;
then [h,g*f] in dom CP & [h*g,f] in dom CP by A5,A8,A10;
then CP.[h,g*f] = h*(g*f) & CP.[h*g,f] = (h*g)*f by Def4;
hence thesis by A3,A8,A9,A10;
end;
let b be Element of the Objects of C;
dom id b = b & cod id b = b & id b = CI.b by A4,Def5;
hence CD.(CI.b) = b & CC.(CI.b) = b by Def2,Def3;
thus for f being Element of the Morphisms of C st CC.f = b
holds CP.[CI.b,f] = f
proof let f be Element of the Morphisms of C such that
A11: CC.f = b;
A12: dom id b = b & id b = CI.b by A4,Def5;
then CD.(CI.b) = b & CC.f = cod f by Def2,Def3;
then (id b)*f = f & [CI.b,f] in dom CP by A4,A5,A11;
hence thesis by A12,Def4;
end;
let g be Element of the Morphisms of C such that
A13: CD.g = b;
A14: cod id b = b & id b = CI.b by A4,Def5;
then CC.(CI.b) = b & CD.g = dom g by Def2,Def3;
then g*(id b) = g & [g,CI.b] in dom CP by A4,A5,A13;
hence thesis by A14,Def4;
end;
definition let o,m;
func 1Cat(o,m) -> strict Category equals
:Def9: CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #);
correctness
proof
consider O,M being non empty set,d,c being (Function of M,O),
p being (PartFunc of [:M,M:],M),i being (Function of O,M),
C being CatStr such that
A1: O = {o} & M = {m} & d = {m}-->o & c = {m}-->o & p = (m,m).-->m
& i = {o}-->m & C = CatStr(# {o},{m},{m}-->o,{m}-->o,
(m,m).-->m,{o}-->m #);
(for f,g being Element of the Morphisms of C holds
[g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f)
& (for f,g being Element of the Morphisms of C
st (the Dom of C).g=(the Cod of C).f
holds
(the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f &
(the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g)
& (for f,g,h being Element of the Morphisms of C
st (the Dom of C).h = (the Cod of C).g &
(the Dom of C).g = (the Cod of C).f
holds
(the Comp of C).[h,(the Comp of C).[g,f]]
= (the Comp of C).[(the Comp of C).[h,g],f] )
& (for b being Element of the Objects of C
holds
(the Dom of C).((the Id of C).b) = b &
(the Cod of C).((the Id of C).b) = b &
(for f being Element of the Morphisms of C st (the Cod of C).f = b
holds (the Comp of C).[(the Id of C).b,f] = f ) &
(for g being Element of the Morphisms of C st (the Dom of C).g = b
holds (the Comp of C).[g,(the Id of C).b] = g ) ) by A1,Lm1;
hence thesis by A1,Def8;
end;
end;
canceled 2;
theorem
o is Object of 1Cat(o,m)
proof
1Cat(o,m) = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9;
hence thesis by TARSKI:def 1;
end;
theorem
m is Morphism of 1Cat(o,m)
proof 1Cat(o,m)=CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #)
by Def9;
hence thesis by TARSKI:def 1;
end;
theorem Th34:
for a being Object of 1Cat(o,m) holds a = o
proof let a be Object of 1Cat(o,m);
1Cat(o,m) = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9;
hence thesis by TARSKI:def 1;
end;
theorem Th35:
for f being Morphism of 1Cat(o,m) holds f = m
proof let f be Morphism of 1Cat(o,m);
1Cat(o,m) = CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #) by Def9;
hence thesis by TARSKI:def 1;
end;
theorem Th36:
for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m)
holds f in Hom(a,b)
proof let a,b be Object of 1Cat(o,m); let f be Morphism of 1Cat(o,m);
dom f = o & cod f = o by Th34; then dom f = a & cod f = b by Th34;
hence f in Hom(a,b) by Th18;
end;
theorem
for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m)
holds f is Morphism of a,b
proof let a,b be Object of 1Cat(o,m); let f be Morphism of 1Cat(o,m);
f in Hom(a,b) by Th36; hence thesis by Def7;
end;
theorem
for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {} by Th36;
theorem
for a,b,c,d being Object of 1Cat(o,m)
for f being Morphism of a,b for g being Morphism of c,d holds f=g
proof let a,b,c,d be Object of 1Cat(o,m);
let f be Morphism of a,b; let g be Morphism of c,d;
f = m & g = m by Th35; hence thesis;
end;
reserve B,C,D for Category;
reserve a,b,c,d for Object of C;
reserve f,f1,f2,g,g1,g2 for Morphism of C;
theorem Th40:
dom(g) = cod(f) iff [g,f] in dom(the Comp of C)
proof dom(g) = (the Dom of C).g & cod(f) = (the Cod of C).f by Def2,Def3;
hence thesis by Def8;
end;
theorem Th41:
dom(g) = cod(f) implies g*f = ( the Comp of C ).[g,f]
proof assume dom(g) = cod(f); then [g,f] in dom(the Comp of C) by Th40;
hence g*f = ( the Comp of C ).[g,f] by Def4;
end;
theorem Th42:
for f,g being Morphism of C
st dom(g) = cod(f) holds dom(g*f) = dom(f) & cod(g*f) = cod(g)
proof let f,g be Morphism of C;
assume
A1: dom(g) = cod(f);
then dom(g) = (the Dom of C).g & cod(g) = (the Cod of C).g &
dom(f) = (the Dom of C).f & cod(f) = (the Cod of C).f &
(the Dom of C).(g*f) = dom(g*f) & (the Cod of C).(g*f) = cod(g*f) &
(the Comp of C).[g,f] = g*f by Def2,Def3,Th41;
hence thesis by A1,Def8;
end;
theorem Th43:
for f,g,h being Morphism of C
st dom(h) = cod(g) & dom(g) = cod(f) holds h*(g*f) = (h*g)*f
proof let f,g,h be Morphism of C; assume
A1: dom(h) = cod(g) & dom(g) = cod(f);
then cod(g*f) = cod(g) & dom(h*g) = dom(g) by Th42;
then dom(g) = (the Dom of C).g & cod(g) = (the Cod of C).g &
dom(h) = (the Dom of C).h & cod(f) = (the Cod of C).f &
(the Dom of C).(g*f) = dom(g*f) & (the Cod of C).(g*f) = cod(g*f) &
(the Comp of C).[h,g*f] = h*(g*f) & (the Comp of C).[h*g,f] = (h*g)*f &
(the Comp of C).[h,g] = h*g & (the Comp of C).[g,f] = g*f
by A1,Def2,Def3,Th41;
hence thesis by A1,Def8;
end;
theorem Th44:
dom(id b) = b & cod(id b) = b
proof dom(id b) = (the Dom of C).(id b) & cod(id b) = (the Cod of C).(id b) &
id b = (the Id of C).b by Def2,Def3,Def5;
hence thesis by Def8;
end;
theorem Th45:
id a = id b implies a = b
proof dom id a = a & dom id b = b by Th44; hence thesis; end;
theorem Th46:
for f being Morphism of C st cod(f) = b holds (id b)*f = f
proof let f be Morphism of C;
assume
A1: cod(f) = b;
then dom(id b) = cod(f) by Th44;
then cod(f) = (the Cod of C).f & id b = (the Id of C).b &
(the Comp of C).[id b,f] = (id b)*f by Def3,Def5,Th41;
hence thesis by A1,Def8;
end;
theorem Th47:
for g being Morphism of C st dom(g) = b holds g*(id b) = g
proof let g be Morphism of C;
assume
A1: dom(g) = b;
then cod(id b) = dom(g) by Th44;
then dom(g) = (the Dom of C).g & id b = (the Id of C).b &
(the Comp of C).[g,id b] = g*(id b) by Def2,Def5,Th41;
hence thesis by A1,Def8;
end;
definition let C,g;
attr g is monic means
for f1,f2 st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g*f1=g*f2
holds f1=f2;
end;
definition let C,f;
attr f is epi means
for g1,g2 st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f=g2*f
holds g1=g2;
end;
definition let C,f;
attr f is invertible means
ex g st dom g = cod f & cod g = dom f & f*g = id cod f & g*f = id dom f;
end;
reserve f,f1,f2 for Morphism of a,b;
reserve f' for Morphism of b,a;
reserve g for Morphism of b,c;
reserve h,h1,h2 for Morphism of c,d;
canceled 3;
theorem Th51:
Hom(a,b)<>{} & Hom(b,c)<>{} implies g*f in Hom(a,c)
proof assume Hom(a,b)<>{} & Hom(b,c)<>{};
then f in Hom(a,b) & g in Hom(b,c) by Def7;
then dom(g)=b & cod(g)=c & dom(f)=a & cod(f)=b by Th18;
then dom(g*f) = a & cod(g*f) = c by Th42;
hence (g*f) in Hom(a,c) by Th18;
end;
theorem
Hom(a,b)<>{} & Hom(b,c)<>{} implies Hom(a,c)<>{} by Th51;
definition let C,a,b,c,f,g;
assume A1: Hom(a,b)<>{} & Hom(b,c)<>{};
func g*f -> Morphism of a,c equals
:Def13: g*f;
correctness
proof g*f in Hom(a,c) by A1,Th51; hence thesis by Def7;
end;
end;
canceled;
theorem Th54:
Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g*f)
proof assume that
A1: Hom(a,b)<>{} and
A2: Hom(b,c)<>{} and
A3: Hom(c,d)<>{};
reconsider ff = f as Morphism of C;
reconsider gg = g as Morphism of C;
reconsider hh = h as Morphism of C;
f in Hom(a,b) & g in Hom(b,c) & h in Hom(c,d) by A1,A2,A3,Def7;
then A4: dom(h) = c & cod(g) = c & dom(g) = b & cod(f) = b by Th18;
A5: Hom(a,c)<>{} by A1,A2,Th51;
Hom(b,d) <> {} by A2,A3,Th51;
hence (h*g)*f = (h*g)*ff by A1,Def13 .= (hh*gg)*ff by A2,A3,Def13
.= hh*(gg*ff) by A4,Th43 .= hh*(g*f) by A1,A2,Def13
.= h*(g*f) by A3,A5,Def13;
end;
theorem Th55:
id a in Hom(a,a)
proof dom(id a)=a & cod(id a)=a by Th44; hence thesis by Th18; end;
theorem
Hom(a,a) <> {} by Th55;
definition let C,a;
redefine func id a -> Morphism of a,a;
coherence
proof id a in Hom(a,a) by Th55; hence id a is Morphism of a,a by Def7; end;
end;
theorem Th57:
Hom(a,b)<>{} implies (id b)*f=f
proof assume
A1: Hom(a,b)<>{};
then f in Hom(a,b) by Def7; then cod(f) = b by Th18;
then (id b)*(f qua Morphism of C) = f & Hom(b,b) <> {} by Th46,Th55;
hence (id b)*f = f by A1,Def13;
end;
theorem Th58:
Hom(b,c)<>{} implies g*(id b)=g
proof assume
A1: Hom(b,c)<>{};
then g in Hom(b,c) by Def7; then dom(g) = b by Th18;
then g*((id b) qua Morphism of C) = g & Hom(b,b) <> {} by Th47,Th55;
hence g*(id b) = g by A1,Def13;
end;
theorem Th59:
(id a)*(id a) = id a
proof Hom(a,a) <> {} by Th55; hence thesis by Th57; end;
:: Monics, Epis
theorem Th60:
Hom(b,c) <> {} implies
(g is monic iff for a
for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2)
proof assume
A1: Hom(b,c) <> {};
thus g is monic implies for a
for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2
proof assume
A2: for f1,f2 being Morphism of C
st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g*f1=g*f2
holds f1=f2;
let a; let f1,f2 be Morphism of a,b;
assume Hom(a,b)<>{};
then dom f1 = a & dom f2 = a & cod f1 = b & cod f2 = b & dom g = b &
g*f2 = g*(f2 qua Morphism of C) & g*f1 = g*(f1 qua Morphism of C)
by A1,Def13,Th23;
hence thesis by A2;
end;
assume
A3: for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2;
let f1,f2 be Morphism of C such that
A4: dom f1 = dom f2 and
A5: cod f1 = dom g and
A6: cod f2 = dom g;
A7: dom g = b by A1,Th23;
set a = dom(f1);
reconsider f1 as Morphism of a,b by A5,A7,Th22;
reconsider f2 as Morphism of a,b by A4,A6,A7,Th22;
A8: Hom(a,b) <> {} by A5,A7,Th18;
then g*f2 = g*(f2 qua Morphism of C) & g*f1 = g*(f1 qua Morphism of C)
by A1,Def13;
hence thesis by A3,A8;
end;
theorem
Hom(b,c)<>{} & Hom(c,d)<>{} & g is monic & h is monic implies h*g is monic
proof assume that
A1: Hom(b,c)<>{} & Hom(c,d)<>{} and
A2: g is monic and
A3: h is monic;
A4: Hom(b,d) <> {} by A1,Th51;
now let a,f1,f2 such that
A5: Hom(a,b)<>{} and
A6: (h*g)*f1 = (h*g)*f2;
h*(g*f1) = (h*g)*f1 & (h*g)*f2 = h*(g*f2) & Hom(a,c) <> {}
by A1,A5,Th51,Th54; then g*f1 = g*f2 by A1,A3,A6,Th60;
hence f1 = f2 by A1,A2,A5,Th60;
end;
hence thesis by A4,Th60;
end;
theorem
Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic
proof assume that
A1: Hom(b,c)<>{} & Hom(c,d)<>{} and
A2: h*g is monic;
now let a,f1,f2; assume
A3: Hom(a,b)<>{};
then Hom(b,d) <> {} & h*(g*f1) = (h*g)*f1 & h*(g*f2) = (h*g)*f2
by A1,Th51,Th54;
hence g*f1 = g*f2 implies f1 = f2 by A2,A3,Th60;
end;
hence thesis by A1,Th60;
end;
theorem
for h being Morphism of a,b for g being Morphism of b,a
st Hom(a,b) <> {} & Hom(b,a) <> {} & h*g = id b
holds g is monic
proof let h be Morphism of a,b; let g be Morphism of b,a such that
A1: Hom(a,b) <> {} and
A2: Hom(b,a) <> {} and
A3: h*g = id b;
now let c;
let g1,g2 be Morphism of c,b such that
A4: Hom(c,b) <> {} and
A5: g*g1 = g*g2;
thus g1 = (h*g)*g1 by A3,A4,Th57
.= h*(g*g2) by A1,A2,A4,A5,Th54
.= (h*g)*g2 by A1,A2,A4,Th54
.= g2 by A3,A4,Th57;
end;
hence thesis by A2,Th60;
end;
theorem
id b is monic
proof
A1: Hom(b,b) <> {} by Th55;
now let a; let f1,f2 be Morphism of a,b;
assume Hom(a,b)<>{}; then (id b)*f1 = f1 & (id b)*f2 = f2 by Th57;
hence (id b)*f1 = (id b)*f2 implies f1 = f2;
end;
hence thesis by A1,Th60;
end;
theorem Th65:
Hom(a,b) <> {} implies
(f is epi iff for c
for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2)
proof assume
A1: Hom(a,b) <> {};
thus f is epi implies for c
for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2
proof assume
A2: for g1,g2 being Morphism of C
st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f = g2*f
holds g1=g2;
let c; let g1,g2 be Morphism of b,c;
assume Hom(b,c)<>{};
then dom g1 = b & dom g2 = b & cod g1 = c & cod g2 = c & cod f = b &
g1*f = g1*(f qua Morphism of C) & g2*f = g2*(f qua Morphism of C)
by A1,Def13,Th23;
hence thesis by A2;
end;
assume
A3: for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2;
let g1,g2 be Morphism of C such that
A4: dom g1 = cod f and
A5: dom g2 = cod f and
A6: cod g1 = cod g2;
A7: cod f = b by A1,Th23;
set c = cod g1;
reconsider g1 as Morphism of b,c by A4,A7,Th22;
reconsider g2 as Morphism of b,c by A5,A6,A7,Th22;
A8: Hom(b,c) <> {} by A4,A7,Th18;
then g1*f = g1*(f qua Morphism of C) & g2*f = g2*(f qua Morphism of C)
by A1,Def13;
hence thesis by A3,A8;
end;
theorem
Hom(a,b)<>{} & Hom(b,c)<>{} & f is epi & g is epi implies g*f is epi
proof assume that
A1: Hom(a,b)<>{} & Hom(b,c)<>{} and
A2: f is epi and
A3: g is epi;
A4: Hom(a,c) <> {} by A1,Th51;
now let d,h1,h2 such that
A5: Hom(c,d)<>{} and
A6: h1*(g*f) = h2*(g*f);
h1*(g*f) = (h1*g)*f & (h2*g)*f = h2*(g*f) & Hom(b,d) <> {}
by A1,A5,Th51,Th54;
then h1*g = h2*g by A1,A2,A6,Th65;
hence h1 = h2 by A1,A3,A5,Th65;
end;
hence thesis by A4,Th65;
end;
theorem
Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi
proof assume that
A1: Hom(a,b)<>{} & Hom(b,c)<>{} and
A2: g*f is epi;
now let d,h1,h2; assume
A3: Hom(c,d)<>{};
then Hom(a,c) <> {} & h1*(g*f) = (h1*g)*f & h2*(g*f) = (h2*g)*f
by A1,Th51,Th54;
hence h1*g = h2*g implies h1 = h2 by A2,A3,Th65;
end;
hence thesis by A1,Th65;
end;
theorem
for h being Morphism of a,b for g being Morphism of b,a
st Hom(a,b) <> {} & Hom(b,a) <> {} & h*g = id b holds h is epi
proof let h be Morphism of a,b; let g be Morphism of b,a;
assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,a) <> {} and
A3: h*g = id b;
now let c;
let h1,h2 be Morphism of b,c such that
A4: Hom(b,c) <> {} and
A5: h1*h = h2*h;
thus h1 = h1*(h*g) by A3,A4,Th58
.= (h2*h)*g by A1,A2,A4,A5,Th54
.= h2*(h*g) by A1,A2,A4,Th54
.= h2 by A3,A4,Th58;
end;
hence thesis by A1,Th65;
end;
theorem
id b is epi
proof
A1: Hom(b,b) <> {} by Th55;
now let c; let g1,g2 be Morphism of b,c;
assume Hom(b,c)<>{}; then g1*(id b) = g1 & g2*(id b) = g2 by Th58;
hence g1*(id b) = g2*(id b) implies g1 = g2;
end;
hence thesis by A1,Th65;
end;
theorem Th70:
Hom(a,b) <> {} implies
(f is invertible iff
Hom(b,a)<>{} & ex g being Morphism of b,a st f*g=id b & g*f=id a)
proof assume
A1: Hom(a,b) <> {};
thus f is invertible implies
Hom(b,a)<>{} & ex g being Morphism of b,a st f*g=id b & g*f=id a
proof given g being Morphism of C such that
A2: dom g = cod f & cod g = dom f and
A3: f*g = id cod f & g*f = id dom f;
A4: dom f = a & cod f = b by A1,Th23;
hence
A5: Hom(b,a) <> {} by A2,Th18;
reconsider g as Morphism of b,a by A2,A4,Th22;
take g;
thus thesis by A1,A3,A4,A5,Def13;
end;
assume
A6: Hom(b,a)<>{};
given g being Morphism of b,a such that
A7: f*g=id b & g*f=id a;
reconsider g as Morphism of C;
take g; dom f = a & cod g = a & cod f = b & dom g = b by A1,A6,Th23;
hence thesis by A1,A6,A7,Def13;
end;
theorem Th71:
Hom(a,b) <> {} & Hom(b,a) <> {} implies
for g1,g2 being Morphism of b,a st f*g1=id b & g2*f=id a holds g1=g2
proof assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,a) <> {};
let g1,g2 be Morphism of b,a; assume
A3: f*g1=id b;
assume g2*f=id a;
hence g1 = (g2*f)*g1 by A2,Th57 .= g2*(id b) by A1,A2,A3,Th54
.= g2 by A2,Th58;
end;
definition let C,a,b,f;
assume that A1: Hom(a,b) <> {} and A2: f is invertible;
func f" -> Morphism of b,a means
:Def14: f*it = id b & it*f = id a;
existence by A1,A2,Th70;
uniqueness proof Hom(b,a) <> {} by A1,A2,Th70; hence thesis by A1,Th71; end;
end;
canceled;
theorem
Hom(a,b)<>{} & f is invertible implies f is monic & f is epi
proof assume that
A1: Hom(a,b)<>{} and
A2: f is invertible;
A3: Hom(b,a)<>{} by A1,A2,Th70;
consider k being Morphism of b,a such that
A4: f*k=id b and
A5: k*f=id a by A1,A2,Th70;
now
let c be (Object of C),g,h be Morphism of c,a such that
A6: Hom(c,a)<>{} and
A7: f*g=f*h;
g = (k*f)*g by A5,A6,Th57 .= k*(f*h) by A1,A3,A6,A7,Th54
.= (id a)*h by A1,A3,A5,A6,Th54;
hence g=h by A6,Th57;
end;
hence f is monic by A1,Th60;
now let c be (Object of C), g,h be Morphism of b,c such that
A8: Hom(b,c)<>{} and
A9: g*f=h*f;
g = g*(f*k) by A4,A8,Th58 .= (h*f)*k by A1,A3,A8,A9,Th54
.= h*(id b) by A1,A3,A4,A8,Th54;
hence g=h by A8,Th58;
end;
hence f is epi by A1,Th65;
end;
theorem
id a is invertible
proof Hom(a,a) <> {} & (id a)*(id a) = id a by Th55,Th59;
hence thesis by Th70;
end;
theorem Th75:
Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible
implies g*f is invertible
proof assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,c) <> {};
assume
A3: f is invertible;
then A4: Hom(b,a) <> {} by A1,Th70;
consider f1 being Morphism of b,a such that
A5: f*f1 = id b and
A6: f1*f = id a by A1,A3,Th70;
assume
A7: g is invertible;
then A8: Hom(c,b) <> {} by A2,Th70;
consider g1 being Morphism of c,b such that
A9: g*g1 = id c and
A10: g1*g = id b by A2,A7,Th70;
A11: Hom(a,c) <> {} by A1,A2,Th51;
now thus
A12: Hom(c,a) <> {} by A4,A8,Th51;
take f1g1 = f1*g1;
thus (g*f)*(f1g1) = g*(f*(f1*g1)) by A1,A2,A12,Th54
.= g*((id b )*g1) by A1,A4,A5,A8,Th54 .= id c by A8,A9,Th57;
Hom(a,c) <> {} by A1,A2,Th51;
hence (f1g1)*(g*f) = f1*(g1*(g*f)) by A4,A8,Th54
.= f1*((id b)*f) by A1,A2,A8,A10,Th54 .= id a by A1,A6,Th57;
end;
hence thesis by A11,Th70;
end;
theorem
Hom(a,b)<>{} & f is invertible implies f" is invertible
proof assume
A1: Hom(a,b) <> {};
assume f is invertible;
then Hom(b,a) <> {} & (f")*f = id a & f*(f") = id b by A1,Def14,Th70;
hence thesis by A1,Th70;
end;
theorem
Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible
implies (g*f)" = f"*g"
proof assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,c) <> {} and
A3: f is invertible and
A4: g is invertible;
now thus Hom(a,c) <> {} by A1,A2,Th51;
thus g*f is invertible by A1,A2,A3,A4,Th75;
A5: Hom(b,a) <> {} by A1,A3,Th70;
A6: Hom(c,b) <> {} by A2,A4,Th70;
then A7: Hom(c,a) <> {} by A5,Th51;
hence (g*f)*(f"*g")
= g*(f*(f"*g")) by A1,A2,Th54
.= g*((f*f")*g") by A1,A5,A6,Th54
.= g*((id b)*g") by A1,A3,Def14
.= g*g" by A6,Th57
.= id c by A2,A4,Def14;
thus (f"*g")*(g*f)
= ((f"*g")*g)*f by A1,A2,A7,Th54
.= (f"*(g"*g))*f by A2,A5,A6,Th54
.= (f"*(id b))*f by A2,A4,Def14
.= f"*f by A5,Th58
.= id a by A1,A3,Def14;
end;
hence thesis by Def14;
end;
definition let C,a;
attr a is terminal means
:Def15: Hom(b,a)<>{} &
ex f being Morphism of b,a st for g being Morphism of b,a holds f=g;
attr a is initial means
:Def16: Hom(a,b)<>{} &
ex f being Morphism of a,b st for g being Morphism of a,b holds f=g;
let b;
pred a,b are_isomorphic means
:Def17: Hom(a,b)<>{} & ex f st f is invertible;
end;
canceled 3;
theorem Th81:
a,b are_isomorphic iff
Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f' st f*f' = id b & f'*f = id a
proof
thus a,b are_isomorphic implies
Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f' st f*f' = id b & f'*f = id a
proof assume
A1: Hom(a,b) <> {};
given f such that
A2: f is invertible;
thus Hom(a,b) <> {} & Hom(b,a) <> {} by A1,A2,Th70;
take f; thus thesis by A1,A2,Th70;
end;
assume that
A3: Hom(a,b)<>{} and
A4: Hom(b,a)<>{};
given f such that
A5: ex f' st f*f' = id b & f'*f = id a;
thus Hom(a,b) <> {} by A3;
take f; thus thesis by A3,A4,A5,Th70;
end;
theorem
a is initial iff
for b ex f being Morphism of a,b st Hom(a,b) = {f}
proof
thus a is initial implies
for b ex f being Morphism of a,b st Hom(a,b) = {f}
proof assume
A1: a is initial;
let b;
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1,Def16;
take f;
Hom(a,b) <> {} by A1,Def16;
hence thesis by A2,Th26;
end;
assume
A3: for b ex f being Morphism of a,b st Hom(a,b) = {f};
let b;
consider f being Morphism of a,b such that
A4: Hom(a,b) = {f} by A3;
thus Hom(a,b) <> {} by A4;
take f;
thus thesis by A4,Th25;
end;
theorem Th83:
a is initial implies for h being Morphism of a,a holds id a = h
proof assume a is initial;
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g by Def16;
let h be Morphism of a,a;
id a = f by A1;
hence thesis by A1;
end;
theorem
a is initial & b is initial implies a,b are_isomorphic
proof assume that
A1: a is initial and
A2: b is initial;
thus
A3: Hom(a,b) <> {} by A1,Def16;
consider f being Morphism of a,b;
consider g being Morphism of b,a;
take f;
now thus Hom(b,a) <> {} by A2,Def16;
take g; thus f*g = id b & g*f = id a by A1,A2,Th83;
end;
hence thesis by A3,Th70;
end;
theorem
a is initial & a,b are_isomorphic implies b is initial
proof assume that
A1: a is initial and
A2: a,b are_isomorphic;
let c;
consider h being Morphism of a,c such that
A3: for g being Morphism of a,c holds h = g by A1,Def16;
consider f,f' such that
A4: f*f' = id b and f'*f = id a by A2,Th81;
A5: Hom(b,a) <> {} by A2,Th81;
Hom(a,c) <> {} by A1,Def16;
hence
A6: Hom(b,c) <> {} by A5,Th51;
take h*f';
A7: Hom(a,b) <> {} by A2,Def17;
let h' be Morphism of b,c;
thus h' = h'*(f*f') by A4,A6,Th58 .= (h'*f)*f' by A5,A6,A7,Th54
.= h*f' by A3;
end;
theorem
b is terminal iff
for a ex f being Morphism of a,b st Hom(a,b) = {f}
proof
thus b is terminal implies
for a ex f being Morphism of a,b st Hom(a,b) = {f}
proof assume
A1: b is terminal;
let a;
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1,Def15;
take f;
Hom(a,b) <> {} by A1,Def15;
hence thesis by A2,Th26;
end;
assume
A3: for a ex f being Morphism of a,b st Hom(a,b) = {f};
let a;
consider f being Morphism of a,b such that
A4: Hom(a,b) = {f} by A3;
thus Hom(a,b) <> {} by A4;
take f; thus thesis by A4,Th25;
end;
theorem Th87:
a is terminal implies for h being Morphism of a,a holds id a = h
proof assume a is terminal;
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g by Def15;
let h be Morphism of a,a;
id a = f by A1;
hence thesis by A1;
end;
theorem
a is terminal & b is terminal implies a,b are_isomorphic
proof assume that
A1: a is terminal and
A2: b is terminal;
thus
A3: Hom(a,b) <> {} by A2,Def15;
consider f being Morphism of a,b;
consider g being Morphism of b,a;
take f;
now thus Hom(b,a) <> {} by A1,Def15;
take g; thus f*g = id b & g*f = id a by A1,A2,Th87;
end;
hence thesis by A3,Th70;
end;
theorem
b is terminal & a,b are_isomorphic implies a is terminal
proof assume that
A1: b is terminal and
A2: a,b are_isomorphic;
let c;
consider h being Morphism of c,b such that
A3: for g being Morphism of c,b holds h = g by A1,Def15;
consider f,f' such that f*f' = id b and
A4: f'*f = id a by A2,Th81;
A5: Hom(b,a) <> {} by A2,Th81;
Hom(c,b) <> {} by A1,Def15;
hence
A6: Hom(c,a) <> {} by A5,Th51;
take f'*h;
A7: Hom(a,b) <> {} by A2,Def17;
let h' be Morphism of c,a;
thus f'*h = f'*(f*h') by A3 .= (f'*f)*h' by A5,A6,A7,Th54
.= h' by A4,A6,Th57;
end;
theorem
Hom(a,b) <> {} & a is terminal implies f is monic
proof assume that
A1: Hom(a,b) <> {} and
A2: a is terminal;
now let c be (Object of C),g,h be Morphism of c,a such that
Hom(c,a)<>{} and f*g=f*h;
consider ff being Morphism of c,a such that
A3: for gg being Morphism of c,a holds ff=gg by A2,Def15;
ff = g by A3; hence g=h by A3;
end;
hence thesis by A1,Th60;
end;
theorem
a,a are_isomorphic
proof thus
A1: Hom(a,a) <> {} by Th55;
take id a; (id a)*(id a) = id a by Th59;
hence thesis by A1,Th70;
end;
theorem
a,b are_isomorphic implies b,a are_isomorphic
proof assume
A1: Hom(a,b) <> {};
given f being Morphism of a,b such that
A2: f is invertible;
thus
A3: Hom(b,a) <> {} by A1,A2,Th70;
consider g being Morphism of b,a such that
A4: f*g = id b & g*f = id a by A1,A2,Th70;
take g; thus thesis by A1,A3,A4,Th70;
end;
theorem
a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic
proof assume
A1: Hom(a,b) <> {};
given f being Morphism of a,b such that
A2: f is invertible;
assume
A3: Hom(b,c) <> {};
given g being Morphism of b,c such that
A4: g is invertible;
thus Hom(a,c) <> {} by A1,A3,Th51;
take g*f; thus thesis by A1,A2,A3,A4,Th75;
end;
:: Functors (Covariant Functors)
definition let C,D;
mode Functor of C,D -> Function of the Morphisms of C,the Morphisms of D
means
:Def18:
( for c being Element of the Objects of C
ex d being Element of the Objects of D
st it.((the Id of C).c) = (the Id of D).d )
& ( for f being Element of the Morphisms of C holds
it.((the Id of C).((the Dom of C).f)) =
(the Id of D).((the Dom of D).(it.f)) &
it.((the Id of C).((the Cod of C).f)) =
(the Id of D).((the Cod of D).(it.f)) )
& ( for f,g being Element of the Morphisms of C
st [g,f] in dom(the Comp of C)
holds it.((the Comp of C).[g,f]) = (the Comp of D).[it.g,it.f] );
existence
proof consider d being Element of the Objects of D;
deffunc F(set) = (the Id of D).d;
consider F being Function of the Morphisms of C,the Morphisms of D such that
A1: for f being Element of the Morphisms of C holds F.f = F(f) from LambdaD;
take F;
thus for c being Element of the Objects of C
ex d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d
proof let c be Element of the Objects of C;
take d; thus thesis by A1;
end;
thus for f being Element of the Morphisms of C holds
F.((the Id of C).((the Dom of C).f)) =
(the Id of D).((the Dom of D).(F.f)) &
F.((the Id of C).((the Cod of C).f)) =
(the Id of D).((the Cod of D).(F.f))
proof let f be Element of the Morphisms of C;
A2: F.f = (the Id of D).d by A1;
thus F.((the Id of C).((the Dom of C).f))
= (the Id of D).d by A1
.= (the Id of D).((the Dom of D).(F.f)) by A2,Def8;
thus F.((the Id of C).((the Cod of C).f))
= (the Id of D).d by A1
.= (the Id of D).((the Cod of D).(F.f)) by A2,Def8;
end;
let f,g be Element of the Morphisms of C such that
A3: [g,f] in dom(the Comp of C);
set f' = F.f;
A4: (the Id of D).d = id d by Def5;
F.g = (the Id of D).d & F.f = (the Id of D).d by A1;
then (the Dom of D).(F.g) = d & (the Cod of D).(F.f) = d by Def8;
then A5: [F.g,F.f] in dom(the Comp of D) by Def8;
A6: Hom(d,d) <> {} by Th55;
(the Comp of C).[g,f] is Element of the Morphisms of C by A3,PARTFUN1:27;
hence F.((the Comp of C).[g,f])
= (the Id of D).d by A1
.= (id d)*(id d) by A4,Th59
.= (id d)*((id d) qua Morphism of D) by A6,Def13
.= (id d)*f' by A1,A4
.= F.g*f' by A1,A4
.= (the Comp of D).[F.g,F.f] by A5,Def4;
end;
end;
canceled 2;
theorem Th96:
for T being Function of the Morphisms of C,the Morphisms of D
st ( for c being Object of C ex d being Object of D st T.(id c) = id d )
& ( for f being Morphism of C
holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) )
& ( for f,g being Morphism of C st dom g = cod f
holds T.(g*f) = (T.g)*(T.f))
holds T is Functor of C,D
proof let T be Function of the Morphisms of C,the Morphisms of D such that
A1: for c being Object of C ex d being Object of D st T.(id c) = id d and
A2: for f being Morphism of C
holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) and
A3: for f,g being Morphism of C st dom g = cod f holds T.(g*f) = (T.g)*(T.f);
thus for c being Element of the Objects of C
ex d being Element of the Objects of D
st T.((the Id of C).c) = (the Id of D).d
proof let c be Element of the Objects of C;
consider d being Object of D such that
A4: T.(id c) = id d by A1;
id c = (the Id of C).c & id d = (the Id of D).d by Def5;
hence thesis by A4;
end;
thus for f being Element of the Morphisms of C holds
T.((the Id of C).((the Dom of C).f)) =
(the Id of D).((the Dom of D).(T.f)) &
T.((the Id of C).((the Cod of C).f)) =
(the Id of D).((the Cod of D).(T.f))
proof let f be Element of the Morphisms of C;
(the Dom of C).f = dom f & (the Id of C).(dom f) = id dom f &
(the Dom of D).(T.f) = dom(T.f) &
(the Id of D).(dom (T.f)) = id dom(T.f) &
(the Cod of C).f = cod f & (the Id of C).(cod f) = id cod f &
(the Cod of D).(T.f) = cod(T.f) &
(the Id of D).(cod (T.f)) = id cod(T.f) by Def2,Def3,Def5;
hence thesis by A2;
end;
let f,g be Element of the Morphisms of C;
assume [g,f] in dom(the Comp of C);
then A5: dom g = cod f by Th40;
then id dom (T.g) = T.(id cod f) by A2 .= id cod (T.f) by A2;
then dom (T.g) = cod (T.f) by Th45;
then (the Comp of C).[g,f] = g*f &
(the Comp of D).[T.g,T.f] = (T.g)*(T.f) by A5,Th41;
hence thesis by A3,A5;
end;
theorem Th97:
for T being Functor of C,D for c being Object of C
ex d being Object of D st T.(id c) = id d
proof let T be Functor of C,D; let c be Object of C;
consider d being Element of the Objects of D such that
A1: T.((the Id of C).c) = (the Id of D).d by Def18;
id c = (the Id of C).c & id d = (the Id of D).d by Def5;
hence thesis by A1;
end;
theorem Th98:
for T being Functor of C,D for f being Morphism of C
holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f)
proof let T be Functor of C,D; let f be Morphism of C;
(the Dom of C).f = dom f & (the Id of C).(dom f) = id dom f &
(the Dom of D).(T.f) = dom(T.f) & (the Id of D).(dom (T.f)) = id dom(T.f) &
(the Cod of C).f = cod f & (the Id of C).(cod f) = id cod f &
(the Cod of D).(T.f) = cod(T.f) & (the Id of D).(cod (T.f)) = id cod(T.f)
by Def2,Def3,Def5;
hence thesis by Def18;
end;
theorem Th99:
for T being Functor of C,D for f,g being Morphism of C st dom g = cod f
holds dom(T.g) = cod(T.f) & T.(g*f) = (T.g)*(T.f)
proof let T be Functor of C,D; let f,g be Morphism of C;
assume
A1: dom g = cod f;
then id dom (T.g) = T.(id cod f) by Th98 .= id cod (T.f) by Th98;
hence dom (T.g) = cod (T.f) by Th45;
then (the Comp of C).[g,f] = g*f & (the Comp of D).[T.g,T.f] = (T.g)*(T.f)
&
[g,f] in dom(the Comp of C) by A1,Th40,Th41;
hence thesis by Def18;
end;
theorem Th100:
for T being Function of the Morphisms of C,the Morphisms of D
for F being Function of the Objects of C, the Objects of D
st ( for c being Object of C holds T.(id c) = id(F.c) )
& ( for f being Morphism of C
holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f) )
& ( for f,g being Morphism of C st dom g = cod f
holds T.(g*f) = (T.g)*(T.f))
holds T is Functor of C,D
proof let T be Function of the Morphisms of C,the Morphisms of D;
let F be Function of the Objects of C, the Objects of D;
assume that
A1: for c being Object of C holds T.(id c) = id(F.c) and
A2: for f being Morphism of C
holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f) and
A3: for f,g being Morphism of C st dom g = cod f holds T.(g*f) = (T.g)*(T.f);
now
thus for c being Object of C ex d being Object of D st T.(id c) = id d
proof let c be Object of C;
take F.c;
thus thesis by A1;
end;
thus for f being Morphism of C
holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f)
proof let f be Morphism of C;
thus T.(id dom f) = id (F.(dom f)) by A1 .= id dom (T.f) by A2;
thus T.(id cod f) = id (F.(cod f)) by A1 .= id cod (T.f) by A2;
end;
end;
hence thesis by A3,Th96;
end;
:: Object Function of a Functor
definition let C,D;
let F be Function of the Morphisms of C,the Morphisms of D;
assume
A1: for c being Element of the Objects of C
ex d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d;
func Obj(F) -> Function of the Objects of C,the Objects of D means
:Def19:
for c being Element of the Objects of C
for d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d holds it.c = d;
existence
proof
defpred P[set,set] means
for d being Element of the Objects of D
st F.((the Id of C).$1) = (the Id of D).d holds $2 = d;
A2: for c being Element of the Objects of C
ex y being Element of the Objects of D st P[c,y]
proof let c be Element of the Objects of C;
consider y being Element of the Objects of D such that
A3: F.((the Id of C).c) = (the Id of D).y by A1;
take y;
let d be Element of the Objects of D;
assume
A4: F.((the Id of C).c) = (the Id of D).d;
id d = (the Id of D).d & id y = (the Id of D).y by Def5;
hence y = d by A3,A4,Th45;
end;
thus ex f being Function of the Objects of C,the Objects of D st
for x being Element of the Objects of C holds P[x,f.x] from FuncExD(A2);
end;
uniqueness
proof
let F1,F2 be Function of the Objects of C,the Objects of D such that
A5: for c being Element of the Objects of C
for d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d holds F1.c = d and
A6: for c being Element of the Objects of C
for d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d holds F2.c = d;
for c being Element of the Objects of C holds F1.c = F2.c
proof let c be Element of the Objects of C;
consider d1 being Element of the Objects of D such that
A7: F.((the Id of C).c) = (the Id of D).d1 by A1;
consider d2 being Element of the Objects of D such that
A8: F.((the Id of C).c) = (the Id of D).d2 by A1;
id d1 = (the Id of D).d1 & id d2 = ( the Id of D ).d2 &
dom id d1 = d1 & dom id d2 = d2 & c is Object of C
by Def5,Th44;
then F1.c = d1 & F2.c = d2 & d1 = d2 by A5,A6,A7,A8;
hence thesis;
end;
hence thesis by FUNCT_2:113;
end;
end;
canceled;
theorem Th102:
for T being Function of the Morphisms of C,the Morphisms of D
st for c being Object of C ex d being Object of D st T.(id c) = id d
for c being Object of C for d being Object of D
st T.(id c) = id d holds (Obj T).c = d
proof let T be Function of the Morphisms of C,the Morphisms of D such that
A1: for c being Object of C ex d being Object of D st T.(id c) = id d;
A2: for c being Element of the Objects of C
ex d being Element of the Objects of D
st T.((the Id of C).c) = (the Id of D).d
proof let c be Element of the Objects of C;
consider d being Object of D such that
A3: T.(id c) = id d by A1;
take d;
(the Id of C).c = id c & (the Id of D).d = id d by Def5;
hence thesis by A3;
end;
let c be Object of C; let d be Object of D;
(the Id of C).c = id c & (the Id of D).d = id d by Def5;
hence thesis by A2,Def19;
end;
theorem Th103:
for T being Functor of C,D
for c being Object of C for d being Object of D st T.(id c) = id d
holds (Obj T).c = d
proof let T be Functor of C,D;
for c being Object of C ex d being Object of D st T.(id c) = id d by Th97;
hence thesis by Th102;
end;
theorem Th104:
for T being (Functor of C,D),c being Object of C
holds T.(id c) = id((Obj T).c)
proof let T be (Functor of C,D),c be Object of C;
ex d being Object of D st T.(id c) = id d by Th97;
hence thesis by Th103;
end;
theorem Th105:
for T being (Functor of C,D), f being Morphism of C
holds (Obj T).(dom f) = dom (T.f) & (Obj T).(cod f) = cod (T.f)
proof let T be (Functor of C,D), f be Morphism of C;
T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) by Th98;
hence thesis by Th103;
end;
definition let C,D be Category;
let T be Functor of C,D; let c be Object of C;
func T.c -> Object of D equals
:Def20: (Obj T).c;
correctness;
end;
canceled;
theorem
for T being Functor of C,D
for c being Object of C for d being Object of D st T.(id c) = id d
holds T.c = d
proof let T be Functor of C,D; let c be Object of C; let d be Object of D;
T.c = (Obj T).c by Def20; hence thesis by Th103;
end;
theorem Th108:
for T being (Functor of C, D),c being Object of C
holds T.(id c) = id(T.c)
proof let T be (Functor of C, D),c be Object of C;
T.c = (Obj T).c by Def20; hence thesis by Th104;
end;
theorem Th109:
for T being (Functor of C, D), f being Morphism of C
holds T.(dom f) = dom (T.f) & T.(cod f) = cod (T.f)
proof let T be (Functor of C, D), f be Morphism of C;
T.(dom f) = (Obj T).(dom f) & T.(cod f) = (Obj T).(cod f) by Def20;
hence thesis by Th105;
end;
theorem Th110:
for T being Functor of B,C for S being Functor of C,D
holds S*T is Functor of B,D
proof let T be Functor of B,C; let S be Functor of C,D;
reconsider FF = (Obj S)*(Obj T)
as Function of the Objects of B , the Objects of D;
reconsider TT = S*T
as Function of the Morphisms of B , the Morphisms of D;
now
thus for b being Object of B holds TT.(id b) = id(FF.b)
proof let b be Object of B;
thus TT.(id b) = S.(T.(id b)) by FUNCT_2:21
.= S.(id(T.b)) by Th108
.= id((S.(T.b))) by Th108
.= id((S.((Obj T).b))) by Def20
.= id(((Obj S).((Obj T).b))) by Def20
.= id(FF.b) by FUNCT_2:21;
end;
thus for f being Morphism of B
holds FF.(dom f) = dom (TT.f) & FF.(cod f) = cod (TT.f)
proof let f be Morphism of B;
thus FF.(dom f) = (Obj S).((Obj T).(dom f)) by FUNCT_2:21
.= (Obj S).(dom (T.f)) by Th105
.= (dom (S.(T.f))) by Th105
.= dom (TT.f) by FUNCT_2:21;
thus FF.(cod f) = (Obj S).((Obj T).(cod f)) by FUNCT_2:21
.= (Obj S).(cod (T.f)) by Th105
.= (cod (S.(T.f))) by Th105
.= cod (TT.f) by FUNCT_2:21;
end;
let f,g be Morphism of B;
assume
A1: dom g = cod f;
then A2: dom(T.g) = cod(T.f) by Th99;
thus TT.(g*f) = S.(T.(g*f)) by FUNCT_2:21
.= S.((T.g)*(T.f)) by A1,Th99
.= (S.(T.g))*(S.(T.f)) by A2,Th99
.= ((TT.g)*(S.(T.f))) by FUNCT_2:21
.= (TT.g)*(TT.f) by FUNCT_2:21;
end;
hence thesis by Th100;
end;
:: Composition of Functors
definition let B,C,D;
let T be Functor of B,C; let S be Functor of C,D;
redefine func S*T -> Functor of B,D;
coherence by Th110;
end;
theorem Th111:
id the Morphisms of C is Functor of C,C
proof
set F = id the Objects of C;
set T = id the Morphisms of C;
now
thus for c being Object of C holds T.(id c) = id(F.c)
proof let c be Object of C;
F.c = c by FUNCT_1:35;
hence thesis by FUNCT_1:35;
end;
thus for f being Morphism of C
holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f)
proof let f be Morphism of C;
T.f = f by FUNCT_1:35;
hence thesis by FUNCT_1:35;
end;
let f,g be Morphism of C;
assume dom g = cod f;
thus T.(g*f) = g*f by FUNCT_1:35 .= (T.g)*f by FUNCT_1:35
.= (T.g)*(T.f) by FUNCT_1:35;
end;
hence thesis by Th100;
end;
theorem Th112:
for T being (Functor of B,C),S being (Functor of C,D),b being Object of B
holds (Obj (S*T)).b = (Obj S).((Obj T).b)
proof let T be (Functor of B,C),S be (Functor of C,D),b be Object of B;
consider d being Object of D such that
A1: (S*T).(id b) = id d by Th97;
consider c being Object of C such that
A2: T.(id b) = id c by Th97;
A3: (S*T).(id b) = S.(T.(id b)) by FUNCT_2:21;
thus (Obj (S*T)).b = d by A1,Th103 .= (Obj S).c by A1,A2,A3,Th103
.= (Obj S).((Obj T).b) by A2,Th103;
end;
theorem Th113:
for T being Functor of B,C for S being Functor of C,D
for b being Object of B holds (S*T).b = S.(T.b)
proof let T be Functor of B,C; let S be Functor of C,D;
let b be Object of B;
thus (S*T).b = (Obj (S*T)).b by Def20
.= (Obj S).((Obj T).b) by Th112
.= (Obj S).(T.b) by Def20
.= S.(T.b) by Def20;
end;
:: Identity Functor
definition let C;
func id C -> Functor of C,C equals
:Def21: id the Morphisms of C;
coherence by Th111;
end;
canceled;
theorem Th115:
for f being Morphism of C holds (id C).f = f
proof let f be Morphism of C;
thus (id C).f = (id the Morphisms of C).f by Def21 .= f by FUNCT_1:35;
end;
theorem Th116:
for c being Object of C holds (Obj id C).c = c
proof let c be Object of C; (id C).(id c) = id c by Th115;
hence (Obj id C).c = c by Th103;
end;
theorem Th117:
Obj id C = id the Objects of C
proof
dom Obj id C = the Objects of C & for x be set holds x in the Objects of
C
implies (Obj id C).x = x by Th116,FUNCT_2:def 1;
hence thesis by FUNCT_1:34;
end;
theorem
for c being Object of C holds (id C).c = c
proof let c be Object of C; (Obj id C).c = c by Th116;
hence thesis by Def20;
end;
definition let C,D be Category; let T be Functor of C,D;
attr T is isomorphic means
T is one-to-one & rng T = the Morphisms of D & rng Obj T = the Objects of D
;
synonym T is_an_isomorphism;
attr T is full means :Def23:
for c,c' being Object of C st Hom(T.c,T.c') <> {}
for g being Morphism of T.c,T.c' holds
Hom(c,c') <> {} & ex f being Morphism of c,c' st g = T.f;
attr T is faithful means :Def24:
for c,c' being Object of C st Hom(c,c') <> {}
for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2;
end;
canceled 3;
theorem
id C is_an_isomorphism
proof
rng id the Morphisms of C
= the Morphisms of C & rng id the Objects of C = the Objects of C &
id the Morphisms of C is one-to-one by FUNCT_1:52,RELAT_1:71;
hence id C is one-to-one
& rng id C = the Morphisms of C & rng Obj id C = the Objects of C
by Def21,Th117;
end;
theorem Th123:
for T being Functor of C,D for c,c' being Object of C
for f being set st f in Hom(c,c') holds T.f in Hom(T.c,T.c')
proof let T be Functor of C,D; let c,c' be Object of C;
let f be set;
assume
A1: f in Hom(c,c');
then reconsider f' = f as Morphism of c,c' by Def7;
dom f' = c & cod f' = c' by A1,Th18;
then T.c = dom (T.f') & T.c' = cod(T.f') by Th109;
hence T.f in Hom(T.c,T.c') by Th18;
end;
theorem Th124:
for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {}
for f being Morphism of c,c' holds T.f in Hom(T.c,T.c')
proof let T be Functor of C,D; let c,c' be Object of C such that
A1: Hom(c,c') <> {};
let f be Morphism of c,c'; f in Hom(c,c') by A1,Def7;
hence thesis by Th123;
end;
theorem Th125:
for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {}
for f being Morphism of c,c' holds T.f is Morphism of T.c,T.c'
proof let T be Functor of C,D; let c,c' be Object of C such that
A1: Hom(c,c') <> {};
let f be Morphism of c,c'; T.f in Hom(T.c,T.c') by A1,Th124;
hence T.f is Morphism of T.c,T.c' by Def7;
end;
theorem Th126:
for T being Functor of C,D for c,c' being Object of C
st Hom(c,c') <> {} holds Hom(T.c,T.c') <> {}
proof let T be Functor of C,D; let c,c' be Object of C;
assume A1: Hom(c,c') <> {};
consider f being Element of Hom(c,c');
f in Hom(c,c') by A1;
hence Hom(T.c,T.c') <> {} by Th123;
end;
theorem
for T being Functor of B,C for S being Functor of C,D
st T is full & S is full holds S*T is full
proof let T be Functor of B,C; let S be Functor of C,D;
assume that
A1: T is full and
A2: S is full;
let b,b' be Object of B such that
A3: Hom((S*T).b,(S*T).b') <> {};
let g be Morphism of (S*T).b,(S*T).b';
A4: (S*T).b = S.(T.b) & (S*T).b' = S.(T.b') by Th113;
then consider f being Morphism of T.b,T.b' such that
A5: g = S.f by A2,A3,Def23;
A6: Hom(T.b,T.b') <> {} by A2,A3,A4,Def23;
hence Hom(b,b') <> {} by A1,Def23;
consider h being Morphism of b,b' such that
A7: f = T.h by A1,A6,Def23;
take h;
thus g = (S*T).h by A5,A7,FUNCT_2:21;
end;
theorem
for T being Functor of B,C for S being Functor of C,D
st T is faithful & S is faithful holds S*T is faithful
proof let T be Functor of B,C; let S be Functor of C,D;
assume that
A1: T is faithful and
A2: S is faithful;
let b,b' be Object of B such that
A3: Hom(b,b') <> {};
let f1,f2 be Morphism of b,b';
assume
A4: (S*T).f1 = (S*T).f2;
Hom(T.b,T.b') <> {} & (S*T).f1 = S.(T.f1) & (S*T).f2 = S.(T.f2) &
T.f1 is Morphism of T.b,T.b' & T.f2 is Morphism of T.b,T.b'
by A3,Th125,Th126,FUNCT_2:21;
then T.f1 = T.f2 by A2,A4,Def24;
hence f1 = f2 by A1,A3,Def24;
end;
theorem Th129:
for T being Functor of C,D for c,c' being Object of C
holds T.:Hom(c,c') c= Hom(T.c,T.c')
proof let T be Functor of C,D; let c,c' be Object of C;
let f be set;
assume f in T.:Hom(c,c');
then ex g being Element of the Morphisms of C
st g in Hom(c,c') & f = T.g by FUNCT_2:116;
hence f in Hom(T.c,T.c') by Th123;
end;
definition let C,D be Category;
let T be Functor of C,D; let c,c' be Object of C;
func hom(T,c,c') -> Function of Hom(c,c') , Hom(T.c,T.c') equals
:Def25: T|Hom(c,c');
correctness
proof
T is Function of the Morphisms of C, the Morphisms of D &
Hom(c,c') c= the Morphisms of C & T.:Hom(c,c') c= Hom(T.c,T.c')
by Th129;
hence thesis by Th4;
end;
end;
canceled;
theorem Th131:
for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {}
for f being Morphism of c,c' holds hom(T,c,c').f = T.f
proof let T be Functor of C,D; let c,c' be Object of C;
assume A1: Hom(c,c') <> {};
let f be Morphism of c,c';
T is Function of the Morphisms of C,the Morphisms of D & f in Hom(c,c')
by A1,Def7;
then (T|Hom(c,c')).f = T.f by FUNCT_1:72; hence thesis by Def25;
end;
theorem
for T being Functor of C,D holds
T is full iff
for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c')
proof let T be Functor of C,D;
thus T is full implies
for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c')
proof assume
A1: T is full;
let c,c' be Object of C;
A2: now assume
A3: Hom(T.c,T.c') = {};
then Hom(c,c') = {} by Th126;
hence rng hom(T,c,c') = Hom(T.c,T.c') by A3,PARTFUN1:54;
end;
now assume
A4: Hom(T.c,T.c') <> {};
for g being set holds g in rng hom(T,c,c') iff g in Hom(T.c,T.c')
proof let g be set;
thus g in rng hom(T,c,c') implies g in Hom(T.c,T.c')
proof assume g in rng hom(T,c,c');
then consider f being set such that
A5: f in dom hom(T,c,c') and
A6: hom(T,c,c').f = g by FUNCT_1:def 5;
f in Hom(c,c') by A4,A5,FUNCT_2:def 1;
hence thesis by A4,A6,FUNCT_2:7;
end;
assume g in Hom(T.c,T.c');
then g is Morphism of T.c,T.c' by Def7;
then consider f being Morphism of c,c' such that
A7: g = T.f by A1,A4,Def23;
A8: Hom(c,c') <> {} by A1,A4,Def23;
then f in Hom(c,c') by Def7;
then hom(T,c,c').f in rng hom(T,c,c') by A4,FUNCT_2:6;
hence g in rng hom(T,c,c') by A7,A8,Th131;
end;
hence rng hom(T,c,c') = Hom(T.c,T.c') by TARSKI:2;
end;
hence thesis by A2;
end;
assume
A9: for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c');
let c,c' be Object of C such that
A10: Hom(T.c,T.c') <> {};
let g be Morphism of T.c,T.c';
g in Hom(T.c,T.c') by A10,Def7;
then g in rng hom(T,c,c') by A9;
then consider f being set such that
A11: f in dom hom(T,c,c') and
A12: hom(T,c,c').f = g by FUNCT_1:def 5;
A13: f in Hom(c,c') by A10,A11,FUNCT_2:def 1;
thus
Hom(c,c') <> {} by A11,FUNCT_2:def 1;
reconsider f as Morphism of c,c' by A13,Def7;
take f; thus T.f = g by A12,A13,Th131;
end;
theorem
for T being Functor of C,D holds
T is faithful iff
for c,c' being Object of C holds hom(T,c,c') is one-to-one
proof let T be Functor of C,D;
thus T is faithful implies
for c,c' being Object of C holds hom(T,c,c') is one-to-one
proof assume
A1: T is faithful;
let c,c' be Object of C;
A2: now assume Hom(T.c,T.c') = {}; then Hom(c,c') = {} by Th126;
hence hom(T,c,c') is one-to-one by PARTFUN1:59;
end;
now assume
A3: Hom(T.c,T.c') <> {};
now let f1,f2 be set;
assume f1 in Hom(c,c') & f2 in Hom(c,c');
then A4: f1 is Morphism of c,c' & f2 is Morphism of c,c' & Hom(c,c') <>
{}
by Def7;
then T.f1 = hom(T,c,c').f1 & T.f2 = hom(T,c,c').f2 by Th131;
hence hom(T,c,c').f1 = hom(T,c,c').f2 implies f1 = f2
by A1,A4,Def24;
end;
hence hom(T,c,c') is one-to-one by A3,FUNCT_2:25;
end;
hence thesis by A2;
end;
assume
A5: for c,c' being Object of C holds hom(T,c,c') is one-to-one;
let c,c' be Object of C such that
A6: Hom(c,c') <> {};
let f1,f2 be Morphism of c,c';
Hom(T.c,T.c') <> {} & f1 in Hom(c,c') & f2 in Hom(c,c') &
hom(T,c,c') is one-to-one & T.f1 = hom(T,c,c').f1 & T.f2 = hom(T,c,c').f2
by A5,A6,Def7,Th126,Th131;
hence thesis by FUNCT_2:25;
end;