let A be Category; for o, m being set holds Functors ((1Cat (o,m)),A) ~= A
let o, m be set ; Functors ((1Cat (o,m)),A) ~= A
reconsider a = o as Object of (1Cat (o,m)) by TARSKI:def 1;
take F = a |-> A; ISOCAT_1:def 4 F is isomorphic
now for x, y being object st x in the carrier' of (Functors ((1Cat (o,m)),A)) & y in the carrier' of (Functors ((1Cat (o,m)),A)) & F . x = F . y holds
x = ylet x,
y be
object ;
( x in the carrier' of (Functors ((1Cat (o,m)),A)) & y in the carrier' of (Functors ((1Cat (o,m)),A)) & F . x = F . y implies x = y )A1:
the
carrier' of
(Functors ((1Cat (o,m)),A)) = NatTrans (
(1Cat (o,m)),
A)
by NATTRA_1:def 17;
assume
x in the
carrier' of
(Functors ((1Cat (o,m)),A))
;
( y in the carrier' of (Functors ((1Cat (o,m)),A)) & F . x = F . y implies x = y )then consider F1,
F2 being
Functor of
1Cat (
o,
m),
A,
t being
natural_transformation of
F1,
F2 such that A2:
x = [[F1,F2],t]
and A3:
F1 is_naturally_transformable_to F2
by A1, NATTRA_1:def 16;
assume
y in the
carrier' of
(Functors ((1Cat (o,m)),A))
;
( F . x = F . y implies x = y )then consider F19,
F29 being
Functor of
1Cat (
o,
m),
A,
t9 being
natural_transformation of
F19,
F29 such that A4:
y = [[F19,F29],t9]
and A5:
F19 is_naturally_transformable_to F29
by A1, NATTRA_1:def 16;
assume
F . x = F . y
;
x = ythen A6:
t . a =
F . y
by A2, A3, Def1
.=
t9 . a
by A4, A5, Def1
;
reconsider G1 =
F1,
G19 =
F19,
G2 =
F2,
G29 =
F29 as
Function of
{m}, the
carrier' of
A ;
reconsider s =
t,
s9 =
t9 as
Function of
{a}, the
carrier' of
A ;
A7:
id a = m
by TARSKI:def 1;
A8:
F1 is_transformable_to F2
by A3;
then A9:
Hom (
(F1 . a),
(F2 . a))
<> {}
;
A10:
F19 is_transformable_to F29
by A5;
then A11:
Hom (
(F19 . a),
(F29 . a))
<> {}
;
then
F1 . a = F19 . a
by A6, A9, CAT_1:6;
then G1 . (id a) =
id (F19 . a)
by CAT_1:71
.=
G19 . (id a)
by CAT_1:71
;
then A12:
F1 = F19
by A7, FUNCT_2:125;
F2 . a = F29 . a
by A6, A9, A11, CAT_1:6;
then G2 . (id a) =
id (F29 . a)
by CAT_1:71
.=
G29 . (id a)
by CAT_1:71
;
then A13:
F2 = F29
by A7, FUNCT_2:125;
s . a =
t9 . a
by A8, A6, NATTRA_1:def 5
.=
s9 . a
by A10, NATTRA_1:def 5
;
hence
x = y
by A2, A4, A12, A13, FUNCT_2:125;
verum end;
hence
F is one-to-one
by FUNCT_2:19; ISOCAT_1:def 3 rng F = the carrier' of A
thus
rng F c= the carrier' of A
; XBOOLE_0:def 10 the carrier' of A c= rng F
let x be object ; TARSKI:def 3 ( not x in the carrier' of A or x in rng F )
assume
x in the carrier' of A
; x in rng F
then reconsider f = x as Morphism of A ;
reconsider F1 = {m} --> (id (dom f)), F2 = {m} --> (id (cod f)) as Function of the carrier' of (1Cat (o,m)), the carrier' of A ;
( ( for c being Object of (1Cat (o,m)) ex d being Object of A st F1 . (id c) = id d ) & ( for c being Object of (1Cat (o,m)) ex d being Object of A st F2 . (id c) = id d ) )
by FUNCOP_1:7;
then reconsider F1 = F1, F2 = F2 as Functor of 1Cat (o,m),A by A14, A15, A19, A17, CAT_1:61;
reconsider t = {a} --> f as Function of the carrier of (1Cat (o,m)), the carrier' of A ;
A20:
for b being Object of (1Cat (o,m)) holds
( F1 . b = dom f & F2 . b = cod f )
then A25:
F1 is_transformable_to F2
;
then reconsider t = t as transformation of F1,F2 by A22, NATTRA_1:def 3;
A26:
for b being Object of (1Cat (o,m)) holds t . b = f
A27:
now for b1, b2 being Object of (1Cat (o,m)) st Hom (b1,b2) <> {} holds
for g being Morphism of b1,b2 holds (t . b2) * (F1 /. g) = (F2 /. g) * (t . b1)let b1,
b2 be
Object of
(1Cat (o,m));
( Hom (b1,b2) <> {} implies for g being Morphism of b1,b2 holds (t . b2) * (F1 /. g) = (F2 /. g) * (t . b1) )assume A28:
Hom (
b1,
b2)
<> {}
;
for g being Morphism of b1,b2 holds (t . b2) * (F1 /. g) = (F2 /. g) * (t . b1)A29:
Hom (
(F2 . b1),
(F2 . b2))
<> {}
by A28, CAT_1:82;
let g be
Morphism of
b1,
b2;
(t . b2) * (F1 /. g) = (F2 /. g) * (t . b1)A30:
(
t . b1 = f &
Hom (
(F1 . b1),
(F2 . b1))
<> {} )
by A24, A26;
A31:
Hom (
(F1 . b1),
(F1 . b2))
<> {}
by A28, CAT_1:82;
A32:
m in {m}
by TARSKI:def 1;
A33:
g = m
by TARSKI:def 1;
then A34:
F2 /. g =
F2 . m
by A28, CAT_3:def 10
.=
id (cod f)
by A32, FUNCOP_1:7
;
A35:
F1 /. g =
F1 . m
by A28, A33, CAT_3:def 10
.=
id (dom f)
by A32, FUNCOP_1:7
;
(
t . b2 = f &
Hom (
(F1 . b2),
(F2 . b2))
<> {} )
by A24, A26;
hence (t . b2) * (F1 /. g) =
f (*) (F1 /. g)
by A31, CAT_1:def 13
.=
f
by A35, CAT_1:22
.=
(F2 /. g) (*) f
by A34, CAT_1:21
.=
(F2 /. g) * (t . b1)
by A30, A29, CAT_1:def 13
;
verum end;
F1 is_transformable_to F2
by A24;
then A36:
F1 is_naturally_transformable_to F2
by A27;
then reconsider t = t as natural_transformation of F1,F2 by A27, NATTRA_1:def 8;
[[F1,F2],t] in NatTrans ((1Cat (o,m)),A)
by A36, NATTRA_1:def 16;
then A37:
[[F1,F2],t] in the carrier' of (Functors ((1Cat (o,m)),A))
by NATTRA_1:def 17;
F . [[F1,F2],t] =
t . a
by A36, Def1
.=
f
by A26
;
hence
x in rng F
by A37, FUNCT_2:4; verum