:: Category Ens
:: by Czes{\l}aw Byli\'nski
::
:: Received August 1, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, FUNCT_2, TARSKI, FUNCT_1, RELAT_1, ZFMISC_1,
MCART_1, GRAPH_1, PARTFUN1, CAT_1, STRUCT_0, QC_LANG1, CLASSES2,
FUNCOP_1, FUNCT_4, CAT_2, OPPCAT_1, FUNCT_5, ARYTM_0, ENS_1, MONOID_0,
RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1,
DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_4,
CLASSES2, FUNCOP_1, FUNCT_5, STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1;
constructors PARTFUN1, DOMAIN_1, CLASSES2, CAT_2, OPPCAT_1, FUNCOP_1,
RELSET_1, FUNCT_5, XTUPLE_0, XFAMILY, FUNCT_4;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, RELSET_1, STRUCT_0,
PARTFUN1, CAT_1, XTUPLE_0, OPPCAT_1, CAT_2;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, CAT_1, CAT_2, RELAT_1;
equalities CAT_1, CAT_2, BINOP_1, GRAPH_1, OPPCAT_1;
expansions TARSKI, FUNCT_1, CAT_1;
theorems TARSKI, ENUMSET1, ZFMISC_1, DOMAIN_1, FUNCT_1, FUNCT_2, PARTFUN1,
FUNCOP_1, FUNCT_4, CLASSES2, CAT_1, CAT_2, OPPCAT_1, GRFUNC_1, RELAT_1,
RELSET_1, XBOOLE_0, BINOP_1, FUNCT_5, XTUPLE_0;
schemes FUNCT_2, BINOP_1, FUNCT_1;
begin :: Mappings
reserve V for non empty set,
A,B,A9,B9 for Element of V;
definition
let V;
func Funcs(V) -> set equals
union the set of all Funcs(A,B);
coherence;
end;
registration
let V;
cluster Funcs(V) -> functional non empty;
coherence
proof
set F = the set of all Funcs(A,B);
set A = the Element of V;
id A in Funcs(A,A) & Funcs(A,A) in F by FUNCT_2:9;
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
A1: f in C and
A2: C in F by TARSKI:def 4;
ex A,B st C = Funcs(A,B) by A2;
hence f is Function by A1;
end;
hence thesis;
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 = the set of all Funcs(A,B);
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
A1: f in C and
A2: C in F by TARSKI:def 4;
consider A,B such that
A3: C = Funcs(A,B) by A2;
take A,B;
thus thesis by A1,A3,FUNCT_2:66;
end;
given A,B such that
A4: ( B={} implies A={})& f is Function of A,B;
A5: Funcs(A,B) in F;
f in Funcs(A,B) by A4,FUNCT_2:8;
hence thesis by A5,TARSKI:def 4;
end;
theorem
Funcs(A,B) c= Funcs(V)
proof
let x be object;
assume
A1: x in Funcs(A,B);
then
A2: x is Function of A,B by FUNCT_2:66;
B={} implies A={} by A1;
hence thesis by A2,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 object;
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,f9 for Element of Funcs(V);
definition
let V;
func Maps(V) -> set equals
{ [[A,B],f]: (B={} implies A={}) & f is Function
of A,B};
coherence;
end;
registration
let V;
cluster Maps(V) -> non empty;
coherence
proof
set FV = { [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
set A = the Element of V;
now
set f = id A;
take m = [[A,A],f];
A1: A = {} implies A = {};
f in Funcs(V) by Th1;
hence m in FV by A1;
end;
hence thesis;
end;
end;
reserve m,m1,m2,m3,m9 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 { [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
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;
hence thesis by A1;
end;
theorem
Maps V c= [:[:V,V:],Funcs V:]
proof
let m be object;
assume m in Maps V;
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 object;
assume x in Maps W;
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;
hence thesis by A1;
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 XTUPLE_0:1;
hence thesis by XTUPLE_0:1;
end;
registration
let V be non empty set, m be Element of Maps V;
cluster m`2 -> Function-like Relation-like for set;
coherence
proof
ex f be Element of Funcs(V), A,B be Element of V st m = [[ A,B],f] &( B
= {} implies A = {})& f is Function of A,B by Th4;
hence thesis;
end;
end;
definition
let V,m;
func dom m -> Element of V equals
m`1`1;
coherence
proof
consider f,A,B such that
A1: m = [[A,B],f] and
B = {} implies A = {} and
f is Function of A,B by Th4;
[A,B] = m`1 by A1;
hence thesis;
end;
func cod m -> Element of V equals
m`1`2;
coherence
proof
consider f,A,B such that
A2: m = [[A,B],f] and
B = {} implies A = {} and
f is Function of A,B by Th4;
[A,B] = m`1 by A2;
hence thesis;
end;
end;
theorem Th8:
m = [[dom m,cod m],m`2]
proof
consider f,A,B such that
A1: m = [[A,B],f] &( B = {} implies A = {})& f is Function of A,B
by Th4;
thus thesis by A1;
end;
Lm2: m`2 = m9`2 & dom m = dom m9 & cod m = cod m9 implies m = m9
proof
m = [[dom m,cod m],m`2] by Th8;
hence thesis by Th8;
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;
thus thesis by A1,A2;
end;
Lm3: dom m`2 = dom m & rng m`2 c= cod m
proof
A1: m`2 is Function of dom m,cod m by Th9;
cod m <> {} or dom m = {} by Th9;
hence thesis by A1,FUNCT_2:def 1,RELAT_1:def 19;
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 f9,A9,B9 such that
A1: [[A,B],f] = [[A9,B9],f9] and
A2: ( B9 = {} implies A9 = {})& f9 is Function of A9,B9 by Th4;
f = f9 & A = A9 by A1,Lm1,XTUPLE_0:1;
hence thesis by A1,A2,Lm1;
end;
definition
let V,A;
func id$ A -> Element of Maps V equals
[[A,A],id A];
coherence by Th5;
end;
theorem
(id$ A)`2 = id A & dom id$ A = A & cod id$ A = A;
definition
let V,m1,m2;
assume
A1: cod m1 = dom m2;
func m2*m1 -> Element of Maps V equals
:Def6:
[[dom m1,cod m2],m2`2*m1`2];
coherence
proof
A2: cod m2 <> {} or dom m2 = {} by Th9;
A3: cod m1 <> {} or dom m1 = {} by Th9;
m1`2 is Function of dom m1,cod m1 & 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,A3,FUNCT_2:13;
hence thesis by A1,A3,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 Def6
.= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th8;
hence thesis by Lm1,XTUPLE_0:1;
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;
A3: cod(m2*m1) = cod m2 by A1,Th12;
(m2*m1)`2 = m2`2*m1`2 by A1,Th12;
then
A4: (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) by A2,A3,Th12;
A5: dom(m3*m2) = dom m2 by A2,Th12;
then
A6: dom((m3*m2)*m1) = dom m1 by A1,Th12;
dom(m2*m1) = dom m1 by A1,Th12;
then
A7: dom(m3*(m2*m1)) = dom m1 by A2,A3,Th12;
cod(m3*m2) = cod m3 by A2,Th12;
then
A8: cod((m3*m2)*m1) = cod m3 by A1,A5,Th12;
(m3*m2)`2 = m3`2*m2`2 by A2,Th12;
then
A9: ((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 by A1,A5,Th12;
cod(m3*(m2*m1)) = cod m3 by A2,A3,Th12;
hence thesis by A4,A7,A9,A6,A8,Lm2,RELAT_1:36;
end;
theorem Th14:
m*(id$ dom m) = m & (id$ cod m)*m = m
proof
set i1 = id$ dom m, i2 = id$ cod m;
A1: m`2 is Function of dom m,cod m by Th9;
then
A2: rng m`2 c= cod m by RELAT_1:def 19;
cod m <> {} or dom m = {} by Th9;
then
A3: dom m`2 = dom m by A1,FUNCT_2:def 1;
A4: cod i1 = dom m;
then
A5: cod(m*i1) = cod m by Th12;
(m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 by A4,Th12;
hence m*i1 = m by A3,A5,Lm2,RELAT_1:52;
A6: dom i2 = cod m;
then
A7: cod(i2*m) = cod i2 by Th12;
(i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m by A6,Th12;
hence thesis by A2,A7,Lm2,RELAT_1:53;
end;
definition
let V,A,B;
func Maps(A,B) -> set equals
{ [[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) by Th1,Th5;
hence thesis;
end;
theorem Th16:
m in Maps(A,B) implies m = [[A,B],m`2]
proof
assume m in Maps(A,B);
then
A1: ex f being Element of Funcs(V) st m = [[A,B],f] & [[A,B],f] in Maps( V);
thus thesis by A1;
end;
theorem Th17:
Maps(A,B) c= Maps V
proof
let z be object;
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);
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
A1: Maps(A,B) c= Maps V by Th17;
let f be Function;
assume [[A,B],f] in Maps(A,B);
hence thesis by A1,Th10;
end;
theorem
Maps V = union the set of all Maps(A,B)
proof
set M = the set of all Maps(A,B);
now
let z be object;
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;
A2: Maps(A,B) in M;
z in Maps(A,B) by A1,Th15;
hence thesis by A2,TARSKI:def 4;
end;
assume z in union M;
then consider C being set such that
A3: z in C and
A4: C in M by TARSKI:def 4;
consider A,B such that
A5: C = Maps(A,B) by A4;
ex f being Element of Funcs(V) st z = [[A,B],f] & [[A,B],f] in Maps(V
) by A3,A5;
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
A1: m`2 is Function of dom m,cod m by Th9;
thus m in Maps(A,B) implies dom m = A & cod m = B
proof
assume m in Maps(A,B);
then
A2: m = [[A,B],m`2] by Th16;
thus thesis by A2;
end;
cod m <> {} or dom m = {} by Th9;
then [[dom m,cod m],m`2] in Maps(dom m,cod m) by A1,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
A2: m = [[A,B],m`2] by Th16;
then
A3: m`2 is Function of A,B by A1,Lm4;
B = {} implies A = {} by A1,A2,Lm4;
hence thesis by A3,FUNCT_2:8;
end;
Lm5: for W being non empty Subset of V, A,B being Element of W, A9,B9 being
Element of V st A = A9 & B = B9 holds Maps(A,B) = Maps(A9,B9)
proof
let W be non empty Subset of V;
let A,B be Element of W, A9,B9 be Element of V such that
A1: A = A9 & B = B9;
now
let x be object;
thus x in Maps(A,B) implies x in Maps(A9,B9)
proof
A2: Maps W c= Maps V by Th7;
assume
A3: x in Maps(A,B);
A4: Maps(A,B) c= Maps W by Th17;
then reconsider m = x as Element of Maps W by A3;
x in Maps W by A3,A4;
then reconsider m9 = x as Element of Maps V by A2;
A5: dom m = dom m9 & cod m = cod m9;
m = [[A,B],m `2 ] by A3,Th16;
then dom m = A & cod m = B;
hence thesis by A1,A5,Th19;
end;
assume
A6: x in Maps(A9,B9);
Maps(A9,B9) c= Maps V by Th17;
then reconsider m9 = x as Element of Maps V by A6;
A7: m9 = [[A9,B9],m9`2] by A6,Th16;
then
A8: m9`2 is Function of A9,B9 by A6,Lm4;
B9 = {} implies A9 = {} by A6,A7,Lm4;
hence x in Maps(A,B) by A1,A7,A8,Th15;
end;
hence thesis by TARSKI:2;
end;
definition
let V,m;
attr m is surjective means
rng m`2 = cod(m);
end;
begin :: Category Ens
definition
let V;
func fDom V -> Function of Maps V,V means
:Def9:
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 FUNCT_2
:sch 4;
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:63;
end;
func fCod V -> Function of Maps V,V means
:Def10:
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 FUNCT_2
:sch 4;
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:63;
end;
func fComp V -> PartFunc of [:Maps V,Maps V:],Maps V means
:Def11:
(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[object,object,object] means
for m2,m1 st m2=$1 & m1=$2 holds dom m2 = cod
m1 & $3 = m2*m1;
A5: for x,y,z1,z2 being object 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 object;
assume x in Maps(V) & y in Maps(V);
then reconsider m2 = x, m1 = y as Element of Maps(V);
assume that
A6: P[x,y,z1] and
A7: P[x,y,z2];
z1 = m2*m1 by A6;
hence thesis by A7;
end;
A8: for x,y,z being object st x in Maps(V) & y in Maps(V) & P[x,y,z] holds z
in Maps(V)
proof
let x,y,z be object;
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;
consider h being PartFunc of [:Maps(V),Maps(V):],Maps(V) such that
A9: for x,y being object holds [x,y] in dom h iff x in Maps(V) & y in
Maps(V) & ex z being object st P[x,y,z] and
A10: for x,y being object st [x,y] in dom h holds P[x,y,h.(x,y)] from
BINOP_1:sch 5(A8,A5);
take h;
thus
A11: 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 object st P[m2,m1,z] by A9;
hence thesis;
end;
assume dom m2 = cod m1;
then P[m2,m1,m2*m1];
hence thesis by A9;
end;
let m2,m1;
assume dom m2 = cod m1;
then [m2,m1] in dom h by A11;
then P[m2,m1,h.(m2,m1)] by A10;
hence thesis;
end;
uniqueness
proof
let h1,h2 be PartFunc of [:Maps V,Maps V:],Maps V such that
A12: for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A13: for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A14: for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A15: for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
A16: dom h2 c= [:Maps V,Maps V:] by RELAT_1:def 18;
A17: dom h1 c= [:Maps V,Maps V:] by RELAT_1:def 18;
A18: dom h1 = dom h2
proof
let x,y be object;
thus [x,y] in dom h1 implies [x,y] in dom h2
proof
assume
A19: [x,y] in dom h1;
then reconsider m2 = x, m1 = y as Element of Maps V by A17,ZFMISC_1:87;
dom m2 = cod m1 by A12,A19;
hence thesis by A14;
end;
assume
A20: [x,y] in dom h2;
then reconsider m2 = x, m1 = y as Element of Maps V by A16,ZFMISC_1:87;
dom m2 = cod m1 by A14,A20;
hence thesis by A12;
end;
now
let m be Element of [:Maps V,Maps V:];
consider m2,m1 such that
A21: m = [m2,m1] by DOMAIN_1:1;
assume m in dom h1;
then
A22: dom m2 = cod m1 by A12,A21;
then h1.[m2,m1] = m2*m1 by A13;
hence h1.m = h2.m by A15,A21,A22;
end;
hence thesis by A18,PARTFUN1:5;
end;
end;
definition
::$CD
let V;
func Ens(V) -> non empty non void strict CatStr equals
CatStr(# V,Maps V,fDom V,fCod V,fComp V#);
coherence;
end;
registration
let V;
cluster Ens(V) -> Category-like
reflexive transitive associative with_identities;
coherence
proof
set M = Maps V, d = fDom V, c = fCod V, p = fComp V;
reconsider C = CatStr(#V,M,d,c,p#) as non empty non void CatStr;
A1: C is Category-like
proof
let ff,gg be Morphism of C;
reconsider f=ff, g=gg as Element of M;
d.g = dom g & c.f = cod f by Def9,Def10;
hence thesis by Def11;
end;
A2: C is transitive
proof
let ff,gg be Morphism of C such that
A3: dom gg=cod ff;
[gg,ff] in dom the Comp of C by A3,A1;
then
A4: (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
reconsider f=ff, g=gg as Element of M;
A5: d.g = dom g & c.f = cod f by Def9,Def10;
then
A6: p.[g,f] = g*f by A3,Def11;
A7: d.f = dom f & c.g = cod g by Def9,Def10;
dom(g*f) = dom f & cod(g*f) = cod g by A3,A5,Th12;
hence thesis by A6,A7,Def9,Def10,A4;
end;
A8: C is associative
proof
let ff,gg,hh be Morphism of C such that
A9: dom hh = cod gg and
A10: dom gg = cod ff;
reconsider f=ff, g=gg, h=hh as Element of M;
A11: dom h = d.h & cod g = c.g by Def9,Def10;
then
A12: dom(h*g) = dom g by A9,Th12;
A13: dom g = d.g & cod f = c.f by Def9,Def10;
then
A14: cod(g*f) = dom h by A9,A10,A11,Th12;
[hh,gg] in dom the Comp of C by A9,A1;
then
A15: hh(*)gg =(the Comp of C).(hh,gg) by CAT_1:def 1;
dom(hh(*)gg) = dom gg by A2,A9;
then
A16: [hh(*)gg,ff] in dom the Comp of C by A1,A10;
[gg,ff] in dom the Comp of C by A10,A1;
then
A17: gg(*)ff =(the Comp of C).(gg,ff) by CAT_1:def 1;
cod(gg(*)ff) = cod gg by A2,A10;
then [hh,gg(*)ff] in dom the Comp of C by A1,A9;
hence hh(*)(gg(*)ff)
= (the Comp of C).(hh,(the Comp of C).(gg,ff)) by A17,CAT_1:def 1
.= p.[h,g*f] by A10,A13,Def11
.= h*(g*f) by A14,Def11
.= (h*g)*f by A9,A10,A11,A13,Th13
.= p.[h*g,f] by A10,A13,A12,Def11
.= (the Comp of C).((the Comp of C).(hh,gg),ff) by A9,A11,Def11
.= hh(*)gg(*)ff by A16,A15,CAT_1:def 1;
end;
A18: C is reflexive
proof let a be Element of C;
reconsider aa=a as Element of V;
reconsider ii = id$aa as Morphism of C;
A19: cod ii = cod id$ aa by Def10
.= a;
dom ii = dom id$ aa by Def9
.= a;
then ii in Hom(a,a) by A19;
hence Hom(a,a)<>{};
end;
C is with_identities
proof let a be Element of C;
reconsider aa=a as Element of V;
reconsider ii = id$ aa as Morphism of C;
A20: cod ii = cod id$ aa by Def10
.= a;
A21: dom ii = dom id$ aa by Def9
.= a;
then reconsider ii as Morphism of a,a by A20,CAT_1:4;
take ii;
let b be Element of C;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A22: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Element of Maps V;
A23: dom gg = dom g by Def9
.= aa by A22,CAT_1:5;
then
A24: cod id$ aa = dom gg;
dom g = a by A22,CAT_1:5;
then [g,ii] in dom p by A20,A1;
hence g(*)ii = p.(g,ii) by CAT_1:def 1
.= gg*(id$ aa) by A24,Def11
.= g by A23,Th14;
end;
assume
A25: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Element of Maps V;
A26: cod gg = cod g by Def10
.= aa by A25,CAT_1:5;
then
A27: dom id$ aa = cod gg;
cod g = a by A25,CAT_1:5;
then [ii,g] in dom p by A21,A1;
hence ii(*)g = p.(ii,g) by CAT_1:def 1
.= (id$ aa)*gg by A27,Def11
.= g by A26,Th14;
end;
hence thesis by A1,A2,A8,A18;
end;
end;
reserve a,b for Object of Ens(V);
::$CT
theorem
A is Object of Ens(V);
definition
let V,A;
func @A -> Object of Ens(V) equals
A;
coherence;
end;
theorem
a is Element of V;
definition
let V,a;
func @a -> Element of V equals
a;
coherence;
end;
reserve f,g,f1,f2 for Morphism of Ens(V);
theorem
m is Morphism of Ens(V);
definition
let V,m;
func @m -> Morphism of Ens(V) equals
m;
coherence;
end;
theorem
f is Element of Maps(V);
definition
let V,f;
func @f -> Element of Maps(V) equals
f;
coherence;
end;
theorem
dom f = dom(@f) & cod f = cod(@f) by Def9,Def10;
theorem Th26:
Hom(a,b) = Maps(@a,@b)
proof
now
let x be object;
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);
cod(f) = b by A1,CAT_1:1;
then
A2: cod(@f) = @b by Def10;
dom(f) = a by A1,CAT_1:1;
then dom(@f) = @a by Def9;
hence thesis by A2,Th19;
end;
assume
A3: x in Maps(@a,@b);
Maps(@a,@b) c= Maps V by Th17;
then reconsider m = x as Element of Maps V by A3;
cod(m) = @b by A3,Th19;
then
A4: cod(@m) = b by Def10;
dom(m) = @a by A3,Th19;
then dom(@m) = a by Def9;
hence x in Hom(a,b) by A4;
end;
hence thesis by TARSKI:2;
end;
Lm6: Hom(a,b) <> {} implies Funcs(@a,@b) <> {}
proof
set m = the Element of Maps(@a,@b);
assume Hom(a,b) <> {};
then
A1: Maps(@a,@b) <> {} by Th26;
reconsider m as Element of Maps(V) by A1,Th17,TARSKI:def 3;
m`2 in Funcs(@a,@b) by A1,Th20;
hence thesis;
end;
theorem Th27:
dom g = cod f implies g(*)f = (@g)*(@f)
proof
assume
A1: dom g = cod f;
then dom(@g) = cod f by Def9;
then
A2: dom(@g) = cod(@f) by Def10;
thus g(*)f = (the Comp of Ens(V)).(@g,f) by A1,CAT_1:16
.= (@g)*(@f) by A2,Def11;
end;
theorem Th28:
id a = id$ @a
proof
reconsider aa=a as Element of V;
reconsider ii = id$ aa as Morphism of Ens V;
A1: cod ii = cod id$ aa by Def10
.= a;
A2: dom ii = dom id$ aa by Def9
.= a;
then reconsider ii as Morphism of a,a by A1,CAT_1:4;
for b being Object of Ens V holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)ii = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds ii(*)f = f)
proof
let b be Element of Ens V;
set p = the Comp of Ens V;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A3: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Element of Maps V;
A4: dom gg = dom g by Def9
.= aa by A3,CAT_1:5;
then
A5: cod id$ aa = dom gg;
dom g = a by A3,CAT_1:5;
then [g,ii] in dom p by A1,CAT_1:def 6;
hence g(*)ii = p.(g,ii) by CAT_1:def 1
.= gg*(id$ aa) by A5,Def11
.= g by A4,Th14;
end;
assume
A6: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Element of Maps V;
A7: cod gg = cod g by Def10
.= aa by A6,CAT_1:5;
then
A8: dom id$ aa = cod gg;
cod g = a by A6,CAT_1:5;
then [ii,g] in dom p by A2,CAT_1:def 6;
hence ii(*)g = p.(ii,g) by CAT_1:def 1
.= (id$ aa)*gg by A8,Def11
.= g by A7,Th14;
end;
hence thesis by CAT_1:def 12;
end;
theorem
a = {} implies a is initial
proof
assume
A1: a = {};
let b;
Maps(@a,@b) <> {} by A1,Th15;
hence
A2: Hom(a,b)<>{} by Th26;
set m = [[@a,@b],{}];
{} is Function of @a,@b by A1,RELSET_1:12;
then
m in Maps(@a,@b) by A1,Th15;
then m in Hom(a,b) by Th26;
then reconsider f = m as Morphism of a,b by CAT_1:def 5;
take f;
let g be Morphism of a,b;
reconsider m9 = g as Element of Maps(V);
g in Hom(a,b) by A2,CAT_1:def 5;
then
A3: g in Maps(@a,@b) by Th26;
then
A4: m9 = [[@a,@b],m9`2] by Th16;
then m9`2 is Function of @a,@b by A3,Lm4;
hence thesis by A1,A4;
end;
theorem Th30:
{} 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) <> {};
then Funcs(@a,@b) <> {} by Lm6;
hence thesis;
end;
theorem
for W being Universe, a being Object of Ens(W) st a is initial holds a
= {} by Th30,CLASSES2:56;
theorem
(ex x being set st a = {x}) implies a is terminal
proof
given x being set such that
A1: a = {x};
let b;
set h = the Function of @b,@a;
set m = [[@b,@a],h];
A2: m in Maps(@b,@a) by A1,Th15;
hence
A3: Hom(b,a)<>{} by Th26;
m in Hom(b,a) by A2,Th26;
then reconsider f = m as Morphism of b,a by CAT_1:def 5;
take f;
let g be Morphism of b,a;
reconsider m9 = g as Element of Maps(V);
g in Hom(b,a) by A3,CAT_1:def 5;
then
A4: g in Maps(@b,@a) by Th26;
then
A5: m9 = [[@b,@a],m9`2] by Th16;
then m9`2 is Function of @b,@a by A4,Lm4;
hence thesis by A1,A5,FUNCT_2:51;
end;
theorem Th33:
V <> {{}} & a is terminal implies ex x being set st a = {x}
proof
assume that
A1: V <> {{}} and
A2: a is terminal;
set x = the Element of @a;
A3: now
assume
A4: @a = {};
now
consider C being object such that
A5: C in V and
A6: C <> {} by A1,ZFMISC_1:35;
reconsider C as Element of V by A5;
set b = @C;
Hom(b,a) <> {} by A2;
then Funcs(@b,@a) <> {} by Lm6;
hence contradiction by A4,A6;
end;
hence contradiction;
end;
now
assume a <> {x};
then consider y being object such that
A7: y in @a and
A8: y <> x by A3,ZFMISC_1:35;
reconsider fy = @a --> y as Function of @a,@a by A7,FUNCOP_1:45;
reconsider fx = @a --> x as Function of @a,@a by A7,FUNCOP_1:45;
fx.y = x by A7,FUNCOP_1:7;
then
A9: fx <> fy by A7,A8,FUNCOP_1:7;
A10: ([[@a,@a],fx]) in Maps(@a,@a) by Th15;
A11: ([[@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 A10,A11;
A12: m2 in Hom(a,a) by A11,Th26;
m1 in Hom(a,a) by A10,Th26;
then reconsider f = @m1,g = @m2 as Morphism of a,a by A12,CAT_1:def 5;
consider h being Morphism of a,a such that
A13: for h9 being Morphism of a,a holds h = h9 by A2;
f = h by A13
.= g by A13;
hence contradiction by A9,XTUPLE_0:1;
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
A1: {{}} in W by CLASSES2:56,57;
assume W = {{}};
hence contradiction by A1;
end;
hence thesis by Th33;
end;
theorem
for a,b being Object of Ens(V), f being Morphism of a,b st Hom(a,b) <> {}
holds f is monic iff (@f)`2 is one-to-one
proof
let a,b be Object of Ens(V), f be Morphism of a,b such that
A1: Hom(a,b) <> {};
set m = @f;
A2: dom m = dom f by Def9;
then
A3: dom m`2 = dom f by Lm3;
thus f is monic implies (@f)`2 is one-to-one
proof
set A = dom (@f)`2;
assume
A4: f is monic;
let x1,x2 be object such that
A5: x1 in A and
A6: x2 in A and
A7: (@f)`2.x1 = (@f)`2.x2;
A8: A = dom(@f) by Lm3;
then reconsider A as Element of V;
A9: dom f = A by A8,Def9;
reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A5,A6,
FUNCOP_1:45;
reconsider m1 = [[A,A],fx1],m2 = [[A,A],fx2] as Element of Maps(V) by Th5;
set f1 = @m1, f2 = @m2;
set h1 = (@f)`2*(@f1)`2, h2 = (@f)`2*(@f2)`2;
set ff1 = (@f)*(@f1), ff2 = (@f)*(@f2);
A10: cod m2 = A;
then
A11: (ff2)`2 = h2 & dom(ff2) = dom(@f2) by A8,Th12;
cod(ff2) = cod(@f) by A8,A10,Th12;
then
A12: ff2=[[dom(@f2),cod(@f)],h2] by A11,Th8;
dom(@f2) = A;
then
A13: dom f2 = A by Def9;
cod(@f2) = A;
then
A14: cod f2 = A by Def10;
then
A15: f(*)(f2) = ff2 by A9,Th27;
A16: cod m1 = A;
then
A17: (ff1)`2 = h1 & dom(ff1) = dom(@f1) by A8,Th12;
now
thus
A18: dom(h1) = A & dom(h2) = A by A17,A11,Lm3;
let x be object;
assume
A19: x in A;
(@f1)`2.x = x1 by A19,FUNCOP_1:7;
then
A20: h1.x = (@f)`2.x1 by A18,A19,FUNCT_1:12;
(@f2)`2.x = x2 by A19,FUNCOP_1:7;
hence h1.x = h2.x by A7,A18,A19,A20,FUNCT_1:12;
end;
then
A21: h1 = h2;
cod(ff1) = cod(@f) by A8,A16,Th12;
then
A22: ff1=[[dom(@f1),cod(@f)],h1] by A17,Th8;
dom(@f1) = A;
then
A23: dom f1 = A by Def9;
cod(@f1) = A;
then
A24: cod f1 = A by Def10;
reconsider A as Object of Ens(V);
A25: dom f = a by A1,CAT_1:5;
then
A26: f1 in Hom(A,a) & f2 in Hom(A,a) by A23,A9,A24,A13,A14;
then reconsider f1,f2 as Morphism of A,a by CAT_1:def 5;
A27: f*f1 = f(*)f1 by A1,A26,CAT_1:def 13
.= f(*)f2 by A22,A12,A21,A15,A24,A9,Th27
.= f*f2 by A1,A26,CAT_1:def 13;
Hom(A,a) <> {} by A25,A9;
then f1 = f2 by A4,A27;
then fx1 = fx2 by XTUPLE_0:1;
hence x1 = fx2.x1 by A5,FUNCOP_1:7
.= x2 by A5,FUNCOP_1:7;
end;
assume
A28: m`2 is one-to-one;
thus Hom(a,b) <> {} by A1;
let c be Object of Ens(V) such that
A29: Hom(c,a) <> {};
let f1,f2 be Morphism of c,a;
A30: dom f1 = c by A29,CAT_1:5 .= dom f2 by A29,CAT_1:5;
A31: cod f1 = a by A29,CAT_1:5 .= dom f by A1,CAT_1:5;
A32: cod f2 = a by A29,CAT_1:5 .= dom f by A1,CAT_1:5;
assume
A33: f*f1 = f*f2;
set m1 = @f1, m2 = @f2;
A34: m*m1 = f(*)f1 by A31,Th27
.= f*f1 by A29,A1,CAT_1:def 13;
A35: m*m2 = f(*)f2 by A32,Th27
.= f*f2 by A29,A1,CAT_1:def 13;
A36: m1=[[dom m1,cod m1],m1`2] by Th8;
A37: dom m2 = dom f2 by Def9;
then
A38: dom m2`2 = dom f2 by Lm3;
A39: cod m1 = cod f1 by Def10;
then
A40: rng m1`2 c= cod f1 by Lm3;
A41: cod m2 = cod f2 by Def10;
then
A42: rng m2`2 c= cod f2 by Lm3;
A43: m*m2 = [[dom m2,cod m],m`2*m2`2] by A32,A41,A2,Def6;
m*m1 = [[dom m1,cod m],m`2*m1`2] by A31,A39,A2,Def6;
then
A44: (m`2)*(m1`2) = (m`2)*(m2`2) by A35,A33,A34,A43,XTUPLE_0:1;
A45: dom m1 = dom f1 by Def9;
then dom m1`2 = dom f1 by Lm3;
then m1`2 = m2`2 by A28,A30,A31,A32,A38,A3,A40,A42,A44,FUNCT_1:27;
hence thesis by A30,A31,A32,A45,A37,A39,A41,A36,Th8;
end;
theorem Th36:
for a,b being Object of Ens(V), f being Morphism of a,b
st Hom(a,b) <> {}
holds f is epi & (ex A st ex x1,x2 being set st x1 in A & x2 in A & x1
<> x2) implies @f is surjective
proof
let a,b be Object of Ens(V), f be Morphism of a,b such that
A1: Hom(a,b) <> {};
assume
A2: f is epi;
given B being Element of V, x1,x2 being set such that
A3: x1 in B and
A4: x2 in B and
A5: x1 <> x2;
A6: cod(@f) c= rng (@f)`2
proof
set A = cod(@f);
reconsider g1 = A --> x1 as Function of A,B by A3,FUNCOP_1:45;
let x be object;
assume that
A7: x in A and
A8: not x in rng (@f)`2;
set h = {x} --> x2, g2 = g1 +* h;
A9: dom h = {x} by FUNCOP_1:13;
A10: rng h = {x2} by FUNCOP_1:8;
rng g1 = {x1} by A7,FUNCOP_1:8;
then rng g2 c= {x1} \/ {x2} by A10,FUNCT_4:17;
then
A11: rng g2 c= {x1,x2} by ENUMSET1:1;
{x1,x2} c= B by A3,A4,ZFMISC_1:32;
then
A12: rng g2 c= B by A11;
dom g1 = A by FUNCOP_1:13;
then dom g2 = A \/ {x} by A9,FUNCT_4:def 1
.= A by A7,ZFMISC_1:40;
then reconsider g2 as Function of A,B by A3,A12,FUNCT_2:def 1,RELSET_1:4;
A13: cod f = A by Def10;
A14: x in {x} by TARSKI:def 1;
then h.x = x2 by FUNCOP_1:7;
then
A15: g2.x = x2 by A14,A9,FUNCT_4:13;
A16: g1.x = x1 by A7,FUNCOP_1:7;
reconsider m1 = [[A,B],g1], m2 = [[A,B],g2] as Element of Maps(V) by A3,Th5
;
set f1 = @m1, f2 = @m2;
set h1 = (@f1)`2*(@f)`2, h2 = (@f2)`2*(@f)`2;
set f1f = (@f1)*(@f), f2f = (@f2)*(@f);
A17: dom m1 = A;
then
A18: (f1f)`2 = h1 & dom(f1f) = dom(@f) by Th12;
A19: dom m2 = A;
then
A20: (f2f)`2 = h2 & dom(f2f) = dom(@f) by Th12;
cod(@f2) = B;
then
A21: cod f2 = B by Def10;
dom(@f2) = A;
then
A22: dom f2 = A by Def9;
then
A23: f2(*)f = f2f by A13,Th27;
now
thus
A24: dom(h1) = dom(@f) & dom(h2) = dom(@f) by A18,A20,Lm3;
let z be object;
set y = (@f)`2.z;
assume
A25: z in dom(@f);
then z in dom (@f)`2 by Lm3;
then y in rng (@f)`2 by FUNCT_1:def 3;
then
A26: not y in {x} by A8,TARSKI:def 1;
h1.z = g1.y & h2.z = g2.y by A24,A25,FUNCT_1:12;
hence h1.z = h2.z by A9,A26,FUNCT_4:11;
end;
then
A27: h1 = h2;
cod(f1f) = cod(@f1) by A17,Th12;
then
A28: f1f=[[dom(@f),cod(@f1)],h1] by A18,Th8;
cod(f2f) = cod(@f2) by A19,Th12;
then
A29: f2f=[[dom(@f),cod(@f2)],h2] by A20,Th8;
A30: f1f = f2f by A28,A29,A27;
cod(@f1) = B;
then
A31: cod f1 = B by Def10;
dom(@f1) = A;
then
A32: dom f1 = A by Def9;
reconsider B as Object of Ens(V);
A33: cod f = b by A1,CAT_1:5;
then
A34: f1 in Hom(b,B) by A13,A31,A32;
then reconsider f1 as Morphism of b,B by CAT_1:def 5;
f2 in Hom(b,B) by A13,A21,A22,A33;
then reconsider f2 as Morphism of b,B by CAT_1:def 5;
f1*f = f1(*)f by A1,A34,CAT_1:def 13
.= f2(*)f by A30,A23,A32,A13,Th27
.= f2*f by A1,A34,CAT_1:def 13;
then f1 = f2 by A2,A34;
hence contradiction by A5,A16,A15,XTUPLE_0:1;
end;
rng (@f)`2 c= cod(@f) by Lm3;
hence rng (@f)`2 = cod(@f) by A6,XBOOLE_0:def 10;
end;
theorem
for a,b being Object of Ens(V) st Hom(a,b) <> {}
for f being Morphism of a,b st @f is surjective
holds f is epi
proof
let a,b be Object of Ens(V) such that
A1: Hom(a,b) <> {};
let f be Morphism of a,b;
set m = @f;
assume
A2: rng m`2 = cod m;
thus Hom(a,b) <> {} by A1;
let c be Object of Ens(V) such that
A3: Hom(b,c) <> {};
let f1,f2 be Morphism of b,c;
A4: dom f1 = b by A3,CAT_1:5 .= cod f by A1,CAT_1:5;
A5: dom f2 = b by A3,CAT_1:5 .= cod f by A1,CAT_1:5;
A6: cod f1 = c by A3,CAT_1:5 .= cod f2 by A3,CAT_1:5;
assume
A7: f1*f=f2*f;
set m1 = @f1, m2 = @f2;
A8: m1*m = f1(*)f by A4,Th27
.= f1*f by A1,A3,CAT_1:def 13;
A9: m2*m = f2(*)f by A5,Th27
.= f2*f by A1,A3,CAT_1:def 13;
A10: m1=[[dom m1,cod m1],m1`2] by Th8;
A11: cod m1 = cod f1 & cod m2 = cod f2 by Def10;
A12: dom m2 = dom f2 by Def9;
then
A13: dom m2`2 = dom f2 by Lm3;
A14: cod m = cod f by Def10;
then
A15: m2*m = [[dom m,cod m2],m2`2*m`2] by A5,A12,Def6;
A16: dom m1 = dom f1 by Def9;
then m1*m = [[dom m,cod m1],m1`2*m`2] by A4,A14,Def6;
then
A17: (m1`2)*(m`2) = (m2`2)*(m`2) by A7,A8,A15,A9,XTUPLE_0:1;
dom m1`2 = dom f1 by A16,Lm3;
then m1`2 = m2`2 by A2,A4,A5,A14,A17,A13,FUNCT_1:86;
hence thesis by A4,A5,A6,A16,A12,A11,A10,Th8;
end;
theorem
for W being Universe, a,b being Object of Ens(W) st Hom(a,b) <> {}
for f being Morphism of a,b st f is epi holds @f
is surjective
proof
let W be Universe, a,b being Object of Ens(W) such that
Hom(a,b) <> {};
let f be Morphism of a,b;
{} in W & {{}} in W by CLASSES2:56,57;
then
A1: {{},{{}}} in W by CLASSES2:58;
{} in {{},{{}}} & {{}} in {{},{{}}} by TARSKI:def 2;
hence thesis by A1,Th36;
end;
Lm7:
for W being non empty Subset of V
holds Ens W is Subcategory of Ens V
proof
let W be non empty Subset of V;
A1: for a,b being Object of Ens(W), a9,b9 being Object of Ens(V) st a = a9 &
b = b9 holds Hom(a,b) = Hom(a9,b9)
proof
let a,b be Object of Ens(W), a9,b9 be Object of Ens(V);
assume
A2: a = a9 & b = b9;
Hom(a,b) = Maps(@a,@b) & Hom(a9,b9) = Maps(@a9,@b9) by Th26;
hence thesis by A2,Lm5;
end;
set w = the Comp of Ens(W), v = the Comp of Ens(V);
thus the carrier of Ens(W) c= the carrier of Ens(V);
thus for a,b being Object of Ens(W), a9,b9 being Object of Ens(V) st a =
a9 & b = b9 holds Hom(a,b) c= Hom(a9,b9) by A1;
now
A3: dom w c= [:Maps W,Maps W:] by RELAT_1:def 18;
thus
A4: dom w c= dom v
proof
let x,y be object;
assume
A5: [x,y] in dom w;
then consider m2,m1 being Element of Maps W such that
A6: [x,y] = [m2,m1] by A3,DOMAIN_1:1;
reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7,TARSKI:def 3;
A7: dom m29 = dom m2 & cod m19 = cod m1;
dom m2 = cod m1 by A5,A6,Def11;
hence thesis by A6,A7,Def11;
end;
let x be object;
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:1;
reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7,TARSKI:def 3;
A10: dom m29 = cod m19 by A4,A8,A9,Def11;
A11: dom m2 = cod m1 by A8,A9,Def11;
then
A12: m2*m1=[[dom m1,cod m2],m2`2*m1`2] by Def6;
dom m1 = dom m19 & cod m2 = cod m29;
then m29*m19=[[dom m1,cod m2], m2`2*m1`2] by A10,Def6;
hence w.x = m29*m19 by A9,A11,A12,Def11
.= v.x by A9,A10,Def11;
end;
hence the Comp of Ens(W) c= the Comp of Ens(V) by GRFUNC_1:2;
let a be Object of Ens(W), a9 be Object of Ens(V);
A13: id$(@a) = [[@a,@a],id(@a)];
assume a = a9;
hence id a = id$(@a9) by A13,Th28
.= id a9 by Th28;
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;
reconsider E = Ens W as Subcategory of Ens V by Lm7;
for a,b being Object of E, a9,b9 being Object of Ens(V) st a = a9 &
b = b9 holds Hom(a,b) = Hom(a9,b9)
proof
let a,b be Object of E, a9,b9 be Object of Ens(V);
assume
A1: a = a9 & b = b9;
reconsider aa=a, bb=b as Element of Ens W;
Hom(aa,bb) = Maps(@aa,@bb) & Hom(a9,b9) = Maps(@a9,@b9) by Th26;
hence thesis by A1,Lm5;
end;
hence thesis by CAT_2:def 6;
end;
begin :: Representable Functors
reserve C for Category,
a,b,a9,b9,c for Object of C,
f,g,h,f9,g9 for Morphism of C;
definition
let C;
func Hom(C) -> set equals
the set of all Hom(a,b);
coherence;
end;
registration
let C;
cluster Hom(C) -> non empty;
coherence
proof
set a = the Object of C;
Hom(a,a) in the set of all Hom(a9,b9);
hence thesis;
end;
end;
theorem
Hom(a,b) in Hom(C);
:: 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:2;
hence thesis by CAT_1:24;
end;
definition
let C,a,f;
func hom(a,f) -> Function of Hom(a,dom f),Hom(a,cod f) means
:Def18:
for g st g in Hom(a,dom f) holds it.g = f(*)g;
existence
proof
defpred P[object,object] means for g st g = $1 holds $2 = f(*)g;
set X = Hom(a,dom f), Y = Hom(a,cod f);
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume
A2: x in X;
then reconsider g = x as Morphism of a,dom f by CAT_1:def 5;
take f(*)g;
Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f by CAT_1:1,4;
hence thesis by A2,CAT_1:23;
end;
consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A1);
Hom(dom f,cod f) <> {} by CAT_1:2;
then Y = {} implies X = {} by CAT_1:24;
then reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:4;
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
let x be object;
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:12;
end;
func hom(f,a) -> Function of Hom(cod f,a),Hom(dom f,a) means
:Def19:
for g st g in Hom(cod f,a) holds it.g = g(*)f;
existence
proof
defpred P[object,object] means for g st g = $1 holds $2 = g(*)f;
set X = Hom(cod f,a), Y = Hom(dom f,a);
A8: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume
A9: x in X;
then reconsider g = x as Morphism of cod f,a by CAT_1:def 5;
take g(*)f;
Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f by CAT_1:2,4;
hence thesis by A9,CAT_1:23;
end;
consider h being Function such that
A10: dom h = X & rng h c= Y and
A11: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A8);
Hom(dom f,cod f) <> {} by CAT_1:2;
then Y = {} implies X = {} by CAT_1:24;
then reconsider h as Function of X,Y by A10,FUNCT_2:def 1,RELSET_1:4;
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
let x be object;
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:12;
end;
end;
theorem Th42:
hom(a,id c) = id Hom(a,c)
proof
set A = Hom(a,c);
now
A = {} implies A = {};
hence dom hom(a,id c) = A by FUNCT_2:def 1;
let x be object;
assume
A1: x in A;
then reconsider g = x as Morphism of C;
A2: cod g = c by A1,CAT_1:1;
thus hom(a,id c).x = id(c)(*)g by A1,Def18
.= x by A2,CAT_1:21;
end;
hence thesis by FUNCT_1:17;
end;
theorem Th43:
hom(id c,a) = id Hom(c,a)
proof
set A = Hom(c,a);
now
A = {} implies A = {};
hence dom hom(id c,a) = A by FUNCT_2:def 1;
let x be object;
assume
A1: x in A;
then reconsider g = x as Morphism of C;
A2: dom g = c by A1,CAT_1:1;
thus hom(id(c),a).x = g(*)id(c) by A1,Def19
.= x by A2,CAT_1:22;
end;
hence thesis by FUNCT_1:17;
end;
theorem Th44:
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 by CAT_1:17;
A3: cod(g(*)f) = cod g by A1,CAT_1:17;
now
set h = hom(a,g(*)f), h2 = hom(a,g), h1 = hom(a,f);
A4: Hom(dom f,cod f) <> {} by CAT_1:2;
then
A5: Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:24;
Hom(dom g,cod g) <> {} by CAT_1:2;
then
A6: Hom(a,cod g) = {} implies Hom(a,dom g) = {} by CAT_1:24;
hence dom h = Hom(a,dom f) by A1,A2,A3,A5,FUNCT_2:def 1;
thus
A7: dom(h2*h1) = Hom(a,dom f) by A1,A5,A6,FUNCT_2:def 1;
let x be object;
assume
A8: x in Hom(a,dom f);
then reconsider f9 = x as Morphism of C;
A9: cod f9 = dom f by A8,CAT_1:1;
A10: h1.x in Hom(a,dom g) by A1,A4,A8,CAT_1:24,FUNCT_2:5;
then reconsider g9 = h1.x as Morphism of C;
thus h.x = g(*)f(*)f9 by A2,A8,Def18
.= g(*)(f(*)f9) by A1,A9,CAT_1:18
.= g(*)g9 by A8,Def18
.= h2.g9 by A10,Def18
.= (h2*h1).x by A7,A8,FUNCT_1:12;
end;
hence thesis;
end;
theorem Th45:
dom g = cod f implies hom(g(*)f,a) = hom(f,a)*hom(g,a)
proof
assume
A1: dom g = cod f;
then
A2: cod(g(*)f) = cod g by CAT_1:17;
A3: dom(g(*)f) = dom f by A1,CAT_1:17;
now
set h = hom(g(*)f,a), h2 = hom(g,a), h1 = hom(f,a);
A4: Hom(dom g,cod g) <> {} by CAT_1:2;
then
A5: Hom(dom g,a) = {} implies Hom(cod g,a) = {} by CAT_1:24;
Hom(dom f,cod f) <> {} by CAT_1:2;
then
A6: Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:24;
hence dom h = Hom(cod g,a) by A1,A3,A2,A5,FUNCT_2:def 1;
thus
A7: dom(h1*h2) = Hom(cod g,a) by A1,A6,A5,FUNCT_2:def 1;
let x be object;
assume
A8: x in Hom(cod g,a);
then reconsider f9 = x as Morphism of C;
A9: dom f9 = cod g by A8,CAT_1:1;
A10: h2.x in Hom(cod f,a) by A1,A4,A8,CAT_1:24,FUNCT_2:5;
then reconsider g9 = h2.x as Morphism of C;
thus h.x = f9(*)(g(*)f) by A2,A8,Def19
.= f9(*)g(*)f by A1,A9,CAT_1:18
.= g9(*)f by A8,Def19
.= h1.g9 by A10,Def19
.= (h1*h2).x by A7,A8,FUNCT_1:12;
end;
hence thesis;
end;
theorem Th46:
[[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:2;
then
A1: Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:24;
Hom(a,dom f) in Hom(C) & Hom(a,cod f) in Hom(C);
hence thesis by A1,Th5;
end;
theorem Th47:
[[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:2;
then
A1: Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:24;
Hom(dom f,a) in Hom(C) & Hom(cod f,a) in Hom(C);
hence thesis by A1,Th5;
end;
definition
let C,a;
func hom?-(a) -> Function of the carrier' of C, Maps(Hom(C)) means
:Def20:
for f holds it.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
existence
proof
defpred P[object,object] means
for f st f = $1 holds $2 = [[Hom(a,dom f),Hom(a,
cod f)],hom(a,f)];
set X = the carrier' of C, Y = Maps(Hom(C));
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
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 Th46;
hence thesis;
end;
consider h being Function such that
A2: dom h = X & rng h c= Y and
A3: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A1);
reconsider h as Function of X,Y by A2,FUNCT_2:def 1,RELSET_1:4;
take h;
thus thesis by A3;
end;
uniqueness
proof
let h1,h2 be Function of the carrier' 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:63;
end;
func hom-?(a) -> Function of the carrier' of C, Maps(Hom(C)) means
:Def21:
for f holds it.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
existence
proof
defpred P[object,object] means
for f st f = $1 holds $2 = [[Hom(cod f,a),Hom(dom
f,a)],hom(f,a)];
set X = the carrier' of C, Y = Maps(Hom(C));
A6: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
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 Th47;
hence thesis;
end;
consider h being Function such that
A7: dom h = X & rng h c= Y and
A8: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A6);
reconsider h as Function of X,Y by A7,FUNCT_2:def 1,RELSET_1:4;
take h;
thus thesis by A8;
end;
uniqueness
proof
let h1,h2 be Function of the carrier' 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:63;
end;
end;
Lm8: for T being Function of the carrier' of C, Maps(Hom(C)) st Hom(C) c= V
holds T is Function of the carrier' of C, the carrier' of Ens V
proof
let T be Function of the carrier' of C, Maps(Hom(C));
assume Hom(C) c= V;
then Maps(Hom(C)) c= Maps(V) by Th7;
hence thesis by FUNCT_2:7;
end;
Lm9: 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
A1: Hom(a,c) in Hom(C);
assume Hom(C) c= V;
then reconsider A = Hom(a,c) as Element of V by A1;
A2: hom(a,id c) = id A by Th42;
let d be Object of Ens(V);
assume d = Hom(a,c);
hence (hom?-(a)).(id c) = id$ @d by A2,Def20
.= id d by Th28;
end;
Lm10: 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
A1: Hom(c,a) in Hom(C);
assume Hom(C) c= V;
then reconsider A = Hom(c,a) as Element of V by A1;
A2: hom(id(c),a) = id A by Th43;
let d be Object of Ens(V);
assume d = Hom(c,a);
hence (hom-?(a)).(id c) = id$ @d by A2,Def21
.= id d by Th28;
end;
theorem Th48:
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 carrier' of C, the carrier' of
Ens V by Lm8;
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);
then reconsider A = Hom(a,c) as Element of V by A1;
take d = @A;
thus thesis by A1,Lm9;
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;
set g = T.f;
Hom(a,b) in Hom(C) & Hom(a,c) in Hom(C);
then reconsider A = Hom(a,b), B = Hom(a,c) as Element of V by A1;
A2: [[Hom(a,b),Hom(a,c)],hom(a,f)] = @g by Def20
.= [[dom(@g), cod(@g)],(@g)`2] by Th8
.= [[dom g, cod(@g)],(@g)`2] by Def9
.= [[dom g, cod g],(@g)`2] by Def10;
thus T.(id b) = id @A by A1,Lm9
.= id dom (T.f) by A2,Lm1;
thus T.(id c) = id @B by A1,Lm9
.= id cod (T.f) by A2,Lm1;
end;
let f,g be Morphism of C such that
A3: dom g = cod f;
A4: [[Hom(a,dom g),Hom(a,cod g)],hom(a,g)] = @(T.g) by Def20
.= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
.= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Def9
.= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Def10;
then
A5: (@(T.g))`2=hom(a,g) by XTUPLE_0:1;
cod(T.g)=Hom(a,cod g ) by A4,Lm1;
then
A6: cod(@(T.g))=Hom(a,cod g) by Def10;
A7: dom(T.g)=Hom(a,dom g) by A4,Lm1;
then
A8: dom(@(T.g))=Hom(a,dom g) by Def9;
A9: [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] = @(T.f) by Def20
.= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
.= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Def9
.= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Def10;
then
A10: (@(T.f))`2=hom(a,f) by XTUPLE_0:1;
dom(T.f)=Hom(a,dom f) by A9,Lm1;
then
A11: dom(@(T.f))=Hom(a,dom f) by Def9;
A12: cod(T.f)=Hom(a,cod f ) by A9,Lm1;
then
A13: cod(@(T.f))=Hom(a,cod f) by Def10;
dom(g(*)f) = dom f & cod(g(*)f) = cod g by A3,CAT_1:17;
hence T.(g(*)f) = [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g(*)f)] by Def20
.= [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g)*hom(a,f)] by A3,Th44
.= (@(T.g))*(@(T.f)) by A3,A10,A11,A13,A5,A8,A6,Def6
.= (T.g)(*)(T.f) by A3,A12,A7,Th27;
end;
hence thesis by CAT_1:61;
end;
theorem Th49:
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 carrier' of C, the carrier' of
Ens V by Lm8;
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);
then reconsider A = Hom(c,a) as Element of V by A1;
take d = @A;
thus thesis by A1,Lm10;
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;
set g = T.f;
Hom(b,a) in Hom(C) & Hom(c,a) in Hom(C);
then reconsider A = Hom(b,a), B = Hom(c,a) as Element of V by A1;
A2: [[Hom(b,a),Hom(c,a)],hom(f,a)] = @g by Def21
.= [[dom(@g), cod(@g)],(@g)`2] by Th8
.= [[dom g, cod(@g)],(@g)`2] by Def9
.= [[dom g, cod g],(@g)`2] by Def10;
thus T.(id c) = id @B by A1,Lm10
.= id cod (T.f) by A2,Lm1;
thus T.(id b) = id @A by A1,Lm10
.= id dom (T.f) by A2,Lm1;
end;
let f,g be Morphism of C such that
A3: dom g = cod f;
A4: [[Hom(cod g,a),Hom(dom g,a)],hom(g,a)] = @(T.g) by Def21
.= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
.= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Def9
.= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Def10;
then
A5: (@(T.g))`2=hom(g,a) by XTUPLE_0:1;
dom(T.g)=Hom(cod g,a) by A4,Lm1;
then
A6: dom(@(T.g))=Hom(cod g,a) by Def9;
A7: cod(T.g)=Hom(dom g,a ) by A4,Lm1;
then
A8: cod(@(T.g))=Hom(dom g,a) by Def10;
A9: [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] = @(T.f) by Def21
.= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
.= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Def9
.= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Def10;
then
A10: (@(T.f))`2=hom(f,a) by XTUPLE_0:1;
cod(T.f)=Hom(dom f,a ) by A9,Lm1;
then
A11: cod(@(T.f))=Hom(dom f,a) by Def10;
A12: dom(T.f)=Hom(cod f,a) by A9,Lm1;
then
A13: dom(@(T.f))=Hom(cod f,a) by Def9;
dom(g(*)f) = dom f & cod(g(*)f) = cod g by A3,CAT_1:17;
hence T.(g(*)f) = [[Hom(cod(g),a),Hom(dom(f),a)],hom(g(*)f,a)] by Def21
.= [[Hom(cod(g),a),Hom(dom(f),a)],hom(f,a)*hom(g,a)] by A3,Th45
.= (@(T.f))*(@(T.g)) by A3,A10,A13,A11,A5,A6,A8,Def6
.= (T.f)(*)(T.g) by A3,A12,A7,Th27;
end;
hence thesis by OPPCAT_1:def 9;
end;
:: hom-bifunctor
theorem Th50:
Hom(dom f,cod f9) = {} implies Hom(cod f,dom f9) = {}
proof
assume that
A1: Hom(dom f,cod f9) = {} and
A2: Hom(cod f,dom f9) <> {};
A3: Hom(dom f9,cod f9) <> {} by CAT_1:2;
Hom(dom f,cod f) <> {} by CAT_1:2;
then Hom(dom f,dom f9) <> {} by A2,CAT_1:24;
hence contradiction by A1,A3,CAT_1:24;
end;
definition
let C,f,g;
func hom(f,g) -> Function of Hom(cod f,dom g),Hom(dom f,cod g) means
:Def22:
for h st h in Hom(cod f,dom g) holds it.h = g(*)h(*)f;
existence
proof
defpred P[object,object] means for h st h = $1 holds $2 = g(*)h(*)f;
set X = Hom(cod f,dom g), Y = Hom(dom f,cod g);
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
A2: Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f by CAT_1:2,4;
assume
A3: x in X;
then reconsider h = x as Morphism of cod f,dom g by CAT_1:def 5;
take g(*)h(*)f;
Hom(dom g,cod g) <> {} & g is Morphism of dom g,cod g by CAT_1:2,4;
then
A4: g(*)h in Hom(cod f,cod g) by A3,CAT_1:23;
then g(*)h is Morphism of cod f,cod g by CAT_1:def 5;
hence thesis by A4,A2,CAT_1:23;
end;
consider h being Function such that
A5: dom h = X & rng h c= Y and
A6: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A1);
Y = {} implies X = {} by Th50;
then reconsider h as Function of X,Y by A5,FUNCT_2:def 1,RELSET_1:4;
take h;
thus thesis by A6;
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
A7: for h st h in X holds h1.h = g(*)h(*)f and
A8: for h st h in X holds h2.h = g(*)h(*)f;
now
let x be object;
assume
A9: x in X;
then reconsider h = x as Morphism of C;
thus h1.x = g(*)h(*)f by A7,A9
.= h2.x by A8,A9;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th51:
[[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] is Element of Maps(Hom(C))
proof
A1: 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 Th50;
hence thesis by A1,Th5;
end;
theorem Th52:
hom(id a,f) = hom(a,f) & hom(f,id a) = hom(f,a)
proof
A1: cod id a = a;
now
Hom(dom f,cod f) <> {} by CAT_1:2;
then Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:24;
hence
dom hom(id a,f) = Hom(a,dom f) & dom hom(a,f) = Hom(a,dom f)
by FUNCT_2:def 1;
let x be object;
assume
A2: x in Hom(a,dom f);
then reconsider g = x as Morphism of C;
A3: dom g = a by A2,CAT_1:1;
A4: cod g = dom f by A2,CAT_1:1;
thus hom(id a,f).x = f(*)g(*)(id a) by A2,Def22
.= f(*)(g(*)(id a)) by A1,A3,A4,CAT_1:18
.= f(*)g by A3,CAT_1:22
.= hom(a,f).x by A2,Def18;
end;
hence hom(id a,f) = hom(a,f);
now
Hom(dom f,cod f) <> {} by CAT_1:2;
then Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:24;
hence
dom hom(f,id a) = Hom(cod f,a) & dom hom(f,a) = Hom(cod f,a)
by FUNCT_2:def 1;
let x be object;
assume
A5: x in Hom(cod f,a);
then reconsider g = x as Morphism of C;
A6: cod g = a by A5,CAT_1:1;
thus hom(f,id a).x = (id a)(*)g(*)f by A5,Def22
.= g(*)f by A6,CAT_1:21
.= hom(f,a).x by A5,Def19;
end;
hence thesis;
end;
theorem Th53:
hom(id a,id b) = id Hom(a,b)
proof
thus hom(id a,id b) = hom(a,id b) by Th52
.= id Hom(a,b) by Th42;
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 Th50;
hence dom hom(f,g) = Hom(cod f,dom g) by FUNCT_2:def 1;
Hom(dom f,cod f) <> {} by CAT_1:2;
then Hom(dom f,dom g) = {} implies Hom(cod f,dom g) = {} by CAT_1:24;
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 object;
assume
A3: x in Hom(cod f,dom g);
then reconsider h = x as Morphism of C;
A4: dom h = cod f by A3,CAT_1:1;
then
A5: dom(h(*)f) = dom f by CAT_1:17;
A6: cod h = dom g by A3,CAT_1:1;
then cod(h(*)f) = dom g by A4,CAT_1:17;
then
A7: h(*)f in Hom(dom f,dom g) by A5;
thus hom(f,g).x = g(*)h(*)f by A3,Def22
.= g(*)(h(*)f) by A4,A6,CAT_1:18
.= hom(dom f,g).(h(*)f) by A7,Def18
.= hom(dom f,g).((hom(f,dom g)).h) by A3,Def19
.= (hom(dom f,g)*hom(f,dom g)).x by A2,A3,FUNCT_1:12;
end;
hence thesis;
end;
theorem Th55:
cod g = dom f & dom g9 = cod f9 implies
hom(f(*)g,g9(*)f9) = hom(g, g9)*hom(f,f9)
proof
assume that
A1: cod g = dom f and
A2: dom g9 = cod f9;
A3: dom(g9(*)f9) = dom f9 by A2,CAT_1:17;
A4: cod(f(*)g) = cod f by A1,CAT_1:17;
A5: cod(g9(*)f9) = cod g9 & dom(f(*)g) = dom g by A1,A2,CAT_1:17;
now
set h = hom(f(*)g,g9(*)f9), h2 = hom(g,g9), h1 = hom(f,f9);
A6: Hom(dom f,cod f9) = {} implies Hom(cod f,dom f9) = {} by Th50;
A7: Hom(dom g,cod g9) = {} implies Hom(cod g,dom g9) = {} by Th50;
hence dom h = Hom(cod f,dom f9) by A1,A2,A3,A5,A4,A6,FUNCT_2:def 1;
thus
A8: dom(h2*h1) = Hom(cod f,dom f9) by A1,A2,A7,A6,FUNCT_2:def 1;
let x be object;
assume
A9: x in Hom(cod f,dom f9);
then reconsider k = x as Morphism of C;
A10: h1.x in Hom(cod g,dom g9) by A1,A2,A9,Th50,FUNCT_2:5;
then reconsider l = h1.x as Morphism of C;
A11: dom k = cod f by A9,CAT_1:1;
then
A12: cod(k(*)(f(*)g)) = cod k by A4,CAT_1:17;
A13: cod k = dom f9 by A9,CAT_1:1;
then
A14: dom(f9(*)k) = dom k by CAT_1:17;
then
A15: dom (f9(*)k(*)f) = dom f by A11,CAT_1:17;
cod(f9(*)k) = cod f9 by A13,CAT_1:17;
then
A16: cod(f9(*)k(*)f) = cod f9 by A11,A14,CAT_1:17;
thus h.x = (g9(*)f9)(*)k(*)(f(*)g) by A3,A4,A9,Def22
.= (g9(*)f9)(*)(k(*)(f(*)g)) by A3,A4,A13,A11,CAT_1:18
.= g9(*)(f9(*)(k(*)(f(*)g))) by A2,A13,A12,CAT_1:18
.= g9(*)(f9(*)k(*)(f(*)g)) by A4,A13,A11,CAT_1:18
.= g9(*)(f9(*)k(*)f(*)g) by A1,A11,A14,CAT_1:18
.= g9(*)(f9(*)k(*)f)(*)g by A1,A2,A15,A16,CAT_1:18
.= g9(*)l(*)g by A9,Def22
.= h2.l by A10,Def22
.= (h2*h1).x by A8,A9,FUNCT_1:12;
end;
hence thesis;
end;
definition
let C;
func hom??(C) -> Function of the carrier' of [:C,C:], Maps(Hom(C)) means
:
Def23: for
f,g holds it.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
existence
proof
defpred P[object,object] means
for f,g st $1=[f,g] holds $2=[[Hom(cod f,dom g),
Hom(dom f,cod g)],hom(f,g)];
set X = the carrier' of [:C,C:], Y = Maps(Hom(C));
A1: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume x in X;
then consider f,g such that
A2: x = [f,g] by DOMAIN_1:1;
take y = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
y is Element of Y by Th51;
hence y in Y;
let f9,g9;
assume x = [f9,g9];
then f9 = f & g9 = g by A2,XTUPLE_0:1;
hence thesis;
end;
consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A1);
reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:4;
take h;
thus thesis by A4;
end;
uniqueness
proof
let h1,h2 be Function of the carrier' 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 carrier' of [:C,C:] = [:the carrier' of C,the carrier' of C:];
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 BINOP_1:2;
end;
end;
theorem Th56:
hom?-(a) = (curry (hom??(C))).(id a) & hom-?(a) = (curry' (hom?? (C))).(id a)
proof
reconsider T = hom??(C) as Function of [:the carrier' of C,the carrier' of C
:],Maps(Hom(C));
now
let f;
thus ((curry T).(id a)).f = T.(id a,f) by FUNCT_5:69
.= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(id a,f)] by Def23
.= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(a,f)] by Th52
.= [[Hom(a,dom f),Hom(dom id a,cod f)],hom(a,f)]
.= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)]
.= (hom?-(a)).f by Def20;
end;
hence hom?-(a) = (curry (hom??(C))).(id a) by FUNCT_2:63;
now
let f;
thus ((curry' T).(id a)).f = T.(f,id a) by FUNCT_5:70
.= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,id a)] by Def23
.= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,a)] by Th52
.= [[Hom(cod f,a),Hom(dom f,cod id a)],hom(f,a)]
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
.= (hom-?(a)).f by Def21;
end;
hence thesis by FUNCT_2:63;
end;
Lm11: 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
A1: Hom(a,b) in Hom(C);
assume Hom(C) c= V;
then reconsider A = Hom(a,b) as Element of V by A1;
A2: hom(id a,id b) = id A by Th53;
let d be Object of Ens(V);
assume d = Hom(a,b);
hence (hom??(C)).[id a,id b] = id$ @d by A2,Def23
.= id d by Th28;
end;
theorem Th57:
Hom(C) c= V implies hom??(C) is Functor of [:C opp,C:],Ens(V)
proof
assume
A1: Hom(C) c= V;
then C opp = CatStr (#the carrier of C, the carrier' of C, the Target of C,
the Source of C, ~(the Comp of C)#) & Maps(Hom(C)) c= Maps(V) by Th7;
then reconsider T = hom??(C) as Function of the carrier' of [:C opp,C:], the
carrier' of Ens V by FUNCT_2:7;
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
A2: c = [a,b] by DOMAIN_1:1;
Hom(opp a,b) in Hom(C);
then reconsider A = Hom(opp a,b) as Element of V by A1;
take d = @A;
A3: id opp a = id a by OPPCAT_1:72;
id c = [id opp a,id b] by A3,A2,CAT_2:31;
hence thesis by A1,Lm11;
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
A4: fg = [f,g] by DOMAIN_1:1;
Hom(cod opp f,dom g) in Hom(C) & Hom(dom opp f,cod g) in Hom(C);
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;
A5: id opp dom f = id dom f by OPPCAT_1:72;
A6: id opp cod f = id cod f by OPPCAT_1:72;
A7: [[Hom(cod opp f,dom g),Hom(dom opp f,cod g)],hom(opp f,g)] = @h by A4
,Def23
.= [[dom(@h), cod(@h)],(@h)`2] by Th8
.= [[dom h, cod(@h)],(@h)`2] by Def9
.= [[dom h, cod h],(@h)`2] by Def10;
thus T.(id dom fg) = T.(id [dom f,dom g]) by A4,CAT_2:28
.= T.[id dom f,id dom g] by CAT_2:31
.= id @A by A1,Lm11,A5
.= id dom (T.fg) by A7,Lm1;
thus T.(id cod fg) = T.(id [cod f,cod g]) by A4,CAT_2:28
.= T.[id cod f,id cod g] by CAT_2:31
.= id @B by A1,Lm11,A6
.= id cod (T.fg) by A7,Lm1;
end;
let ff,gg be Morphism of [:C opp,C:] such that
A8: dom gg = cod ff;
consider g being (Morphism of C opp), g9 such that
A9: gg = [g,g9] by DOMAIN_1:1;
A10: [[Hom(cod opp g,dom g9),Hom(dom opp g,cod g9)],hom(opp g,g9)] = @(T.
gg) by A9,Def23
.= [[dom(@(T.gg)),cod(@(T.gg))],(@(T.gg))`2] by Th8
.= [[dom(T.gg),cod(@(T.gg))],(@(T.gg))`2] by Def9
.= [[dom(T.gg),cod(T.gg)],(@(T.gg))`2] by Def10;
then
A11: (@(T.gg))`2=hom(opp g,g9) by XTUPLE_0:1;
cod(T.gg)=Hom(dom opp g,cod g9) by A10,Lm1;
then
A12: cod(@(T.gg))=Hom(dom opp g, cod g9) by Def10;
A13: dom(T.gg)=Hom(cod opp g,dom g9) by A10,Lm1;
then
A14: dom(@(T.gg))=Hom(cod opp g,dom g9) by Def9;
consider f being (Morphism of C opp), f9 such that
A15: ff = [f,f9] by DOMAIN_1:1;
A16: [[Hom(cod opp f,dom f9),Hom(dom opp f,cod f9)],hom(opp f,f9)] = @(T.
ff) by A15,Def23
.= [[dom(@(T.ff)),cod(@(T.ff))],(@(T.ff))`2] by Th8
.= [[dom(T.ff),cod(@(T.ff))],(@(T.ff))`2] by Def9
.= [[dom(T.ff),cod(T.ff)],(@(T.ff))`2] by Def10;
then
A17: (@(T.ff))`2=hom(opp f,f9) by XTUPLE_0:1;
dom(T.ff)=Hom(cod opp f,dom f9) by A16,Lm1;
then
A18: dom(@(T.ff))=Hom(cod opp f,dom f9) by Def9;
A19: cod(T.ff)=Hom(dom opp f,cod f9) by A16,Lm1;
then
A20: cod(@(T.ff))=Hom(dom opp f, cod f9) by Def10;
A21: cod ff = [cod f,cod f9] by A15,CAT_2:28;
A22: dom gg = [dom g,dom g9] by A9,CAT_2:28;
then
A23: cod opp g = dom opp f by A8,A21,XTUPLE_0:1;
then
A24: dom((opp f)(*)(opp g)) = dom opp g & cod((opp f)(*)(opp g)) = cod opp f
by CAT_1:17;
A25: dom g = cod f by A8,A22,A21,XTUPLE_0:1;
A26: dom g9 = cod f9 by A8,A22,A21,XTUPLE_0:1;
then
A27: dom(g9(*)f9) = dom f9 & cod(g9(*)f9) = cod g9 by CAT_1:17;
thus T.(gg(*)ff)
= T.([opp (g(*)f),g9(*)f9]) by A8,A15,A9,CAT_2:30
.= T.([(opp f)(*)(opp g),g9(*)f9]) by A25,OPPCAT_1:18
.= [[Hom(cod((opp f)(*)(opp g)),dom(g9(*)f9)),
Hom(dom((opp f)(*)(opp g)),
cod(g9(*)f9))], hom((opp f)(*)(opp g),g9(*)f9)] by Def23
.= [[Hom(cod opp f,dom f9),Hom(dom opp g,cod g9)], hom(opp g,g9)*hom(
opp f,f9)] by A23,A26,A27,A24,Th55
.= (@(T.gg))*(@(T.ff)) by A17,A18,A20,A11,A14,A12,A23,A26,Def6
.= (T.gg)(*)(T.ff) by A19,A13,A23,A26,Th27;
end;
hence thesis by CAT_1:61;
end;
definition
let V,C,a;
assume
A1: Hom(C) c= V;
func hom?-(V,a) -> Functor of C,Ens(V) equals
:Def24:
hom?-(a);
coherence by A1,Th48;
func hom-?(V,a) -> Contravariant_Functor of C,Ens(V) equals
:Def25:
hom-?(a);
coherence by A1,Th49;
end;
definition
let V,C;
assume
A1: Hom(C) c= V;
func hom??(V,C) -> Functor of [:C opp,C:],Ens(V) equals
:Def26:
hom??(C);
coherence by A1,Th57;
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 Def24
.= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by Def20;
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);
then reconsider A = Hom(a,b) as Element of V by A1;
set d = @A;
(hom?-(V,a)).(id b) = (hom?-(a)).(id b) by A1,Def24
.= id d by A1,Lm9;
hence thesis by CAT_1:67;
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 Def25
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by Def21;
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);
then reconsider A = Hom(b,a) as Element of V by A1;
set d = @A;
(hom-?(V,a)).(id b) = (hom-?(a)).(id b) by A1,Def25
.= id d by A1,Lm10;
hence thesis by OPPCAT_1:30;
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??(C)).[f,g] by A1,Def26
.= [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] by Def23;
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);
then reconsider A = Hom(a,b) as Element of V by A1;
A2: id(a opp) = id a by OPPCAT_1:71;
set d = @A;
(hom??(V,C)).(id[a opp,b]) = (hom??(V,C)).[id(a opp),id b] by CAT_2:31
.= (hom??(C)).[id a,id b] by A1,Def26,A2
.= id d by A1,Lm11;
hence thesis by CAT_1:67;
end;
theorem
Hom(C) c= V implies hom??(V,C)?-(a opp) = hom?-(V,a)
proof
assume
A1: Hom(C) c= V;
A2: id(a opp) = id a by OPPCAT_1:71;
thus hom??(V,C)?-(a opp)
= (curry hom??(C)).(id a) by A1,Def26,A2
.= hom?-(a) by Th56
.= hom?-(V,a) by A1,Def24;
end;
theorem
Hom(C) c= V implies hom??(V,C)-?a = hom-?(V,a)
proof
assume
A1: Hom(C) c= V;
hence hom??(V,C)-?a = (curry' hom??(C)).(id a) by Def26
.= hom-?(a) by Th56
.= hom-?(V,a) by A1,Def25;
end;