Copyright (c) 1991 Association of Mizar Users
environ
vocabulary FUNCT_2, TARSKI, FRAENKEL, FUNCT_1, BOOLE, MCART_1, RELAT_1, CAT_1,
PARTFUN1, QC_LANG1, CLASSES2, FUNCOP_1, FUNCT_4, CAT_2, OPPCAT_1,
FUNCT_5, ENS_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, RELAT_1,
FUNCT_1, FUNCT_2, PARTFUN1, FUNCT_4, FUNCT_5, FRAENKEL, CLASSES2,
FUNCOP_1, CAT_1, CAT_2, OPPCAT_1;
constructors DOMAIN_1, CLASSES2, CAT_2, OPPCAT_1, PARTFUN1, MEMBERED,
XBOOLE_0;
clusters RELAT_1, FUNCT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2,
XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, CAT_1, CAT_2;
theorems TARSKI, ENUMSET1, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2,
PARTFUN1, FUNCOP_1, FUNCT_4, FRAENKEL, CLASSES2, CAT_1, CAT_2, OPPCAT_1,
GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, PARTFUN1, COMPTS_1;
begin :: Mappings
reserve V for non empty set, A,B,A',B' for Element of V;
definition let V;
func Funcs(V) -> set equals
:Def1: union { Funcs(A,B): not contradiction };
coherence;
end;
definition let V;
cluster Funcs(V) -> functional non empty;
coherence
proof set F = { Funcs(A,B): not contradiction};
A1:Funcs V = union F by Def1;
consider A;
id A in Funcs(A,A) & Funcs(A,A) in F by FUNCT_2:12;
then reconsider UF = union F as non empty set by TARSKI:def 4;
now let f be set;
assume f in UF;
then consider C being set such that
A2: f in C and
A3: C in F by TARSKI:def 4;
ex A,B st C = Funcs(A,B) by A3;
hence f is Function by A2,FUNCT_2:121;
end;
hence thesis by A1,FRAENKEL:def 1;
end;
end;
theorem Th1:
for f being set holds f in Funcs(V) iff
ex A,B st (B={} implies A={}) & f is Function of A,B
proof let f be set;
set F = { Funcs(A,B): not contradiction};
A1: Funcs V = union F by Def1;
thus f in Funcs(V) implies
ex A,B st (B={} implies A={}) & f is Function of A,B
proof assume f in Funcs(V);
then consider C being set such that
A2: f in C and
A3: C in F by A1,TARSKI:def 4;
consider A,B such that
A4: C = Funcs(A,B) by A3;
take A,B;
thus thesis by A2,A4,FUNCT_2:14,121;
end;
given A,B such that
A5: (B={} implies A={}) & f is Function of A,B;
f in Funcs(A,B) & Funcs(A,B) in F by A5,FUNCT_2:11;
hence thesis by A1,TARSKI:def 4;
end;
theorem
Funcs(A,B) c= Funcs(V)
proof let x be set;
assume
x in Funcs(A,B);
then (B={} implies A={}) & x is Function of A,B by FUNCT_2:14,121;
hence thesis by Th1;
end;
theorem Th3:
for W be non empty Subset of V holds Funcs W c= Funcs V
proof let W be non empty Subset of V;
let f be set;
assume f in Funcs W;
then ex A,B being Element of W st(B={} implies A={}) & f is Function of A,B
by Th1;
hence thesis by Th1;
end;
reserve f,f' for Element of Funcs(V);
definition let V;
func Maps(V) -> set equals
:Def2: { [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
coherence;
end;
definition let V;
cluster Maps(V) -> non empty;
coherence
proof
set FV = { [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
consider A;
now
set f = id A;
take m = [[A,A],f];
A1: A = {} implies A = {};
then f in Funcs(V) & [A,A] in [:V,V:] by Th1;
hence m in FV by A1;
end;
hence thesis by Def2;
end;
end;
reserve m,m1,m2,m3,m' for Element of Maps V;
theorem Th4:
ex f,A,B st m = [[A,B],f] & (B = {} implies A = {}) & f is Function of A,B
proof m in Maps V;
then m in { [[A,B],f]: (B={} implies A={}) & f is Function of A,B} by Def2;
then ex A,B,f st m = [[A,B],f] & (B={} implies A={}) & f is Function of A,B;
hence thesis;
end;
theorem Th5:
for f being Function of A,B st B={} implies A={} holds [[A,B],f] in Maps V
proof let f be Function of A,B; assume
A1: B = {} implies A = {};
then f in Funcs(V) by Th1;
then [[A,B],f] in {[[A',B'],f']:(B'={} implies A'={}
) & f' is Function of A',B'}
by A1;
hence thesis by Def2;
end;
theorem
Maps V c= [:[:V,V:],Funcs V:]
proof let m be set;
assume m in Maps V;
then m in { [[A,B],f]: (B={} implies A={}) & f is Function of A,B} by Def2;
then ex A,B,f st m = [[A,B],f] & (B={} implies A={}) & f is Function of A,B;
hence thesis;
end;
theorem Th7:
for W be non empty Subset of V holds Maps W c= Maps V
proof let W be non empty Subset of V;
let x be set;
assume x in Maps W;
then x in { [[A,B],f]
where A is Element of W, B is Element of W, f is Element of Funcs(W)
: (B={} implies A={}) & f is Function of A,B }
by Def2;
then consider A,B be Element of W, f be Element of Funcs(W) such that
A1: x = [[A,B],f] & (B = {} implies A = {}) & f is Function of A,B;
Funcs W c= Funcs V & f in Funcs(W) by Th3;
then x in {[[A',B'],f']:(B'={} implies A'={}
) & f' is Function of A',B'} by A1;
hence thesis by Def2;
end;
Lm1: for x1,y1,x2,y2,x3,y3 being set st [[x1,x2],x3] = [[y1,y2],y3]
holds x1 = y1 & x2 = y2
proof let x1,y1,x2,y2,x3,y3 be set;
assume [[x1,x2],x3] = [[y1,y2],y3];
then [x1,x2] = [y1,y2] by ZFMISC_1:33;
hence thesis by ZFMISC_1:33;
end;
definition let V be non empty set, m be Element of Maps V;
cluster m`2 -> Function-like Relation-like;
coherence
proof
consider f be Element of Funcs(V),
A,B be Element of V such that
A1: m = [[A,B],f] and (B = {} implies A = {}) and
A2: f is Function of A,B by Th4;
thus thesis by A1,A2,MCART_1:7;
end;
end;
definition let V,m;
canceled;
func dom m -> Element of V equals
:Def4: m`1`1;
coherence
proof
consider f,A,B such that
A1: m = [[A,B],f] and (B = {} implies A = {}) & f is Function of A,B by Th4;
[A,B] = m`1 by A1,MCART_1:7;
hence thesis by MCART_1:7;
end;
func cod m -> Element of V equals
:Def5: m`1`2;
coherence
proof
consider f,A,B such that
A2: m = [[A,B],f] and (B = {} implies A = {}) & f is Function of A,B by Th4;
[A,B] = m`1 by A2,MCART_1:7;
hence thesis by MCART_1:7;
end;
end;
theorem Th8:
m = [[dom m,cod m],m`2]
proof
consider f,A,B such that
A1: m = [[A,B],f] and (B = {} implies A = {}) & f is Function of A,B by Th4;
dom m = m`1`1 & cod m = m`1`2 & [A,B] = m`1 by A1,Def4,Def5,MCART_1:7;
then m`1 = [dom m,cod m] & m`2 = m`2 by MCART_1:8;
hence thesis by A1,MCART_1:8;
end;
Lm2: m`2 = m'`2 & dom m = dom m' & cod m = cod m' implies m = m'
proof m = [[dom m,cod m],m`2] & m' = [[dom m',cod m'],m'`2] by Th8;
hence thesis;
end;
theorem Th9:
(cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m
proof
consider f, A,B such that
A1: m = [[A,B],f] and
A2: (B = {} implies A = {}) & f is Function of A,B by Th4;
m = [[dom m,cod m],m`2] by Th8;
then f = m`2 & A = dom m & B = cod m by A1,Lm1,ZFMISC_1:33;
hence thesis by A2;
end;
Lm3: dom m`2 = dom m & rng m`2 c= cod m
proof (cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m by Th9;
hence thesis by FUNCT_2:def 1,RELSET_1:12;
end;
theorem Th10:
for f being Function, A,B being set st [[A,B],f] in Maps(V) holds
(B = {} implies A = {}) & f is Function of A,B
proof let f be Function, A,B be set;
assume [[A,B],f] in Maps(V);
then consider f',A',B' such that
A1: [[A,B],f] = [[A',B'],f'] and
A2: (B' = {} implies A' = {}) & f' is Function of A',B' by Th4;
f = f' & A = A' & B = B' by A1,Lm1,ZFMISC_1:33;
hence thesis by A2;
end;
definition let V,A;
func id$ A -> Element of Maps V equals
:Def6: [[A,A],id A];
coherence
proof A = {} implies A = {};
hence thesis by Th5;
end;
end;
theorem Th11:
(id$ A)`2 = id A & dom id$ A = A & cod id$ A = A
proof [[dom id$ A,cod id$ A],(id$ A)`2] = id$ A by Th8
.= [[A,A],id A] by Def6;
hence thesis by Lm1,ZFMISC_1:33;
end;
definition let V,m1,m2;
assume A1: cod m1 = dom m2;
func m2*m1 -> Element of Maps V equals
:Def7: [[dom m1,cod m2],m2`2*m1`2];
coherence
proof
A2: (cod m1 <> {} or dom m1 = {}) & m1`2 is Function of dom m1,cod m1 &
(cod m2 <> {} or dom m2 = {}) & m2`2 is Function of dom m2,cod m2 by Th9;
then m2`2*m1`2 is Function of dom m1,cod m2 by A1,FUNCT_2:19;
hence thesis by A1,A2,Th5;
end;
end;
theorem Th12:
dom m2 = cod m1 implies
(m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom m1 & cod(m2*m1) = cod m2
proof assume dom m2 = cod m1;
then [[dom m1,cod m2],m2`2*m1`2]
= m2*m1 by Def7
.= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th8;
hence thesis by Lm1,ZFMISC_1:33;
end;
theorem Th13:
dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)*m1
proof assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2;
(m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom m1 & cod(m2*m1) = cod m2 &
(m3*m2)`2 = m3`2*m2`2 & dom(m3*m2) = dom m2 & cod(m3*m2) = cod m3
by A1,A2,Th12;
then (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) &
dom(m3*(m2*m1)) = dom m1 & cod(m3*(m2*m1)) = cod m3 &
((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 &
dom((m3*m2)*m1) = dom m1 & cod((m3*m2)*m1) = cod m3 &
m3`2*(m2`2*m1`2) = (m3`2*m2`2)*m1`2 by A1,A2,Th12,RELAT_1:55;
hence thesis by Lm2;
end;
theorem Th14:
m*(id$ dom m) = m & (id$ cod m)*m = m
proof set i1 = id$ dom m, i2 = id$ cod m;
A1: (cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m by Th9;
cod i1 = dom m by Th11;
then dom m`2 = dom m &
i1`2 = id dom m & dom i1 = dom m &
(m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 & cod(m*i1) = cod m &
m`2*(id dom m`2) = m`2 by A1,Th11,Th12,FUNCT_1:42,FUNCT_2:def 1;
hence m*i1 = m by Lm2;
dom i2 = cod m & rng m`2 c= cod m by A1,Th11,RELSET_1:12;
then i2`2 = id cod m & cod i2 = cod m &
(i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m & cod(i2*m) = cod i2 &
(id cod m)*m`2 = m`2 by Th11,Th12,RELAT_1:79;
hence thesis by Lm2;
end;
definition let V,A,B;
func Maps(A,B) -> set equals
:Def8: { [[A,B],f] where f is Element of Funcs V: [[A,B],f] in Maps V };
correctness;
end;
theorem Th15:
for f being Function of A,B st B = {} implies A = {}
holds [[A,B],f] in Maps(A,B)
proof let f be Function of A,B;
assume B = {} implies A = {};
then f in Funcs(V) & [[A,B],f] in Maps(V) &
Maps(A,B) = {[[A,B],f'] where f' is Element of Funcs V: [[A,B],f'] in
Maps V}
by Def8,Th1,Th5;
hence thesis;
end;
theorem Th16:
m in Maps(A,B) implies m = [[A,B],m`2]
proof
A1: Maps(A,B) = { [[A,B],f] where f is Element of Funcs V: [[A,B],f] in
Maps V }
by Def8;
assume m in Maps(A,B);
then A2: ex f being Element of Funcs(V) st m = [[A,B],f] &
[[A,B],f] in Maps(V) by A1;
m = [[dom m,cod m],m`2] by Th8;
hence thesis by A2,ZFMISC_1:33;
end;
theorem Th17:
Maps(A,B) c= Maps V
proof let z be set;
A1: Maps(A,B) = {[[A,B],f] where f is Element of Funcs V: [[A,B],f] in Maps V}
by Def8;
assume z in Maps(A,B);
then ex f being Element of Funcs(V) st z = [[A,B],f] & [[A,B],f] in Maps(V)
by A1;
hence thesis;
end;
Lm4: for f being Function st [[A,B],f] in Maps(A,B) holds
(B = {} implies A = {}) & f is Function of A,B
proof let f be Function such that
A1: [[A,B],f] in Maps(A,B);
Maps(A,B) c= Maps V by Th17;
hence thesis by A1,Th10;
end;
theorem
Maps V = union { Maps(A,B): not contradiction }
proof set M = { Maps(A,B): not contradiction };
now let z be set;
thus z in Maps V implies z in union M
proof assume z in Maps V;
then consider f being Element of Funcs(V),A,B being Element of V such that
A1: z = [[A,B],f] & (B = {} implies A = {}) & f is Function of A,B by Th4;
z in Maps(A,B) & Maps(A,B) in M by A1,Th15;
hence thesis by TARSKI:def 4;
end;
assume z in union M;
then consider C being set such that
A2: z in C and
A3: C in M by TARSKI:def 4;
consider A,B such that
A4: C = Maps(A,B) by A3;
Maps(A,B) = { [[A,B],f] where f is Element of Funcs V: [[A,B],f] in
Maps V }
by Def8;
then ex f being Element of Funcs(V) st z = [[A,B],f] & [[A,B],f] in Maps(V)
by A2,A4;
hence z in Maps(V);
end;
hence thesis by TARSKI:2;
end;
theorem Th19:
m in Maps(A,B) iff dom m = A & cod m = B
proof
thus m in Maps(A,B) implies dom m = A & cod m = B
proof assume m in Maps(A,B);
then m = [[A,B],m`2] & m = [[dom m,cod m],m`2] by Th8,Th16;
hence thesis by Lm1;
end;
(cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m by Th9;
then [[dom m,cod m],m`2] in Maps(dom m,cod m) by Th15;
hence thesis by Th8;
end;
theorem Th20:
m in Maps(A,B) implies m`2 in Funcs(A,B)
proof assume
A1: m in Maps(A,B);
then m = [[A,B],m`2] by Th16;
then (B = {} implies A = {}) & m`2 is Function of A,B by A1,Lm4;
hence thesis by FUNCT_2:11;
end;
Lm5:
for W being non empty Subset of V,
A,B being Element of W, A',B' being Element of V st A = A' & B = B'
holds Maps(A,B) = Maps(A',B')
proof let W be non empty Subset of V;
let A,B be Element of W, A',B' be Element of V such that
A1: A = A' & B = B';
now let x be set;
thus x in Maps(A,B) implies x in Maps(A',B')
proof assume
A2: x in Maps(A,B);
A3: Maps(A,B) c= Maps W by Th17;
then A4: x in Maps W by A2;
reconsider m = x as Element of Maps W by A2,A3;
Maps W c= Maps V by Th7;
then reconsider m' = x as Element of Maps V by A4;
m = [[dom m,cod m],m`2] & m' = [[dom m',cod m'],m'`2] & m = [[A,B],m`2]
by A2,Th8,Th16;
then dom m = A & cod m = B & dom m = dom m' & cod m = cod m' by Lm1;
hence thesis by A1,Th19;
end;
assume
A5: x in Maps(A',B');
Maps(A',B') c= Maps V by Th17;
then reconsider m' = x as Element of Maps V by A5;
A6: m' = [[A',B'],m'`2] by A5,Th16;
then (B' = {} implies A' = {}) & m'`2 is Function of A',B' by A5,Lm4;
hence x in Maps(A,B) by A1,A6,Th15;
end;
hence thesis by TARSKI:2;
end;
definition let V,m;
attr m is surjective means rng m`2 = cod(m);
synonym m is_a_surjection;
end;
begin :: Category Ens
definition let V;
func fDom V -> Function of Maps V,V means
:Def10: for m holds it.m = dom m;
existence
proof
deffunc F(Element of Maps V) = dom $1;
ex F being Function of Maps V,V st for m holds F.m = F(m) from LambdaD;
hence thesis;
end;
uniqueness
proof let h1,h2 be Function of Maps V,V such that
A1: for m holds h1.m = dom m and
A2: for m holds h2.m = dom m;
now let m; thus h1.m = dom m by A1 .= h2.m by A2; end;
hence thesis by FUNCT_2:113;
end;
func fCod V -> Function of Maps V,V means
:Def11: for m holds it.m = cod m;
existence
proof
deffunc F(Element of Maps V) = cod $1;
ex F being Function of Maps V,V st for m holds F.m = F(m) from LambdaD;
hence thesis;
end;
uniqueness
proof let h1,h2 be Function of Maps V,V such that
A3: for m holds h1.m = cod m and
A4: for m holds h2.m = cod m;
now let m; thus h1.m = cod m by A3 .= h2.m by A4; end;
hence thesis by FUNCT_2:113;
end;
func fComp V -> PartFunc of [:Maps V,Maps V:],Maps V means
:Def12:
(for m2,m1 holds [m2,m1] in dom it iff dom m2 = cod m1) &
(for m2,m1 st dom m2 = cod m1 holds it.[m2,m1] = m2*m1);
existence
proof
defpred P[set,set,set] means
for m2,m1 st m2=$1 & m1=$2 holds dom m2 = cod m1 & $3 = m2*m1;
A5: for x,y,z being set st x in Maps(V) & y in Maps(V) & P[x,y,z]
holds z in Maps(V)
proof let x,y,z be set;
assume x in Maps(V) & y in Maps(V);
then reconsider m2 = x, m1 = y as Element of Maps(V);
assume P[x,y,z];
then z = m2*m1;
hence thesis;
end;
A6: for x,y,z1,z2 being set
st x in Maps(V) & y in Maps(V) & P[x,y,z1] & P[x,y,z2]
holds z1 = z2
proof let x,y,z1,z2 be set;
assume x in Maps(V) & y in Maps(V);
then reconsider m2 = x, m1 = y as Element of Maps(V);
assume P[x,y,z1] & P[x,y,z2];
then z1 = m2*m1 & z2 = m2*m1;
hence thesis;
end;
consider h being PartFunc of [:Maps(V),Maps(V):],Maps(V) such that
A7: for x,y being set holds [x,y] in dom h iff x in Maps(V) & y in Maps(V) &
ex z being set st P[x,y,z] and
A8: for x,y being set st [x,y] in dom h holds P[x,y,h.[x,y]]
from PartFuncEx2(A5,A6);
take h;
thus
A9: for m2,m1 holds [m2,m1] in dom h iff dom m2 = cod m1
proof let m2,m1;
thus [m2,m1] in dom h implies dom m2 = cod m1
proof assume [m2,m1] in dom h;
then ex z being set st P[m2,m1,z] by A7;
hence thesis;
end;
assume dom m2 = cod m1;
then P[m2,m1,m2*m1];
hence thesis by A7;
end;
let m2,m1;
assume dom m2 = cod m1;
then [m2,m1] in dom h by A9;
hence thesis by A8;
end;
uniqueness
proof let h1,h2 be PartFunc of [:Maps V,Maps V:],Maps V such that
A10: for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A11: for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A12: for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A13: for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
now
thus
A14: dom h1 c= [:Maps V,Maps V:] by RELSET_1:12;
thus
A15: dom h2 c= [:Maps V,Maps V:] by RELSET_1:12;
let x,y be set;
thus [x,y] in dom h1 implies [x,y] in dom h2
proof assume
A16: [x,y] in dom h1;
then reconsider m2 = x, m1 = y as Element of Maps V by A14,ZFMISC_1:106;
dom m2 = cod m1 by A10,A16;
hence thesis by A12;
end;
assume
A17: [x,y] in dom h2;
then reconsider m2 = x, m1 = y as Element of Maps V by A15,ZFMISC_1:106;
dom m2 = cod m1 by A12,A17;
hence [x,y] in dom h1 by A10;
end;
then A18: dom h1 = dom h2 by ZFMISC_1:110;
now let m be Element of [:Maps V,Maps V:];
assume
A19: m in dom h1;
consider m2,m1 such that
A20: m = [m2,m1] by DOMAIN_1:9;
dom m2 = cod m1 by A10,A19,A20;
then h1.[m2,m1] = m2*m1 & h2.[m2,m1] = m2*m1 by A11,A13;
hence h1.m = h2.m by A20;
end;
hence thesis by A18,PARTFUN1:34;
end;
func fId V -> Function of V,Maps V means
:Def13: for A holds it.A = id$ A;
existence
proof
deffunc F(Element of V) = id$ $1;
ex F being Function of V, Maps V st for A holds F.A = F(A) from LambdaD;
hence thesis;
end;
uniqueness
proof let h1,h2 be Function of V,Maps V such that
A21: for A holds h1.A = id$ A and
A22: for A holds h2.A = id$ A;
now let A; thus h1.A = id$ A by A21 .= h2.A by A22; end;
hence thesis by FUNCT_2:113;
end;
end;
definition let V;
func Ens(V) -> CatStr equals
:Def14: CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #);
coherence;
end;
theorem Th21:
CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) is Category
proof
set M = Maps V, d = fDom V, c = fCod V, p = fComp V, i = fId V;
now
thus for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f
proof let f,g be Element of M;
d.g = dom g & c.f = cod f by Def10,Def11;
hence thesis by Def12;
end;
thus for f,g being Element of M
st d.g=c.f holds d.(p.[g,f]) = d.f & c.(p.[g,f]) = c.g
proof let f,g be Element of M such that
A1: d.g=c.f;
d.g = dom g & c.f = cod f by Def10,Def11;
then dom(g*f) = dom f & cod(g*f) = cod g & p.[g,f] = g*f &
d.f = dom f & c.g = cod g by A1,Def10,Def11,Def12,Th12;
hence thesis by Def10,Def11;
end;
thus for f,g,h being Element of M
st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f]
proof let f,g,h be Element of M such that
A2: d.h = c.g and
A3: d.g = c.f;
A4: dom h = d.h & cod g = c.g & dom g = d.g & cod f = c.f by Def10,Def11;
then A5: cod(g*f) = dom h & dom(h*g) = dom g by A2,A3,Th12;
thus p.[h,p.[g,f]]
= p.[h,g*f] by A3,A4,Def12
.= h*(g*f) by A5,Def12
.= (h*g)*f by A2,A3,A4,Th13
.= p.[h*g,f] by A3,A4,A5,Def12
.= p.[p.[h,g],f] by A2,A4,Def12;
end;
let b be Element of V;
A6: i.b = id$ b & dom id$ b = b & cod id$ b = b by Def13,Th11;
hence d.(i.b) = b & c.(i.b) = b by Def10,Def11;
thus for f being Element of M st c.f=b holds p.[i.b,f] = f
proof let f be Element of M such that
A7: c.f = b;
A8: cod f = c.f by Def11;
then (id$ b)*f = f by A7,Th14;
hence thesis by A6,A7,A8,Def12;
end;
let g be Element of M such that
A9: d.g=b;
A10: dom g = d.g by Def10;
then g*(id$ b) = g by A9,Th14;
hence p.[g,i.b] = g by A6,A9,A10,Def12;
end;
hence thesis by CAT_1:def 8;
end;
definition let V;
cluster Ens(V) -> strict Category-like;
coherence
proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
hence thesis by Th21;
end;
end;
reserve a,b for Object of Ens(V);
theorem Th22:
A is Object of Ens(V)
proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
hence thesis;
end;
definition let V,A;
func @A -> Object of Ens(V) equals
:Def15: A;
coherence by Th22;
end;
theorem Th23:
a is Element of V
proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
hence thesis;
end;
definition let V,a;
func @a -> Element of V equals
:Def16: a;
coherence by Th23;
end;
Lm6: @@A = A & @@a = a
proof
thus @@A = @A by Def16 .= A by Def15;
thus @@a = @a by Def15 .= a by Def16;
end;
reserve f,g,f1,f2 for Morphism of Ens(V);
theorem Th24:
m is Morphism of Ens(V)
proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
hence thesis;
end;
definition let V,m;
func @m -> Morphism of Ens(V) equals
:Def17: m;
coherence by Th24;
end;
theorem Th25:
f is Element of Maps(V)
proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
hence thesis;
end;
definition let V,f;
func @f -> Element of Maps(V) equals
:Def18: f;
coherence by Th25;
end;
Lm7: @@m = m & @@f = f
proof
thus @@m = @m by Def18 .= m by Def17;
thus @@f = @f by Def17 .= f by Def18;
end;
theorem Th26:
dom f = dom(@f) & cod f = cod(@f)
proof
A1: Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
hence dom(@f) = (the Dom of Ens(V)).@f by Def10
.= (the Dom of Ens(V)).f by Def18
.= dom f by CAT_1:def 2;
thus cod(@f) = (the Cod of Ens(V)).@f by A1,Def11
.= (the Cod of Ens(V)).f by Def18
.= cod f by CAT_1:def 3;
end;
theorem Th27:
Hom(a,b) = Maps(@a,@b)
proof
now let x be set;
thus x in Hom(a,b) implies x in Maps(@a,@b)
proof assume
A1: x in Hom(a,b);
then reconsider f = x as Morphism of Ens(V);
dom(f) = a & cod(f) = b by A1,CAT_1:18;
then dom(@f) = a & cod(@f) = b by Th26;
then dom(@f) = @a & cod(@f) = @b by Def16;
then @f in Maps(@a,@b) by Th19;
hence thesis by Def18;
end;
assume
A2: x in Maps(@a,@b);
Maps(@a,@b) c= Maps V by Th17;
then reconsider m = x as Element of Maps V by A2;
dom(m) = @a & cod(m) = @b by A2,Th19;
then dom(m) = a & cod(m) = b by Def16;
then dom(@@m) = a & cod(@@m) = b by Lm7;
then dom(@m) = a & cod(@m) = b by Th26;
then @m in Hom(a,b) by CAT_1:18;
hence x in Hom(a,b) by Def17;
end;
hence thesis by TARSKI:2;
end;
Lm8: Hom(a,b) <> {} implies Funcs(@a,@b) <> {}
proof assume Hom(a,b) <> {};
then A1: Maps(@a,@b) <> {} by Th27;
consider m being Element of Maps(@a,@b);
Maps(@a,@b) c= Maps V by Th17;
then reconsider m as Element of Maps(V) by A1,TARSKI:def 3;
m`2 in Funcs(@a,@b) by A1,Th20;
hence Funcs(@a,@b) <> {};
end;
theorem Th28:
dom g = cod f implies g*f = (@g)*(@f)
proof assume
A1: dom g = cod f;
A2: Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
dom(@g) = cod f by A1,Th26;
then A3: dom(@g) = cod(@f) by Th26;
thus g*f = (the Comp of Ens(V)).[g,f] by A1,CAT_1:41
.= (the Comp of Ens(V)).[@g,f] by Def18
.= (fComp V).[@g,@f] by A2,Def18
.= (@g)*(@f) by A3,Def12;
end;
theorem Th29:
id a = id$(@a)
proof
A1: Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
thus id a = (the Id of Ens(V)).a by CAT_1:def 5
.= (fId V).(@a) by A1,Def16
.= id$(@a) by Def13;
end;
theorem
a = {} implies a is initial
proof assume a = {};
then A1: @a = {} by Def16;
let b;
set m = [[@a,@b],{}];
{} is Function of @a,@b by A1,FUNCT_2:55,RELAT_1:60;
then A2: m in Maps(@a,@b) by A1,Th15;
Maps(@a,@b) <> {} by A1,Th15;
hence
A3: Hom(a,b)<>{} by Th27;
m in Hom(a,b) by A2,Th27;
then reconsider f = m as Morphism of a,b by CAT_1:def 7;
take f;
let g be Morphism of a,b;
g in Hom(a,b) by A3,CAT_1:def 7;
then A4: g in Maps(@a,@b) by Th27;
Maps(@a,@b) c= Maps V by Th17;
then reconsider m, m' = g as Element of Maps(V) by A2,A4;
A5: m' = [[@a,@b],m'`2] by A4,Th16;
m = [[dom m,cod m],m`2] by Th8;
then m`2 = {} & m'`2 is Function of @a,@b by A4,A5,Lm4,ZFMISC_1:33;
hence thesis by A1,A5,PARTFUN1:57;
end;
theorem Th31:
{} in V & a is initial implies a = {}
proof assume {} in V;
then reconsider B = {} as Element of V;
set b = @B;
assume a is initial;
then Hom(a,b) <> {} & b = {} by Def15,CAT_1:def 16;
then Funcs(@a,@b) <> {} & @b = {} by Def16,Lm8;
then @a = {} by FUNCT_2:14;
hence thesis by Def16;
end;
theorem
for W being Universe, a being Object of Ens(W) st a is initial
holds a = {}
proof let W be Universe, a be Object of Ens(W);
{} in W by CLASSES2:62; hence thesis by Th31;
end;
theorem
(ex x being set st a = {x}) implies a is terminal
proof given x being set such that
A1: a = {x};
A2: @a = {x} by A1,Def16;
let b;
consider h being Function of @b,@a;
set m = [[@b,@a],h];
A3: m in Maps(@b,@a) by A2,Th15;
then m in Hom(b,a) by Th27;
then reconsider f = m as Morphism of b,a by CAT_1:def 7;
thus
A4: Hom(b,a)<>{} by A3,Th27;
take f;
let g be Morphism of b,a;
g in Hom(b,a) by A4,CAT_1:def 7;
then A5: g in Maps(@b,@a) by Th27;
Maps(@b,@a) c= Maps V by Th17;
then reconsider m, m' = g as Element of Maps(V) by A3,A5;
A6: m' = [[@b,@a],m'`2] by A5,Th16;
m = [[dom m,cod m],m`2] by Th8;
then m`2 = h & m'`2 is Function of @b,@a by A5,A6,Lm4,ZFMISC_1:33;
hence thesis by A2,A6,FUNCT_2:66;
end;
theorem Th34:
V <> {{}} & a is terminal implies ex x being set st a = {x}
proof assume that
A1: V <> {{}} and
A2: a is terminal;
A3:
now assume
A4: @a = {};
now
consider C being set such that
A5: C in V and
A6: C <> {} by A1,ZFMISC_1:41;
reconsider C as Element of V by A5;
set b = @C;
Hom(b,a) <> {} & b <> {} by A2,A6,Def15,CAT_1:def 15;
then Funcs(@b,@a) <> {} & @b <> {} by Def16,Lm8;
hence contradiction by A4,FUNCT_2:14;
end;
hence contradiction;
end;
consider x being Element of @a;
now assume a <> {x};
then @a <> {x} by Def16;
then consider y being set such that
A7: y in @a and
A8: y <> x by A3,ZFMISC_1:41;
deffunc F(set) = x;
deffunc G(set) = y;
A9: for z being set st z in @a holds F(z) in @a;
consider fx being Function of @a,@a such that
A10: for z being set st z in @a holds fx.z = F(z) from Lambda1(A9);
A11: for z being set st z in @a holds G(z) in @a by A7;
consider fy being Function of @a,@a such that
A12: for z being set st z in @a holds fy.z = G(z) from Lambda1(A11);
@a = {} implies @a = {};
then A13: ([[@a,@a],fx]) in Maps(@a,@a) & ([[@a,@a],fy]) in Maps(@a,@a) by
Th15;
Maps(@a,@a) c= Maps V by Th17;
then reconsider m1 = [[@a,@a],fx],m2 = [[@a,@a],fy] as Element of Maps(V)
by A13;
m1 in Hom(a,a) & m2 in Hom(a,a) by A13,Th27;
then (@m1) in Hom(a,a) & (@m2) in Hom(a,a) by Def17;
then reconsider f = @m1,g = @m2 as Morphism of a,a by CAT_1:def 7;
consider h being Morphism of a,a such that
A14: for h' being Morphism of a,a holds h = h' by A2,CAT_1:def 15;
now thus f = h by A14 .= g by A14;
thus f = [[@a,@a],fx] & g = [[@a,@a],fy] by Def17;
fx.y = x & fy.y = y by A7,A10,A12;
hence fx <> fy by A8;
end;
hence contradiction by ZFMISC_1:33;
end;
hence thesis;
end;
theorem
for W being Universe, a being Object of Ens(W) st a is terminal
ex x being set st a = {x}
proof let W be Universe, a be Object of Ens(W);
now assume
A1: W = {{}};
{} in W by CLASSES2:62;
then {{}} in W by CLASSES2:63;
hence contradiction by A1;
end;
hence thesis by Th34;
end;
theorem
f is monic iff (@f)`2 is one-to-one
proof set m = @f;
thus f is monic implies (@f)`2 is one-to-one
proof assume
A1: f is monic;
set A = dom (@f)`2;
let x1,x2 be set such that
A2: x1 in A & x2 in A and
A3: (@f)`2.x1 = (@f)`2.x2;
A4: A = dom(@f) by Lm3;
then reconsider A as Element of V;
reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A
by A2,FUNCOP_1:57;
reconsider m1 = [[A,A],fx1],m2 = [[A,A],fx2] as Element of Maps(V) by A2,
Th5;
set f1 = @m1, f2 = @m2;
A5: m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] by Th8;
then dom m1 = A & dom m2 = A & cod m1 = A & cod m2 = A by Lm1;
then A6: dom(@f1) = A & dom(@f2) = A & cod(@f1) = A & cod(@f2) = A
by Lm7;
then A7: dom f1 = A & dom f2 = A & cod f1 = A & cod f2 = A & dom f = A
by A4,Th26;
set h1 = (@f)`2*(@f1)`2, h2 = (@f)`2*(@f2)`2;
set ff1 = (@f)*(@f1), ff2 = (@f)*(@f2);
now
A8: (ff1)`2 = h1 & dom(ff1) = dom(@f1) & cod(ff1) = cod(@f) &
(ff2)`2 = h2 & dom(ff2) = dom(@f2) & cod(ff2) = cod(@f) by A4,A6,Th12;
hence ff1=[[dom(@f1),cod(@f)],h1] & ff2=[[dom(@f2),cod(@f)],h2] by Th8;
now
thus
A9: dom(h1) = A & dom(h2) = A by A6,A8,Lm3;
let x be set;
assume
A10: x in A;
fx1 = m1`2 & fx2 = m2`2 by A5,ZFMISC_1:33;
then fx1 = (@f1)`2 & fx2 =(@f2)`2 by Lm7;
then (@f1)`2.x = x1 & (@f2)`2.x = x2 by A10,FUNCOP_1:13;
then h1.x = (@f)`2.x1 & h2.x = (@f)`2.x2 by A9,A10,FUNCT_1:22;
hence h1.x = h2.x by A3;
end;
hence h1 = h2 by FUNCT_1:9;
end;
then ff1 = ff2 & f*(f1) = ff1 & f*(f2) = ff2 by A6,A7,Th28;
then f1 = f2 & @m1 = m1 & @m2 = m2 by A1,A7,Def17,CAT_1:def 10;
then fx1 = fx2 by ZFMISC_1:33;
hence x1 = fx2.x1 by A2,FUNCOP_1:13 .= x2 by A2,FUNCOP_1:13;
end;
assume
A11: m`2 is one-to-one;
let f1,f2 such that
A12: dom f1 = dom f2 and
A13: cod f1 = dom f & cod f2 = dom f and
A14: f*f1 = f*f2;
set m1 = @f1, m2 = @f2;
A15: dom m1 = dom f1 & dom m2 = dom f2 & cod m1 = cod f1 & cod m2 = cod f2 &
dom m = dom f by Th26;
then m*m1 = f*f1 & m*m2 = f*f2 &
m*m1 = [[dom m1,cod m],m`2*m1`2] & m*m2 = [[dom m2,cod m],m`2*m2`2]
by A13,Def7,Th28;
then dom m1`2 = dom f1 & dom m2`2 = dom f2 & dom m`2 = dom f &
rng m1`2 c= cod f1 & rng m2`2 c= cod f2 & (m`2)*(m1`2) = (m`2)*(m2`2)
by A14,A15,Lm3,ZFMISC_1:33;
then m1`2 = m2`2 & m1=[[dom m1,cod m1],m1`2] & m2=[[dom m2,cod m2],m2`2]
by A11,A12,A13,Th8,FUNCT_1:49;
hence f1 = m2 by A12,A13,A15,Def18 .= f2 by Def18;
end;
theorem Th37:
f is epi & (ex A st ex x1,x2 being set st x1 in A & x2 in A & x1 <> x2)
implies @f is_a_surjection
proof
assume
A1: f is epi;
given B being Element of V, x1,x2 being set such that
A2: x1 in B & x2 in B and
A3: x1 <> x2;
A4: rng (@f)`2 c= cod(@f) by Lm3;
cod(@f) c= rng (@f)`2
proof let x be set;
set A = cod(@f);
assume that
A5: x in A and
A6: not x in rng (@f)`2;
reconsider g1 = A --> x1 as Function of A,B by A2,FUNCOP_1:57;
set h = {x} --> x2, g2 = g1 +* h;
A7: x in {x} by TARSKI:def 1;
A8: dom g1 = A & dom h = {x} by FUNCOP_1:19;
then A9: dom g2 = A \/ {x} by FUNCT_4:def 1 .= A by A5,ZFMISC_1:46;
rng g1 = {x1} & rng h = {x2} by A5,FUNCOP_1:14;
then rng g2 c= {x1} \/ {x2} by FUNCT_4:18;
then rng g2 c= {x1,x2} & {x1,x2} c= B by A2,ENUMSET1:41,ZFMISC_1:38;
then rng g2 c= B by XBOOLE_1:1;
then reconsider g2 as Function of A,B by A2,A9,FUNCT_2:def 1,RELSET_1:11;
reconsider m1 = [[A,B],g1], m2 = [[A,B],g2]
as Element of Maps(V) by A2,Th5;
set f1 = @m1, f2 = @m2;
A10: m1 = f1 & m2 = f2 by Def17;
A11: m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] by Th8;
then dom m1 = A & dom m2 = A & cod m1 = B & cod m2 = B by Lm1;
then A12: dom(@f1) = A & dom(@f2) = A & cod(@f1) = B & cod(@f2) = B
by Lm7;
then A13: dom f1 = A & dom f2 = A & cod f1 = B & cod f2 = B & cod f = A
by Th26;
A14: g1 = m1`2 & g2 = m2`2 by A11,ZFMISC_1:33;
set h1 = (@f1)`2*(@f)`2, h2 = (@f2)`2*(@f)`2;
set f1f = (@f1)*(@f), f2f = (@f2)*(@f);
now
A15: (f1f)`2 = h1 & dom(f1f) = dom(@f) & cod(f1f) = cod(@f1) &
(f2f)`2 = h2 & dom(f2f) = dom(@f) & cod(f2f) = cod(@f2) by A12,Th12;
hence f1f=[[dom(@f),cod(@f1)],h1] & f2f=[[dom(@f),cod(@f2)],h2] by Th8;
now
thus
A16: dom(h1) = dom(@f) & dom(h2) = dom(@f) by A15,Lm3;
let z be set;
set y = (@f)`2.z;
assume
A17: z in dom(@f);
then z in dom (@f)`2 by Lm3;
then y in rng (@f)`2 by FUNCT_1:def 5;
then g1 = (@f1)`2 & g2 =(@f2)`2 & y in A & not y in {x}
by A4,A6,A14,Lm7,TARSKI:def 1;
then h1.z = g1.y & h2.z = g2.y & not y in {x} & g1.y = x1
by A16,A17,FUNCOP_1:13,FUNCT_1:22;
hence h1.z = h2.z by A8,FUNCT_4:12;
end;
hence h1 = h2 by FUNCT_1:9;
end;
then f1f = f2f & f1*f = f1f & f2*f = f2f & h.x = x2
by A7,A12,A13,Th28,FUNCOP_1:13;
then f1 = f2 & g1.x = x1 & g2.x = x2
by A1,A5,A7,A8,A13,CAT_1:def 11,FUNCOP_1:13,FUNCT_4:14;
hence contradiction by A3,A10,ZFMISC_1:33;
end;
hence rng (@f)`2 = cod(@f) by A4,XBOOLE_0:def 10;
end;
theorem
@f is_a_surjection implies f is epi
proof set m = @f;
assume
A1: rng m`2 = cod m;
let f1,f2 such that
A2: dom f1 = cod f & dom f2 = cod f & cod f1 = cod f2 and
A3: f1*f=f2*f;
set m1 = @f1, m2 = @f2;
A4: dom m1 = dom f1 & dom m2 = dom f2 & cod m1 = cod f1 & cod m2 = cod f2 &
cod m = cod f by Th26;
then m1*m = f1*f & m2*m = f2*f &
m1*m = [[dom m,cod m1],m1`2*m`2] & m2*m = [[dom m,cod m2],m2`2*m`2]
by A2,Def7,Th28;
then (m1`2)*(m`2) = (m2`2)*(m`2) & dom m1`2 = dom f1 & dom m2`2 = dom f2
by A3,A4,Lm3,ZFMISC_1:33;
then m1`2 = m2`2 & m1=[[dom m1,cod m1],m1`2] & m2=[[dom m2,cod m2],m2`2]
by A1,A2,A4,Th8,FUNCT_1:156;
hence f1 = m2 by A2,A4,Def18 .= f2 by Def18;
end;
theorem
for W being Universe, f being Morphism of Ens(W) st f is epi
holds @f is_a_surjection
proof let W be Universe, f be Morphism of Ens(W);
A1: {} in W by CLASSES2:62;
then {{}} in W by CLASSES2:63;
then {{},{{}}} in W & {} in {{},{{}}} & {{}} in {{},{{}}} & {{}} <> {}
by A1,CLASSES2:64,TARSKI:def 2;
hence thesis by Th37;
end;
theorem
for W being non empty Subset of V holds Ens(W) is_full_subcategory_of Ens(
V
)
proof let W be non empty Subset of V;
A1: Ens(W) = CatStr(# W,Maps W,fDom W,fCod W,fComp W,fId W #) &
Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
A2: for a,b being Object of Ens(W), a',b' being Object of Ens(V)
st a = a' & b = b' holds Hom(a,b) = Hom(a',b')
proof let a,b be Object of Ens(W), a',b' be Object of Ens(V);
assume a = a' & b = b';
then @a = a & @a' = a & @b = b & @b' = b &
Hom(a,b) = Maps(@a,@b) & Hom(a',b') = Maps(@a',@b') by Def16,Th27;
hence Hom(a,b) = Hom(a',b') by Lm5;
end;
thus Ens(W) is Subcategory of Ens(V)
proof
thus the Objects of Ens(W) c= the Objects of Ens(V) by A1;
thus for a,b being Object of Ens(W), a',b' being Object of Ens(V)
st a = a' & b = b' holds Hom(a,b) c= Hom(a',b') by A2;
set w = the Comp of Ens(W), v = the Comp of Ens(V);
now
A3: dom w c= [:Maps W,Maps W:] & dom v c= [:Maps V,Maps V:]
by A1,RELSET_1:12;
A4: Maps W c= Maps V by Th7;
thus
A5: dom w c= dom v
proof let x be set; assume
A6: x in dom w;
then consider m2,m1 being Element of Maps W such that
A7: x = [m2,m1] by A3,DOMAIN_1:9;
reconsider m1' = m1, m2' = m2 as Element of Maps V by A4,TARSKI:def 3;
m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] &
m1' = [[dom m1',cod m1'],m1'`2] & m2' = [[dom m2',cod m2'],m2'`2]
by Th8;
then dom m2' = dom m2 & cod m1' = cod m1 & dom m2 = cod m1
by A1,A6,A7,Def12,Lm1;
hence x in dom v by A1,A7,Def12;
end;
let x be set; assume
A8: x in dom w;
then consider m2,m1 being Element of Maps W such that
A9: x = [m2,m1] by A3,DOMAIN_1:9;
reconsider m1' = m1, m2' = m2 as Element of Maps V by A4,TARSKI:def 3;
A10: dom m2' = cod m1' & dom m2 = cod m1 by A1,A5,A8,A9,Def12;
m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] &
m1' = [[dom m1',cod m1'],m1'`2] & m2' = [[dom m2',cod m2'],m2'`2] by Th8;
then m1`2 = m1'`2 & m2`2 = m2'`2 & dom m1 = dom m1' & cod m2 = cod m2'
by Lm1;
then m2*m1=[[dom m1,cod m2],m2`2*m1`2] & m2'*m1'=[[dom m1,cod m2],
m2`2*m1`2]
by A10,Def7;
hence w.x = m2'*m1' by A1,A9,A10,Def12 .= v.x by A1,A9,A10,Def12;
end;
hence the Comp of Ens(W) <= the Comp of Ens(V) by GRFUNC_1:8;
let a be Object of Ens(W), a' be Object of Ens(V);
assume a = a';
then @a = a & @a' = a by Def16;
then id$(@a) = [[@a,@a],id(@a)] & id$(@a') = [[@a,@a],id(@a)] by Def6;
hence id a = id$(@a') by Th29 .= id a' by Th29;
end;
thus thesis by A2;
end;
begin :: Representable Functors
reserve C for Category, a,b,a',b',c for Object of C,
f,g,h,f',g' for Morphism of C;
definition let C;
func Hom(C) -> set equals
:Def19: { Hom(a,b): not contradiction };
coherence;
end;
definition let C;
cluster Hom(C) -> non empty;
coherence
proof consider a;
Hom(a,a) in { Hom(a',b'): not contradiction };
hence thesis by Def19;
end;
end;
theorem Th41:
Hom(a,b) in Hom(C)
proof Hom(C) = { Hom(a',b'): not contradiction } by Def19; hence thesis; end
;
:: hom-functors
theorem
(Hom(a,cod f) = {} implies Hom(a,dom f) = {}) &
(Hom(dom f,a) = {} implies Hom(cod f,a) = {})
proof Hom(dom f,cod f) <> {} by CAT_1:19; hence thesis by CAT_1:52; end;
definition let C,a,f;
func hom(a,f) -> Function of Hom(a,dom f),Hom(a,cod f) means
:Def20: for g st g in Hom(a,dom f) holds it.g = f*g;
existence
proof set X = Hom(a,dom f), Y = Hom(a,cod f);
defpred P[set,set] means for g st g = $1 holds $2 = f*g;
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
proof let x be set; assume
A2: x in X;
then reconsider g = x as Morphism of a,dom f by CAT_1:def 7;
take f*g;
X <> {} & Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f
by A2,CAT_1:18,22;
hence thesis by CAT_1:51;
end;
consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being set st x in X holds P[x,h.x] from NonUniqBoundFuncEx(A1);
Hom(dom f,cod f) <> {} by CAT_1:19;
then Y = {} implies X = {} by CAT_1:52;
then reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:11;
take h; thus thesis by A4;
end;
uniqueness
proof set X = Hom(a,dom f), Y = Hom(a,cod f);
let h1,h2 be Function of X,Y such that
A5: for g st g in X holds h1.g = f*g and
A6: for g st g in X holds h2.g = f*g;
now
now let x be set;
assume
A7: x in X;
then reconsider g = x as Morphism of C;
thus h1.x = f*g by A5,A7 .= h2.x by A6,A7;
end;
hence thesis by FUNCT_2:18;
end;
hence thesis;
end;
func hom(f,a) -> Function of Hom(cod f,a),Hom(dom f,a) means
:Def21: for g st g in Hom(cod f,a) holds it.g = g*f;
existence
proof set X = Hom(cod f,a), Y = Hom(dom f,a);
defpred P[set,set] means for g st g = $1 holds $2 = g*f;
A8: for x being set st x in X ex y being set st y in Y & P[x,y]
proof let x be set; assume
A9: x in X;
then reconsider g = x as Morphism of cod f,a by CAT_1:def 7;
take g*f;
X <> {} & Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f
by A9,CAT_1:19,22;
hence thesis by CAT_1:51;
end;
consider h being Function such that
A10: dom h = X & rng h c= Y and
A11: for x being set st x in X holds P[x,h.x] from NonUniqBoundFuncEx(A8);
Hom(dom f,cod f) <> {} by CAT_1:19;
then Y = {} implies X = {} by CAT_1:52;
then reconsider h as Function of X,Y by A10,FUNCT_2:def 1,RELSET_1:11;
take h; thus thesis by A11;
end;
uniqueness
proof set X = Hom(cod f,a), Y = Hom(dom f,a);
let h1,h2 be Function of X,Y such that
A12: for g st g in X holds h1.g = g*f and
A13: for g st g in X holds h2.g = g*f;
now
now let x be set;
assume
A14: x in X;
then reconsider g = x as Morphism of C;
thus h1.x = g*f by A12,A14 .= h2.x by A13,A14;
end;
hence thesis by FUNCT_2:18;
end;
hence thesis;
end;
end;
theorem Th43:
hom(a,id c) = id Hom(a,c)
proof set A = Hom(a,c);
A1: dom id c = c & cod id c = c by CAT_1:44;
now
A = {} implies A = {};
hence dom hom(a,id c) = A by A1,FUNCT_2:def 1;
let x be set;
assume
A2: x in A;
then reconsider g = x as Morphism of C;
A3: cod g = c by A2,CAT_1:18;
thus hom(a,id c).x = id(c)*g by A1,A2,Def20
.= x by A3,CAT_1:46;
end;
hence thesis by FUNCT_1:34;
end;
theorem Th44:
hom(id c,a) = id Hom(c,a)
proof
set A = Hom(c,a);
A1: dom id c = c & cod id c = c by CAT_1:44;
now
A = {} implies A = {};
hence dom hom(id c,a) = A by A1,FUNCT_2:def 1;
let x be set;
assume
A2: x in A;
then reconsider g = x as Morphism of C;
A3: dom g = c by A2,CAT_1:18;
thus hom(id(c),a).x = g * id(c) by A1,A2,Def21
.= x by A3,CAT_1:47;
end;
hence thesis by FUNCT_1:34;
end;
theorem Th45:
dom g = cod f implies hom(a,g*f) = hom(a,g)*hom(a,f)
proof assume
A1: dom g = cod f;
then A2: dom(g*f) = dom f & cod(g*f) = cod g by CAT_1:42;
now set h = hom(a,g*f), h2 = hom(a,g), h1 = hom(a,f);
Hom(dom f,cod f) <> {} by CAT_1:19;
then A3: Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:52;
Hom(dom g,cod g) <> {} by CAT_1:19;
then A4: Hom(a,cod g) = {} implies Hom(a,dom g) = {} by CAT_1:52;
hence dom h = Hom(a,dom f) by A1,A2,A3,FUNCT_2:def 1;
h2*h1 is Function of Hom(a,dom f),Hom(a,cod g) by A1,A3,FUNCT_2:19;
hence
A5: dom(h2*h1) = Hom(a,dom f) by A1,A3,A4,FUNCT_2:def 1;
let x be set;
assume
A6: x in Hom(a,dom f);
then reconsider f' = x as Morphism of C;
A7: h1.x in Hom(a,dom g) by A1,A3,A6,FUNCT_2:7;
then reconsider g' = h1.x as Morphism of C;
A8: cod f' = dom f by A6,CAT_1:18;
thus h.x = g*f*f' by A2,A6,Def20
.= g*(f*f') by A1,A8,CAT_1:43
.= g*g' by A6,Def20
.= h2.g' by A7,Def20
.= (h2*h1).x by A5,A6,FUNCT_1:22;
end;
hence thesis by FUNCT_1:9;
end;
theorem Th46:
dom g = cod f implies hom(g*f,a) = hom(f,a)*hom(g,a)
proof assume
A1: dom g = cod f;
then A2: dom(g*f) = dom f & cod(g*f) = cod g by CAT_1:42;
now set h = hom(g*f,a), h2 = hom(g,a), h1 = hom(f,a);
Hom(dom f,cod f) <> {} by CAT_1:19;
then A3: Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:52;
Hom(dom g,cod g) <> {} by CAT_1:19;
then A4: Hom(dom g,a) = {} implies Hom(cod g,a) = {} by CAT_1:52;
hence dom h = Hom(cod g,a) by A1,A2,A3,FUNCT_2:def 1;
h1*h2 is Function of Hom(cod g,a),Hom(dom f,a) by A1,A4,FUNCT_2:19;
hence
A5: dom(h1*h2) = Hom(cod g,a) by A1,A3,A4,FUNCT_2:def 1;
let x be set;
assume
A6: x in Hom(cod g,a);
then reconsider f' = x as Morphism of C;
A7: h2.x in Hom(cod f,a) by A1,A4,A6,FUNCT_2:7;
then reconsider g' = h2.x as Morphism of C;
A8: dom f' = cod g by A6,CAT_1:18;
thus h.x = f'*(g*f) by A2,A6,Def21
.= f'*g*f by A1,A8,CAT_1:43
.= g'*f by A6,Def21
.= h1.g' by A7,Def21
.= (h1*h2).x by A5,A6,FUNCT_1:22;
end;
hence thesis by FUNCT_1:9;
end;
theorem Th47:
[[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] is Element of Maps(Hom(C))
proof
Hom(dom f,cod f) <> {} by CAT_1:19;
then (Hom(a,cod f) = {} implies Hom(a,dom f) = {}) &
Hom(a,dom f) in Hom(C) & Hom(a,cod f) in Hom(C) by Th41,CAT_1:52;
hence thesis by Th5;
end;
theorem Th48:
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] is Element of Maps(Hom(C))
proof
Hom(dom f,cod f) <> {} by CAT_1:19;
then (Hom(dom f,a) = {} implies Hom(cod f,a) = {}) &
Hom(dom f,a) in Hom(C) & Hom(cod f,a) in Hom(C) by Th41,CAT_1:52;
hence thesis by Th5;
end;
definition let C,a;
func hom?-(a) -> Function of the Morphisms of C, Maps(Hom(C)) means
:Def22: for f holds it.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
existence
proof set X = the Morphisms of C, Y = Maps(Hom(C));
defpred P[set,set] means
for f st f = $1 holds $2 = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
proof let x be set;
assume x in X;
then reconsider f = x as Morphism of C;
take y = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
y is Element of Y by Th47;
hence thesis;
end;
consider h being Function such that
A2: dom h = X & rng h c= Y and
A3: for x being set st x in X holds P[x,h.x] from NonUniqBoundFuncEx(A1);
reconsider h as Function of X,Y by A2,FUNCT_2:def 1,RELSET_1:11;
take h; thus thesis by A3;
end;
uniqueness
proof let h1,h2 be Function of the Morphisms of C, Maps(Hom(C)) such that
A4: for f holds h1.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] and
A5: for f holds h2.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
now let f;
thus h1.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by A4 .= h2.f by A5;
end;
hence thesis by FUNCT_2:113;
end;
func hom-?(a) -> Function of the Morphisms of C, Maps(Hom(C)) means
:Def23: for f holds it.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
existence
proof set X = the Morphisms of C, Y = Maps(Hom(C));
defpred P[set,set] means
for f st f = $1 holds $2 = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
A6: for x being set st x in X ex y being set st y in Y & P[x,y]
proof let x be set;
assume x in X;
then reconsider f = x as Morphism of C;
take y = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
y is Element of Y by Th48;
hence thesis;
end;
consider h being Function such that
A7: dom h = X & rng h c= Y and
A8: for x being set st x in X holds P[x,h.x] from NonUniqBoundFuncEx(A6);
reconsider h as Function of X,Y by A7,FUNCT_2:def 1,RELSET_1:11;
take h; thus thesis by A8;
end;
uniqueness
proof let h1,h2 be Function of the Morphisms of C, Maps(Hom(C)) such that
A9: for f holds h1.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] and
A10: for f holds h2.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
now let f;
thus h1.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by A9 .= h2.f by A10;
end;
hence thesis by FUNCT_2:113;
end;
end;
Lm9: for T being Function of the Morphisms of C, Maps(Hom(C)) st Hom(C) c= V
holds T is Function of the Morphisms of C, the Morphisms of Ens V
proof let T be Function of the Morphisms of C, Maps(Hom(C));
assume Hom(C) c= V;
then Hom(C) is non empty Subset of V &
Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #)
by Def14;
then Maps(Hom(C)) c= Maps(V) & the Morphisms of Ens V = Maps V &
Maps(Hom(C)) <> {} by Th7;
hence thesis by FUNCT_2:9;
end;
Lm10:
Hom(C) c= V implies
for d being Object of Ens(V) st d = Hom(a,c) holds (hom?-(a)).(id c) = id d
proof
assume
A1: Hom(C) c= V;
let d be Object of Ens(V) such that
A2: d = Hom(a,c);
Hom(a,c) in Hom(C) by Th41;
then reconsider A = Hom(a,c) as Element of V by A1;
dom id c = c & cod id c = c & hom(a,id c) = id A by Th43,CAT_1:44;
hence (hom?-(a)).(id c)
= [[A,A],id A] by Def22
.= id$ A by Def6
.= id$ @@A by Lm6
.= id$ @d by A2,Def15
.= id d by Th29;
end;
Lm11:
Hom(C) c= V implies
for d being Object of Ens(V) st d = Hom(c,a) holds (hom-?(a)).(id c) = id d
proof
assume
A1: Hom(C) c= V;
let d be Object of Ens(V) such that
A2: d = Hom(c,a);
Hom(c,a) in Hom(C) by Th41;
then reconsider A = Hom(c,a) as Element of V by A1;
dom id c = c & cod id c = c & hom(id(c),a) = id A by Th44,CAT_1:44;
hence (hom-?(a)).(id c)
= [[A,A],id A] by Def23
.= id$ A by Def6
.= id$ @@A by Lm6
.= id$ @d by A2,Def15
.= id d by Th29;
end;
theorem Th49:
Hom(C) c= V implies hom?-(a) is Functor of C,Ens(V)
proof assume
A1: Hom(C) c= V;
then reconsider T = hom?-(a) as
Function of the Morphisms of C, the Morphisms of Ens V by Lm9;
now
thus for c being Object of C ex d being Object of Ens V st T.(id c) = id d
proof let c be Object of C;
Hom(a,c) in Hom(C) by Th41;
then reconsider A = Hom(a,c) as Element of V by A1;
take d = @A;
d = A by Def15;
hence thesis by A1,Lm10;
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;
set b = dom f, c = cod f;
Hom(a,b) in Hom(C) & Hom(a,c) in Hom(C) by Th41;
then reconsider A = Hom(a,b), B = Hom(a,c) as Element of V by A1;
set g = T.f;
A2: [[Hom(a,b),Hom(a,c)],hom(a,f)]
= g by Def22
.= @g by Def18
.= [[dom(@g), cod(@g)],(@g)`2] by Th8
.= [[dom g, cod(@g)],(@g)`2] by Th26
.= [[dom g, cod g],(@g)`2] by Th26;
A3: A = @A by Def15;
hence T.(id b)
= id @A by A1,Lm10
.= id dom (T.f) by A2,A3,Lm1;
A4: B = @B by Def15;
hence T.(id c)
= id @B by A1,Lm10
.= id cod (T.f) by A2,A4,Lm1;
end;
let f,g be Morphism of C such that
A5: dom g = cod f;
[[Hom(a,dom f),Hom(a,cod f)],hom(a,f)]
= T.f by Def22
.= @(T.f) by Def18
.= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
.= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Th26
.= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Th26;
then A6: (@(T.f))`2=hom(a,f) & dom(T.f)=Hom(a,dom f) & cod(T.f)=Hom(a,cod f)
by Lm1,ZFMISC_1:33;
then A7: dom(@(T.f))=Hom(a,dom f) & cod(@(T.f))=Hom(a,cod f)
by Th26;
[[Hom(a,dom g),Hom(a,cod g)],hom(a,g)]
= T.g by Def22
.= @(T.g) by Def18
.= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
.= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Th26
.= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Th26;
then A8: (@(T.g))`2=hom(a,g) & dom(T.g)=Hom(a,dom g) & cod(T.g)=Hom(a,cod g)
by Lm1,ZFMISC_1:33;
then A9: dom(@(T.g))=Hom(a,dom g) & cod(@(T.g))=Hom(a,cod g) by Th26;
dom(g*f) = dom f & cod(g*f) = cod g by A5,CAT_1:42;
hence T.(g*f) = [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g*f)] by Def22
.= [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g)*hom(a,f)] by A5,Th45
.= (@(T.g))*(@(T.f)) by A5,A6,A7,A8,A9,Def7
.= (T.g)*(T.f) by A5,A6,A8,Th28;
end;
hence thesis by CAT_1:96;
end;
theorem Th50:
Hom(C) c= V implies hom-?(a) is Contravariant_Functor of C,Ens(V)
proof assume
A1: Hom(C) c= V;
then reconsider T = hom-?(a) as
Function of the Morphisms of C, the Morphisms of Ens V by Lm9;
now
thus for c being Object of C ex d being Object of Ens V st T.(id c) = id d
proof let c be Object of C;
Hom(c,a) in Hom(C) by Th41;
then reconsider A = Hom(c,a) as Element of V by A1;
take d = @A;
d = A by Def15;
hence thesis by A1,Lm11;
end;
thus for f being Morphism of C
holds T.(id dom f) = id cod (T.f) & T.(id cod f) = id dom (T.f)
proof let f be Morphism of C;
set b = cod f, c = dom f;
Hom(b,a) in Hom(C) & Hom(c,a) in Hom(C) by Th41;
then reconsider A = Hom(b,a), B = Hom(c,a) as Element of V by A1;
set g = T.f;
A2: [[Hom(b,a),Hom(c,a)],hom(f,a)]
= g by Def23
.= @g by Def18
.= [[dom(@g), cod(@g)],(@g)`2] by Th8
.= [[dom g, cod(@g)],(@g)`2] by Th26
.= [[dom g, cod g],(@g)`2] by Th26;
A3: B = @B by Def15;
hence T.(id c)
= id @B by A1,Lm11
.= id cod (T.f) by A2,A3,Lm1;
A4: A = @A by Def15;
hence T.(id b)
= id @A by A1,Lm11
.= id dom (T.f) by A2,A4,Lm1;
end;
let f,g be Morphism of C such that
A5: dom g = cod f;
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
= T.f by Def23
.= @(T.f) by Def18
.= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
.= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Th26
.= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Th26;
then A6: (@(T.f))`2=hom(f,a) & dom(T.f)=Hom(cod f,a) & cod(T.f)=Hom(dom f,a)
by Lm1,ZFMISC_1:33;
then A7: dom(@(T.f))=Hom(cod f,a) & cod(@(T.f))=Hom(dom f,a)
by Th26;
[[Hom(cod g,a),Hom(dom g,a)],hom(g,a)]
= T.g by Def23
.= @(T.g) by Def18
.= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
.= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Th26
.= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Th26;
then A8: (@(T.g))`2=hom(g,a) & dom(T.g)=Hom(cod g,a) & cod(T.g)=Hom(dom g,a)
by Lm1,ZFMISC_1:33;
then A9: dom(@(T.g))=Hom(cod g,a) & cod(@(T.g))=Hom(dom g,a)
by Th26;
dom(g*f) = dom f & cod(g*f) = cod g by A5,CAT_1:42;
hence T.(g*f) = [[Hom(cod(g),a),Hom(dom(f),a)],hom(g*f,a)] by Def23
.= [[Hom(cod(g),a),Hom(dom(f),a)],hom(f,a)*hom(g,a)] by A5,Th46
.= (@(T.f))*(@(T.g)) by A5,A6,A7,A8,A9,Def7
.= (T.f)*(T.g) by A5,A6,A8,Th28;
end;
hence thesis by OPPCAT_1:def 7;
end;
:: hom-bifunctor
theorem Th51:
Hom(dom f,cod f') = {} implies Hom(cod f,dom f') = {}
proof assume that
A1: Hom(dom f,cod f') = {} and
A2: Hom(cod f,dom f') <> {};
Hom(dom f,cod f) <> {} by CAT_1:19;
then Hom(dom f,dom f') <> {} & Hom(dom f',cod f') <> {} by A2,CAT_1:19,52;
hence contradiction by A1,CAT_1:52;
end;
definition let C,f,g;
func hom(f,g) -> Function of Hom(cod f,dom g),Hom(dom f,cod g) means
:Def24: for h st h in Hom(cod f,dom g) holds it.h = g*h*f;
existence
proof set X = Hom(cod f,dom g), Y = Hom(dom f,cod g);
defpred P[set,set] means for h st h = $1 holds $2 = g*h*f;
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
proof let x be set;
assume
A2: x in X;
then reconsider h = x as Morphism of cod f,dom g by CAT_1:def 7;
take g*h*f;
X <> {} & Hom(dom g,cod g) <> {} & g is Morphism of dom g,cod g
by A2,CAT_1:19,22;
then g*h in Hom(cod f,cod g) by CAT_1:51;
then Hom(dom f,cod f) <> {} & Hom(cod f,cod g) <> {} &
g*h is Morphism of cod f,cod g & f is Morphism of dom f,cod f
by CAT_1:19,22,def 7;
hence thesis by CAT_1:51;
end;
consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being set st x in X holds P[x,h.x] from NonUniqBoundFuncEx(A1);
Y = {} implies X = {} by Th51;
then reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:11;
take h; thus thesis by A4;
end;
uniqueness
proof set X = Hom(cod f,dom g), Y = Hom(dom f,cod g);
let h1,h2 be Function of X,Y such that
A5: for h st h in X holds h1.h = g*h*f and
A6: for h st h in X holds h2.h = g*h*f;
now let x be set;
assume
A7: x in X;
then reconsider h = x as Morphism of C;
thus h1.x = g*h*f by A5,A7 .= h2.x by A6,A7;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Th52:
[[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] is Element of Maps(Hom(C))
proof
Hom(dom f,cod g) in Hom(C) & Hom(cod f,dom g) in Hom(C) &
(Hom(dom f,cod g) = {} implies Hom(cod f,dom g) = {}) by Th41,Th51;
hence thesis by Th5;
end;
theorem Th53:
hom(id a,f) = hom(a,f) & hom(f,id a) = hom(f,a)
proof
A1: dom id a = a & cod id a = a by CAT_1:44;
now
Hom(dom f,cod f) <> {} by CAT_1:19;
then Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:52;
hence dom hom(id a,f) = Hom(a,dom f) & dom hom(a,f) = Hom(a,dom f)
by A1,FUNCT_2:def 1;
let x be set;
assume
A2: x in Hom(a,dom f);
then reconsider g = x as Morphism of C;
A3: dom g = a & cod g = dom f by A2,CAT_1:18;
thus hom(id a,f).x = f*g*(id a) by A1,A2,Def24
.= f*(g*(id a)) by A1,A3,CAT_1:43
.= f*g by A3,CAT_1:47
.= hom(a,f).x by A2,Def20;
end;
hence hom(id a,f) = hom(a,f) by FUNCT_1:9;
now
Hom(dom f,cod f) <> {} by CAT_1:19;
then Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:52;
hence dom hom(f,id a) = Hom(cod f,a) & dom hom(f,a) = Hom(cod f,a)
by A1,FUNCT_2:def 1;
let x be set;
assume
A4: x in Hom(cod f,a);
then reconsider g = x as Morphism of C;
A5: dom g = cod f & cod g = a by A4,CAT_1:18;
thus hom(f,id a).x = (id a)*g*f by A1,A4,Def24
.= g*f by A5,CAT_1:46
.= hom(f,a).x by A4,Def21;
end;
hence hom(f,id a) = hom(f,a) by FUNCT_1:9;
end;
theorem Th54:
hom(id a,id b) = id Hom(a,b)
proof
thus hom(id a,id b) = hom(a,id b) by Th53 .= id Hom(a,b) by Th43;
end;
theorem
hom(f,g) = hom(dom f,g)*hom(f,dom g)
proof
now
A1: Hom(dom f,cod g) = {} implies Hom(cod f,dom g) = {} by Th51;
hence dom hom(f,g) = Hom(cod f,dom g) by FUNCT_2:def 1;
now
Hom(dom f,cod f) <> {} by CAT_1:19;
hence Hom(dom f,dom g) = {} implies Hom(cod f,dom g) = {} by CAT_1:52;
Hom(dom g,cod g) <> {} by CAT_1:19;
hence Hom(dom f,cod g) = {} implies Hom(dom f,dom g) = {} by CAT_1:52;
end;
then hom(dom f,g)*hom(f,dom g)
is Function of Hom(cod f,dom g),Hom(dom f,cod g) by FUNCT_2:19;
hence
A2: dom(hom(dom f,g)*hom(f,dom g)) = Hom(cod f,dom g) by A1,FUNCT_2:def 1;
let x be set;
assume
A3: x in Hom(cod f,dom g);
then reconsider h = x as Morphism of C;
A4: dom h = cod f & cod h = dom g by A3,CAT_1:18;
then dom(h*f) = dom f & cod(h*f) = dom g by CAT_1:42;
then A5: h*f in Hom(dom f,dom g) by CAT_1:18;
thus hom(f,g).x = g*h*f by A3,Def24
.= g*(h*f) by A4,CAT_1:43
.= hom(dom f,g).(h*f) by A5,Def20
.= hom(dom f,g).((hom(f,dom g)).h) by A3,Def21
.= (hom(dom f,g)*hom(f,dom g)).x by A2,A3,FUNCT_1:22;
end;
hence thesis by FUNCT_1:9;
end;
theorem Th56:
cod g = dom f & dom g' = cod f' implies hom(f*g,g'*f') = hom(g,g')*hom(f,f')
proof assume
A1: cod g = dom f & dom g' = cod f';
then A2: dom(g'*f') = dom f' & cod(g'*f') = cod g' &
dom(f*g) = dom g & cod(f*g) = cod f by CAT_1:42;
now set h = hom(f*g,g'*f'), h2 = hom(g,g'), h1 = hom(f,f');
A3: Hom(dom g,cod g') = {} implies Hom(cod g,dom g') = {} by Th51;
A4: Hom(dom f,cod f') = {} implies Hom(cod f,dom f') = {} by Th51;
hence dom h = Hom(cod f,dom f') by A1,A2,A3,FUNCT_2:def 1;
h2*h1 is Function of Hom(cod f,dom f'),Hom(dom g,cod g')
by A1,A4,FUNCT_2:19;
hence
A5: dom(h2*h1) = Hom(cod f,dom f') by A1,A3,A4,FUNCT_2:def 1;
let x be set;
assume
A6: x in Hom(cod f,dom f');
then reconsider k = x as Morphism of C;
A7: h1.x in Hom(cod g,dom g') by A1,A4,A6,FUNCT_2:7;
then reconsider l = h1.x as Morphism of C;
A8: cod k = dom f' by A6,CAT_1:18;
A9: dom k = cod f by A6,CAT_1:18;
then A10: cod(k*(f*g)) = cod k by A2,CAT_1:42;
A11: dom(f'*k) = dom k & cod(f'*k) = cod f' by A8,CAT_1:42;
then A12: dom (f'*k*f) = dom f & cod(f'*k*f) = cod f' by A9,CAT_1:42;
thus h.x = (g'*f')*k*(f*g) by A2,A6,Def24
.= (g'*f')*(k*(f*g)) by A2,A8,A9,CAT_1:43
.= g'*(f'*(k*(f*g))) by A1,A8,A10,CAT_1:43
.= g'*(f'*k*(f*g)) by A2,A8,A9,CAT_1:43
.= g'*(f'*k*f*g) by A1,A9,A11,CAT_1:43
.= g'*(f'*k*f)*g by A1,A12,CAT_1:43
.= g'*l*g by A6,Def24
.= h2.l by A7,Def24
.= (h2*h1).x by A5,A6,FUNCT_1:22;
end;
hence thesis by FUNCT_1:9;
end;
definition let C;
func hom??(C) -> Function of the Morphisms of [:C,C:], Maps(Hom(C)) means
:Def25: for f,g holds it.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)]
;
existence
proof set X = the Morphisms of [:C,C:], Y = Maps(Hom(C));
defpred P[set,set] means
for f,g st $1=[f,g] holds $2=[[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
proof let x be set;
assume x in X;
then consider f,g such that
A2: x = [f,g] by CAT_2:37;
take y = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
y is Element of Y by Th52;
hence y in Y;
let f',g';
assume x = [f',g'];
then f' = f & g' = g by A2,ZFMISC_1:33;
hence thesis;
end;
consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being set st x in X holds P[x,h.x] from NonUniqBoundFuncEx(A1);
reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:11;
take h; thus thesis by A4;
end;
uniqueness
proof
let h1,h2 be Function of the Morphisms of [:C,C:], Maps(Hom(C)) such that
A5: for f,g holds h1.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] and
A6: for f,g holds h2.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
now
thus the Morphisms of [:C,C:] = [:the Morphisms of C,the Morphisms of C:]
by CAT_2:33;
let f,g;
thus h1.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] by A5
.= h2.[f,g] by A6;
end;
hence thesis by FUNCT_2:120;
end;
end;
theorem Th57:
hom?-(a) = (curry (hom??(C))).(id a) & hom-?(a) = (curry' (hom??(C))).(id a)
proof
[:the Morphisms of C,the Morphisms of C:] = the Morphisms of [:C, C:]
by CAT_2:33;
then reconsider T = hom??(C)
as Function of [:the Morphisms of C,the Morphisms of C:],Maps(Hom(C));
now let f;
thus ((curry T).(id a)).f
= T.[id a,f] by CAT_2:3
.= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(id a,f)] by Def25
.= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(a,f)] by Th53
.= [[Hom(a,dom f),Hom(dom id a,cod f)],hom(a,f)] by CAT_1:44
.= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by CAT_1:44
.= (hom?-(a)).f by Def22;
end;
hence hom?-(a) = (curry (hom??(C))).(id a) by FUNCT_2:113;
now let f;
thus ((curry' T).(id a)).f
= T.[f,id a] by CAT_2:4
.= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,id a)] by Def25
.= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,a)] by Th53
.= [[Hom(cod f,a),Hom(dom f,cod id a)],hom(f,a)] by CAT_1:44
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by CAT_1:44
.= (hom-?(a)).f by Def23;
end;
hence hom-?(a) = (curry' (hom??(C))).(id a) by FUNCT_2:113;
end;
Lm12:
Hom(C) c= V implies
for d being Object of Ens(V) st d = Hom(a,b)
holds (hom??(C)).[id a,id b] = id d
proof
assume
A1: Hom(C) c= V;
let d be Object of Ens(V) such that
A2: d = Hom(a,b);
Hom(a,b) in Hom(C) by Th41;
then reconsider A = Hom(a,b) as Element of V by A1;
dom id a = a & cod id a = a & dom id b = b & cod id b = b &
hom(id a,id b) = id A by Th54,CAT_1:44;
hence (hom??(C)).[id a,id b]
= [[A,A],id A] by Def25
.= id$ A by Def6
.= id$ @@A by Lm6
.= id$ @d by A2,Def15
.= id d by Th29;
end;
theorem Th58:
Hom(C) c= V implies hom??(C) is Functor of [:C opp,C:],Ens(V)
proof assume
A1: Hom(C) c= V;
C opp = CatStr (#the Objects of C, the Morphisms of C,
the Cod of C, the Dom of C,
~(the Comp of C), the Id of C#) by OPPCAT_1:def 1;
then Hom(C) is non empty Subset of V &
the Morphisms of [:C opp,C:]=[:the Morphisms of C,the Morphisms of C:] &
Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #)
by A1,Def14,CAT_2:33;
then the Morphisms of [:C opp,C:] = the Morphisms of [:C,C:] &
Maps(Hom(C)) c= Maps(V) & the Morphisms of Ens V = Maps V &
Maps(Hom(C)) <> {} by Th7,CAT_2:33;
then reconsider T = hom??(C) as
Function of the Morphisms of [:C opp,C:], the Morphisms of Ens V
by FUNCT_2:9;
A2: for f being Morphism of C opp holds opp f = f
proof let f be Morphism of C opp;
thus opp f = f opp by OPPCAT_1:def 5 .= f by OPPCAT_1:def 4;
end;
A3: for a being Object of C opp holds opp a = a
proof let a be Object of C opp;
thus opp a = a opp by OPPCAT_1:def 3 .= a by OPPCAT_1:def 2;
end;
now
thus for c being Object of [:C opp,C:]
ex d being Object of Ens V st T.(id c) = id d
proof let c be Object of [:C opp,C:];
consider a being Object of C opp, b such that
A4: c = [a,b] by CAT_2:35;
Hom(opp a,b) in Hom(C) by Th41;
then reconsider A = Hom(opp a,b) as Element of V by A1;
take d = @A;
now
thus id c = [id a,id b] by A4,CAT_2:41
.= [opp(id a), id b] by A2
.= [id(opp a),id b] by OPPCAT_1:22;
thus d = A by Def15;
end;
hence thesis by A1,Lm12;
end;
thus for fg being Morphism of [:C opp,C:]
holds T.(id dom fg) = id dom (T.fg) & T.(id cod fg) = id cod (T.fg)
proof let fg be Morphism of [:C opp,C:];
consider f being (Morphism of C opp), g such that
A5: fg = [f,g] by CAT_2:37;
Hom(cod opp f,dom g) in Hom(C) & Hom(dom opp f,cod g) in Hom(C) by Th41;
then reconsider A=Hom(cod opp f,dom g), B=Hom(dom opp f,cod g) as Element
of V
by A1;
set h = T.fg;
opp f = f by A2;
then A6: [[Hom(cod opp f,dom g),Hom(dom opp f,cod g)],hom(opp f,g)]
= h by A5,Def25
.= @h by Def18
.= [[dom(@h), cod(@h)],(@h)`2] by Th8
.= [[dom h, cod(@h)],(@h)`2] by Th26
.= [[dom h, cod h],(@h)`2] by Th26;
A7: A = @A by Def15;
thus T.(id dom fg)
= T.(id [dom f,dom g]) by A5,CAT_2:38
.= T.[id dom f,id dom g] by CAT_2:41
.= T.[opp (id dom f),id dom g] by A2
.= T.[id opp(dom f),id dom g] by OPPCAT_1:22
.= T.[id cod opp f,id dom g] by OPPCAT_1:12
.= id @A by A1,A7,Lm12
.= id dom (T.fg) by A6,A7,Lm1;
A8: B = @B by Def15;
thus T.(id cod fg)
= T.(id [cod f,cod g]) by A5,CAT_2:38
.= T.[id cod f,id cod g] by CAT_2:41
.= T.[opp(id cod f),id cod g] by A2
.= T.[id opp(cod f),id cod g] by OPPCAT_1:22
.= T.[id dom opp f,id cod g] by OPPCAT_1:12
.= id @B by A1,A8,Lm12
.= id cod (T.fg) by A6,A8,Lm1;
end;
let ff,gg be Morphism of [:C opp,C:] such that
A9: dom gg = cod ff;
consider f being (Morphism of C opp), f' such that
A10: ff = [f,f'] by CAT_2:37;
consider g being (Morphism of C opp), g' such that
A11: gg = [g,g'] by CAT_2:37;
opp f = f by A2;
then [[Hom(cod opp f,dom f'),Hom(dom opp f,cod f')],hom(opp f,f')]
= T.ff by A10,Def25
.= @(T.ff) by Def18
.= [[dom(@(T.ff)),cod(@(T.ff))],(@(T.ff))`2] by Th8
.= [[dom(T.ff),cod(@(T.ff))],(@(T.ff))`2] by Th26
.= [[dom(T.ff),cod(T.ff)],(@(T.ff))`2] by Th26;
then A12: (@(T.ff))`2=hom(opp f,f') &
dom(T.ff)=Hom(cod opp f,dom f') & cod(T.ff)=Hom(dom opp f,cod f')
by Lm1,ZFMISC_1:33;
then A13: dom(@(T.ff))=Hom(cod opp f,dom f') & cod(@(T.ff))=Hom(dom opp f,cod
f')
by Th26;
opp g = g by A2;
then [[Hom(cod opp g,dom g'),Hom(dom opp g,cod g')],hom(opp g,g')]
= T.gg by A11,Def25
.= @(T.gg) by Def18
.= [[dom(@(T.gg)),cod(@(T.gg))],(@(T.gg))`2] by Th8
.= [[dom(T.gg),cod(@(T.gg))],(@(T.gg))`2] by Th26
.= [[dom(T.gg),cod(T.gg)],(@(T.gg))`2] by Th26;
then A14: (@(T.gg))`2=hom(opp g,g') &
dom(T.gg)=Hom(cod opp g,dom g') & cod(T.gg)=Hom(dom opp g,cod g')
by Lm1,ZFMISC_1:33;
then A15: dom(@(T.gg))=Hom(cod opp g,dom g') & cod(@(T.gg))=Hom(dom opp g,cod
g')
by Th26;
A16: dom gg = [dom g,dom g'] & cod ff = [cod f,cod f'] by A10,A11,CAT_2:38;
then A17: dom g = cod f by A9,ZFMISC_1:33;
now
thus dom gg = [opp dom g,dom g'] by A3,A16
.= [cod opp g,dom g'] by OPPCAT_1:12;
thus cod ff = [opp cod f,cod f'] by A3,A16
.= [dom opp f,cod f'] by OPPCAT_1:12;
end;
then A18: cod opp g = dom opp f & dom g' = cod f' by A9,ZFMISC_1:33;
then A19: dom(g'*f') = dom f' & cod(g'*f') = cod g' &
dom((opp f)*(opp g)) = dom opp g & cod((opp f)*(opp g)) = cod opp f
by CAT_1:42;
thus T.(gg*ff)
= T.([g*f,g'*f']) by A9,A10,A11,CAT_2:40
.= T.([opp (g*f),g'*f']) by A2
.= T.([(opp f)*(opp g),g'*f']) by A17,OPPCAT_1:19
.= [[Hom(cod((opp f)*(opp g)),dom(g'*f')),
Hom(dom((opp f)*(opp g)),cod(g'*f'))],
hom((opp f)*(opp g),g'*f')] by Def25
.= [[Hom(cod opp f,dom f'),Hom(dom opp g,cod g')],
hom(opp g,g')*hom(opp f,f')] by A18,A19,Th56
.= (@(T.gg))*(@(T.ff)) by A12,A13,A14,A15,A18,Def7
.= (T.gg)*(T.ff) by A12,A14,A18,Th28;
end;
hence thesis by CAT_1:96;
end;
definition let V,C,a;
assume A1: Hom(C) c= V;
func hom?-(V,a) -> Functor of C,Ens(V) equals
:Def26: hom?-(a);
coherence by A1,Th49;
func hom-?(V,a) -> Contravariant_Functor of C,Ens(V) equals
:Def27: hom-?(a);
coherence by A1,Th50;
end;
definition let V,C;
assume A1: Hom(C) c= V;
func hom??(V,C) -> Functor of [:C opp,C:],Ens(V) equals
:Def28: hom??(C);
coherence by A1,Th58;
end;
theorem
Hom(C) c= V implies (hom?-(V,a)).f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)]
proof assume Hom(C) c= V;
hence (hom?-(V,a)).f = (hom?-(a)).f by Def26
.= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by Def22;
end;
theorem
Hom(C) c= V implies (Obj (hom?-(V,a))).b = Hom(a,b)
proof assume
A1: Hom(C) c= V;
Hom(a,b) in Hom(C) by Th41;
then reconsider A = Hom(a,b) as Element of V by A1;
set d = @A;
A2: d = A by Def15;
(hom?-(V,a)).(id b) = (hom?-(a)).(id b) by A1,Def26
.= id d by A1,A2,Lm10;
hence thesis by A2,CAT_1:103;
end;
theorem
Hom(C) c= V implies (hom-?(V,a)).f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
proof assume Hom(C) c= V;
hence (hom-?(V,a)).f = (hom-?(a)).f by Def27
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by Def23;
end;
theorem
Hom(C) c= V implies (Obj (hom-?(V,a))).b = Hom(b,a)
proof assume
A1: Hom(C) c= V;
Hom(b,a) in Hom(C) by Th41;
then reconsider A = Hom(b,a) as Element of V by A1;
set d = @A;
A2: d = A by Def15;
(hom-?(V,a)).(id b) = (hom-?(a)).(id b) by A1,Def27
.= id d by A1,A2,Lm11;
hence thesis by A2,OPPCAT_1:31;
end;
theorem
Hom(C) c= V
implies hom??(V,C).[f opp,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)]
proof assume
A1: Hom(C) c= V;
thus (hom??(V,C)).[f opp,g]
= (hom??(V,C)).[f,g] by OPPCAT_1:def 4
.= (hom??(C)).[f,g] by A1,Def28
.= [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] by Def25;
end;
theorem
Hom(C) c= V implies (Obj (hom??(V,C))).[a opp,b] = Hom(a,b)
proof assume
A1: Hom(C) c= V;
Hom(a,b) in Hom(C) by Th41;
then reconsider A = Hom(a,b) as Element of V by A1;
set d = @A;
A2: d = A by Def15;
(hom??(V,C)).(id[a opp,b]) = (hom??(V,C)).[id(a opp),id b] by CAT_2:41
.= (hom??(V,C)).[(id a) opp,id b] by OPPCAT_1:21
.= (hom??(V,C)).[id a,id b] by OPPCAT_1:def 4
.= (hom??(C)).[id a,id b] by A1,Def28
.= id d by A1,A2,Lm12;
hence thesis by A2,CAT_1:103;
end;
theorem
Hom(C) c= V implies hom??(V,C)?-(a opp) = hom?-(V,a)
proof assume
A1: Hom(C) c= V;
thus hom??(V,C)?-(a opp) = (curry hom??(V,C)).(id (a opp)) by CAT_2:def 8
.= (curry hom??(V,C)).((id a) opp) by OPPCAT_1:21
.= (curry hom??(V,C)).(id a) by OPPCAT_1:def 4
.= (curry hom??(C)).(id a) by A1,Def28
.= hom?-(a) by Th57
.= hom?-(V,a) by A1,Def26;
end;
theorem
Hom(C) c= V implies hom??(V,C)-?a = hom-?(V,a)
proof assume
A1: Hom(C) c= V;
thus hom??(V,C)-?a = (curry' hom??(V,C)).(id a) by CAT_2:def 9
.= (curry' hom??(C)).(id a) by A1,Def28
.= hom-?(a) by Th57
.= hom-?(V,a) by A1,Def27;
end;