let A be Category; :: thesis: for o, m being set holds Functors (1Cat o,m),A ~= A
let o, m be set ; :: thesis: Functors (1Cat o,m),A ~= A
reconsider a = o as Object of (1Cat o,m) by TARSKI:def 1;
take F = a |-> A; :: according to ISOCAT_1:def 4 :: thesis: F is isomorphic
now let x,
y be
set ;
:: thesis: ( 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 18;
assume
x in the
carrier' of
(Functors (1Cat o,m),A)
;
:: thesis: ( 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] &
F1 is_naturally_transformable_to F2 )
by A1, NATTRA_1:def 16;
assume
y in the
carrier' of
(Functors (1Cat o,m),A)
;
:: thesis: ( 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 A3:
(
y = [[F1',F2'],t'] &
F1' is_naturally_transformable_to F2' )
by A1, NATTRA_1:def 16;
reconsider s =
t,
s' =
t' as
Function of
{a},the
carrier' of
A ;
reconsider G1 =
F1,
G1' =
F1',
G2 =
F2,
G2' =
F2' as
Function of
{m},the
carrier' of
A ;
A4:
(
F1 is_transformable_to F2 &
F1' is_transformable_to F2' )
by A2, A3, NATTRA_1:def 7;
assume
F . x = F . y
;
:: thesis: x = ythen A5:
t . a =
F . y
by A2, Def1
.=
t' . a
by A3, Def1
;
then A6:
s . a =
t' . a
by A4, NATTRA_1:def 5
.=
s' . a
by A4, NATTRA_1:def 5
;
A7:
id a = m
by TARSKI:def 1;
(
Hom (F1 . a),
(F2 . a) <> {} &
Hom (F1' . a),
(F2' . a) <> {} )
by A4, NATTRA_1:def 2;
then A8:
(
F1 . a = F1' . a &
F2 . a = F2' . a )
by A5, CAT_1:24;
then A9:
G1 . (id a) =
id (F1' . a)
by CAT_1:108
.=
G1' . (id a)
by CAT_1:108
;
G2 . (id a) =
id (F2' . a)
by A8, CAT_1:108
.=
G2' . (id a)
by CAT_1:108
;
then
(
F1 = F1' &
F2 = F2' )
by A7, A9, Th3;
hence
x = y
by A2, A3, A6, Th3;
:: thesis: verum end;
hence
F is one-to-one
by FUNCT_2:25; :: according to ISOCAT_1:def 3 :: thesis: rng F = the carrier' of A
thus
rng F c= the carrier' of A
; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of A c= rng F
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of A or x in rng F )
assume
x in the carrier' of A
; :: thesis: 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 ;
A13:
for c being Object of (1Cat o,m) ex d being Object of A st F1 . (id c) = id d
by FUNCOP_1:13;
A17:
for c being Object of (1Cat o,m) ex d being Object of A st F2 . (id c) = id d
by FUNCOP_1:13;
then reconsider F1 = F1, F2 = F2 as Functor of 1Cat o,m,A by A13, A14, A15, A17, A18, CAT_1:96;
A20:
for b being Object of (1Cat o,m) holds
( F1 . b = dom f & F2 . b = cod f )
then A22:
F1 is_transformable_to F2
by NATTRA_1:def 2;
reconsider t = {a} --> f as Function of the carrier of (1Cat o,m),the carrier' of A ;
then reconsider t = t as transformation of F1,F2 by A22, NATTRA_1:def 3;
A25:
for b being Object of (1Cat o,m) holds t . b = f
A26:
now let b1,
b2 be
Object of
(1Cat o,m);
:: thesis: ( Hom b1,b2 <> {} implies for g being Morphism of b1,b2 holds (t . b2) * (F1 . g) = (F2 . g) * (t . b1) )assume A27:
Hom b1,
b2 <> {}
;
:: thesis: for g being Morphism of b1,b2 holds (t . b2) * (F1 . g) = (F2 . g) * (t . b1)let g be
Morphism of
b1,
b2;
:: thesis: (t . b2) * (F1 . g) = (F2 . g) * (t . b1)A28:
t . b1 = f
by A25;
A29:
t . b2 = f
by A25;
A30:
g = m
by TARSKI:def 1;
A31:
m in {m}
by TARSKI:def 1;
A32:
(
Hom (F1 . b1),
(F2 . b1) <> {} &
Hom (F2 . b1),
(F2 . b2) <> {} )
by A21, A27, CAT_1:124;
A33:
(
Hom (F1 . b2),
(F2 . b2) <> {} &
Hom (F1 . b1),
(F1 . b2) <> {} )
by A21, A27, CAT_1:124;
A34:
F2 . g =
F2 . m
by A27, A30, NATTRA_1:def 1
.=
id (cod f)
by A31, FUNCOP_1:13
;
A35:
F1 . g =
F1 . m
by A27, A30, NATTRA_1:def 1
.=
id (dom f)
by A31, FUNCOP_1:13
;
thus (t . b2) * (F1 . g) =
f * (F1 . g)
by A29, A33, CAT_1:def 13
.=
f
by A35, CAT_1:47
.=
(F2 . g) * f
by A34, CAT_1:46
.=
(F2 . g) * (t . b1)
by A28, A32, CAT_1:def 13
;
:: thesis: verum end;
A36:
F1 is_naturally_transformable_to F2
proof
thus
F1 is_transformable_to F2
by A21, NATTRA_1:def 2;
:: according to NATTRA_1:def 7 :: thesis: ex b1 being transformation of F1,F2 st
for b2, b3 being Element of the carrier of (1Cat o,m) holds
( Hom b2,b3 = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (F1 . b4) = (F2 . b4) * (b1 . b2) )
thus
ex
b1 being
transformation of
F1,
F2 st
for
b2,
b3 being
Element of the
carrier of
(1Cat o,m) holds
(
Hom b2,
b3 = {} or for
b4 being
Morphism of
b2,
b3 holds
(b1 . b3) * (F1 . b4) = (F2 . b4) * (b1 . b2) )
by A26;
:: thesis: verum
end;
then reconsider t = t as natural_transformation of F1,F2 by A26, 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 18;
F . [[F1,F2],t] =
t . a
by A36, Def1
.=
f
by A25
;
hence
x in rng F
by A37, FUNCT_2:6; :: thesis: verum