:: by Miros{\l}aw Wojciechowski

::

:: Received June 12, 1997

:: Copyright (c) 1997-2019 Association of Mizar Users

theorem Th1: :: YONEDA_1:1

for A being Category

for f, g being Function

for 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

for f, g being Function

for 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 end;

definition
end;

:: deftheorem defines <| YONEDA_1:def 2 :

for A being Category

for a being Object of A holds <|a,?> = hom?- a;

for A being Category

for a being Object of A holds <|a,?> = hom?- a;

theorem Th2: :: YONEDA_1:2

for A being Category

for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>

for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>

proof end;

definition

let A be Category;

let f be Morphism of A;

ex b_{1} being natural_transformation of <|(cod f),?>,<|(dom f),?> st

for o being Object of A holds b_{1} . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]

for b_{1}, b_{2} being natural_transformation of <|(cod f),?>,<|(dom f),?> st ( for o being Object of A holds b_{1} . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) & ( for o being Object of A holds b_{2} . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) holds

b_{1} = b_{2}

end;
let f be Morphism of A;

func <|f,?> -> natural_transformation of <|(cod f),?>,<|(dom f),?> means :Def3: :: YONEDA_1:def 3

for o being Object of A holds it . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))];

existence for o being Object of A holds it . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))];

ex b

for o being Object of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines <| YONEDA_1:def 3 :

for A being Category

for f being Morphism of A

for b_{3} being natural_transformation of <|(cod f),?>,<|(dom f),?> holds

( b_{3} = <|f,?> iff for o being Object of A holds b_{3} . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] );

for A being Category

for f being Morphism of A

for b

( b

theorem Th3: :: YONEDA_1:3

for A being Category

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)))

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 end;

definition

let A be Category;

ex b_{1} being Contravariant_Functor of A, Functors (A,(EnsHom A)) st

for f being Morphism of A holds b_{1} . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]

for b_{1}, b_{2} being Contravariant_Functor of A, Functors (A,(EnsHom A)) st ( for f being Morphism of A holds b_{1} . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds b_{2} . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds

b_{1} = b_{2}

end;
func Yoneda A -> Contravariant_Functor of A, Functors (A,(EnsHom A)) means :Def4: :: YONEDA_1:def 4

for f being Morphism of A holds it . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>];

existence for f being Morphism of A holds it . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>];

ex b

for f being Morphism of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines Yoneda YONEDA_1:def 4 :

for A being Category

for b_{2} being Contravariant_Functor of A, Functors (A,(EnsHom A)) holds

( b_{2} = Yoneda A iff for f being Morphism of A holds b_{2} . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] );

for A being Category

for b

( b

definition

let A, B be Category;

let F be Contravariant_Functor of A,B;

let c be Object of A;

correctness

coherence

(Obj F) . c is Object of B;

;

end;
let F be Contravariant_Functor of A,B;

let c be Object of A;

correctness

coherence

(Obj F) . c is Object of B;

;

:: deftheorem defines . YONEDA_1:def 5 :

for A, B being Category

for F being Contravariant_Functor of A,B

for c being Object of A holds F . c = (Obj F) . c;

for A, B being Category

for F being Contravariant_Functor of A,B

for c being Object of A holds F . c = (Obj F) . c;

theorem :: YONEDA_1:4

for A being Category

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

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 end;

:: deftheorem defines faithful YONEDA_1:def 6 :

for C, D being Category

for T being Contravariant_Functor of C,D holds

( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds

f1 = f2 );

for C, D being Category

for T being Contravariant_Functor of C,D holds

( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds

for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds

f1 = f2 );

theorem Th5: :: YONEDA_1:5

for A being Category

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

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 end;

registration
end;

registration
end;

:: deftheorem defines full YONEDA_1:def 7 :

for C, D being Category

for T being Contravariant_Functor of C,D holds

( T is full iff for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds

for g being Morphism of T . c9,T . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

for C, D being Category

for T being Contravariant_Functor of C,D holds

( T is full iff for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds

for g being Morphism of T . c9,T . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

registration
end;