Copyright (c) 1997 Association of Mizar Users
environ
vocabulary CAT_1, ENS_1, FUNCT_1, RELAT_1, MCART_1, NATTRA_1, BOOLE, OPPCAT_1,
CAT_2, FUNCT_2, YONEDA_1;
notation TARSKI, XBOOLE_0, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2,
CAT_1, CAT_2, OPPCAT_1, ENS_1, NATTRA_1;
constructors DOMAIN_1, ENS_1, NATTRA_1, PARTFUN1;
clusters FUNCT_1, RELSET_1, ENS_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems ZFMISC_1, MCART_1, FUNCT_1, FUNCT_2, CAT_1, CAT_2, OPPCAT_1, ENS_1,
NATTRA_1, ISOCAT_1, RELSET_1, RELAT_1;
schemes SUPINF_2;
begin
reserve y for set;
reserve A for Category, a,o for Object of A;
reserve f for Morphism of A;
definition let A;
func EnsHom(A) -> Category equals
:Def1: Ens(Hom(A));
correctness;
end;
theorem Th1:
for f,g being Function, m1,m2 being Morphism of EnsHom A st
cod m1 = dom m2 & [[dom m1,cod m1],f] = m1 & [[dom m2,cod m2],g] = m2
holds [[dom m1,cod m2],g*f] = m2*m1
proof
let f,g be Function;
let m1,m2 be Morphism of EnsHom A such that
A1: cod m1 = dom m2 & [[dom m1,cod m1],f] = m1 &
[[dom m2,cod m2],g] = m2;
A2: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,fComp Hom A,fId Hom A
#)
by ENS_1:def 14;
then reconsider m1'=m1 as Element of Maps Hom A;
reconsider m2'=m2 as Element of Maps Hom A by A2;
A3: [m2,m1] in dom(the Comp of EnsHom A) by A1,CAT_1:40;
A4: cod m1'= m1`1`2 by ENS_1:def 5
.=[dom m1,cod m1]`2 by A1,MCART_1:7
.=dom m2 by A1,MCART_1:7
.=[dom m2,cod m2]`1 by MCART_1:7
.=m2`1`1 by A1,MCART_1:7
.= dom m2' by ENS_1:def 4;
A5: dom m1'=dom m1 & cod m2'=cod m2
proof
A6: dom m1'= m1`1`1 by ENS_1:def 4
.=[dom m1,cod m1]`1 by A1,MCART_1:7
.=dom m1 by MCART_1:7;
cod m2 =[dom m2,cod m2]`2 by MCART_1:7
.=m2`1`2 by A1,MCART_1:7
.= cod m2' by ENS_1:def 5;
hence thesis by A6;
end;
A7: m2'`2= g & m1'`2=f
proof
A8: [[dom m2',cod m2'],m2'`2] =m2 by ENS_1:8;
[[dom m1',cod m1'],m1'`2] =m1 by ENS_1:8;
hence thesis by A1,A8,ZFMISC_1:33;
end;
m2*m1 = (fComp Hom A).[m2',m1'] by A2,A3,CAT_1:def 4
.= m2'*m1' by A4,ENS_1:def 12
.= [[dom m1,cod m2],g*f] by A4,A5,A7,ENS_1:def 7;
hence thesis;
end;
theorem Th2:
hom?-(a) is Functor of A,EnsHom(A)
proof
EnsHom(A) = Ens Hom A by Def1;
hence thesis by ENS_1:49;
end;
definition let A,a;
func <|a,?> -> Functor of A,EnsHom(A) equals
:Def2: hom?-(a);
coherence by Th2;
end;
theorem Th3:
for f being Morphism of A holds
<|cod f,?> is_naturally_transformable_to <|dom f,?>
proof
let f;
set F1=<|cod f,?> ,F2=<|dom f,?>;
A1: for a being Object of A holds
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] in Hom(F1.a,F2.a)
proof
let a be Object of A;
A2: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,
fComp Hom A,fId Hom A #) by ENS_1:def 14;
then reconsider m = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
as Morphism of EnsHom A by ENS_1:48;
reconsider m'=m as Element of Maps Hom A by ENS_1:48;
A3: EnsHom A = Ens Hom A by Def1;
A4: <|cod f,?> = hom?-(cod f) by Def2;
A5: dom(m)=(fDom Hom A).m by A2,CAT_1:def 2
.= dom m' by ENS_1:def 10
.= m`1`1 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`1 by MCART_1:7
.= Hom(cod f,a) by MCART_1:7
.= (Obj (hom?-(Hom A,cod f))).a by ENS_1:60
.= (hom?-(Hom A,cod f)).a by CAT_1:def 20
.=F1.a by A3,A4,ENS_1:def 26;
A6: <|dom f,?> = hom?-(dom f) by Def2;
cod(m)= (fCod Hom A).m by A2,CAT_1:def 3
.= cod m' by ENS_1:def 11
.= m`1`2 by ENS_1:def 5
.= [Hom(cod f,a),Hom(dom f,a)]`2 by MCART_1:7
.= Hom(dom f,a) by MCART_1:7
.= (Obj (hom?-(Hom A,dom f))).a by ENS_1:60
.= (hom?-(Hom A,dom f)).a by CAT_1:def 20
.= F2.a by A3,A6,ENS_1:def 26;
hence thesis by A5,CAT_1:18;
end;
then for a being Object of A holds Hom(F1.a,F2.a) <> {};
then A7: F1 is_transformable_to F2 by NATTRA_1:def 2;
set B = EnsHom(A);
deffunc F(Element of the Objects of A) =
[[Hom(cod f,$1),Hom(dom f,$1)],hom(f,$1)];
A8: for a being Element of the Objects of A holds F(a) in the Morphisms of B
proof
let a;
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] in Hom(F1.a,F2.a) by A1;
hence thesis;
end;
consider t being Function of the Objects of A, the Morphisms of B such that
A9: for o being Element of the Objects of A holds
t.o = F(o) from FunctR_ealEx(A8);
for a being Object of A holds t.a is Morphism of F1.a,F2.a
proof
let a;
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] in Hom(F1.a,F2.a) by A1;
then [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] is Morphism of F1.a,F2.a
by CAT_1:def 7;
hence thesis by A9;
end;
then reconsider t as transformation of F1,F2 by A7,NATTRA_1:def 3;
for a,b being Object of A st Hom(a,b) <> {}
for g being Morphism of a,b holds t.b*F1.g = F2.g*t.a
proof
let a,b be Object of A such that
A10: Hom(a,b) <> {};
let g be Morphism of a,b;
A11: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,
fComp Hom A,fId Hom A #) by ENS_1:def 14;
reconsider f1=t.b as Morphism of EnsHom A;
reconsider f2=F1.g as Morphism of EnsHom A;
A12: t.b= (t qua Function of the Objects of A, the Morphisms of B).b
by A7,NATTRA_1:def 5
.= [[Hom(cod f,b),Hom(dom f,b)],hom(f,b)] by A9;
then reconsider f1'=f1 as Element of Maps Hom A by ENS_1:48;
A13: dom f1 =Hom(cod f,b) & cod f1 =Hom(dom f,b)
proof
A14: dom(f1) =(fDom Hom A).f1 by A11,CAT_1:def 2
.= dom f1' by ENS_1:def 10
.= f1`1`1 by ENS_1:def 4
.=[Hom(cod f,b),Hom(dom f,b)]`1 by A12,MCART_1:7
.=Hom(cod f,b) by MCART_1:7;
cod(f1) = (fCod Hom A).f1 by A11,CAT_1:def 3
.= cod f1' by ENS_1:def 11
.= f1`1`2 by ENS_1:def 5
.= [Hom(cod f,b),Hom(dom f,b)]`2 by A12,MCART_1:7
.= Hom(dom f,b) by MCART_1:7;
hence thesis by A14;
end;
A15: f2 =(<|cod f,?> qua Function).g by A10,NATTRA_1:def 1
.= (hom?-(cod f)).g by Def2
.=[[Hom(cod f,dom g),Hom(cod f,cod g)],hom(cod f,g)]
by ENS_1:def 22;
then reconsider f2'=f2 as Element of Maps Hom A by ENS_1:47;
A16: dom f2=Hom(cod f,dom g) & cod f2=Hom(cod f,cod g)
proof
A17: dom(f2) = (fDom Hom A).f2 by A11,CAT_1:def 2
.= dom f2' by ENS_1:def 10
.= f2`1`1 by ENS_1:def 4
.= [Hom(cod f,dom g),Hom(cod f,cod g)]`1 by A15,MCART_1:7
.= Hom(cod f,dom g) by MCART_1:7;
cod(f2) = (fCod Hom A).f2 by A11,CAT_1:def 3
.= cod f2' by ENS_1:def 11
.= f2`1`2 by ENS_1:def 5
.= [Hom(cod f,dom g),Hom(cod f,cod g)]`2 by A15,MCART_1:7
.= Hom(cod f,cod g) by MCART_1:7;
hence thesis by A17;
end;
then A18: cod f2 = dom f1 by A10,A13,CAT_1:23;
reconsider f3 = F2.g as Morphism of EnsHom A;
reconsider f4 = t.a as Morphism of EnsHom A;
A19: f3=(<|dom f,?> qua Function).g by A10,NATTRA_1:def 1
.= (hom?-(dom f)).g by Def2
.=[[Hom(dom f,dom g),Hom(dom f,cod g)],hom(dom f,g)]
by ENS_1:def 22;
then reconsider f3'=f3 as Element of Maps Hom A by ENS_1:47;
A20: dom f3=Hom(dom f,dom g) & cod f3=Hom(dom f,cod g)
proof
A21: dom(f3) =(fDom Hom A).f3 by A11,CAT_1:def 2
.= dom f3' by ENS_1:def 10
.= f3`1`1 by ENS_1:def 4
.= [Hom(dom f,dom g),Hom(dom f,cod g)]`1 by A19,MCART_1:7
.= Hom(dom f,dom g) by MCART_1:7;
cod(f3) = (fCod Hom A).f3 by A11,CAT_1:def 3
.= cod f3' by ENS_1:def 11
.= f3`1`2 by ENS_1:def 5
.= [Hom(dom f,dom g),Hom(dom f,cod g)]`2 by A19,MCART_1:7
.= Hom(dom f,cod g) by MCART_1:7;
hence thesis by A21;
end;
A22: t.a = (t qua Function of the Objects of A, the Morphisms of B).a
by A7,NATTRA_1:def 5
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by A9;
then reconsider f4'=f4 as Element of Maps Hom A by ENS_1:48;
A23: dom f4 =Hom(cod f,a) & cod f4 =Hom(dom f,a)
proof
A24: dom(f4) = (fDom Hom A).f4 by A11,CAT_1:def 2
.= dom f4' by ENS_1:def 10
.= f4`1`1 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`1 by A22,MCART_1:7
.=Hom(cod f,a) by MCART_1:7;
cod(f4) = (fCod Hom A).f4 by A11,CAT_1:def 3
.= cod f4' by ENS_1:def 11
.= f4`1`2 by ENS_1:def 5
.= [Hom(cod f,a),Hom(dom f,a)]`2 by A22,MCART_1:7
.= Hom(dom f,a) by MCART_1:7;
hence thesis by A24;
end;
then A25: cod f4 = dom f3 by A10,A20,CAT_1:23;
A26: rng hom(cod f,g) c= dom hom(f,b)
proof
A27: cod g =b by A10,CAT_1:23;
per cases;
suppose Hom(dom f,b) = {};
then A28: Hom(cod f,b) = {} by ENS_1:42;
rng hom(cod f,g) c= Hom(cod f,cod g) by RELSET_1:12;
hence thesis by A27,A28,FUNCT_2:def 1;
suppose
A29: Hom(dom f,b) <> {};
let e be set;
assume
A30: e in rng hom(cod f,g);
A31: cod g = b by A10,CAT_1:23;
A32: rng hom(cod f,g) c= Hom(cod f,cod g) by RELSET_1:12;
Hom(cod f,cod g)=dom hom(f,b) by A29,A31,FUNCT_2:def 1;
hence thesis by A30,A32;
end;
A33: rng hom(f,a) c= dom hom(dom f,g)
proof
A34: dom g =a by A10,CAT_1:23;
per cases;
suppose
Hom(dom f,cod g) = {};
then A35: Hom(dom f,dom g) = {} by ENS_1:42;
rng hom(f,a) c= Hom(dom f,a) by RELSET_1:12;
hence thesis by A34,A35,FUNCT_2:def 1;
suppose
A36: Hom(dom f,cod g) <> {};
let e be set;
assume
A37: e in rng hom(f,a);
A38: rng hom(f,a) c= Hom(dom f,a) by RELSET_1:12;
Hom(dom f,a) = dom hom(dom f,g) by A34,A36,FUNCT_2:def 1;
hence thesis by A37,A38;
end;
A39: dom g =a & cod g =b by A10,CAT_1:23;
A40: dom (hom(f,b)*hom(cod f,g)) = dom(hom(dom f,g)*hom(f,a))
proof
per cases;
suppose
A41: Hom(cod f,dom g)= {};
dom (hom(f,b)*hom(cod f,g))=dom (hom(cod f,g)) by A26,RELAT_1:46
.=Hom(cod f,dom g) by A41,FUNCT_2:def 1
.=dom (hom(f,a)) by A39,A41,FUNCT_2:def 1
.=dom(hom(dom f,g)*hom(f,a)) by A33,RELAT_1:46;
hence thesis;
suppose
A42: Hom(cod f,dom g) <> {};
then A43: Hom(cod f,cod g) <> {} by ENS_1:42;
A44: Hom(dom f,a) <> {} by A39,A42,ENS_1:42;
dom (hom(f,b)*hom(cod f,g))=dom (hom(cod f,g)) by A26,RELAT_1:46
.=Hom(cod f,dom g) by A43,FUNCT_2:def 1
.=Hom(cod f,a) by A10,CAT_1:23
.=dom (hom(f,a)) by A44,FUNCT_2:def 1
.=dom(hom(dom f,g)*hom(f,a))
by A33,RELAT_1:46;
hence thesis;
end;
A45: for x being set st x in dom (hom(f,b)*hom(cod f,g))
holds (hom(f,b)*hom(cod f,g)).x = (hom(dom f,g)*hom(f,a)).x
proof
let x be set such that
A46: x in dom (hom(f,b)*hom(cod f,g));
per cases;
suppose
Hom(cod f,dom g) <> {};
then A47: Hom(cod f,cod g) <> {} by ENS_1:42;
x in dom hom(cod f,g) by A46,FUNCT_1:21;
then A48: x in Hom(cod f,dom g) by A47,FUNCT_2:def 1;
then reconsider x as Morphism of A;
A49: g*x in Hom(cod f,b)
proof
A50: dom(g) = cod(x) by A48,CAT_1:18;
then A51: dom(g*x) =dom x by CAT_1:42
.=cod f by A48,CAT_1:18;
cod(g*x)=cod(g) by A50,CAT_1:42
.=b by A10,CAT_1:23;
hence thesis by A51,CAT_1:18;
end;
A52: hom(f,a).x in Hom(dom f,dom g)
proof
A53: hom(f,a).x =x*f by A39,A48,ENS_1:def 21;
A54: dom(x) = cod(f) by A48,CAT_1:18;
then A55: dom(x*f) =dom f by CAT_1:42;
cod(x*f)=cod(x) by A54,CAT_1:42
.=dom g by A48,CAT_1:18;
hence thesis by A53,A55,CAT_1:18;
end;
then reconsider h=hom(f,a).x as Morphism of A;
A56: dom(g) = cod(x) by A48,CAT_1:18;
A57: dom(x) = cod(f) by A48,CAT_1:18;
(hom(f,b)*hom(cod f,g)).x = hom(f,b).(hom(cod f,g).x)
by A46,FUNCT_1:22
.=hom(f,b).(g*x) by A48,ENS_1:def 20
.=(g*x)*f by A49,ENS_1:def 21
.= g*(x*f) by A56,A57,CAT_1:43
.= g*(h) by A39,A48,ENS_1:def 21
.= hom(dom f,g).(hom(f,a).x)
by A52,ENS_1:def 20
.= (hom(dom f,g)*hom(f,a)).x
by A40,A46,FUNCT_1:22;
hence thesis;
suppose
A58: Hom(cod f,dom g) = {};
x in dom hom(cod f,g) by A46,FUNCT_1:21;
hence thesis by A58,FUNCT_2:def 1;
end;
A59: Hom(F1.b,F2.b)<>{} & Hom(F1.a,F1.b)<>{} by A1,A10,CAT_1:126;
A60: Hom(F2.a,F2.b)<>{} & Hom(F1.a,F2.a)<>{} by A1,A10,CAT_1:126;
t.b*F1.g = f1*f2 by A59,CAT_1:def 13
.= [[Hom(cod f,dom g),Hom(dom f,b)],hom(f,b)*hom(cod f,g)]
by A12,A13,A15,A16,A18,Th1
.= [[ Hom(cod f,a),Hom(dom f,cod g)],hom(dom f,g)*hom(f,a)]
by A39,A40,A45,FUNCT_1:9
.= f3*f4 by A19,A20,A22,A23,A25,Th1
.= F2.g*t.a by A60,CAT_1:def 13;
hence thesis;
end;
hence thesis by A7,NATTRA_1:def 7;
end;
definition let A,f;
func <|f,?> -> natural_transformation of <|cod f,?>, <|dom f,?> means
:Def3: for o be Object of A holds
it.o = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)];
existence
proof
set F1=<|cod f,?> ,
F2=<|dom f,?>;
A1: for o being Object of A holds
[[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] in Hom(F1.o,F2.o)
proof
let o be Object of A;
A2: hom(f,id o)=hom(f,o) by ENS_1:53;
A3: EnsHom A = Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,
fComp Hom A,fId Hom A #) by ENS_1:def 14;
then reconsider m = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)]
as Morphism of EnsHom A by A2,ENS_1:48;
reconsider m'=m as Element of Maps Hom A by A2,ENS_1:48;
A4: EnsHom A = Ens Hom A by Def1;
A5: <|cod f,?> = hom?-(cod f) by Def2;
A6: dom(m) = (fDom Hom A).m by A3,CAT_1:def 2
.= dom m' by ENS_1:def 10
.= m`1`1 by ENS_1:def 4
.= [Hom(cod f,o),Hom(dom f,o)]`1 by MCART_1:7
.= Hom(cod f,o) by MCART_1:7
.= (Obj (hom?-(Hom A,cod f))).o by ENS_1:60
.= (hom?-(Hom A,cod f)).o by CAT_1:def 20
.= F1.o by A4,A5,ENS_1:def 26;
A7: <|dom f,?> = hom?-(dom f) by Def2;
cod(m) = (fCod Hom A).m by A3,CAT_1:def 3
.= cod m' by ENS_1:def 11
.= m`1`2 by ENS_1:def 5
.= [Hom(cod f,o),Hom(dom f,o)]`2 by MCART_1:7
.= Hom(dom f,o) by MCART_1:7
.= (Obj (hom?-(Hom A,dom f))).o by ENS_1:60
.= (hom?-(Hom A,dom f)).o by CAT_1:def 20
.=F2.o by A4,A7,ENS_1:def 26;
hence thesis by A6,CAT_1:18;
end;
deffunc F(Element of the Objects of A) =
[[Hom(cod f,$1),Hom(dom f,$1)],hom(f,id $1)];
A8: for o being Element of the Objects of A holds
F(o) in the Morphisms of EnsHom(A)
proof
let o;
[[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] in Hom(F1.o,F2.o)
by A1;
hence thesis;
end;
consider t being Function of the Objects of A, the Morphisms of EnsHom(A)
such that
A9: for o being Element of the Objects of A holds t.o = F(o)
from FunctR_ealEx(A8);
A10: F1 is_naturally_transformable_to F2 by Th3;
for o being Object of A holds Hom(F1.o,F2.o) <> {} by A1;
then A11: F1 is_transformable_to F2 by NATTRA_1:def 2;
for o being Object of A holds t.o is Morphism of F1.o,F2.o
proof
let o;
[[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] in Hom(F1.o,F2.o)
by A1;
then [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)]
is Morphism of F1.o,F2.o by CAT_1:def 7;
hence thesis by A9;
end;
then reconsider t as transformation of F1,F2 by A11,NATTRA_1:def 3;
set B=EnsHom A;
for a,b being Object of A st Hom(a,b) <> {}
for g being Morphism of a,b holds t.b*F1.g = F2.g*t.a
proof
let a,b be Object of A such that
A12: Hom(a,b) <> {};
let g be Morphism of a,b;
A13: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,
fComp Hom A,fId Hom A #) by ENS_1:def 14;
reconsider f1=t.b as Morphism of EnsHom A;
reconsider f2=F1.g as Morphism of EnsHom A;
A14: t.b = (t qua Function of the Objects of A, the Morphisms of B).b
by A11,NATTRA_1:def 5
.= [[Hom(cod f,b),Hom(dom f,b)],hom(f,id b)] by A9
.=[[Hom(cod f,b),Hom(dom f,b)],hom(f,b)] by ENS_1:53;
then reconsider f1'=f1
as Element of Maps Hom A by ENS_1:48;
A15: dom f1 =Hom(cod f,b) & cod f1 =Hom(dom f,b)
proof
A16: dom(f1) = (fDom Hom A).f1 by A13,CAT_1:def 2
.= dom f1' by ENS_1:def 10
.= f1`1`1 by ENS_1:def 4
.= [Hom(cod f,b),Hom(dom f,b)]`1 by A14,MCART_1:7
.= Hom(cod f,b) by MCART_1:7;
cod(f1) = (fCod Hom A).f1 by A13,CAT_1:def 3
.= cod f1' by ENS_1:def 11
.= f1`1`2 by ENS_1:def 5
.= [Hom(cod f,b),Hom(dom f,b)]`2 by A14,MCART_1:7
.= Hom(dom f,b) by MCART_1:7;
hence thesis by A16;
end;
A17: f2 =(<|cod f,?> qua Function).g by A12,NATTRA_1:def 1
.= (hom?-(cod f)).g by Def2
.=[[Hom(cod f,dom g),Hom(cod f,cod g)],hom(cod f,g)]
by ENS_1:def 22;
then reconsider f2'=f2
as Element of Maps Hom A by ENS_1:47;
A18: dom f2=Hom(cod f,dom g) & cod f2=Hom(cod f,cod g)
proof
A19: dom(f2) =(fDom Hom A).f2 by A13,CAT_1:def 2
.= dom f2' by ENS_1:def 10
.= f2`1`1 by ENS_1:def 4
.=[Hom(cod f,dom g),Hom(cod f,cod g)]`1 by A17,MCART_1:7
.=Hom(cod f,dom g) by MCART_1:7;
cod(f2) = (fCod Hom A).f2 by A13,CAT_1:def 3
.= cod f2' by ENS_1:def 11
.= f2`1`2 by ENS_1:def 5
.= [Hom(cod f,dom g),Hom(cod f,cod g)]`2 by A17,MCART_1:7
.= Hom(cod f,cod g) by MCART_1:7;
hence thesis by A19;
end;
then A20: cod f2 = dom f1 by A12,A15,CAT_1:23;
reconsider f3=F2.g as Morphism of EnsHom A;
reconsider f4=t.a as Morphism of EnsHom A;
A21: f3 =(<|dom f,?> qua Function).g by A12,NATTRA_1:def 1
.= (hom?-(dom f)).g by Def2
.=[[Hom(dom f,dom g),Hom(dom f,cod g)],hom(dom f,g)]
by ENS_1:def 22;
then reconsider f3'=f3
as Element of Maps Hom A by ENS_1:47;
A22: dom f3=Hom(dom f,dom g) & cod f3=Hom(dom f,cod g)
proof
A23: dom(f3) =(fDom Hom A).f3 by A13,CAT_1:def 2
.= dom f3' by ENS_1:def 10
.= f3`1`1 by ENS_1:def 4
.=[Hom(dom f,dom g),Hom(dom f,cod g)]`1 by A21,MCART_1:7
.=Hom(dom f,dom g) by MCART_1:7;
cod(f3) = (fCod Hom A).f3 by A13,CAT_1:def 3
.= cod f3' by ENS_1:def 11
.= f3`1`2 by ENS_1:def 5
.= [Hom(dom f,dom g),Hom(dom f,cod g)]`2 by A21,MCART_1:7
.= Hom(dom f,cod g) by MCART_1:7;
hence thesis by A23;
end;
A24: t.a = (t qua Function of the Objects of A, the Morphisms of B).a
by A11,NATTRA_1:def 5
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,id a)] by A9
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by ENS_1:53;
then reconsider f4'=f4
as Element of Maps Hom A by ENS_1:48;
A25: dom f4 =Hom(cod f,a) & cod f4 =Hom(dom f,a)
proof
A26: dom(f4) =(fDom Hom A).f4 by A13,CAT_1:def 2
.= dom f4' by ENS_1:def 10
.= f4`1`1 by ENS_1:def 4
.=[Hom(cod f,a),Hom(dom f,a)]`1 by A24,MCART_1:7
.=Hom(cod f,a) by MCART_1:7;
cod(f4) = (fCod Hom A).f4 by A13,CAT_1:def 3
.= cod f4' by ENS_1:def 11
.= f4`1`2 by ENS_1:def 5
.= [Hom(cod f,a),Hom(dom f,a)]`2 by A24,MCART_1:7
.= Hom(dom f,a) by MCART_1:7;
hence thesis by A26;
end;
then A27: cod f4 = dom f3 by A12,A22,CAT_1:23;
A28: rng hom(cod f,g) c= dom hom(f,b)
proof
A29: cod g =b by A12,CAT_1:23;
per cases;
suppose
Hom(dom f,b) = {};
then A30: Hom(cod f,b) = {} by ENS_1:42;
rng hom(cod f,g) c= Hom(cod f,cod g) by RELSET_1:12;
hence thesis by A29,A30,FUNCT_2:def 1;
suppose
A31: Hom(dom f,b) <> {};
let e be set;
assume
A32: e in rng hom(cod f,g);
A33: cod g =b by A12,CAT_1:23;
A34: rng hom(cod f,g) c= Hom(cod f,cod g) by RELSET_1:12;
Hom(cod f,cod g)=dom hom(f,b) by A31,A33,FUNCT_2:def 1;
hence thesis by A32,A34;
end;
A35: rng hom(f,a) c= dom hom(dom f,g)
proof
A36: dom g =a by A12,CAT_1:23;
per cases;
suppose
Hom(dom f,cod g) = {};
then A37: Hom(dom f,dom g) = {} by ENS_1:42;
rng hom(f,a) c= Hom(dom f,a) by RELSET_1:12;
hence thesis by A36,A37,FUNCT_2:def 1;
suppose
A38: Hom(dom f,cod g) <> {};
let e be set;
assume
A39: e in rng hom(f,a);
A40: rng hom(f,a) c= Hom(dom f,a) by RELSET_1:12;
Hom(dom f,a)=dom hom(dom f,g) by A36,A38,FUNCT_2:def 1;
hence thesis by A39,A40;
end;
A41: dom g =a & cod g =b by A12,CAT_1:23;
A42: dom (hom(f,b)*hom(cod f,g)) = dom(hom(dom f,g)*hom(f,a))
proof
per cases;
suppose
A43: Hom(cod f,dom g)= {};
dom (hom(f,b)*hom(cod f,g)) = dom (hom(cod f,g)) by A28,RELAT_1
:46
.=Hom(cod f,a) by A41,A43,FUNCT_2:def 1
.=dom (hom(f,a)) by A41,A43,FUNCT_2:def 1
.=dom(hom(dom f,g)*hom(f,a)) by A35,RELAT_1:46;
hence thesis;
suppose
A44: Hom(cod f,dom g) <> {};
then A45: Hom(cod f,cod g) <> {} by ENS_1:42;
A46: Hom(dom f,a) <> {} by A41,A44,ENS_1:42;
dom (hom(f,b)*hom(cod f,g)) = dom (hom(cod f,g)) by A28,RELAT_1:
46
.=Hom(cod f,a) by A41,A45,FUNCT_2:def 1
.=dom (hom(f,a)) by A46,FUNCT_2:def 1
.=dom(hom(dom f,g)*hom(f,a))
by A35,RELAT_1:46;
hence thesis;
end;
A47: for x being set st x in dom (hom(f,b)*hom(cod f,g))
holds (hom(f,b)*hom(cod f,g)).x = (hom(dom f,g)*hom(f,a)).x
proof
let x be set such that
A48: x in dom (hom(f,b)*hom(cod f,g));
per cases;
suppose
Hom(cod f,dom g) <> {};
then A49: Hom(cod f,cod g) <> {} by ENS_1:42;
x in dom hom(cod f,g) by A48,FUNCT_1:21;
then A50: x in Hom(cod f,dom g) by A49,FUNCT_2:def 1;
then reconsider x as Morphism of A;
A51: g*x in Hom(cod f,b)
proof
A52: dom(g) = cod(x) by A50,CAT_1:18;
A53: cod g =b by A12,CAT_1:23;
A54: dom(g*x) =dom x by A52,CAT_1:42
.=cod f by A50,CAT_1:18;
cod(g*x)=b by A52,A53,CAT_1:42;
hence thesis by A54,CAT_1:18;
end;
A55: hom(f,a).x in Hom(dom f,dom g)
proof
A56: hom(f,a).x =x*f by A41,A50,ENS_1:def 21;
A57: dom(x) = cod(f) by A50,CAT_1:18;
then A58: dom(x*f) =dom f by CAT_1:42;
cod(x*f)=cod(x) by A57,CAT_1:42
.=dom g by A50,CAT_1:18;
hence thesis by A56,A58,CAT_1:18;
end;
then reconsider h=hom(f,a).x as Morphism of A;
A59: dom(g) = cod(x) by A50,CAT_1:18;
A60: dom(x) = cod(f) by A50,CAT_1:18;
(hom(f,b)*hom(cod f,g)).x = hom(f,b).(hom(cod f,g).x)
by A48,FUNCT_1:22
.=hom(f,b).(g*x) by A50,ENS_1:def 20
.=(g*x)*f by A51,ENS_1:def 21
.= g*(x*f) by A59,A60,CAT_1:43
.= g*(h) by A41,A50,ENS_1:def 21
.= hom(dom f,g).(hom(f,a).x)
by A55,ENS_1:def 20
.= (hom(dom f,g)*hom(f,a)).x
by A42,A48,FUNCT_1:22;
hence thesis;
suppose
A61: Hom(cod f,dom g) = {};
x in dom hom(cod f,g) by A48,FUNCT_1:21;
hence thesis by A61,FUNCT_2:def 1;
end;
A62: Hom(F1.b,F2.b)<>{} & Hom(F1.a,F1.b)<>{} by A1,A12,CAT_1:126;
A63: Hom(F2.a,F2.b)<>{} & Hom(F1.a,F2.a)<>{} by A1,A12,CAT_1:126;
t.b*F1.g = f1*f2 by A62,CAT_1:def 13
.=[[Hom(cod f,dom g),Hom(dom f,b)],hom(f,b)*hom(cod f,g)]
by A14,A15,A17,A18,A20,Th1
.=[[ Hom(cod f,a),Hom(dom f,cod g)],hom(dom f,g)*hom(f,a)]
by A41,A42,A47,FUNCT_1:9
.=f3*f4 by A21,A22,A24,A25,A27,Th1
.= F2.g*t.a by A63,CAT_1:def 13;
hence thesis;
end;
then reconsider t as natural_transformation of F1,F2 by A10,NATTRA_1:def 8;
for o be Element of the Objects of A
holds t.o= [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)]
proof
let o;
t.o =(t qua Function).o by A11,NATTRA_1:def 5
.= [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] by A9;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let h1,h2 be natural_transformation of <|cod f,?>, <|dom f,?>
such that
A64: for o be Object of A holds
h1.o = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] and
A65: for o be Object of A
holds h2.o =[[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)];
for a being Object of A holds
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] in Hom(<|cod f,?>.a,<|dom f,?>.a)
proof
let a be Object of A;
A66: EnsHom A = Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,
fComp Hom A,fId Hom A #) by ENS_1:def 14;
then reconsider m = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
as Morphism of EnsHom A by ENS_1:48;
reconsider m'=m as Element of Maps Hom A by ENS_1:48;
A67: EnsHom A = Ens Hom A by Def1;
A68: <|cod f,?> = hom?-(cod f) by Def2;
A69: dom(m) =(fDom Hom A).m by A66,CAT_1:def 2
.= dom m' by ENS_1:def 10
.= m`1`1 by ENS_1:def 4
.=[Hom(cod f,a),Hom(dom f,a)]`1 by MCART_1:7
.=Hom(cod f,a) by MCART_1:7
.= (Obj (hom?-(Hom A,cod f))).a by ENS_1:60
.= (hom?-(Hom A,cod f)).a by CAT_1:def 20
.=<|cod f,?>.a by A67,A68,ENS_1:def 26;
A70: <|dom f,?> = hom?-(dom f) by Def2;
cod(m) = (fCod Hom A).m by A66,CAT_1:def 3
.= cod m' by ENS_1:def 11
.= m`1`2 by ENS_1:def 5
.= [Hom(cod f,a),Hom(dom f,a)]`2 by MCART_1:7
.= Hom(dom f,a) by MCART_1:7
.= (Obj (hom?-(Hom A,dom f))).a by ENS_1:60
.= (hom?-(Hom A,dom f)).a by CAT_1:def 20
.=<|dom f,?>.a by A67,A70,ENS_1:def 26;
hence thesis by A69,CAT_1:18;
end;
then for a being Object of A holds Hom(<|cod f,?>.a,<|dom f,?>.a) <> {};
then A71: <|cod f,?> is_transformable_to <|dom f,?> by NATTRA_1:def 2;
now
let o;
thus h1.o =[[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] by A64
.= h2.o by A65;
end;
hence thesis by A71,NATTRA_1:20;
end;
end;
theorem Th4: for f being Element of the Morphisms of A holds
[[<|cod f,?>,<|dom f,?>],<|f,?>] is Element of the Morphisms of
Functors(A,EnsHom(A))
proof
let f be Element of the Morphisms of A;
<|cod f,?> is_naturally_transformable_to <|dom f,?> by Th3;
then [[<|cod f,?>,<|dom f,?>],<|f,?>] in NatTrans(A,EnsHom(A))
by NATTRA_1:def 16;
hence thesis by NATTRA_1:def 18;
end;
definition let A;
func Yoneda(A) -> Contravariant_Functor of A,Functors(A,EnsHom(A)) means
:Def4: for f being Morphism of A holds
it.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];
existence
proof
deffunc F(Element of the Morphisms of A)
= [[<|cod $1,?>,<|dom $1,?>],<|$1,?>];
A1: for f being Element of the Morphisms of A holds
F(f) in the Morphisms of Functors(A,EnsHom(A))
proof
let f;
[[<|cod f,?>,<|dom f,?>],<|f,?>] is
Morphism of Functors(A,EnsHom(A)) by Th4;
hence thesis;
end;
consider F being
Function of the Morphisms of A, the Morphisms of Functors(A,EnsHom(A))
such that
A2: for f being Element of the Morphisms of A holds
F.f = F(f) from FunctR_ealEx(A1);
A3: for c being Object of A ex d being Object of Functors(A,EnsHom(A))
st F.(id c)= id d
proof
let c be Object of A;
<|c,?> in Funct(A,EnsHom(A)) by CAT_2:def 2;
then reconsider d=<|c,?> as Object of Functors(A,EnsHom(A)) by
NATTRA_1:def 18;
take d;
set X= dom <|id c,?>;
A4: dom <|id c,?> = the Objects of A by FUNCT_2:def 1
.= dom id <|c,?> by FUNCT_2:def 1;
for y st y in X holds
(<|id c,?>).y =(id <|c,?>).y
proof
let y; assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A5: <|c,?> =hom?-(c) by Def2;
<|cod id c,?> is_transformable_to <|c,?> by CAT_1:44;
then A6: <|cod id c,?> is_transformable_to <|dom id c,?> by CAT_1:
44;
A7: Hom(z,z) <> {} by CAT_1:56;
reconsider zz= id z as Morphism of z,z;
(<|id c,?>).z
= [[Hom(cod id c,z),Hom(dom id c,z)],hom(id c,id z)]
by Def3
.= [[Hom(c,z),Hom(dom id c,z)],hom(id c,id z)]
by CAT_1:44
.= [[Hom(c,z),Hom(c,z)],hom(id c,id z)] by CAT_1:44
.= [[Hom(c,z),Hom(c,z)],hom(c,id z)] by ENS_1:53
.= [[Hom(c,z),Hom(c,cod id z)],hom(c,id z)]
by CAT_1:44
.= [[Hom(c,dom id z),Hom(c,cod id z)],hom(c,id z)]
by CAT_1:44
.=(<|c,?> qua Function ).id z by A5,ENS_1:def 22
.=(<|c,?>).zz by A7,NATTRA_1:def 1
.= id (<|c,?>.z) by NATTRA_1:15
.=(id <|c,?> ).z by NATTRA_1:21
.=(id <|c,?> qua Function).z by NATTRA_1:def 5;
hence thesis by A6,NATTRA_1:def 5;
end;
then A8: <|id c,?>= id <|c,?> by A4,FUNCT_1:9;
F.(id c) = [[<|cod id c,?>,<|dom id c,?>],<|id c,?>] by A2
.=[[<|c,?>,<|dom id c,?>],<|id c,?>] by CAT_1:44
.= [[<|c,?>,<|c,?>],id <|c,?>] by A8,CAT_1:44
.=id d by NATTRA_1:def 18;
hence thesis;
end;
A9: for f being Morphism of A
holds F.(id dom f) = id cod (F.f) & F.(id cod f) = id dom (F.f)
proof
let f;
set g =F.f;
A10: g = [[<|cod f,?>,<|dom f,?>],<|f,?>] by A2;
then A11: cod g =<|dom f,?> by NATTRA_1:39;
A12: dom g =<|cod f,?> by A10,NATTRA_1:39;
A13: F.(id dom f)
=[[<|cod (id dom f),?>,<|dom (id dom f),?>],<|(id dom f),?>]
by A2
.=[[<|dom f,?>,<| dom (id dom f),?>],<|(id dom f),?>]
by CAT_1:44
.=[[<|dom f,?>,<|dom f,?>],<|id dom f,?>] by CAT_1:44;
A14: [[<|dom f,?>,<|dom f,?>],id <|dom f,?>]
= id cod (F.f) by A11,NATTRA_1:def 18;
set X= dom <|id dom f,?>;
A15: dom <|id dom f,?> = the Objects of A by FUNCT_2:def 1
.= dom id <|dom f,?> by FUNCT_2:def 1;
A16: for y st y in X holds
(<|id dom f,?>).y =(id <|dom f,?>).y
proof
let y; assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A17: <|dom f,?> =hom?-(dom f) by Def2;
<|cod id dom f,?> is_transformable_to <|dom f,?>
by CAT_1:44;
then A18: <|cod id dom f,?> is_transformable_to <|dom id dom f,?>
by CAT_1:44;
A19: Hom(z,z) <> {} by CAT_1:56;
reconsider zz= id z as Morphism of z,z;
(<|id dom f,?>).z
= [[Hom(cod id dom f,z),Hom(dom id dom f,z)]
,hom(id dom f,id z)] by Def3
.= [[Hom(dom f,z),Hom(dom id dom f,z)],
hom(id dom f,id z)] by CAT_1:44
.= [[Hom(dom f,z),Hom(dom f,z)],
hom(id dom f,id z)] by CAT_1:44
.= [[Hom(dom f,z),Hom(dom f,z)],
hom(dom f,id z)] by ENS_1:53
.= [[Hom(dom f,z),Hom(dom f,cod id z)],
hom(dom f,id z)] by CAT_1:44
.= [[Hom(dom f,dom id z),Hom(dom f,cod id z)],
hom(dom f,id z)] by CAT_1:44
.= (<|dom f,?> qua Function ).id z by A17,ENS_1:
def 22
.= (<|dom f,?>).zz by A19,NATTRA_1:def 1
.= id (<|dom f,?>.z) by NATTRA_1:15
.= (id <|dom f,?> ).z by NATTRA_1:21
.= (id <|dom f,?> qua Function).z
by NATTRA_1:def 5;
hence thesis by A18,NATTRA_1:def 5;
end;
A20: F.(id cod f) = [[<|cod (id cod f),?>,<|dom (id cod f),?>],
<|(id cod f),?>] by A2
.= [[<|cod f,?>,<| dom (id cod f),?>],<|(id cod f),?>]
by CAT_1:44
.= [[<|cod f,?>,<|cod f,?>],<|id cod f,?>] by CAT_1:44;
set X= dom <|id cod f,?>;
A21: dom <|id cod f,?> = the Objects of A by FUNCT_2:def 1
.= dom id <|cod f,?> by FUNCT_2:def 1;
for y st y in X holds
(<|id cod f,?>).y =(id <|cod f,?>).y
proof
let y; assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A22: <|cod f,?> =hom?-(cod f) by Def2;
<|cod id cod f,?> is_transformable_to <|cod f,?>
by CAT_1:44;
then A23: <|cod id cod f,?> is_transformable_to <|dom id cod f,?>
by CAT_1:44;
A24: Hom(z,z) <> {} by CAT_1:56;
(<|id cod f,?>).z
= [[Hom(cod id cod f,z),Hom(dom id cod f,z)],
hom(id cod f,id z)] by Def3
.= [[Hom(cod f,z),Hom(dom id cod f,z)],
hom(id cod f,id z)] by CAT_1:44
.= [[Hom(cod f,z),Hom(cod f,z)],
hom(id cod f,id z)] by CAT_1:44
.= [[Hom(cod f,z),Hom(cod f,z)],
hom(cod f,id z)] by ENS_1:53
.= [[Hom(cod f,z),Hom(cod f,cod id z)],
hom(cod f,id z)] by CAT_1:44
.= [[Hom(cod f,dom id z),Hom(cod f,cod id z)],
hom(cod f,id z)] by CAT_1:44
.= (<|cod f,?> qua Function).id z by A22,ENS_1:
def 22
.= (<|cod f,?>).id z by A24,NATTRA_1:def 1
.= id (<|cod f,?>.z) by NATTRA_1:15
.= (id <|cod f,?>).z by NATTRA_1:21
.= (id <|cod f,?> qua Function).z
by NATTRA_1:def 5;
hence thesis by A23,NATTRA_1:def 5;
end;
then <|id cod f,?> =id <|cod f,?> by A21,FUNCT_1:9;
hence thesis by A12,A13,A14,A15,A16,A20,FUNCT_1:9,NATTRA_1:def 18;
end;
for f,g being Morphism of A st dom g = cod f holds
F.(g*f) = (F.f)*(F.g)
proof
let f,g be Morphism of A; assume
A25: dom g = cod f;
then reconsider t=<|f,?> as natural_transformation of
<|dom g,?>,<|dom f,?>;
reconsider t1=<|g,?> as natural_transformation of
<|cod g,?>,<|dom g,?>;
A26: F.f =[[<|dom g,?>,<|dom f,?>],t] by A2,A25;
A27: F.g =[[<|cod g,?>,<|dom g,?>],t1] by A2;
then A28: [F.f,F.g] in dom (the Comp of Functors(A,EnsHom(A)))
by A26,NATTRA_1:41;
then consider F',F1',F2' being Functor of A,EnsHom(A),
t' being natural_transformation of F',F1',
t1' being natural_transformation of F1',F2' such that
A29: F.g=[[F',F1'],t'] & F.f = [[F1',F2'],t1'] and
A30: (the Comp of Functors(A,EnsHom(A))).[F.f,F.g]
= [[F',F2'],t1'`*`t'] by NATTRA_1:def 18;
A31: [F',F1'] = [<|cod g,?>,<|dom g,?>] &
[F1',F2'] = [<|dom g,?>,<|dom f,?>] &
<|g,?> = t' & <|f,?> = t1' by A26,A27,A29,ZFMISC_1:33;
then <|cod g,?> = F' & <|dom g,?> = F1' & <|dom f,?> = F2'
by ZFMISC_1:33;
then A32: F.f*F.g = [[<|cod g,?>,<|dom f,?>],t`*`t1] by A28,A30,A31,
CAT_1:def 4;
A33: dom(g*f) = dom f & cod(g*f) = cod g by A25,CAT_1:42;
then reconsider tt=t`*`t1
as natural_transformation of <|cod(g*f),?>,<|dom(g*f),?>;
A34: <|cod(g*f),?> is_naturally_transformable_to
<|dom(g*f),?> by Th3;
for o being Object of A holds (<|g*f,?>).o =tt.o
proof
let o be Object of A;
reconsider f1=t.o as Morphism of EnsHom(A);
reconsider f2=t1.o as Morphism of EnsHom(A);
A35: t.o = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)]
by A25,Def3;
A36: f2 = [[Hom(cod g,o),Hom(dom g,o)],hom(g,id o)] by Def3;
A37: <|dom g,?> is_naturally_transformable_to
<|dom f,?> by A25,Th3;
A38: EnsHom A = Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,
fComp Hom A,fId Hom A #)
by ENS_1:def 14;
then reconsider f1'=f1 as Element of Maps Hom A;
reconsider f2'=f2 as Element of Maps Hom A by A38;
A39: cod f2 = dom f1
proof
A40: dom(f1) =(fDom Hom A).f1 by A38,CAT_1:def 2
.= dom f1' by ENS_1:def 10
.= f1`1`1 by ENS_1:def 4
.=[Hom(cod f,o),Hom(dom f,o)]`1 by A35,MCART_1:7
.=Hom(cod f,o) by MCART_1:7;
cod(f2) = (fCod Hom A).f2 by A38,CAT_1:def 3
.= cod f2' by ENS_1:def 11
.= f2`1`2 by ENS_1:def 5
.= [Hom(cod g,o),Hom(dom g,o)]`2 by A36,MCART_1:7
.= Hom(dom g,o) by MCART_1:7;
hence thesis by A25,A40;
end;
A41: dom f2 =Hom(cod g,o) & cod f2 =Hom(dom g,o)
proof
A42: dom(f2) = (fDom Hom A).f2 by A38,CAT_1:def 2
.= dom f2' by ENS_1:def 10
.= f2`1`1 by ENS_1:def 4
.= [Hom(cod g,o),Hom(dom g,o)]`1 by A36,MCART_1:7
.= Hom(cod g,o) by MCART_1:7;
cod(f2) = (fCod Hom A).f2 by A38,CAT_1:def 3
.= cod f2' by ENS_1:def 11
.= f2`1`2 by ENS_1:def 5
.= [Hom(cod g,o),Hom(dom g,o)]`2 by A36,MCART_1:7
.= Hom(dom g,o) by MCART_1:7;
hence thesis by A42;
end;
A43: cod f1 = Hom(dom f,o) & dom f1 =Hom(cod f,o)
proof
A44: cod(f1) = (fCod Hom A).f1 by A38,CAT_1:def 3
.= cod f1' by ENS_1:def 11
.= f1`1`2 by ENS_1:def 5
.= [Hom(cod f,o),Hom(dom f,o)]`2 by A35,MCART_1:7
.= Hom(dom f,o) by MCART_1:7;
dom(f1) = (fDom Hom A).f1 by A38,CAT_1:def 2
.= dom f1' by ENS_1:def 10
.= f1`1`1 by ENS_1:def 4
.= [Hom(cod f,o),Hom(dom f,o)]`1 by A35,MCART_1:7
.= Hom(cod f,o) by MCART_1:7;
hence thesis by A44;
end;
A45: <|cod g,?> is_naturally_transformable_to <|dom g,?> by Th3
;
set F1=<|cod f,?> ,
F2=<|dom f,?>;
A46: for a being Object of A holds
[[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] in Hom(F1.a,F2.a)
proof
let a be Object of A;
A47: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,
fCod Hom A,fComp Hom A,fId Hom A #)
by ENS_1:def 14;
then reconsider m = [[Hom(cod f,a),Hom(dom f,a)],hom(f,
a)]
as Morphism of EnsHom A by ENS_1:48;
reconsider m'=m as Element of Maps Hom A by ENS_1:48;
A48: EnsHom A = Ens Hom A by Def1;
A49: <|cod f,?> = hom?-(cod f) by Def2;
A50: dom(m) = (fDom Hom A).m by A47,CAT_1:def 2
.= dom m' by ENS_1:def 10
.= m`1`1 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`1 by MCART_1:7
.= Hom(cod f,a) by MCART_1:7
.= (Obj (hom?-(Hom A,cod f))).a by ENS_1:60
.= (hom?-(Hom A,cod f)).a by CAT_1:def 20
.=F1.a by A48,A49,ENS_1:def 26;
A51: <|dom f,?> = hom?-(dom f) by Def2;
cod(m) = (fCod Hom A).m by A47,CAT_1:def 3
.= cod m' by ENS_1:def 11
.= m`1`2 by ENS_1:def 5
.= [Hom(cod f,a),Hom(dom f,a)]`2 by MCART_1:7
.= Hom(dom f,a) by MCART_1:7
.= (Obj (hom?-(Hom A,dom f))).a by ENS_1:60
.= (hom?-(Hom A,dom f)).a by CAT_1:def 20
.= F2.a by A48,A51,ENS_1:def 26;
hence thesis by A50,CAT_1:18;
end;
for a being Object of A holds
[[Hom(cod g,a),Hom(dom g,a)],hom(g,a)] in
Hom(<|cod g,?>.a,<|dom g,?>.a)
proof
let a be Object of A;
A52: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,
fCod Hom A,fComp Hom A,fId Hom A #)
by ENS_1:def 14;
then reconsider m =
[[Hom(cod g,a),Hom(dom g,a)],hom(g,a)]
as Morphism of EnsHom A by ENS_1:48;
reconsider m'=m as Element of Maps Hom A
by ENS_1:48;
A53: EnsHom A = Ens Hom A by Def1;
A54: <|cod g,?> = hom?-(cod g) by Def2;
A55: dom(m) = (fDom Hom A).m by A52,CAT_1:def 2
.= dom m' by ENS_1:def 10
.= m`1`1 by ENS_1:def 4
.= [Hom(cod g,a),Hom(dom g,a)]`1
by MCART_1:7
.= Hom(cod g,a) by MCART_1:7
.= (Obj (hom?-(Hom A,cod g))).a by ENS_1:60
.= (hom?-(Hom A,cod g)).a by CAT_1:def 20
.=<|cod g,?>.a by A53,A54,ENS_1:def 26;
A56: <|dom g,?> = hom?-(dom g) by Def2;
cod(m) = (fCod Hom A).m by A52,CAT_1:def 3
.= cod m' by ENS_1:def 11
.= m`1`2 by ENS_1:def 5
.= [Hom(cod g,a),Hom(dom g,a)]`2
by MCART_1:7
.= Hom(dom g,a) by MCART_1:7
.= (Obj (hom?-(Hom A,dom g))).a by ENS_1:60
.= (hom?-(Hom A,dom g)).a by CAT_1:def 20
.= <|dom g,?>.a by A53,A56,ENS_1:def 26;
hence thesis by A55,CAT_1:18;
end;
then A57: Hom(F1.o,F2.o)<> {}
& Hom(<|cod g,?>.o,<|dom g,?>.o)<> {}
by A46;
A58: (tt).o = (t.o)*(t1.o) by A33,A37,A45,NATTRA_1:27
.= f1 * f2 by A25,A57,CAT_1:def 13
.= [[Hom(cod g,o),Hom(dom f,o)],
hom(f,id o)*hom(g,id o)] by A35,A36,A39,A41,A43,
Th1
.= [[Hom(cod g,o),Hom(dom f,o)],hom(f,o)*hom(g,id o)]
by ENS_1:53
.= [[Hom(cod g,o),Hom(dom f,o)],hom(f,o)*hom(g,o)]
by ENS_1:53
.= [[Hom(cod g,o),Hom(dom f,o)],hom(g*f,o)]
by A25,ENS_1:46;
(<|g*f,?>).o = [[Hom(cod(g),o),Hom(dom(g*f),o)],
hom(g*f,id o)] by A33,Def3
.= [[Hom(cod g,o),Hom(dom f,o)],hom(g*f,o)]
by A33,ENS_1:53;
hence thesis by A58;
end;
then (<|g*f,?> )=tt by A34,ISOCAT_1:31;
hence thesis by A2,A32,A33;
end;
then reconsider F as Contravariant_Functor of A,Functors(A,EnsHom(A))
by A3,A9,OPPCAT_1:def 7;
for f being Element of the Morphisms of A holds
F.f = [[<|cod f,?>,<|dom f,?>],<|f,?>] by A2;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Contravariant_Functor of A,Functors(A,EnsHom(A))
such that
A59: for f holds h1.f = [[<|cod f,?>,<|dom f,?>],<|f,?>] and
A60: for f holds h2.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];
now
let f;
thus h1.f = [[<|cod f,?>,<|dom f,?>],<|f,?>] by A59
.= h2.f by A60;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let A,B be Category;
let F be Contravariant_Functor of A,B;
let c be Object of A;
func F.c -> Object of B equals
:Def5: (Obj F).c;
correctness;
end;
theorem
for F being Functor of A,Functors(A,EnsHom(A)) st
Obj F is one-to-one & F is faithful holds F is one-to-one
proof
let F be Functor of A,Functors(A,EnsHom(A));
assume
A1: Obj F is one-to-one;
assume
A2: F is faithful;
for x1,x2 be set st x1 in dom F & x2 in dom F & F.x1 = F.x2 holds x1 =
x2
proof
let x1,x2 be set;
assume
A3: x1 in dom F & x2 in dom F & F.x1 = F.x2;
then reconsider m1=x1,m2=x2 as Morphism of A by FUNCT_2:def 1;
A4: m1 is Morphism of dom m1,cod m1 by CAT_1:22;
set o1=dom m1,o2=cod m1;
A5: m2 is Morphism of dom m2,cod m2 by CAT_1:22;
set o3=dom m2,o4=cod m2;
reconsider m1'=m1 as Morphism of o1,o2 by CAT_1:22;
reconsider m2'=m2 as Morphism of o3,o4 by CAT_1:22;
A6: Hom(o1,o2) <> {} by CAT_1:19;
A7: Hom(o3,o4) <> {} by CAT_1:19;
then A8: Hom(F.o3,F.o4) <> {} by CAT_1:126;
A9: F.m1'= F.m2 by A3,A6,NATTRA_1:def 1
.= F.m2' by A7,NATTRA_1:def 1;
A10: Hom(F.o1,F.o2) <> {} by A6,CAT_1:126;
A11: (Obj F).o3 = F.o3 by CAT_1:def 20;
(Obj F).o1 = F.o1 by CAT_1:def 20
.=dom (F.m2') by A9,A10,CAT_1:23
.= (Obj F).o3 by A8,A11,CAT_1:23;
then A12: o1=o3 by A1,FUNCT_2:25;
A13: (Obj F).o4=(F).o4 by CAT_1:def 20;
(Obj F).o2 = F.o2 by CAT_1:def 20
.=cod(F.m2') by A9,A10,CAT_1:23
.=(Obj F).o4 by A8,A13,CAT_1:23;
then m2 is Morphism of o1,o2 by A1,A5,A12,FUNCT_2:25;
hence thesis by A2,A3,A4,A6,CAT_1:def 24;
end;
hence thesis by FUNCT_1:def 8;
end;
definition let C,D be Category;
let T be Contravariant_Functor of C,D;
attr T is faithful means :Def6:
for c,c' being Object of C st Hom(c,c') <> {}
for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2;
end;
theorem Th6:
for F being Contravariant_Functor of A,Functors(A,EnsHom(A)) st
Obj F is one-to-one & F is faithful holds F is one-to-one
proof
let F be Contravariant_Functor of A,Functors(A,EnsHom(A));
assume
A1: Obj F is one-to-one;
assume
A2: F is faithful;
for x1,x2 be set st x1 in dom F & x2 in
dom F & F.x1 = F.x2 holds x1 = x2
proof
let x1,x2 be set;
assume
A3: x1 in dom F & x2 in dom F & F.x1 = F.x2;
then reconsider m1=x1,m2=x2 as Morphism of A by FUNCT_2:def 1;
A4: m1 is Morphism of dom m1,cod m1 by CAT_1:22;
set o1=dom m1,o2=cod m1;
A5: m2 is Morphism of dom m2,cod m2 by CAT_1:22;
set o3=dom m2,o4=cod m2;
reconsider m2'=m2 as Morphism of o3,o4 by CAT_1:22;
A6: Hom(o1,o2) <> {} by CAT_1:19;
(Obj F).o1 = cod (F.m2') by A3,OPPCAT_1:33
.= (Obj F).o3 by OPPCAT_1:33;
then A7: o1=o3 by A1,FUNCT_2:25;
(Obj F).o2 =dom(F.m2') by A3,OPPCAT_1:33
.=(Obj F).o4 by OPPCAT_1:33;
then m2 is Morphism of o1,o2 by A1,A5,A7,FUNCT_2:25;
hence thesis by A2,A3,A4,A6,Def6;
end;
hence thesis by FUNCT_1:def 8;
end;
theorem Th7:
Yoneda A is faithful
proof
set F = Yoneda A;
for o1,o2 being Object of A st Hom(o1,o2) <> {}
for x1,x2 being Morphism of o1,o2 holds F.x1 = F.x2 implies x1 = x2
proof
let o1,o2 be Object of A;
assume
A1: Hom(o1,o2) <> {};
let x1,x2 be Morphism of o1,o2;
assume
A2: F.x1 = F.x2;
A3: x1 in Hom(o1,o2) by A1,CAT_1:def 7;
A4: x2 in Hom(o1,o2) by A1,CAT_1:def 7;
reconsider dd=(id o2 ) as Morphism of A;
id o2 in Hom(o2,o2) by CAT_1:55;
then id o2 in Hom(cod x1,o2) by A3,CAT_1:18;
then A5: id o2 in Hom(cod x1,dom id o2) by CAT_1:44;
id o2 in Hom(o2,o2) by CAT_1:55;
then id o2 in Hom(cod x2,o2) by A4,CAT_1:18;
then A6: id o2 in Hom(cod x2,dom id o2) by CAT_1:44;
A7: Hom(o2,o2) <> {} by CAT_1:56;
then A8: (id o2)*dd =(id o2)*(id o2) by CAT_1:def 13;
then A9: hom(x1,id o2).dd =(id o2)*(id o2)*(x1 qua Morphism of A) by A5,
ENS_1:def 24
.=(id o2)*(x1 qua Morphism of A) by CAT_1:59
.=(id o2)*x1 by A1,A7,CAT_1:def 13
.=x1 by A1,CAT_1:57;
A10: hom(x2,id o2).dd =(id o2)*(id o2)*(x2 qua Morphism of A) by A6,A8,
ENS_1:def 24
.=(id o2)*(x2 qua Morphism of A) by CAT_1:59
.=(id o2)*x2 by A1,A7,CAT_1:def 13
.=x2 by A1,CAT_1:57;
A11: cod x1 = o2 by A3,CAT_1:18 .= cod x2 by A4,CAT_1:18;
A12: dom x1 = o1 by A3,CAT_1:18 .= dom x2 by A4,CAT_1:18;
[[<|cod x1,?>,<|dom x1,?>],<|x1,?>]=F.x2 by A2,Def4;
then [[<|cod x1,?>,<|dom x1,?>],<|x1,?>]=
[[<|cod x2,?>,<|dom x2,?>],<|x2,?>] by Def4;
then [<|cod x1,?>,<|dom x1,?>,<|x1,?>]=
[[<|cod x2,?>,<|dom x2,?>],<|x2,?>] by MCART_1:def 3;
then [<|cod x1,?>,<|dom x1,?>,<|x1,?>] =
[<|cod x2,?>,<|dom x2,?>,<|x2,?>] by MCART_1:def 3;
then <|x1,?>= <|x2,?> by MCART_1:28;
then [[Hom(cod x1,o2),Hom(dom x1,o2)],hom(x1,id o2)]=
<|x2,?>.o2 by A11,A12,Def3
;
then [[Hom(cod x1,o2),Hom(dom x1,o2)],hom(x1,id o2)]=
[[Hom(cod x2,o2),Hom(dom x2,o2)],hom(x2,id o2)] by Def3;
then [[Hom(o2,o2),Hom(dom x1,o2)],hom(x1,id o2)]=
[[Hom(cod x2,o2),Hom(dom x2,o2)],hom(x2,id o2)]
by A3,CAT_1:18;
then [[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]=
[[Hom(cod x2,o2),Hom(dom x2,o2)],hom(x2,id o2)]
by A3,CAT_1:18;
then [[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]=
[[Hom(o2,o2),Hom(dom x2,o2)],hom(x2,id o2)]
by A4,CAT_1:18;
then [[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]=
[[Hom(o2,o2),Hom(o1,o2)],hom(x2,id o2)] by A4,CAT_1:18;
then [[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]=
[Hom(o2,o2),Hom(o1,o2),hom(x2,id o2)] by MCART_1:def 3;
then [Hom(o2,o2),Hom(o1,o2),hom(x1,id o2)]=
[Hom(o2,o2),Hom(o1,o2),hom(x2,id o2)] by MCART_1:def 3;
hence thesis by A9,A10,MCART_1:28;
end;
hence thesis by Def6;
end;
theorem
Yoneda A is one-to-one
proof
set F = Yoneda A;
A1: Obj F is one-to-one
proof
for x1,x2 be set st x1 in dom (Obj F) & x2 in dom (Obj F)
& (Obj F).x1 = (Obj F).x2 holds x1 = x2
proof
let x1,x2 be set;
assume
A2: x1 in dom (Obj F) & x2 in dom (Obj F) & (Obj F).x1 = (Obj F).x2;
then reconsider c =x1,c1=x2 as Object of A by FUNCT_2:def 1;
<|c,?> in Funct(A,EnsHom(A)) by CAT_2:def 2;
then reconsider d=<|c,?> as Object of Functors(A,EnsHom(A)) by
NATTRA_1:def 18;
F.(id c)= id d
proof
set X= dom <|id c,?>;
A3: dom <|id c,?> = the Objects of A by FUNCT_2:def 1
.= dom id <|c,?> by FUNCT_2:def 1;
for y st y in X holds
(<|id c,?>).y =(id <|c,?>).y
proof
let y; assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A4: <|c,?> =hom?-(c) by Def2;
<|cod id c,?> is_transformable_to <|c,?>
by CAT_1:44;
then A5: <|cod id c,?> is_transformable_to <|dom id c,?> by
CAT_1:44;
A6: Hom(z,z) <> {} by CAT_1:56;
reconsider zz= id z as Morphism of z,z;
(<|id c,?>).z
= [[Hom(cod id c,z),Hom(dom id c,z)],hom(id c,id z)]
by Def3
.= [[Hom(c,z),Hom(dom id c,z)],hom(id c,id z)]
by CAT_1:44
.= [[Hom(c,z),Hom(c,z)],hom(id c,id z)] by CAT_1:44
.= [[Hom(c,z),Hom(c,z)],hom(c,id z)] by ENS_1:53
.= [[Hom(c,z),Hom(c,cod id z)],hom(c,id z)]
by CAT_1:44
.= [[Hom(c,dom id z),Hom(c,cod id z)],hom(c,id z)]
by CAT_1:44
.=(<|c,?> qua Function ).id z by A4,ENS_1:def 22
.=(<|c,?>).zz by A6,NATTRA_1:def 1
.= id (<|c,?>.z) by NATTRA_1:15
.=(id <|c,?> ).z by NATTRA_1:21
.=(id <|c,?> qua Function).z by NATTRA_1:def 5;
hence thesis by A5,NATTRA_1:def 5;
end;
then A7: <|id c,?>= id <|c,?> by A3,FUNCT_1:9;
F.(id c) = [[<|cod id c,?>,<|dom id c,?>],<|id c,?>] by Def4
.= [[<|c,?>,<|dom id c,?>],<|id c,?>] by CAT_1:44
.= [[<|c,?>,<|c,?>],id <|c,?>] by A7,CAT_1:44
.=id d by NATTRA_1:def 18;
hence thesis;
end;
then A8: (Obj F).c = d by OPPCAT_1:31;
<|c1,?> in Funct(A,EnsHom(A)) by CAT_2:def 2;
then reconsider d1=<|c1,?> as Object of Functors(A,EnsHom(A)) by
NATTRA_1:def 18;
F.(id c1)= id d1
proof
set X= dom <|id c1,?>;
A9: dom <|id c1,?> = the Objects of A by FUNCT_2:def 1
.= dom id <|c1,?> by FUNCT_2:def 1;
for y st y in X holds
(<|id c1,?>).y =(id <|c1,?>).y
proof
let y; assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A10: <|c1,?> =hom?-(c1) by Def2;
<|cod id c1,?> is_transformable_to <|c1,?> by CAT_1:44;
then A11: <|cod id c1,?> is_transformable_to <|dom id c1,?> by
CAT_1:44;
A12: Hom(z,z) <> {} by CAT_1:56;
reconsider zz= id z as Morphism of z,z;
(<|id c1,?>).z
= [[Hom(cod id c1,z),Hom(dom id c1,z)],hom(id c1,id z)]
by Def3
.= [[Hom(c1,z),Hom(dom id c1,z)],hom(id c1,id z)]
by CAT_1:44
.= [[Hom(c1,z),Hom(c1,z)],hom(id c1,id z)] by CAT_1:44
.= [[Hom(c1,z),Hom(c1,z)],hom(c1,id z)] by ENS_1:53
.= [[Hom(c1,z),Hom(c1,cod id z)],hom(c1,id z)]
by CAT_1:44
.= [[Hom(c1,dom id z),Hom(c1,cod id z)],hom(c1,id z)]
by CAT_1:44
.= (<|c1,?> qua Function ).id z by A10,ENS_1:def 22
.= (<|c1,?>).zz by A12,NATTRA_1:def 1
.= id (<|c1,?>.z) by NATTRA_1:15
.= (id <|c1,?> ).z by NATTRA_1:21
.= (id <|c1,?> qua Function).z by NATTRA_1:def 5;
hence thesis by A11,NATTRA_1:def 5;
end;
then A13: <|id c1,?>= id <|c1,?> by A9,FUNCT_1:9;
F.(id c1) = [[<|cod id c1,?>,<|dom id c1,?>],<|id c1,?>] by Def4
.= [[<|c1,?>,<|dom id c1,?>],<|id c1,?>] by CAT_1:44
.= [[<|c1,?>,<|c1,?>],id <|c1,?>] by A13,CAT_1:44
.=id d1 by NATTRA_1:def 18;
hence thesis;
end;
then A14: (Obj F).c1 = d1 by OPPCAT_1:31;
reconsider f=id c1 as Morphism of c1,c1;
A15: Hom(c1,c1) <> {} by CAT_1:56;
A16: <|c,?> =hom?-(c) by Def2;
<|c1,?> =hom?-(c1) by Def2;
then [[Hom(c,dom f),Hom(c,cod f)],hom(c,f)]= (hom?-(c1)).f
by A2,A8,A14,A16,ENS_1:def 22;
then [[Hom(c,dom f),Hom(c,cod f)],hom(c,f)]=
[[Hom(c1,dom f),Hom(c1,cod f)],hom(c1,f)] by ENS_1:def 22;
then [Hom(c,dom f),Hom(c,cod f),hom(c,f)]=
[[Hom(c1,dom f),Hom(c1,cod f)],hom(c1,f)] by MCART_1:def 3
;
then [Hom(c,dom f),Hom(c,cod f),hom(c,f)]=
[Hom(c1,dom f),Hom(c1,cod f),hom(c1,f)] by MCART_1:def 3
;
then Hom(c,dom f)=Hom(c1,dom f) by MCART_1:28;
then Hom(c,dom f)=Hom(c1,c1) by A15,CAT_1:23;
then A17: Hom(c,c1)=Hom(c1,c1) by A15,CAT_1:23;
id c1 in Hom(c1,c1) by CAT_1:55;
then reconsider h=id c1 as Morphism of c,c1 by A17,CAT_1:def 7;
dom f = c1 & dom h = c by A15,A17,CAT_1:23;
hence thesis;
end;
hence thesis by FUNCT_1:def 8;
end;
F is faithful by Th7;
hence thesis by A1,Th6;
end;
definition let C,D be Category;
let T be Contravariant_Functor of C,D;
attr T is full means :Def7:
for c,c' being Object of C st Hom(T.c',T.c) <> {}
for g being Morphism of T.c',T.c holds
Hom(c,c') <> {} & ex f being Morphism of c,c' st g = T.f;
end;
theorem
Yoneda A is full
proof
set F = Yoneda A;
for c,c' being Object of A st Hom(F.c',F.c) <> {}
for g being Morphism of F.c',F.c holds
Hom(c,c') <> {} & ex f being Morphism of c,c' st g = F.f
proof
let c,c' be Object of A;
assume
A1: Hom(F.c',F.c) <> {};
let g be Morphism of F.c',F.c;
g in the Morphisms of Functors(A,EnsHom A);
then g in NatTrans(A,EnsHom A) by NATTRA_1:def 18;
then consider F1,F2 being Functor of A,EnsHom A,
t being natural_transformation of F1,F2 such that
A2: g = [[F1,F2],t] &
F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;
A3: dom g =F1 & cod g = F2 by A2,NATTRA_1:39;
A4: dom g =F.c' & cod g= F.c by A1,CAT_1:23;
A5: F1=F.c' & F2=F.c by A1,A3,CAT_1:23;
<|c,?> in Funct(A,EnsHom(A)) by CAT_2:def 2;
then reconsider d=<|c,?> as Object of Functors(A,EnsHom(A)) by
NATTRA_1:def 18;
F.(id c)= id d
proof
set X= dom <|id c,?>;
A6: dom <|id c,?> = the Objects of A by FUNCT_2:def 1
.= dom id <|c,?> by FUNCT_2:def 1;
for y st y in X holds (<|id c,?>).y =(id <|c,?>).y
proof
let y; assume
y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A7: <|c,?> =hom?-(c) by Def2;
<|cod id c,?> is_transformable_to <|c,?> by CAT_1:44;
then A8: <|cod id c,?> is_transformable_to <|dom id
c,?> by CAT_1:44;
A9: Hom(z,z) <> {} by CAT_1:56;
reconsider zz= id z as Morphism of z,z;
(<|id c,?>).z
= [[Hom(cod id c,z),Hom(dom id c,z)],hom(id c,id z)] by Def3
.= [[Hom(c,z),Hom(dom id c,z)],hom(id c,id z)] by CAT_1:44
.= [[Hom(c,z),Hom(c,z)],hom(id c,id z)] by CAT_1:44
.= [[Hom(c,z),Hom(c,z)],hom(c,id z)] by ENS_1:53
.= [[Hom(c,z),Hom(c,cod id z)],hom(c,id z)] by CAT_1:44
.= [[Hom(c,dom id z),Hom(c,cod id z)],hom(c,id z)] by CAT_1:44
.=(<|c,?> qua Function ).id z by A7,ENS_1:def 22
.=(<|c,?>).zz by A9,NATTRA_1:def 1
.= id (<|c,?>.z) by NATTRA_1:15
.=(id <|c,?> ).z by NATTRA_1:21
.=(id <|c,?> qua Function).z by NATTRA_1:def 5;
hence thesis by A8,NATTRA_1:def 5;
end;
then A10: <|id c,?>= id <|c,?> by A6,FUNCT_1:9;
F.(id c) = [[<|cod id c,?>,<|dom id c,?>],<|id c,?>] by Def4
.=[[<|c,?>,<|dom id c,?>],<|id c,?>] by CAT_1:44
.= [[<|c,?>,<|c,?>],id <|c,?>] by A10,CAT_1:44
.=id d by NATTRA_1:def 18;
hence thesis;
end;
then A11: (Obj F).c = d by OPPCAT_1:31;
<|c',?> in Funct(A,EnsHom(A)) by CAT_2:def 2;
then reconsider d1=<|c',?> as Object of Functors(A,EnsHom(A)) by
NATTRA_1:def 18;
F.(id c')= id d1
proof
set X= dom <|id c',?>;
A12: dom <|id c',?> = the Objects of A by FUNCT_2:def 1
.= dom id <|c',?> by FUNCT_2:def 1;
for y st y in X holds (<|id c',?>).y =(id <|c',?>).y
proof
let y; assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A13: <|c',?> =hom?-(c') by Def2;
<|cod id c',?> is_transformable_to <|c',?> by CAT_1:44;
then A14: <|cod id c',?> is_transformable_to <|dom
id c',?> by CAT_1:44;
A15: Hom(z,z) <> {} by CAT_1:56;
reconsider zz= id z as Morphism of z,z;
(<|id c',?>).z
= [[Hom(cod id c',z),Hom(dom id c',z)],hom(id c',id z)] by Def3
.= [[Hom(c',z),Hom(dom id c',z)],hom(id c',id z)] by CAT_1:44
.= [[Hom(c',z),Hom(c',z)],hom(id c',id z)] by CAT_1:44
.= [[Hom(c',z),Hom(c',z)],hom(c',id z)] by ENS_1:53
.= [[Hom(c',z),Hom(c',cod id z)],hom(c',id z)] by CAT_1:44
.=[[Hom(c',dom id z),Hom(c',cod id z)],hom(c',id z)] by CAT_1:44
.=(<|c',?> qua Function ).id z by A13,ENS_1:def 22
.=(<|c',?>).zz by A15,NATTRA_1:def 1
.= id (<|c',?>.z) by NATTRA_1:15
.=(id <|c',?> ).z by NATTRA_1:21
.=(id <|c',?> qua Function).z by NATTRA_1:def 5;
hence thesis by A14,NATTRA_1:def 5;
end;
then A16: <|id c',?>= id <|c',?> by A12,FUNCT_1:9;
F.(id c') = [[<|cod id c',?>,<|dom id c',?>],<|id c',?>] by Def4
.=[[<|c',?>,<|dom id c',?>],<|id c',?>] by CAT_1:44
.= [[<|c',?>,<|c',?>],id <|c',?>] by A16,CAT_1:44
.=id d1 by NATTRA_1:def 18;
hence thesis;
end;
then A17: (Obj F).c' = d1 by OPPCAT_1:31;
A18: EnsHom A = Ens Hom A by Def1;
<|c,?> = hom?-(c) by Def2;
then A19: <|c,?>.c' = (hom?-(Hom A,c)).c' by A18,ENS_1:def 26
.= (Obj (hom?-(Hom A,c))).c' by CAT_1:def 20
.= Hom(c,c') by ENS_1:60;
<|c',?> = hom?-(c') by Def2;
then A20: <|c',?>.c' = (hom?-(Hom A,c')).c' by A18,ENS_1:def 26
.= (Obj (hom?-(Hom A,c'))).c' by CAT_1:def 20
.= Hom(c',c') by ENS_1:60;
A21: F.c'= d1 by A17,Def5;
A22: F.c = d by A11,Def5;
then A23: <|c',?> is_transformable_to <|c,?> by A2,A3,A4,A21,NATTRA_1:def 7;
reconsider t as
natural_transformation of <|c',?>,<|c,?> by A3,A4,A17,A22,Def5;
Hom(<|c',?>.c',<|c,?>.c') <> {} by A23,NATTRA_1:def 2;
then A24: (t.c') in Hom(<|c',?>.c',<|c,?>.c') by CAT_1:def 7;
then A25: dom (t.c') =<|c',?>.c' & cod (t.c') =<|c,?>.c' by CAT_1:18;
A26: EnsHom A =Ens Hom A by Def1
.= CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,fComp Hom A,fId Hom A
#)
by ENS_1:def 14;
then reconsider t1=t.c' as Element of Maps Hom A;
<|c',?>.c' <> {} by A20,CAT_1:56;
then (the Dom of EnsHom A).(t.c') <> {} by A25,CAT_1:def 2;
then A27: dom t1 <> {} by A26,ENS_1:def 10;
t1 in Maps (dom t1,cod t1) by ENS_1:19;
then A28: t1`2 in Funcs(dom t1,cod t1) by ENS_1:20;
then A29: cod t1 <> {} by A27,FUNCT_2:14;
then A30: (fCod Hom A).t1 <> {} by ENS_1:def 11;
A31: (the Cod of EnsHom A).t1 <> {} by A26,A29,ENS_1:def 11;
A32: cod (t.c') <> {} by A26,A30,CAT_1:def 3;
A33: <|c,?>.c' <> {} by A25,A31,CAT_1:def 3;
thus
Hom(c,c') <> {} by A19,A24,A32,CAT_1:18;
A34: dom (t.c')
=(fDom Hom A).(t.c') by A26,CAT_1:def 2
.= dom t1 by ENS_1:def 10;
cod (t.c')
= (fCod Hom A).(t.c') by A26,CAT_1:def 3
.= cod t1 by ENS_1:def 11;
then t1`2 is Function of <|c',?>.c',<|c,?>.c' by A25,A28,A34,FUNCT_2:121;
then A35: dom t1`2 = Hom(c',c') & rng t1`2 c= Hom(c,c')
by A19,A20,A25,A32,FUNCT_2:def 1,RELSET_1:12;
then id c' in dom t1`2 by CAT_1:55;
then t1`2.id c' in rng t1`2 by FUNCT_1:def 5;
then t1`2.id c' in Hom(c,c') by A35;
then reconsider f = t1`2.id c'
as Morphism of c,c' by CAT_1:def 7;
take f;
A36: dom f = c & cod f = c' by A19,A33,CAT_1:23;
A37: <|c',?> is_transformable_to <|c,?> by A2,A5,A21,A22,NATTRA_1:def 7;
for a being Object of A holds <|f,?>.a =t.a
proof
let a be Object of A;
A38: Hom(<|c',?>.a,<|c,?>.a) <> {} by A37,NATTRA_1:def 2;
then A39: dom(t.a) =<|c',?>.a & cod (t.a) =<|c,?>.a by CAT_1:23;
reconsider ta1=t.a as Element of Maps Hom A by A26;
A40: dom (t.a)
=(fDom Hom A).(t.a) by A26,CAT_1:def 2
.= dom ta1 by ENS_1:def 10;
A41: cod (t.a)
= (fCod Hom A).(t.a) by A26,CAT_1:def 3
.= cod ta1 by ENS_1:def 11;
<|c',?> = hom?-(c') by Def2;
then A42: <|c',?>.a = (hom?-(Hom A,c')).a by A18,ENS_1:def 26
.= (Obj (hom?-(Hom A,c'))).a by CAT_1:def 20
.= Hom(c',a) by ENS_1:60;
<|c,?> = hom?-(c) by Def2;
then A43: <|c,?>.a = (hom?-(Hom A,c)).a by A18,ENS_1:def 26
.= (Obj (hom?-(Hom A,c))).a by CAT_1:def 20
.= Hom(c,a) by ENS_1:60;
A44: ta1 =[[<|c',?>.a,<|c,?>.a],ta1`2] by A39,A40,A41,ENS_1:8;
ta1 in Maps (dom ta1,cod ta1) by ENS_1:19;
then A45: ta1`2 in Funcs(dom ta1,cod ta1) by ENS_1:20;
then A46: ta1`2 is Function of dom ta1,cod ta1 by FUNCT_2:121;
A47: ta1`2 is Function of dom(t.a),cod(t.a) by A40,A41,A45,FUNCT_2:121;
A48: dom ta1`2 = Hom(c',a)
proof
per cases;
suppose
Hom(c',a) = {};
hence thesis by A39,A40,A42,A46,FUNCT_2:def 1;
suppose
Hom(c',a) <> {};
then Hom(dom f,a) <> {} by A36,ENS_1:42;
hence thesis by A36,A39,A42,A43,A47,FUNCT_2:def 1;
end;
dom hom(f,a) = Hom(cod f,a)
proof
per cases;
suppose
Hom(cod f,a) = {};
hence thesis by FUNCT_2:def 1;
suppose
Hom(cod f,a) <> {};
then Hom(c,a) <> {} by A36,ENS_1:42;
hence thesis by A36,FUNCT_2:def 1;
end;
then A49: dom ta1`2 = dom hom(f,id a) by A36,A48,ENS_1:53;
set X=dom ta1`2;
for x be set st x in X holds hom(f,id a).x = ta1`2.x
proof
let x be set;assume
A50: x in X;
then reconsider y = x as Morphism of cod f,a by A36,A48,CAT_1:def
7;
reconsider h=y as Morphism of c',a by A19,A25,A32,CAT_1:23;
A51: dom h = c' & cod h =a by A48,A50,CAT_1:23;
A52: dom y =cod f & cod y = a by A36,A48,A50,CAT_1:23;
A53: Hom(<|c',?>.c',<|c',?>.a ) <> {} by A48,A50,CAT_1:126;
A54: Hom(<|c,?>.c',<|c,?>.a ) <> {} by A48,A50,CAT_1:126;
reconsider tc'=<|c',?>.h as Element of Maps Hom A by A26;
reconsider tch=<|c,?>.h as Element of Maps Hom A by A26;
reconsider t1=t.c' as Element of Maps Hom A by A26;
A55: Hom(<|c',?>.c',<|c,?>.c') <> {} by A37,NATTRA_1:def 2;
then (t.c') in Hom(<|c',?>.c',<|c,?>.c') by CAT_1:def 7;
then A56: dom (t.c') =<|c',?>.c' &
cod (t.c') = <|c,?>.c' by CAT_1:18;
A57: cod (t.c') = (fCod Hom A).(t.c') by A26,CAT_1:def 3
.= cod t1 by ENS_1:def 11;
A58: tc' =[[dom tc',cod tc'],tc'`2] by ENS_1:8;
A59: tch =[[dom tch,cod tch],tch`2] by ENS_1:8;
A60: dom (<|c',?>.h)
=(fDom Hom A).(<|c',?>.h) by A26,CAT_1:def 2
.= dom tc' by ENS_1:def 10;
A61: cod (<|c',?>.h)
= (fCod Hom A).(<|c',?>.h) by A26,CAT_1:def 3
.= cod tc' by ENS_1:def 11;
A62: dom (<|c,?>.h)
=(fDom Hom A).(<|c,?>.h) by A26,CAT_1:def 2
.= dom tch by ENS_1:def 10;
<|c,?>=hom?-(c) by Def2;
then A63: [[Hom(c,dom h),Hom(c,cod h)],hom(c,h)]
=(<|c,?> qua Function ).h by ENS_1:def
22
.=(<|c,?>).h by A48,A50,NATTRA_1:def 1;
<|c',?>=hom?-(c') by Def2;
then A64: [[Hom(c',dom h),Hom(c',cod h)],hom(c',h)]
=(<|c',?> qua Function ).h by ENS_1:def
22
.=(<|c',?>).h by A48,A50,NATTRA_1:def 1;
then [dom tc',cod tc',tc'`2]
= [[Hom(c',dom h),Hom(c',cod h)],hom(c',h)] by A58,MCART_1:def 3
;
then [dom tc',cod tc',tc'`2]
= [Hom(c',dom h),Hom(c',cod h),hom(c',h)] by MCART_1:def 3
;
then A65: tc'`2=hom(c',h) by MCART_1:28;
A66: dom (<|c',?>.h) = (tc')`1`1 by A60,ENS_1:def 4
.= [Hom(c',dom h),Hom(c',cod h)]`1
by A64,MCART_1:7
.=Hom(c',dom h) by MCART_1:7;
A67: cod(<|c',?>.h) =(tc')`1`2 by A61,ENS_1:def 5
.= [Hom(c',dom h),Hom(c',cod h)]`2
by A64,MCART_1:7
.=Hom(c',cod h) by MCART_1:7;
[Hom(c,dom h),Hom(c,cod h),hom(c,h)]=
[[dom tch,cod tch],tch`2] by A59,A63,MCART_1:
def 3
;
then [Hom(c,dom h),Hom(c,cod h),hom(c,h)]=
[dom tch,cod tch,tch`2] by MCART_1:def 3
;
then A68: hom(c,h)=tch`2 by MCART_1:28;
A69: dom (<|c,?>.h) = tch`1`1 by A62,ENS_1:def 4
.=[Hom(c,dom h),Hom(c,cod h)]`1
by A63,MCART_1:7
.=Hom(c,dom h) by MCART_1:7;
A70: cod t1=[Hom(c,dom h),Hom(c,cod h)]`1 by A19,A51,A56,A57,MCART_1:7
.= tch`1`1 by A63,MCART_1:7
.=dom tch by ENS_1:def 4;
A71: cod tc'=(tc')`1`2 by ENS_1:def 5
.= [Hom(c',dom h),Hom(c',cod h)]`2 by A64,MCART_1:7
.= dom ta1 by A39,A40,A42,A51,MCART_1:7;
A72: [(t.a),(<|c',?>.h)] in dom(the Comp of EnsHom A) by A39,A42,A51,
A67,CAT_1:40;
A73: (t.a)*(<|c',?>.h) = (t.a qua Morphism of EnsHom A)*(<|c',?>.h)
by A38,A53,CAT_1:def 13
.= (fComp Hom A).[ta1,tc'] by A26,A72,CAT_1:def 4
.= ta1*tc' by A71,ENS_1:def 12
.= [[dom tc',cod ta1],ta1`2*tc'`2]
by A71,ENS_1:def 7;
A74: [(<|c,?>.h),(t.c')] in dom(the Comp of EnsHom A) by A19,A51,A56,A69
,CAT_1:40;
A75: (<|c,?>.h)*(t.c') =(<|c,?>.h)*(t.c' qua Morphism of EnsHom A)
by A54,A55,CAT_1:def 13
.= (fComp Hom A).[tch,t1] by A26,A74,CAT_1:def 4
.= tch*t1 by A70,ENS_1:def 12
.= [[dom t1,cod tch],tch`2*t1`2]
by A70,ENS_1:def 7;
(t.a)*(<|c',?>.h) =(<|c,?>.h)*(t.c') by A2,A5,A21,A22,A48,A50,
NATTRA_1:def 8;
then [dom tc',cod ta1,(ta1`2*tc'`2)] =
[[dom t1,cod tch],(tch`2*t1`2)]
by A73,A75,MCART_1:def 3;
then [dom tc',cod ta1,(ta1`2*tc'`2)] =
[dom t1,cod tch,(tch`2*t1`2)]
by MCART_1:def 3;
then A76: ta1`2*tc'`2=tch`2*t1`2 by MCART_1:28;
tc' in Maps (dom tc',cod tc') by ENS_1:19;
then A77: tc'`2 in Funcs(dom tc',cod tc') by ENS_1:20;
then A78: tc'`2 is Function of dom(<|c',?>.h),cod(<|c',?>.h)
by A60,A61,FUNCT_2:121;
A79: tc'`2 is Function of Hom(c',dom h),Hom(c',cod h) by A60,A61,
A66,A67,A77,FUNCT_2:121;
dom tc'`2 = Hom(c',c')
proof
per cases;
suppose
Hom(c',c') = {};
hence thesis by A51,A66,A78,FUNCT_2:def 1;
suppose
Hom(c',c') <> {};
thus thesis by A48,A50,A51,A79,FUNCT_2:def 1;
end;
then A80: id c' in dom tc'`2 by CAT_1:55;
A81: id c' in dom t1`2 by A35,CAT_1:55;
A82: f in Hom(c,cod f) by A36,CAT_1:18;
A83: id c' in Hom(c',cod f) by A36,CAT_1:55;
hom(f,id a).x =hom(f,a).y by ENS_1:53
.= y * f by A36,A48,A50,ENS_1:def 21
.= tch`2.(t1`2.id c') by A52,A68,A82,ENS_1:def 20
.= (ta1`2*tc'`2).(id c') by A76,A81,FUNCT_1:23
.= ta1`2.(hom(c',h).id c') by A65,A80,FUNCT_1:23
.= ta1`2.(y * id c') by A52,A83,ENS_1:def 20
.= ta1`2.x by A36,A52,CAT_1:47;
hence thesis;
end;
then hom(f,id a)=ta1`2 by A49,FUNCT_1:9;
hence thesis by A36,A42,A43,A44,Def3;
end;
then <|f,?> = t by A2,A5,A21,A22,A36,ISOCAT_1:31;
hence g =F.f by A2,A3,A4,A21,A22,A36,Def4;
end;
hence thesis by Def7;
end;