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 :: thesis: 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 = y
let x, y be object ; :: 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 17;
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] 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)) ; :: thesis: ( 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 ; :: thesis: x = y
then 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; :: thesis: verum
end;
hence F is one-to-one by FUNCT_2:19; :: 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 object ; :: 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 ;
A14: now :: thesis: for g being Morphism of (1Cat (o,m)) holds
( F1 . (id (dom g)) = id (dom (F1 . g)) & F1 . (id (cod g)) = id (cod (F1 . g)) )
let g be Morphism of (1Cat (o,m)); :: thesis: ( F1 . (id (dom g)) = id (dom (F1 . g)) & F1 . (id (cod g)) = id (cod (F1 . g)) )
thus F1 . (id (dom g)) = id (dom f) by FUNCOP_1:7
.= id (dom (id (dom f)))
.= id (dom (F1 . g)) by FUNCOP_1:7 ; :: thesis: F1 . (id (cod g)) = id (cod (F1 . g))
thus F1 . (id (cod g)) = id (dom f) by FUNCOP_1:7
.= id (cod (id (dom f)))
.= id (cod (F1 . g)) by FUNCOP_1:7 ; :: thesis: verum
end;
A15: now :: thesis: for h, g being Morphism of (1Cat (o,m)) st dom g = cod h holds
F1 . (g (*) h) = (F1 . g) (*) (F1 . h)
let h, g be Morphism of (1Cat (o,m)); :: thesis: ( dom g = cod h implies F1 . (g (*) h) = (F1 . g) (*) (F1 . h) )
assume dom g = cod h ; :: thesis: F1 . (g (*) h) = (F1 . g) (*) (F1 . h)
A16: Hom ((dom f),(dom f)) <> {} ;
thus F1 . (g (*) h) = id (dom f) by FUNCOP_1:7
.= (id (dom f)) * (id (dom f))
.= (id (dom f)) (*) (id (dom f)) by A16, CAT_1:def 13
.= (id (dom f)) (*) (F1 . h) by FUNCOP_1:7
.= (F1 . g) (*) (F1 . h) by FUNCOP_1:7 ; :: thesis: verum
end;
A17: now :: thesis: for h, g being Morphism of (1Cat (o,m)) st dom g = cod h holds
F2 . (g (*) h) = (F2 . g) (*) (F2 . h)
let h, g be Morphism of (1Cat (o,m)); :: thesis: ( dom g = cod h implies F2 . (g (*) h) = (F2 . g) (*) (F2 . h) )
assume dom g = cod h ; :: thesis: F2 . (g (*) h) = (F2 . g) (*) (F2 . h)
A18: Hom ((cod f),(cod f)) <> {} ;
thus F2 . (g (*) h) = id (cod f) by FUNCOP_1:7
.= (id (cod f)) * (id (cod f))
.= (id (cod f)) (*) (id (cod f)) by A18, CAT_1:def 13
.= (id (cod f)) (*) (F2 . h) by FUNCOP_1:7
.= (F2 . g) (*) (F2 . h) by FUNCOP_1:7 ; :: thesis: verum
end;
A19: now :: thesis: for g being Morphism of (1Cat (o,m)) holds
( F2 . (id (dom g)) = id (dom (F2 . g)) & F2 . (id (cod g)) = id (cod (F2 . g)) )
let g be Morphism of (1Cat (o,m)); :: thesis: ( F2 . (id (dom g)) = id (dom (F2 . g)) & F2 . (id (cod g)) = id (cod (F2 . g)) )
thus F2 . (id (dom g)) = id (cod f) by FUNCOP_1:7
.= id (dom (id (cod f)))
.= id (dom (F2 . g)) by FUNCOP_1:7 ; :: thesis: F2 . (id (cod g)) = id (cod (F2 . g))
thus F2 . (id (cod g)) = id (cod f) by FUNCOP_1:7
.= id (cod (id (cod f)))
.= id (cod (F2 . g)) by FUNCOP_1:7 ; :: thesis: verum
end;
( ( 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 )
proof
let b be Object of (1Cat (o,m)); :: thesis: ( F1 . b = dom f & F2 . b = cod f )
F2 . (id b) = id (cod f) by FUNCOP_1:7;
then A21: id (F2 . b) = id (cod f) by CAT_1:71;
F1 . (id b) = id (dom f) by FUNCOP_1:7;
then id (F1 . b) = id (dom f) by CAT_1:71;
hence ( F1 . b = dom f & F2 . b = cod f ) by A21, CAT_1:59; :: thesis: verum
end;
A22: now :: thesis: for b being Object of (1Cat (o,m)) holds t . b is Morphism of F1 . b,F2 . b
let b be Object of (1Cat (o,m)); :: thesis: t . b is Morphism of F1 . b,F2 . b
A23: F2 . b = cod f by A20;
( t . b = f & F1 . b = dom f ) by A20, FUNCOP_1:7;
then t . b in Hom ((F1 . b),(F2 . b)) by A23;
hence t . b is Morphism of F1 . b,F2 . b by CAT_1:def 5; :: thesis: verum
end;
A24: now :: thesis: for b being Object of (1Cat (o,m)) holds Hom ((F1 . b),(F2 . b)) <> {}
let b be Object of (1Cat (o,m)); :: thesis: Hom ((F1 . b),(F2 . b)) <> {}
( F1 . b = dom f & F2 . b = cod f ) by A20;
hence Hom ((F1 . b),(F2 . b)) <> {} by CAT_1:2; :: thesis: verum
end;
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
proof
let b be Object of (1Cat (o,m)); :: thesis: t . b = f
thus f = ({a} --> f) . b by FUNCOP_1:7
.= t . b by A25, NATTRA_1:def 5 ; :: thesis: verum
end;
A27: now :: thesis: 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)); :: thesis: ( 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) <> {} ; :: thesis: 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; :: thesis: (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 ;
:: thesis: 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; :: thesis: verum