:: Yoneda Embedding
:: by Miros{\l}aw Wojciechowski
::
:: Received June 12, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CAT_1, ENS_1, FUNCT_1, GRAPH_1, RELAT_1, SUBSET_1, MCART_1,
NATTRA_1, STRUCT_0, XBOOLE_0, PZFMISC1, TARSKI, OPPCAT_1, CAT_2, FUNCT_2,
YONEDA_1, MONOID_0, PARTFUN1;
notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, RELAT_1,
FUNCT_1, BINOP_1, FUNCT_2, STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1,
ENS_1, CAT_3, NATTRA_1;
constructors DOMAIN_1, NATTRA_1, ENS_1, RELSET_1, CAT_3, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, FUNCT_1, RELSET_1, ENS_1, STRUCT_0, FUNCT_2, CAT_1,
XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities TARSKI, BINOP_1, GRAPH_1, CAT_1, XTUPLE_0;
expansions CAT_1;
theorems FUNCT_1, FUNCT_2, CAT_1, CAT_2, OPPCAT_1, ENS_1, NATTRA_1, ISOCAT_1,
RELAT_1, CAT_3, XTUPLE_0;
schemes FUNCT_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
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 and
A2: [[dom m1,cod m1],f] = m1 and
A3: [[dom m2,cod m2],g] = m2;
A4: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,fComp Hom A#)
by ENS_1:def 13;
then reconsider m19=m1 as Element of Maps Hom A;
reconsider m29=m2 as Element of Maps Hom A by A4;
A5: cod m19= m1`1`2 by ENS_1:def 4
.=[dom m1,cod m1]`2 by A2
.=dom m2 by A1
.=[dom m2,cod m2]`1
.=m2`1`1 by A3
.= dom m29 by ENS_1:def 3;
A6: m19`2=f by A2;
A7: m29`2= g by A3;
A8: cod m2 =[dom m2,cod m2]`2
.=m2`1`2 by A3
.= cod m29 by ENS_1:def 4;
A9: dom m19= m1`1`1 by ENS_1:def 3
.=[dom m1,cod m1]`1 by A2
.=dom m1;
[m2,m1] in dom(the Comp of EnsHom A) by A1,CAT_1:15;
then m2(*)m1 = (fComp Hom A).(m29,m19) by A4,CAT_1:def 1
.= m29*m19 by A5,ENS_1:def 11
.= [[dom m1,cod m2],g*f] by A5,A9,A8,A7,A6,ENS_1:def 6;
hence thesis;
end;
definition
let A,a;
func <|a,?> -> Functor of A,EnsHom(A) equals
hom?-(a);
coherence by ENS_1:49;
end;
theorem Th2:
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,?>;
set B = EnsHom(A);
deffunc F(Element of A) = [[Hom(cod f,$1),Hom(dom f,$1)],hom(
f,$1)];
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 = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A, fComp Hom A #)
by ENS_1:def 13;
then reconsider m = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] as Morphism of
EnsHom A by ENS_1:48;
reconsider m9=m as Element of Maps Hom A by ENS_1:48;
A3: cod(m)= (fCod Hom A).m by A2
.= cod m9 by ENS_1:def 10
.= m`1`2 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`2
.= Hom(dom f,a)
.= (Obj (hom?-(Hom A,dom f))).a by ENS_1:60
.= (hom?-(Hom A,dom f)).a
.= F2.a by ENS_1:def 25;
dom(m)=(fDom Hom A).m by A2
.= dom m9 by ENS_1:def 9
.= m`1`1 by ENS_1:def 3
.= [Hom(cod f,a),Hom(dom f,a)]`1
.= Hom(cod f,a)
.= (Obj (hom?-(Hom A,cod f))).a by ENS_1:60
.= (hom?-(Hom A,cod f)).a
.=F1.a by ENS_1:def 25;
hence thesis by A3;
end;
A4: for a being Element of A holds F(a) in the carrier' 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 carrier of A, the carrier' of B such that
A5: for o being Element of A holds t.o = F(o) from
FUNCT_2:sch 8(A4);
A6: 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 5;
hence thesis by A5;
end;
for a being Object of A holds Hom(F1.a,F2.a) <> {} by A1;
then
A7: F1 is_transformable_to F2 by NATTRA_1:def 2;
then reconsider t as transformation of F1,F2 by A6,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
A8: Hom(a,b) <> {};
A9: Hom(F1.a,F1.b)<>{} by A8,CAT_1:84;
let g be Morphism of a,b;
A10: dom g =a by A8,CAT_1:5;
A11: rng hom(cod f,g) c= dom hom(f,b)
proof
A12: cod g =b by A8,CAT_1:5;
per cases;
suppose
A13: Hom(dom f,b) = {};
Hom(cod f,b) = {} by A13,ENS_1:42;
hence thesis by A12;
end;
suppose
A14: Hom(dom f,b) <> {};
cod g = b by A8,CAT_1:5;
then
A15: rng hom(cod f,g) c= Hom(cod f,cod g) & Hom(cod f,cod g)=dom hom(f
,b) by A14,FUNCT_2:def 1,RELAT_1:def 19;
let e be object;
assume e in rng hom(cod f,g);
hence thesis by A15;
end;
end;
A16: rng hom(f,a) c= dom hom(dom f,g)
proof
A17: dom g =a by A8,CAT_1:5;
per cases;
suppose
A18: Hom(dom f,cod g) = {};
Hom(dom f,dom g) = {} by A18,ENS_1:42;
hence thesis by A17;
end;
suppose
A19: Hom(dom f,cod g) <> {};
let e be object;
assume
A20: e in rng hom(f,a);
rng hom(f,a) c= Hom(dom f,a) & Hom(dom f,a) = dom hom(dom f,g) by A17
,A19,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis by A20;
end;
end;
A21: dom (hom(f,b)*hom(cod f,g)) = dom(hom(dom f,g)*hom(f,a))
proof
per cases;
suppose
A22: Hom(cod f,dom g)= {};
dom (hom(f,b)*hom(cod f,g))=dom (hom(cod f,g)) by A11,RELAT_1:27
.=Hom(cod f,dom g) by A22
.=dom (hom(f,a)) by A10,A22
.=dom(hom(dom f,g)*hom(f,a)) by A16,RELAT_1:27;
hence thesis;
end;
suppose
A23: Hom(cod f,dom g) <> {};
then
A24: Hom(cod f,cod g) <> {} by ENS_1:42;
A25: Hom(dom f,a) <> {} by A10,A23,ENS_1:42;
dom (hom(f,b)*hom(cod f,g))=dom (hom(cod f,g)) by A11,RELAT_1:27
.=Hom(cod f,dom g) by A24,FUNCT_2:def 1
.=Hom(cod f,a) by A8,CAT_1:5
.=dom (hom(f,a)) by A25,FUNCT_2:def 1
.=dom(hom(dom f,g)*hom(f,a)) by A16,RELAT_1:27;
hence thesis;
end;
end;
A26: for x being object 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 object such that
A27: x in dom (hom(f,b)*hom(cod f,g));
per cases;
suppose
A28: Hom(cod f,dom g) <> {};
A29: x in dom hom(cod f,g) by A27,FUNCT_1:11;
Hom(cod f,cod g) <> {} by A28,ENS_1:42;
then
A30: x in Hom(cod f,dom g) by A29,FUNCT_2:def 1;
then reconsider x as Morphism of A;
A31: dom(g) = cod(x) & dom(x) = cod(f) by A30,CAT_1:1;
A32: dom(g) = cod(x) by A30,CAT_1:1;
then
A33: cod(g(*)x)=cod(g) by CAT_1:17
.=b by A8,CAT_1:5;
A34: hom(f,a).x =x(*)f by A10,A30,ENS_1:def 20;
then reconsider h=hom(f,a).x as Morphism of A;
A35: dom(x) = cod(f) by A30,CAT_1:1;
then
A36: dom(x(*)f) =dom f by CAT_1:17;
dom(g(*)x) =dom x by A32,CAT_1:17
.=cod f by A30,CAT_1:1;
then
A37: g(*)x in Hom(cod f,b) by A33;
cod(x(*)f)=cod(x) by A35,CAT_1:17
.=dom g by A30,CAT_1:1;
then
A38: hom(f,a).x in Hom(dom f,dom g) by A34,A36;
(hom(f,b)*hom(cod f,g)).x = hom(f,b).(hom(cod f,g).x) by A27,FUNCT_1:12
.=hom(f,b).(g(*)x) by A30,ENS_1:def 19
.=(g(*)x)(*)f by A37,ENS_1:def 20
.= g(*)(x(*)f) by A31,CAT_1:18
.= g(*)(h) by A10,A30,ENS_1:def 20
.= hom(dom f,g).(hom(f,a).x) by A38,ENS_1:def 19
.= (hom(dom f,g)*hom(f,a)).x by A21,A27,FUNCT_1:12;
hence thesis;
end;
suppose
A39: Hom(cod f,dom g) = {};
x in dom hom(cod f,g) by A27,FUNCT_1:11;
hence thesis by A39;
end;
end;
A40: Hom(F2.a,F2.b)<>{} by A8,CAT_1:84;
A41: cod g =b by A8,CAT_1:5;
reconsider f4 = t.a as Morphism of EnsHom A;
A42: t.a = (t qua Function of the carrier of A, the carrier' of B).a by A7,
NATTRA_1:def 5
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by A5;
then reconsider f49=f4 as Element of Maps Hom A by ENS_1:48;
A43: Hom(F1.a,F2.a)<>{} by A1;
reconsider f1=t.b as Morphism of EnsHom A;
A44: t.b= (t qua Function of the carrier of A, the carrier' of B).b by A7,
NATTRA_1:def 5
.= [[Hom(cod f,b),Hom(dom f,b)],hom(f,b)] by A5;
then reconsider f19=f1 as Element of Maps Hom A by ENS_1:48;
A45: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A, fComp Hom
A #) by ENS_1:def 13;
then
A46: cod(f1) = (fCod Hom A).f1 .= cod f19 by ENS_1:def 10
.= f1`1`2 by ENS_1:def 4
.= [Hom(cod f,b),Hom(dom f,b)]`2 by A44
.= Hom(dom f,b);
A47: dom(f4) = (fDom Hom A).f4 by A45
.= dom f49 by ENS_1:def 9
.= f4`1`1 by ENS_1:def 3
.= [Hom(cod f,a),Hom(dom f,a)]`1 by A42
.=Hom(cod f,a);
A48: cod(f4) = (fCod Hom A).f4 by A45
.= cod f49 by ENS_1:def 10
.= f4`1`2 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`2 by A42
.= Hom(dom f,a);
reconsider f2=F1/.g as Morphism of EnsHom A;
A49: f2 = (hom?-(cod f)).g by A8,CAT_3:def 10
.=[[Hom(cod f,dom g),Hom(cod f,cod g)],hom(cod f,g)] by ENS_1:def 21;
then reconsider f29=f2 as Element of Maps Hom A by ENS_1:47;
A50: dom(f2) = (fDom Hom A).f2 by A45
.= dom f29 by ENS_1:def 9
.= f2`1`1 by ENS_1:def 3
.= [Hom(cod f,dom g),Hom(cod f,cod g)]`1 by A49
.= Hom(cod f,dom g);
A51: cod(f2) = (fCod Hom A).f2 by A45
.= cod f29 by ENS_1:def 10
.= f2`1`2 by ENS_1:def 4
.= [Hom(cod f,dom g),Hom(cod f,cod g)]`2 by A49
.= Hom(cod f,cod g);
A52: dom(f1) =(fDom Hom A).f1 by A45
.= dom f19 by ENS_1:def 9
.= f1`1`1 by ENS_1:def 3
.=[Hom(cod f,b),Hom(dom f,b)]`1 by A44
.=Hom(cod f,b);
then
A53: cod f2 = dom f1 by A8,A51,CAT_1:5;
reconsider f3 = F2/.g as Morphism of EnsHom A;
A54: f3= (hom?-(dom f)).g by A8,CAT_3:def 10
.=[[Hom(dom f,dom g),Hom(dom f,cod g)],hom(dom f,g)] by ENS_1:def 21;
then reconsider f39=f3 as Element of Maps Hom A by ENS_1:47;
A55: cod(f3) = (fCod Hom A).f3 by A45
.= cod f39 by ENS_1:def 10
.= f3`1`2 by ENS_1:def 4
.= [Hom(dom f,dom g),Hom(dom f,cod g)]`2 by A54
.= Hom(dom f,cod g);
A56: dom(f3) =(fDom Hom A).f3 by A45
.= dom f39 by ENS_1:def 9
.= f3`1`1 by ENS_1:def 3
.= [Hom(dom f,dom g),Hom(dom f,cod g)]`1 by A54
.= Hom(dom f,dom g);
then
A57: cod f4 = dom f3 by A8,A48,CAT_1:5;
Hom(F1.b,F2.b)<>{} by A1;
then t.b*F1/.g = f1(*)f2 by A9,CAT_1:def 13
.= [[Hom(cod f,dom g),Hom(dom f,b)],hom(f,b)*hom(cod f,g)] by A44,A52,A46
,A49,A50,A51,A53,Th1
.= [[ Hom(cod f,a),Hom(dom f,cod g)],hom(dom f,g)*hom(f,a)] by A10,A41
,A21,A26,FUNCT_1:2
.= f3(*)f4 by A54,A56,A55,A42,A47,A48,A57,Th1
.= F2/.g*t.a by A40,A43,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 B=EnsHom A;
deffunc F(Element of A) = [[Hom(cod f,$1),Hom(dom f,$1)],
hom(f,id $1)];
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: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A, fComp
Hom A #) by ENS_1:def 13;
A3: hom(f,id o)=hom(f,o) by ENS_1:53;
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 m9=m as Element of Maps Hom A by A3,ENS_1:48;
A4: cod(m) = (fCod Hom A).m by A2
.= cod m9 by ENS_1:def 10
.= m`1`2 by ENS_1:def 4
.= [Hom(cod f,o),Hom(dom f,o)]`2
.= Hom(dom f,o)
.= (Obj (hom?-(Hom A,dom f))).o by ENS_1:60
.= (hom?-(Hom A,dom f)).o
.=F2.o by ENS_1:def 25;
dom(m) = (fDom Hom A).m by A2
.= dom m9 by ENS_1:def 9
.= m`1`1 by ENS_1:def 3
.= [Hom(cod f,o),Hom(dom f,o)]`1
.= Hom(cod f,o)
.= (Obj (hom?-(Hom A,cod f))).o by ENS_1:60
.= (hom?-(Hom A,cod f)).o
.= F1.o by ENS_1:def 25;
hence thesis by A4;
end;
A5: for o being Element of A holds F(o) in the carrier' 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 carrier of A, the carrier' of EnsHom(A)
such that
A6: for o being Element of A holds t.o = F(o) from
FUNCT_2:sch 8(A5);
A7: 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 5;
hence thesis by A6;
end;
for o being Object of A holds Hom(F1.o,F2.o) <> {} by A1;
then
A8: F1 is_transformable_to F2 by NATTRA_1:def 2;
then reconsider t as transformation of F1,F2 by A7,NATTRA_1:def 3;
A9: 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) <> {};
A11: Hom(F1.a,F1.b)<>{} by A10,CAT_1:84;
let g be Morphism of a,b;
A12: dom g =a by A10,CAT_1:5;
A13: rng hom(cod f,g) c= dom hom(f,b)
proof
A14: cod g =b by A10,CAT_1:5;
per cases;
suppose
A15: Hom(dom f,b) = {};
Hom(cod f,b) = {} by A15,ENS_1:42;
hence thesis by A14;
end;
suppose
A16: Hom(dom f,b) <> {};
cod g =b by A10,CAT_1:5;
then
A17: rng hom(cod f,g) c= Hom(cod f,cod g) & Hom(cod f,cod g)=dom hom
(f,b) by A16,FUNCT_2:def 1,RELAT_1:def 19;
let e be object;
assume e in rng hom(cod f,g);
hence thesis by A17;
end;
end;
A18: rng hom(f,a) c= dom hom(dom f,g)
proof
A19: dom g =a by A10,CAT_1:5;
per cases;
suppose
A20: Hom(dom f,cod g) = {};
Hom(dom f,dom g) = {} by A20,ENS_1:42;
hence thesis by A19;
end;
suppose
A21: Hom(dom f,cod g) <> {};
let e be object;
assume
A22: e in rng hom(f,a);
rng hom(f,a) c= Hom(dom f,a) & Hom(dom f,a)=dom hom(dom f,g) by A19
,A21,FUNCT_2:def 1,RELAT_1:def 19;
hence thesis by A22;
end;
end;
A23: dom (hom(f,b)*hom(cod f,g)) = dom(hom(dom f,g)*hom(f,a))
proof
per cases;
suppose
A24: Hom(cod f,dom g)= {};
dom (hom(f,b)*hom(cod f,g)) = dom (hom(cod f,g)) by A13,RELAT_1:27
.=Hom(cod f,a) by A12,A24
.=dom (hom(f,a)) by A12,A24
.=dom(hom(dom f,g)*hom(f,a)) by A18,RELAT_1:27;
hence thesis;
end;
suppose
A25: Hom(cod f,dom g) <> {};
then
A26: Hom(cod f,cod g) <> {} by ENS_1:42;
A27: Hom(dom f,a) <> {} by A12,A25,ENS_1:42;
dom (hom(f,b)*hom(cod f,g)) = dom (hom(cod f,g)) by A13,RELAT_1:27
.=Hom(cod f,a) by A12,A26,FUNCT_2:def 1
.=dom (hom(f,a)) by A27,FUNCT_2:def 1
.=dom(hom(dom f,g)*hom(f,a)) by A18,RELAT_1:27;
hence thesis;
end;
end;
A28: for x being object 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 object such that
A29: x in dom (hom(f,b)*hom(cod f,g));
per cases;
suppose
A30: Hom(cod f,dom g) <> {};
A31: x in dom hom(cod f,g) by A29,FUNCT_1:11;
Hom(cod f,cod g) <> {} by A30,ENS_1:42;
then
A32: x in Hom(cod f,dom g) by A31,FUNCT_2:def 1;
then reconsider x as Morphism of A;
A33: dom(g) = cod(x) by A32,CAT_1:1;
cod g =b by A10,CAT_1:5;
then
A34: cod(g(*)x)=b by A33,CAT_1:17;
dom(g(*)x) =dom x by A33,CAT_1:17
.=cod f by A32,CAT_1:1;
then
A35: g(*)x in Hom(cod f,b) by A34;
A36: dom(x) = cod(f) by A32,CAT_1:1;
then
A37: dom(x(*)f) =dom f by CAT_1:17;
A38: hom(f,a).x =x(*)f by A12,A32,ENS_1:def 20;
then reconsider h=hom(f,a).x as Morphism of A;
A39: dom(g) = cod(x) & dom(x) = cod(f) by A32,CAT_1:1;
cod(x(*)f)=cod(x) by A36,CAT_1:17
.=dom g by A32,CAT_1:1;
then
A40: hom(f,a).x in Hom(dom f,dom g) by A38,A37;
(hom(f,b)*hom(cod f,g)).x = hom(f,b).(hom(cod f,g).x) by A29,
FUNCT_1:12
.=hom(f,b).(g(*)x) by A32,ENS_1:def 19
.=(g(*)x)(*)f by A35,ENS_1:def 20
.= g(*)(x(*)f) by A39,CAT_1:18
.= g(*)(h) by A12,A32,ENS_1:def 20
.= hom(dom f,g).(hom(f,a).x) by A40,ENS_1:def 19
.= (hom(dom f,g)*hom(f,a)).x by A23,A29,FUNCT_1:12;
hence thesis;
end;
suppose
A41: Hom(cod f,dom g) = {};
x in dom hom(cod f,g) by A29,FUNCT_1:11;
hence thesis by A41;
end;
end;
A42: Hom(F2.a,F2.b)<>{} by A10,CAT_1:84;
A43: cod g =b by A10,CAT_1:5;
reconsider f4=t.a as Morphism of EnsHom A;
A44: t.a = (t qua Function of the carrier of A, the carrier' of B).a by A8,
NATTRA_1:def 5
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,id a)] by A6
.= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by ENS_1:53;
then reconsider f49=f4 as Element of Maps Hom A by ENS_1:48;
A45: Hom(F1.a,F2.a)<>{} by A1;
reconsider f1=t.b as Morphism of EnsHom A;
A46: t.b = (t qua Function of the carrier of A, the carrier' of B).b by A8,
NATTRA_1:def 5
.= [[Hom(cod f,b),Hom(dom f,b)],hom(f,id b)] by A6
.=[[Hom(cod f,b),Hom(dom f,b)],hom(f,b)] by ENS_1:53;
then reconsider f19=f1 as Element of Maps Hom A by ENS_1:48;
A47: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A, fComp
Hom A #) by ENS_1:def 13;
then
A48: cod(f1) = (fCod Hom A).f1 .= cod f19 by ENS_1:def 10
.= f1`1`2 by ENS_1:def 4
.= [Hom(cod f,b),Hom(dom f,b)]`2 by A46
.= Hom(dom f,b);
A49: dom(f4) =(fDom Hom A).f4 by A47
.= dom f49 by ENS_1:def 9
.= f4`1`1 by ENS_1:def 3
.=[Hom(cod f,a),Hom(dom f,a)]`1 by A44
.=Hom(cod f,a);
A50: cod(f4) = (fCod Hom A).f4 by A47
.= cod f49 by ENS_1:def 10
.= f4`1`2 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`2 by A44
.= Hom(dom f,a);
reconsider f2=F1/.g as Morphism of EnsHom A;
A51: f2 = (hom?-(cod f)).g by A10,CAT_3:def 10
.=[[Hom(cod f,dom g),Hom(cod f,cod g)],hom(cod f,g)] by ENS_1:def 21;
then reconsider f29=f2 as Element of Maps Hom A by ENS_1:47;
A52: dom(f2) =(fDom Hom A).f2 by A47
.= dom f29 by ENS_1:def 9
.= f2`1`1 by ENS_1:def 3
.=[Hom(cod f,dom g),Hom(cod f,cod g)]`1 by A51
.=Hom(cod f,dom g);
A53: cod(f2) = (fCod Hom A).f2 by A47
.= cod f29 by ENS_1:def 10
.= f2`1`2 by ENS_1:def 4
.= [Hom(cod f,dom g),Hom(cod f,cod g)]`2 by A51
.= Hom(cod f,cod g);
A54: dom(f1) = (fDom Hom A).f1 by A47
.= dom f19 by ENS_1:def 9
.= f1`1`1 by ENS_1:def 3
.= [Hom(cod f,b),Hom(dom f,b)]`1 by A46
.= Hom(cod f,b);
then
A55: cod f2 = dom f1 by A10,A53,CAT_1:5;
reconsider f3=F2/.g as Morphism of EnsHom A;
A56: f3 = (hom?-(dom f)).g by A10,CAT_3:def 10
.=[[Hom(dom f,dom g),Hom(dom f,cod g)],hom(dom f,g)] by ENS_1:def 21;
then reconsider f39=f3 as Element of Maps Hom A by ENS_1:47;
A57: cod(f3) = (fCod Hom A).f3 by A47
.= cod f39 by ENS_1:def 10
.= f3`1`2 by ENS_1:def 4
.= [Hom(dom f,dom g),Hom(dom f,cod g)]`2 by A56
.= Hom(dom f,cod g);
A58: dom(f3) =(fDom Hom A).f3 by A47
.= dom f39 by ENS_1:def 9
.= f3`1`1 by ENS_1:def 3
.=[Hom(dom f,dom g),Hom(dom f,cod g)]`1 by A56
.=Hom(dom f,dom g);
then
A59: cod f4 = dom f3 by A10,A50,CAT_1:5;
Hom(F1.b,F2.b)<>{} by A1;
then t.b*F1/.g = f1(*)f2 by A11,CAT_1:def 13
.=[[Hom(cod f,dom g),Hom(dom f,b)],hom(f,b)*hom(cod f,g)] by A46,A54
,A48,A51,A52,A53,A55,Th1
.=[[ Hom(cod f,a),Hom(dom f,cod g)],hom(dom f,g)*hom(f,a)] by A12,A43
,A23,A28,FUNCT_1:2
.=f3(*)f4 by A56,A58,A57,A44,A49,A50,A59,Th1
.= F2/.g*t.a by A42,A45,CAT_1:def 13;
hence thesis;
end;
F1 is_naturally_transformable_to F2 by Th2;
then reconsider t as natural_transformation of F1,F2 by A9,NATTRA_1:def 8;
for o be Element 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 A8,NATTRA_1:def 5
.= [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] by A6;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
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;
A60: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A, fComp
Hom A #) by ENS_1:def 13;
then reconsider
m = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] as Morphism of
EnsHom A by ENS_1:48;
reconsider m9=m as Element of Maps Hom A by ENS_1:48;
A61: cod(m) = (fCod Hom A).m by A60
.= cod m9 by ENS_1:def 10
.= m`1`2 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`2
.= Hom(dom f,a)
.= (Obj (hom?-(Hom A,dom f))).a by ENS_1:60
.= (hom?-(Hom A,dom f)).a
.=<|dom f,?>.a by ENS_1:def 25;
dom(m) =(fDom Hom A).m by A60
.= dom m9 by ENS_1:def 9
.= m`1`1 by ENS_1:def 3
.=[Hom(cod f,a),Hom(dom f,a)]`1
.=Hom(cod f,a)
.= (Obj (hom?-(Hom A,cod f))).a by ENS_1:60
.= (hom?-(Hom A,cod f)).a
.=<|cod f,?>.a by ENS_1:def 25;
hence thesis by A61;
end;
then for a being Object of A holds Hom(<|cod f,?>.a,<|dom f,?>.a) <> {};
then
A62: <|cod f,?> is_transformable_to <|dom f,?> by NATTRA_1:def 2;
let h1,h2 be natural_transformation of <|cod f,?>, <|dom f,?> such that
A63: for o be Object of A holds h1.o = [[Hom(cod f,o),Hom(dom f,o)],
hom(f,id o)] and
A64: for o be Object of A holds h2.o =[[Hom(cod f,o),Hom(dom f,o)],hom
(f,id o)];
now
let o;
thus h1.o =[[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] by A63
.= h2.o by A64;
end;
hence thesis by A62,NATTRA_1:19;
end;
end;
theorem Th3:
for f being Element of the carrier' of A holds [[<|cod f,?>,<|dom
f,?>],<|f,?>] is Element of the carrier' of Functors(A,EnsHom(A))
proof
let f be Element of the carrier' of A;
<|cod f,?> is_naturally_transformable_to <|dom f,?> by Th2;
then [[<|cod f,?>,<|dom f,?>],<|f,?>] in NatTrans(A,EnsHom(A)) by
NATTRA_1:def 16;
hence thesis by NATTRA_1:def 17;
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 carrier' of A) = [[<|cod $1,?>,<|dom $1,?>],<|$1
,?>];
A1: for f being Element of the carrier' of A holds F(f) in the carrier' of
Functors(A,EnsHom(A))
proof
let f;
[[<|cod f,?>,<|dom f,?>],<|f,?>] is Morphism of Functors(A,EnsHom(A)
) by Th3;
hence thesis;
end;
consider F being Function of the carrier' of A, the carrier' of Functors(A
,EnsHom(A)) such that
A2: for f being Element of the carrier' of A holds F.f = F(f) from
FUNCT_2:sch 8(A1);
A3: 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;
reconsider t1=<|g,?> as natural_transformation of <|cod g,?>,<|dom g,?>;
assume
A4: dom g = cod f;
then reconsider
t=<|f,?> as natural_transformation of <|dom g,?>,<|dom f,?>;
A5: F.g =[[<|cod g,?>,<|dom g,?>],t1] by A2;
A6: dom(g(*)f) = dom f by A4,CAT_1:17;
then reconsider
tt=t`*`t1 as natural_transformation of <|cod(g(*)f),?>,<|dom(g(*)
f),?> by A4,CAT_1:17;
A7: cod(g(*)f) = cod g by A4,CAT_1:17;
for o being Object of A holds (<|g(*)f,?>).o =tt.o
proof
set F1=<|cod f,?> , F2=<|dom f,?>;
let o be Object of A;
reconsider f1=t.o as Morphism of EnsHom(A);
reconsider f2=t1.o as Morphism of EnsHom(A);
A8: f2 = [[Hom(cod g,o),Hom(dom g,o)],hom(g,id o)] by Def3;
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;
A9: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A, fCod Hom A,
fComp Hom A #) by ENS_1:def 13;
then reconsider
m = [[Hom(cod g,a),Hom(dom g,a)],hom(g,a)] as Morphism of
EnsHom A by ENS_1:48;
reconsider m9=m as Element of Maps Hom A by ENS_1:48;
A10: cod(m) = (fCod Hom A).m by A9
.= cod m9 by ENS_1:def 10
.= m`1`2 by ENS_1:def 4
.= [Hom(cod g,a),Hom(dom g,a)]`2
.= Hom(dom g,a)
.= (Obj (hom?-(Hom A,dom g))).a by ENS_1:60
.= (hom?-(Hom A,dom g)).a
.= <|dom g,?>.a by ENS_1:def 25;
dom(m) = (fDom Hom A).m by A9
.= dom m9 by ENS_1:def 9
.= m`1`1 by ENS_1:def 3
.= [Hom(cod g,a),Hom(dom g,a)]`1
.= Hom(cod g,a)
.= (Obj (hom?-(Hom A,cod g))).a by ENS_1:60
.= (hom?-(Hom A,cod g)).a
.=<|cod g,?>.a by ENS_1:def 25;
hence thesis by A10;
end;
then
A11: Hom(<|cod g,?>.o,<|dom g,?>.o)<> {};
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;
A12: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A, fCod Hom A,
fComp Hom A #) by ENS_1:def 13;
then reconsider
m = [[Hom(cod f,a),Hom(dom f,a)],hom(f, a)] as Morphism
of EnsHom A by ENS_1:48;
reconsider m9=m as Element of Maps Hom A by ENS_1:48;
A13: cod(m) = (fCod Hom A).m by A12
.= cod m9 by ENS_1:def 10
.= m`1`2 by ENS_1:def 4
.= [Hom(cod f,a),Hom(dom f,a)]`2
.= Hom(dom f,a)
.= (Obj (hom?-(Hom A,dom f))).a by ENS_1:60
.= (hom?-(Hom A,dom f)).a
.= F2.a by ENS_1:def 25;
dom(m) = (fDom Hom A).m by A12
.= dom m9 by ENS_1:def 9
.= m`1`1 by ENS_1:def 3
.= [Hom(cod f,a),Hom(dom f,a)]`1
.= Hom(cod f,a)
.= (Obj (hom?-(Hom A,cod f))).a by ENS_1:60
.= (hom?-(Hom A,cod f)).a
.=F1.a by ENS_1:def 25;
hence thesis by A13;
end;
then
A14: Hom(F1.o,F2.o)<> {};
A15: (<|g(*)f,?>).o = [[Hom(cod(g),o),Hom(dom(g(*)f),o)], hom(g(*)f,id o)]
by A7,Def3
.= [[Hom(cod g,o),Hom(dom f,o)],hom(g(*)f,o)] by A6,ENS_1:53;
A16: t.o = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)] by A4,Def3;
A17: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A, fComp
Hom A #) by ENS_1:def 13;
then reconsider f19=f1 as Element of Maps Hom A;
reconsider f29=f2 as Element of Maps Hom A by A17;
A18: cod(f2) = (fCod Hom A).f2 by A17
.= cod f29 by ENS_1:def 10
.= f2`1`2 by ENS_1:def 4
.= [Hom(cod g,o),Hom(dom g,o)]`2 by A8
.= Hom(dom g,o);
A19: cod(f1) = (fCod Hom A).f1 by A17
.= cod f19 by ENS_1:def 10
.= f1`1`2 by ENS_1:def 4
.= [Hom(cod f,o),Hom(dom f,o)]`2 by A16
.= Hom(dom f,o);
A20: dom(f1) =(fDom Hom A).f1 by A17
.= dom f19 by ENS_1:def 9
.= f1`1`1 by ENS_1:def 3
.=[Hom(cod f,o),Hom(dom f,o)]`1 by A16
.=Hom(cod f,o);
A21: dom(f2) = (fDom Hom A).f2 by A17
.= dom f29 by ENS_1:def 9
.= f2`1`1 by ENS_1:def 3
.= [Hom(cod g,o),Hom(dom g,o)]`1 by A8
.= Hom(cod g,o);
<|dom g,?> is_naturally_transformable_to <|dom f,?> & <|cod g,?>
is_naturally_transformable_to <|dom g,?> by A4,Th2;
then (tt).o = (t.o)*(t1.o) by A6,A7,NATTRA_1:25
.= f1(*)f2 by A4,A14,A11,CAT_1:def 13
.= [[Hom(cod g,o),Hom(dom f,o)], hom(f,id o)*hom(g,id o)] by A4,A16
,A8,A20,A18,A21,A19,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 A4,ENS_1:46;
hence thesis by A15;
end;
then
A22: (<|g(*)f,?> )=tt by Th2,ISOCAT_1:26;
A23: F.f =[[<|dom g,?>,<|dom f,?>],t] by A2,A4;
then
A24: [F.f,F.g] in dom (the Comp of Functors(A,EnsHom(A))) by A5,NATTRA_1:35;
then consider F9,F19,F29 being Functor of A,EnsHom(A), t9 being
natural_transformation of F9,F19, t19 being natural_transformation of F19,F29
such that
A25: F.g=[[F9,F19],t9] and
A26: F.f = [[F19,F29],t19] and
A27: (the Comp of Functors(A,EnsHom(A))).(F.f,F.g) = [[F9,F29],t19
`*`t9] by NATTRA_1:def 17;
A28: <|f,?> = t19 by A23,A26,XTUPLE_0:1;
[F19,F29] = [<|dom g,?>,<|dom f,?>] by A23,A26,XTUPLE_0:1;
then
A29: <|dom f,?> = F29 by XTUPLE_0:1;
[F9,F19] = [<|cod g,?>,<|dom g,?>] by A5,A25,XTUPLE_0:1;
then
A30: <|cod g,?> = F9 & <|dom g,?> = F19 by XTUPLE_0:1;
<|g,?> = t9 by A5,A25,XTUPLE_0:1;
then (F.f)(*)(F.g)
= [[<|cod g,?>,<|dom f,?>],t`*`t1] by A24,A27,A28,A30,A29,CAT_1:def 1
;
hence thesis by A2,A6,A7,A22;
end;
A31: 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;
set X= dom <|id dom f,?>;
A32: dom <|id dom f,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|dom f,?> by FUNCT_2:def 1;
A33: 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),?>]
.=[[<|dom f,?>,<|dom f,?>],<|id dom f,?>];
A34: g = [[<|cod f,?>,<|dom f,?>],<|f,?>] by A2;
then cod g =<|dom f,?> by NATTRA_1:33;
then
A35: [[<|dom f,?>,<|dom f,?>],id <|dom f,?>] = id cod (F.f) by NATTRA_1:def 17
;
A36: for y being object st y in X holds (<|id dom f,?>).y =(id <|dom f,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
reconsider zz= id z as Morphism of z,z;
A37: Hom(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)]
.= [[Hom(dom f,z),Hom(dom f,z)], hom(id dom f,id z)]
.= [[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)]
.= [[Hom(dom f,dom id z),Hom(dom f,cod id z)], hom(dom f,id z)]
.= (<|dom f,?> qua Function ).id z by ENS_1:def 21
.= (<|dom f,?>)/.zz by A37,CAT_3:def 10
.= id (<|dom f,?>.z) by NATTRA_1:15
.= (id <|dom f,?> ).z by NATTRA_1:20
.= (id <|dom f,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
set X= dom <|id cod f,?>;
A38: for y being object st y in X holds (<|id cod f,?>).y =(id <|cod f,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
A39: Hom(z,z) <> {};
(<|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)]
.= [[Hom(cod f,z),Hom(cod f,z)], hom(id cod f,id z)]
.= [[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)]
.= [[Hom(cod f,dom id z),Hom(cod f,cod id z)], hom(cod f,id z)]
.= (<|cod f,?> qua Function).id z by ENS_1:def 21
.= (<|cod f,?>)/.id z by A39,CAT_3:def 10
.= id (<|cod f,?>.z) by NATTRA_1:15
.= (id <|cod f,?>).z by NATTRA_1:20
.= (id <|cod f,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
dom <|id cod f,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|cod f,?> by FUNCT_2:def 1;
then
A40: <|id cod f,?> =id <|cod f,?> by A38,FUNCT_1:2;
A41: 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),?>]
.= [[<|cod f,?>,<|cod f,?>],<|id cod f,?>];
dom g =<|cod f,?> by A34,NATTRA_1:33;
hence thesis by A33,A35,A32,A36,A41,A40,FUNCT_1:2,NATTRA_1:def 17;
end;
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;
set X= dom <|id c,?>;
<|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 17;
take d;
A42: for y being object st y in X holds (<|id c,?>).y =(id <|c,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
reconsider zz= id z as Morphism of z,z;
A43: Hom(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)]
.= [[Hom(c,z),Hom(c,z)],hom(id c,id z)]
.= [[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)]
.= [[Hom(c,dom id z),Hom(c,cod id z)],hom(c,id z)]
.=(<|c,?> qua Function ).id z by ENS_1:def 21
.=(<|c,?>)/.zz by A43,CAT_3:def 10
.= id (<|c,?>.z) by NATTRA_1:15
.=(id <|c,?> ).z by NATTRA_1:20
.=(id <|c,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
dom <|id c,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|c,?> by FUNCT_2:def 1;
then
A44: <|id c,?>= id <|c,?> by A42,FUNCT_1:2;
F.(id c) = [[<|cod id c,?>,<|dom id c,?>],<|id c,?>] by A2
.=[[<|c,?>,<|dom id c,?>],<|id c,?>]
.= [[<|c,?>,<|c,?>],id <|c,?>] by A44
.=id d by NATTRA_1:def 17;
hence thesis;
end;
then reconsider F as Contravariant_Functor of A,Functors(A,EnsHom(A)) by
A31,A3,OPPCAT_1:def 9;
for f being Element of the carrier' 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
A45: for f holds h1.f = [[<|cod f,?>,<|dom f,?>],<|f,?>] and
A46: for f holds h2.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];
now
let f;
thus h1.f = [[<|cod f,?>,<|dom f,?>],<|f,?>] by A45
.= h2.f by A46;
end;
hence thesis by FUNCT_2:63;
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
(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 object st x1 in dom F & x2 in dom F & F.x1 = F.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A3: x1 in dom F & x2 in dom F and
A4: F.x1 = F.x2;
reconsider m1=x1,m2=x2 as Morphism of A by A3,FUNCT_2:def 1;
set o1=dom m1,o2=cod m1;
set o3=dom m2,o4=cod m2;
reconsider m19=m1 as Morphism of o1,o2 by CAT_1:4;
reconsider m29=m2 as Morphism of o3,o4 by CAT_1:4;
A5: Hom(o1,o2) <> {} by CAT_1:2;
then
A6: Hom(F.o1,F.o2) <> {} by CAT_1:84;
A7: Hom(o3,o4) <> {} by CAT_1:2;
then
A8: Hom(F.o3,F.o4) <> {} by CAT_1:84;
A9: F/.m19= F.m2 by A4,A5,CAT_3:def 10
.= F/.m29 by A7,CAT_3:def 10;
(Obj F).o1 = F.o1
.=dom (F/.m29) by A9,A6,CAT_1:5
.= (Obj F).o3 by A8,CAT_1:5;
then
A10: m2 is Morphism of dom m2,cod m2 & o1=o3 by A1,CAT_1:4,FUNCT_2:19;
(Obj F).o2 = F.o2
.=cod(F/.m29) by A9,A6,CAT_1:5
.=(Obj F).o4 by A8,CAT_1:5;
then m1 is Morphism of dom m1,cod m1 & m2 is Morphism of o1,o2 by A1,A10,
CAT_1:4,FUNCT_2:19;
hence thesis by A2,A4,A5;
end;
hence thesis by FUNCT_1:def 4;
end;
definition
let C,D be Category;
let T be Contravariant_Functor of C,D;
attr T is faithful means
for c,c9 being Object of C st Hom(c,c9) <>
{} for f1,f2 being Morphism of c,c9 holds T.f1 = T.f2 implies f1 = f2;
end;
theorem Th5:
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 object st x1 in dom F & x2 in dom F & F.x1 = F.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A3: x1 in dom F & x2 in dom F and
A4: F.x1 = F.x2;
reconsider m1=x1,m2=x2 as Morphism of A by A3,FUNCT_2:def 1;
set o1=dom m1,o2=cod m1;
set o3=dom m2,o4=cod m2;
reconsider m29=m2 as Morphism of o3,o4 by CAT_1:4;
(Obj F).o1 = cod (F.m29) by A4,OPPCAT_1:32
.= (Obj F).o3 by OPPCAT_1:32;
then
A5: m2 is Morphism of dom m2,cod m2 & o1=o3 by A1,CAT_1:4,FUNCT_2:19;
A6: m1 is Morphism of dom m1,cod m1 & Hom(o1,o2) <> {} by CAT_1:2,4;
(Obj F).o2 =dom(F.m29) by A4,OPPCAT_1:32
.=(Obj F).o4 by OPPCAT_1:32;
then m2 is Morphism of o1,o2 by A1,A5,FUNCT_2:19;
hence thesis by A2,A4,A6;
end;
hence thesis by FUNCT_1:def 4;
end;
registration
let A;
cluster Yoneda A -> faithful;
coherence
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;
A2: x2 in Hom(o1,o2) by A1,CAT_1:def 5;
assume F.x1 = F.x2;
then [[<|cod x1,?>,<|dom x1,?>],<|x1,?>]=F.x2 by 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,?>];
then
[<|cod x1,?>,<|dom x1,?>,<|x1,?>] = [<|cod x2,?>,<|dom x2,?>,<|x2,?>];
then
A3: <|x1,?>= <|x2,?> by XTUPLE_0:3;
A4: x1 in Hom(o1,o2) by A1,CAT_1:def 5;
then
A5: dom x1 = o1 by CAT_1:1
.= dom x2 by A2,CAT_1:1;
cod x1 = o2 by A4,CAT_1:1
.= cod x2 by A2,CAT_1:1;
then [[Hom(cod x1,o2),Hom(dom x1,o2)],hom(x1,id o2)]= <|x2,?>.o2 by A5,A3
,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 A4,CAT_1:1;
then
[[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]= [[Hom(cod x2,o2),Hom(dom x2,
o2)],hom(x2,id o2)] by A4,CAT_1:1;
then
[[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]= [[Hom(o2,o2),Hom(dom x2,o2)]
,hom(x2,id o2)] by A2,CAT_1:1;
then
[[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]= [[Hom(o2,o2),Hom(o1,o2)],hom
(x2,id o2)] by A2,CAT_1:1;
then [[Hom(o2,o2),Hom(o1,o2)],hom(x1,id o2)]= [Hom(o2,o2),Hom(o1,o2),hom(
x2,id o2)];
then
A6: [Hom(o2,o2),Hom(o1,o2),hom(x1,id o2)]= [Hom(o2,o2),Hom(o1,o2),hom(x2,
id o2)];
reconsider dd=(id o2 ) as Morphism of A;
A7: Hom(o2,o2) <> {};
then
A8: (id o2)(*)dd =(id o2)*(id o2) by CAT_1:def 13;
id o2 in Hom(o2,o2) by CAT_1:27;
then id o2 in Hom(cod x2,o2) by A2,CAT_1:1;
then id o2 in Hom(cod x2,dom id o2);
then
A9: hom(x2,id o2).dd =((id o2)*(id o2))(*)(x2 qua Morphism of A)
by A8,ENS_1:def 23
.=(id o2)(*)(x2 qua Morphism of A)
.=(id o2)*x2 by A1,A7,CAT_1:def 13
.=x2 by A1,CAT_1:28;
id o2 in Hom(o2,o2) by CAT_1:27;
then id o2 in Hom(cod x1,o2) by A4,CAT_1:1;
then id o2 in Hom(cod x1,dom id o2);
then hom(x1,id o2).dd
=((id o2)*(id o2))(*)(x1 qua Morphism of A) by A8,ENS_1:def 23
.=(id o2)(*)(x1 qua Morphism of A)
.=(id o2)*x1 by A1,A7,CAT_1:def 13
.=x1 by A1,CAT_1:28;
hence thesis by A9,A6,XTUPLE_0:3;
end;
hence thesis;
end;
end;
registration
let A;
cluster Yoneda A -> one-to-one;
coherence
proof
set F = Yoneda A;
for x1,x2 be object 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 object;
assume that
A1: x1 in dom (Obj F) & x2 in dom (Obj F) and
A2: (Obj F).x1 = (Obj F).x2;
reconsider c =x1,c1=x2 as Object of A by A1,FUNCT_2:def 1;
reconsider f=id c1 as Morphism of c1,c1;
<|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 17;
<|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 17;
F.(id c1)= id d1
proof
set X= dom <|id c1,?>;
A3: for y being object st y in X holds (<|id c1,?>).y =(id <|c1,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
reconsider zz= id z as Morphism of z,z;
A4: Hom(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)]
.= [[Hom(c1,z),Hom(c1,z)],hom(id c1,id z)]
.= [[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)]
.= [[Hom(c1,dom id z),Hom(c1,cod id z)],hom(c1,id z)]
.= (<|c1,?> qua Function ).id z by ENS_1:def 21
.= (<|c1,?>)/.zz by A4,CAT_3:def 10
.= id (<|c1,?>.z) by NATTRA_1:15
.= (id <|c1,?> ).z by NATTRA_1:20
.= (id <|c1,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
dom <|id c1,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|c1,?> by FUNCT_2:def 1;
then
A5: <|id c1,?>= id <|c1,?> by A3,FUNCT_1:2;
F.(id c1) = [[<|cod id c1,?>,<|dom id c1,?>],<|id c1,?>] by Def4
.= [[<|c1,?>,<|dom id c1,?>],<|id c1,?>]
.= [[<|c1,?>,<|c1,?>],id <|c1,?>] by A5
.=id d1 by NATTRA_1:def 17;
hence thesis;
end;
then
A6: (Obj F).c1 = d1 by OPPCAT_1:30;
F.(id c)= id d
proof
set X= dom <|id c,?>;
A7: for y being object st y in X holds (<|id c,?>).y =(id <|c,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
reconsider zz= id z as Morphism of z,z;
A8: Hom(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)]
.= [[Hom(c,z),Hom(c,z)],hom(id c,id z)]
.= [[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)]
.= [[Hom(c,dom id z),Hom(c,cod id z)],hom(c,id z)]
.=(<|c,?> qua Function ).id z by ENS_1:def 21
.=(<|c,?>)/.zz by A8,CAT_3:def 10
.= id (<|c,?>.z) by NATTRA_1:15
.=(id <|c,?> ).z by NATTRA_1:20
.=(id <|c,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
dom <|id c,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|c,?> by FUNCT_2:def 1;
then
A9: <|id c,?>= id <|c,?> by A7,FUNCT_1:2;
F.(id c) = [[<|cod id c,?>,<|dom id c,?>],<|id c,?>] by Def4
.= [[<|c,?>,<|dom id c,?>],<|id c,?>]
.= [[<|c,?>,<|c,?>],id <|c,?>] by A9
.=id d by NATTRA_1:def 17;
hence thesis;
end;
then (Obj F).c = d by OPPCAT_1:30;
then [[Hom(c,dom f),Hom(c,cod f)],hom(c,f)]= (hom?-(c1)).f by A2,A6,
ENS_1:def 21;
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 21;
then
[Hom(c,dom f),Hom(c,cod f),hom(c,f)]= [[Hom(c1,dom f),Hom(c1,cod f)],
hom(c1,f)];
then [Hom(c,dom f),Hom(c,cod f),hom(c,f)]= [Hom(c1,dom f),Hom(c1,cod f),
hom(c1,f)];
then Hom(c,dom f)=Hom(c1,dom f) by XTUPLE_0:3;
then Hom(c,dom f)=Hom(c1,c1);
then
A10: Hom(c,c1)=Hom(c1,c1);
id c1 in Hom(c1,c1) by CAT_1:27;
then reconsider h=id c1 as Morphism of c,c1 by A10,CAT_1:def 5;
dom h = c by A10,CAT_1:5;
hence thesis;
end;
then Obj F is one-to-one by FUNCT_1:def 4;
hence thesis by Th5;
end;
end;
definition
let C,D be Category;
let T be Contravariant_Functor of C,D;
attr T is full means
for c,c9 being Object of C st Hom(T.c9,T.c) <> {}
for g being Morphism of T.c9,T.c holds Hom(c,c9) <> {} &
ex f being Morphism of c,c9 st g = T.f;
end;
::$N Yoneda Lemma
::$L https://en.wikipedia.org/wiki/Yoneda_lemma Yoneda Lemma
registration
let A;
cluster Yoneda A -> full;
coherence
proof
set F = Yoneda A;
for c,c9 being Object of A st Hom(F.c9,F.c) <> {} for g being Morphism
of F.c9,F.c holds Hom(c,c9) <> {} & ex f being Morphism of c,c9 st g = F.f
proof
let c,c9 be Object of A;
assume
A1: Hom(F.c9,F.c) <> {};
A2: <|c9,?>.c9 = (hom?-(Hom A,c9)).c9 by ENS_1:def 25
.= (Obj (hom?-(Hom A,c9))).c9
.= Hom(c9,c9) by ENS_1:60;
let g be Morphism of F.c9,F.c;
g in the carrier' of Functors(A,EnsHom A);
then g in NatTrans(A,EnsHom A) by NATTRA_1:def 17;
then consider
F1,F2 being Functor of A,EnsHom A, t being natural_transformation
of F1,F2 such that
A3: g = [[F1,F2],t] and
A4: F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;
A5: dom g =F1 by A3,NATTRA_1:33;
<|c9,?> in Funct(A,EnsHom(A)) by CAT_2:def 2;
then reconsider d1=<|c9,?> as Object of Functors(A,EnsHom(A)) by
NATTRA_1:def 17;
<|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 17;
A6: F.(id c)= id d
proof
set X= dom <|id c,?>;
A7: for y being object st y in X holds (<|id c,?>).y =(id <|c,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
reconsider zz= id z as Morphism of z,z;
A8: Hom(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)]
.= [[Hom(c,z),Hom(c,z)],hom(id c,id z)]
.= [[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)]
.= [[Hom(c,dom id z),Hom(c,cod id z)],hom(c,id z)]
.=(<|c,?> qua Function ).id z by ENS_1:def 21
.=(<|c,?>)/.zz by A8,CAT_3:def 10
.= id (<|c,?>.z) by NATTRA_1:15
.=(id <|c,?> ).z by NATTRA_1:20
.=(id <|c,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
dom <|id c,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|c,?> by FUNCT_2:def 1;
then
A9: <|id c,?>= id <|c,?> by A7,FUNCT_1:2;
F.(id c) = [[<|cod id c,?>,<|dom id c,?>],<|id c,?>] by Def4
.=[[<|c,?>,<|dom id c,?>],<|id c,?>]
.= [[<|c,?>,<|c,?>],id <|c,?>] by A9
.=id d by NATTRA_1:def 17;
hence thesis;
end;
then
A10: F.c = d by OPPCAT_1:30;
A11: F.(id c9)= id d1
proof
set X= dom <|id c9,?>;
A12: for y being object st y in X holds (<|id c9,?>).y =(id <|c9,?>).y
proof
let y be object;
assume y in X;
then reconsider z=y as Object of A by FUNCT_2:def 1;
reconsider zz= id z as Morphism of z,z;
A13: Hom(z,z) <> {};
(<|id c9,?>).z = [[Hom(cod id c9,z),Hom(dom id c9,z)],hom(id c9,
id z)] by Def3
.= [[Hom(c9,z),Hom(dom id c9,z)],hom(id c9,id z)]
.= [[Hom(c9,z),Hom(c9,z)],hom(id c9,id z)]
.= [[Hom(c9,z),Hom(c9,z)],hom(c9,id z)] by ENS_1:53
.= [[Hom(c9,z),Hom(c9,cod id z)],hom(c9,id z)]
.=[[Hom(c9,dom id z),Hom(c9,cod id z)],hom(c9,id z)]
.=(<|c9,?> qua Function ).id z by ENS_1:def 21
.=(<|c9,?>)/.zz by A13,CAT_3:def 10
.= id (<|c9,?>.z) by NATTRA_1:15
.=(id <|c9,?> ).z by NATTRA_1:20
.=(id <|c9,?> qua Function).z by NATTRA_1:def 5;
hence thesis by NATTRA_1:def 5;
end;
dom <|id c9,?> = the carrier of A by FUNCT_2:def 1
.= dom id <|c9,?> by FUNCT_2:def 1;
then
A14: <|id c9,?>= id <|c9,?> by A12,FUNCT_1:2;
F.(id c9) = [[<|cod id c9,?>,<|dom id c9,?>],<|id c9,?>] by Def4
.=[[<|c9,?>,<|dom id c9,?>],<|id c9,?>]
.= [[<|c9,?>,<|c9,?>],id <|c9,?>] by A14
.=id d1 by NATTRA_1:def 17;
hence thesis;
end;
then
A15: (Obj F).c9 = d1 by OPPCAT_1:30;
A16: cod g = F2 by A3,NATTRA_1:33;
then
A17: F2=F.c by A1,CAT_1:5;
A18: F.c9= d1 by A11,OPPCAT_1:30;
A19: <|c,?>.c9 = (hom?-(Hom A,c)).c9 by ENS_1:def 25
.= (Obj (hom?-(Hom A,c))).c9
.= Hom(c,c9) by ENS_1:60;
A20: dom g =F.c9 & cod g= F.c by A1,CAT_1:5;
then reconsider t as natural_transformation of <|c9,?>,<|c,?> by A5,A16,A11
,A10,OPPCAT_1:30;
(Obj F).c = d by A6,OPPCAT_1:30;
then <|c9,?> is_transformable_to <|c,?> by A4,A5,A16,A20,A18,NATTRA_1:def 7
;
then Hom(<|c9,?>.c9,<|c,?>.c9) <> {} by NATTRA_1:def 2;
then
A21: (t.c9) in Hom(<|c9,?>.c9,<|c,?>.c9) by CAT_1:def 5;
then
A22: cod (t.c9) =<|c,?>.c9 by CAT_1:1;
A23: EnsHom A = CatStr(# Hom A,Maps Hom A,fDom Hom A,fCod Hom A,fComp Hom
A #) by ENS_1:def 13;
then reconsider t1=t.c9 as Element of Maps Hom A;
A24: cod (t.c9) = (fCod Hom A).(t.c9) by A23
.= cod t1 by ENS_1:def 10;
t1 in Maps (dom t1,cod t1) by ENS_1:19;
then
A25: t1`2 in Funcs(dom t1,cod t1) by ENS_1:20;
A26: dom (t.c9) =<|c9,?>.c9 by A21,CAT_1:1;
then (the Source of EnsHom A).(t.c9) <> {} by A2;
then dom t1 <> {} by A23,ENS_1:def 9;
then
A27: cod t1 <> {} by A25;
then
A28: cod (t.c9) <> {} by A23,ENS_1:def 10;
hence Hom(c,c9) <> {} by A19,A21,CAT_1:1;
dom (t.c9) =(fDom Hom A).(t.c9) by A23
.= dom t1 by ENS_1:def 9;
then
A29: t1`2 is Function of <|c9,?>.c9,<|c,?>.c9 by A26,A22,A25,A24,FUNCT_2:66;
then
A30: dom t1`2 = Hom(c9,c9) by A2,A22,A28,FUNCT_2:def 1;
then id c9 in dom t1`2 by CAT_1:27;
then
A31: t1`2.id c9 in rng t1`2 by FUNCT_1:def 3;
rng t1`2 c= Hom(c,c9) by A19,A29,RELAT_1:def 19;
then t1`2.id c9 in Hom(c,c9) by A31;
then reconsider f = t1`2.id c9 as Morphism of c,c9 by CAT_1:def 5;
A32: <|c,?>.c9 <> {} by A22,A23,A27,ENS_1:def 10;
then
A33: dom f = c by A19,CAT_1:5;
take f;
A34: cod f = c9 by A19,A32,CAT_1:5;
A35: F1=F.c9 by A1,A5,CAT_1:5;
then
A36: <|c9,?> is_transformable_to <|c,?> by A4,A17,A15,A10,NATTRA_1:def 7;
for a being Object of A holds <|f,?>.a =t.a
proof
let a be Object of A;
A37: <|c,?>.a = (hom?-(Hom A,c)).a by ENS_1:def 25
.= (Obj (hom?-(Hom A,c))).a
.= Hom(c,a) by ENS_1:60;
reconsider ta1=t.a as Element of Maps Hom A by A23;
A38: <|c9,?>.a = (hom?-(Hom A,c9)).a by ENS_1:def 25
.= (Obj (hom?-(Hom A,c9))).a
.= Hom(c9,a) by ENS_1:60;
ta1 in Maps (dom ta1,cod ta1) by ENS_1:19;
then
A39: ta1`2 in Funcs(dom ta1,cod ta1) by ENS_1:20;
then
A40: ta1`2 is Function of dom ta1,cod ta1 by FUNCT_2:66;
set X=dom ta1`2;
A41: dom (t.a) =(fDom Hom A).(t.a) by A23
.= dom ta1 by ENS_1:def 9;
A42: Hom(<|c9,?>.a,<|c,?>.a) <> {} by A36,NATTRA_1:def 2;
then
A43: dom(t.a) =<|c9,?>.a by CAT_1:5;
A44: cod (t.a) =<|c,?>.a by A42,CAT_1:5;
A45: cod (t.a) = (fCod Hom A).(t.a) by A23
.= cod ta1 by ENS_1:def 10;
then
A46: ta1 =[[<|c9,?>.a,<|c,?>.a],ta1`2] by A43,A44,A41,ENS_1:8;
A47: ta1`2 is Function of dom(t.a),cod(t.a) by A41,A45,A39,FUNCT_2:66;
A48: dom ta1`2 = Hom(c9,a)
proof
per cases;
suppose
Hom(c9,a) = {};
hence thesis by A43,A41,A38,A40;
end;
suppose
Hom(c9,a) <> {};
then Hom(dom f,a) <> {} by A34,ENS_1:42;
hence thesis by A33,A43,A44,A38,A37,A47,FUNCT_2:def 1;
end;
end;
A49: for x be object st x in X holds hom(f,id a).x = ta1`2.x
proof
reconsider t1=t.c9 as Element of Maps Hom A by A23;
let x be object;
A50: f in Hom(c,cod f) by A33;
assume
A51: x in X;
then reconsider y = x as Morphism of cod f,a by A34,A48,CAT_1:def 5;
reconsider h=y as Morphism of c9,a by A19,A22,A28,CAT_1:5;
A52: dom h = c9 by A48,A51,CAT_1:5;
reconsider tc9=<|c9,?>.h as Element of Maps Hom A by A23;
A53: cod h =a by A48,A51,CAT_1:5;
reconsider tch=<|c,?>.h as Element of Maps Hom A by A23;
A54: [[Hom(c,dom h),Hom(c,cod h)],hom(c,h)] =(<|c,?> qua Function ).h
by ENS_1:def 21
.=(<|c,?>).h;
A55: [[Hom(c9,dom h),Hom(c9,cod h)],hom(c9,h)] =(<|c9,?> qua Function
).h by ENS_1:def 21
.=(<|c9,?>).h;
A56: cod (<|c9,?>.h) = (fCod Hom A).(<|c9,?>.h) by A23
.= cod tc9 by ENS_1:def 10;
then
A57: cod(<|c9,?>.h) =(tc9)`1`2 by ENS_1:def 4
.= [Hom(c9,dom h),Hom(c9,cod h)]`2 by A55
.=Hom(c9,cod h);
then
A58: [(t.a),(<|c9,?>.h)] in dom(the Comp of EnsHom A) by A43,A38,A53,
CAT_1:15;
tc9 in Maps (dom tc9,cod tc9) by ENS_1:19;
then
A59: tc9`2 in Funcs(dom tc9,cod tc9) by ENS_1:20;
A60: dom (<|c9,?>.h) =(fDom Hom A).(<|c9,?>.h) by A23
.= dom tc9 by ENS_1:def 9;
then dom (<|c9,?>.h) = (tc9)`1`1 by ENS_1:def 3
.= [Hom(c9,dom h),Hom(c9,cod h)]`1 by A55
.=Hom(c9,dom h);
then tc9`2 is Function of Hom(c9,dom h),Hom(c9,cod h) by A60,A56,A57
,A59,FUNCT_2:66;
then
A61: dom tc9`2 = Hom(c9,c9) by A48,A51,A52,A53,FUNCT_2:def 1;
A62: dom y =cod f by A34,A48,A51,CAT_1:5;
tch =[[dom tch,cod tch],tch`2] by ENS_1:8;
then [Hom(c,dom h),Hom(c,cod h),hom(c,h)]= [[dom tch,cod tch],tch`2]
by A54;
then [Hom(c,dom h),Hom(c,cod h),hom(c,h)]= [dom tch,cod tch,tch`2];
then
A63: hom(c,h)=tch`2 by XTUPLE_0:3;
tc9 =[[dom tc9,cod tc9],tc9`2] by ENS_1:8;
then [dom tc9,cod tc9,tc9`2] = [[Hom(c9,dom h),Hom(c9,cod h)],hom(c9,
h)] by A55;
then [dom tc9,cod tc9,tc9`2] = [Hom(c9,dom h),Hom(c9,cod h),hom(c9,h)
] ;
then
A64: tc9`2=hom(c9,h) by XTUPLE_0:3;
A65: Hom(<|c9,?>.c9,<|c,?>.c9) <> {} by A36,NATTRA_1:def 2;
then (t.c9) in Hom(<|c9,?>.c9,<|c,?>.c9) by CAT_1:def 5;
then
A66: cod (t.c9) = <|c,?>.c9 by CAT_1:1;
dom (<|c,?>.h) =(fDom Hom A).(<|c,?>.h) by A23
.= dom tch by ENS_1:def 9;
then dom (<|c,?>.h) = tch`1`1 by ENS_1:def 3
.=[Hom(c,dom h),Hom(c,cod h)]`1 by A54
.=Hom(c,dom h);
then
A67: [(<|c,?>.h),(t.c9)] in dom(the Comp of EnsHom A) by A19,A52,A66,
CAT_1:15;
cod (t.c9) = (fCod Hom A).(t.c9) by A23
.= cod t1 by ENS_1:def 10;
then
A68: cod t1=[Hom(c,dom h),Hom(c,cod h)]`1 by A19,A52,A66
.= tch`1`1 by A54
.=dom tch by ENS_1:def 3;
A69: h in Hom(c9,a) by A48,A51;
then
A70: <|c,?>/.h = <|c,?>.h by CAT_3:def 10;
Hom(<|c,?>.c9,<|c,?>.a ) <> {} by A48,A51,CAT_1:84;
then
A71: (<|c,?>/.h)*(t.c9)
=(<|c,?>.h)(*)(t.c9 qua Morphism of EnsHom A)
by A65,A70,CAT_1:def 13
.= (fComp Hom A).(tch,t1) by A23,A67,CAT_1:def 1
.= tch*t1 by A68,ENS_1:def 11
.= [[dom t1,cod tch],tch`2*t1`2] by A68,ENS_1:def 6;
A72: cod tc9=(tc9)`1`2 by ENS_1:def 4
.= [Hom(c9,dom h),Hom(c9,cod h)]`2 by A55
.= dom ta1 by A43,A41,A38,A53;
A73: <|c9,?>/.h = <|c9,?>.h by A69,CAT_3:def 10;
Hom(<|c9,?>.c9,<|c9,?>.a ) <> {} by A48,A51,CAT_1:84;
then
A74: (t.a)*(<|c9,?>/.h) = (t.a qua Morphism of EnsHom A)(*)(<|c9,?>.h)
by A42,A73,CAT_1:def 13
.= (fComp Hom A).(ta1,tc9) by A23,A58,CAT_1:def 1
.= ta1*tc9 by A72,ENS_1:def 11
.= [[dom tc9,cod ta1],ta1`2*tc9`2] by A72,ENS_1:def 6;
(t.a)*(<|c9,?>/.h) =(<|c,?>/.h)*(t.c9) by A4,A35,A17,A15,A10,A48,A51,
NATTRA_1:def 8;
then [dom tc9,cod ta1,(ta1`2*tc9`2)] = [[dom t1,cod tch],(tch`2*t1`2)
] by A74,A71;
then [dom tc9,cod ta1,(ta1`2*tc9`2)] = [dom t1,cod tch,(tch`2*t1`2)];
then
A75: ta1`2*tc9`2=tch`2*t1`2 by XTUPLE_0:3;
A76: id c9 in Hom(c9,cod f) by A34,CAT_1:27;
hom(f,id a).x =hom(f,a).y by ENS_1:53
.= y(*)f by A34,A48,A51,ENS_1:def 20
.= tch`2.(t1`2.id c9) by A62,A63,A50,ENS_1:def 19
.= (ta1`2*tc9`2).(id c9) by A30,A75,CAT_1:27,FUNCT_1:13
.= ta1`2.(hom(c9,h).id c9) by A64,A61,CAT_1:27,FUNCT_1:13
.= ta1`2.(y(*)id c9) by A62,A76,ENS_1:def 19
.= ta1`2.x by A34,A62,CAT_1:22;
hence thesis;
end;
dom hom(f,a) = Hom(cod f,a)
proof
per cases;
suppose Hom(cod f,a) = {};
hence thesis;
end;
suppose Hom(cod f,a) <> {};
then Hom(c,a) <> {} by A33,ENS_1:42;
hence thesis by A33,FUNCT_2:def 1;
end;
end;
then dom ta1`2 = dom hom(f,id a) by A34,A48,ENS_1:53;
then hom(f,id a)=ta1`2 by A49,FUNCT_1:2;
hence thesis by A33,A34,A38,A37,A46,Def3;
end;
then <|f,?> = t by A4,A35,A17,A15,A10,A33,A34,ISOCAT_1:26;
hence thesis by A3,A5,A16,A20,A15,A10,A33,A34,Def4;
end;
hence thesis;
end;
end;