:: YONEDA_1 semantic presentation

definition
let c1 be Category;
func EnsHom c1 -> Category equals :: YONEDA_1:def 1
 Ens (Hom a1);
correctness
coherence
Ens (Hom c1) is Category;
;
end;

:: deftheorem Def1 defines EnsHom YONEDA_1:def 1 :
for b1 being Category holds EnsHom b1 = Ens (Hom b1);

theorem Th1: :: YONEDA_1:1
for b1 being Category
for b2, b3 being Function
for b4, b5 being Morphism of (EnsHom b1) st cod b4 = dom b5 & [[(dom b4),(cod b4)],b2] = b4 & [[(dom b5),(cod b5)],b3] = b5 holds
[[(dom b4),(cod b5)],(b3 * b2)] = b5 * b4
proof end;

theorem Th2: :: YONEDA_1:2
for b1 being Category
for b2 being Object of b1 holds hom?- b2 is Functor of b1, EnsHom b1 by ENS_1:49;

definition
let c1 be Category;
let c2 be Object of c1;
func <|c2,?> -> Functor of a1, EnsHom a1 equals :: YONEDA_1:def 2
 hom?- a2;
coherence
hom?- c2 is Functor of c1, EnsHom c1 by Th2;
end;

:: deftheorem Def2 defines <| YONEDA_1:def 2 :
for b1 being Category
for b2 being Object of b1 holds <|b2,?> = hom?- b2;

theorem Th3: :: YONEDA_1:3
for b1 being Category
for b2 being Morphism of b1 holds <|(cod b2),?> is_naturally_transformable_to <|(dom b2),?>
proof end;

definition
let c1 be Category;
let c2 be Morphism of c1;
func <|c2,?> -> natural_transformation of <|(cod a2),?>,<|(dom a2),?> means :Def3: :: YONEDA_1:def 3
for b1 being Object of a1 holds a3 . b1 = [[(Hom (cod a2),b1),(Hom (dom a2),b1)],(hom a2,(id b1))];
existence
ex b1 being natural_transformation of <|(cod c2),?>,<|(dom c2),?> st
for b2 being Object of c1 holds b1 . b2 = [[(Hom (cod c2),b2),(Hom (dom c2),b2)],(hom c2,(id b2))]
proof end;
uniqueness
for b1, b2 being natural_transformation of <|(cod c2),?>,<|(dom c2),?> st ( for b3 being Object of c1 holds b1 . b3 = [[(Hom (cod c2),b3),(Hom (dom c2),b3)],(hom c2,(id b3))] ) & ( for b3 being Object of c1 holds b2 . b3 = [[(Hom (cod c2),b3),(Hom (dom c2),b3)],(hom c2,(id b3))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines <| YONEDA_1:def 3 :
for b1 being Category
for b2 being Morphism of b1
for b3 being natural_transformation of <|(cod b2),?>,<|(dom b2),?> holds
( b3 = <|b2,?> iff for b4 being Object of b1 holds b3 . b4 = [[(Hom (cod b2),b4),(Hom (dom b2),b4)],(hom b2,(id b4))] );

theorem Th4: :: YONEDA_1:4
for b1 being Category
for b2 being Element of the Morphisms of b1 holds [[<|(cod b2),?>,<|(dom b2),?>],<|b2,?>] is Element of the Morphisms of (Functors b1,(EnsHom b1))
proof end;

definition
let c1 be Category;
func Yoneda c1 -> Contravariant_Functor of a1, Functors a1,(EnsHom a1) means :Def4: :: YONEDA_1:def 4
for b1 being Morphism of a1 holds a2 . b1 = [[<|(cod b1),?>,<|(dom b1),?>],<|b1,?>];
existence
ex b1 being Contravariant_Functor of c1, Functors c1,(EnsHom c1) st
for b2 being Morphism of c1 holds b1 . b2 = [[<|(cod b2),?>,<|(dom b2),?>],<|b2,?>]
proof end;
uniqueness
for b1, b2 being Contravariant_Functor of c1, Functors c1,(EnsHom c1) st ( for b3 being Morphism of c1 holds b1 . b3 = [[<|(cod b3),?>,<|(dom b3),?>],<|b3,?>] ) & ( for b3 being Morphism of c1 holds b2 . b3 = [[<|(cod b3),?>,<|(dom b3),?>],<|b3,?>] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Yoneda YONEDA_1:def 4 :
for b1 being Category
for b2 being Contravariant_Functor of b1, Functors b1,(EnsHom b1) holds
( b2 = Yoneda b1 iff for b3 being Morphism of b1 holds b2 . b3 = [[<|(cod b3),?>,<|(dom b3),?>],<|b3,?>] );

definition
let c1, c2 be Category;
let c3 be Contravariant_Functor of c1,c2;
let c4 be Object of c1;
func c3 . c4 -> Object of a2 equals :: YONEDA_1:def 5
(Obj a3) . a4;
correctness
coherence
(Obj c3) . c4 is Object of c2;
;
end;

:: deftheorem Def5 defines . YONEDA_1:def 5 :
for b1, b2 being Category
for b3 being Contravariant_Functor of b1,b2
for b4 being Object of b1 holds b3 . b4 = (Obj b3) . b4;

theorem Th5: :: YONEDA_1:5
for b1 being Category
for b2 being Functor of b1, Functors b1,(EnsHom b1) st Obj b2 is one-to-one & b2 is faithful holds
b2 is one-to-one
proof end;

definition
let c1, c2 be Category;
let c3 be Contravariant_Functor of c1,c2;
attr a3 is faithful means :Def6: :: YONEDA_1:def 6
for b1, b2 being Object of a1 st Hom b1,b2 <> {} holds
for b3, b4 being Morphism of b1,b2 st a3 . b3 = a3 . b4 holds
b3 = b4;
end;

:: deftheorem Def6 defines faithful YONEDA_1:def 6 :
for b1, b2 being Category
for b3 being Contravariant_Functor of b1,b2 holds
( b3 is faithful iff for b4, b5 being Object of b1 st Hom b4,b5 <> {} holds
for b6, b7 being Morphism of b4,b5 st b3 . b6 = b3 . b7 holds
b6 = b7 );

theorem Th6: :: YONEDA_1:6
for b1 being Category
for b2 being Contravariant_Functor of b1, Functors b1,(EnsHom b1) st Obj b2 is one-to-one & b2 is faithful holds
b2 is one-to-one
proof end;

theorem Th7: :: YONEDA_1:7
for b1 being Category holds Yoneda b1 is faithful
proof end;

theorem Th8: :: YONEDA_1:8
for b1 being Category holds Yoneda b1 is one-to-one
proof end;

definition
let c1, c2 be Category;
let c3 be Contravariant_Functor of c1,c2;
attr a3 is full means :Def7: :: YONEDA_1:def 7
for b1, b2 being Object of a1 st Hom (a3 . b2),(a3 . b1) <> {} holds
for b3 being Morphism of a3 . b2,a3 . b1 holds
( Hom b1,b2 <> {} & ex b4 being Morphism of b1,b2 st b3 = a3 . b4 );
end;

:: deftheorem Def7 defines full YONEDA_1:def 7 :
for b1, b2 being Category
for b3 being Contravariant_Functor of b1,b2 holds
( b3 is full iff for b4, b5 being Object of b1 st Hom (b3 . b5),(b3 . b4) <> {} holds
for b6 being Morphism of b3 . b5,b3 . b4 holds
( Hom b4,b5 <> {} & ex b7 being Morphism of b4,b5 st b6 = b3 . b7 ) );

theorem Th9: :: YONEDA_1:9
for b1 being Category holds Yoneda b1 is full
proof end;