:: ISOCAT_2 semantic presentation
begin
definition
let A, B, C be non empty set ;
let f be Function of A,(Funcs (B,C));
:: original: uncurry
redefine func uncurry f -> Function of [:A,B:],C;
coherence
uncurry f is Function of [:A,B:],C
proof
A1: rng f c= Funcs (B,C) ;
dom (uncurry f) = [:(dom f),B:] by A1, FUNCT_5:26
.= [:A,B:] by FUNCT_2:def_1 ;
hence uncurry f is Function of [:A,B:],C ; ::_thesis: verum
end;
end;
theorem Th1: :: ISOCAT_2:1
for A, B, C being non empty set
for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f
proof
let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f
let f be Function of A,(Funcs (B,C)); ::_thesis: curry (uncurry f) = f
rng f c= Funcs (B,C) ;
hence curry (uncurry f) = f by FUNCT_5:48; ::_thesis: verum
end;
theorem Th2: :: ISOCAT_2:2
for A, B, C being non empty set
for f being Function of A,(Funcs (B,C))
for a being Element of A
for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b
proof
let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C))
for a being Element of A
for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b
let f be Function of A,(Funcs (B,C)); ::_thesis: for a being Element of A
for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b
let a be Element of A; ::_thesis: for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b
let b be Element of B; ::_thesis: (uncurry f) . (a,b) = (f . a) . b
( dom f = A & dom (f . a) = B ) by FUNCT_2:def_1;
hence (uncurry f) . (a,b) = (f . a) . b by FUNCT_5:38; ::_thesis: verum
end;
theorem :: ISOCAT_2:3
canceled;
theorem :: ISOCAT_2:4
canceled;
theorem Th5: :: ISOCAT_2:5
for A being Category
for f being Morphism of A holds (id (cod f)) (*) f = f
proof
let A be Category; ::_thesis: for f being Morphism of A holds (id (cod f)) (*) f = f
let f be Morphism of A; ::_thesis: (id (cod f)) (*) f = f
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
A1: Hom ((dom f),(cod f)) <> {} by CAT_1:2;
Hom ((cod f),(cod f)) <> {} ;
hence (id (cod f)) (*) f = (id (cod f)) * f9 by A1, CAT_1:def_13
.= f by A1, CAT_1:28 ;
::_thesis: verum
end;
theorem Th6: :: ISOCAT_2:6
for A being Category
for f being Morphism of A holds f (*) (id (dom f)) = f
proof
let A be Category; ::_thesis: for f being Morphism of A holds f (*) (id (dom f)) = f
let f be Morphism of A; ::_thesis: f (*) (id (dom f)) = f
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
A1: Hom ((dom f),(cod f)) <> {} by CAT_1:2;
Hom ((dom f),(dom f)) <> {} ;
hence f (*) (id (dom f)) = f9 * (id (dom f)) by A1, CAT_1:def_13
.= f by A1, CAT_1:29 ;
::_thesis: verum
end;
theorem Th7: :: ISOCAT_2:7
for A, B being Category
for o being set holds
( o is Object of (Functors (A,B)) iff o is Functor of A,B )
proof
let A, B be Category; ::_thesis: for o being set holds
( o is Object of (Functors (A,B)) iff o is Functor of A,B )
let o be set ; ::_thesis: ( o is Object of (Functors (A,B)) iff o is Functor of A,B )
the carrier of (Functors (A,B)) = Funct (A,B) by NATTRA_1:def_17;
hence ( o is Object of (Functors (A,B)) iff o is Functor of A,B ) by CAT_2:def_2; ::_thesis: verum
end;
theorem Th8: :: ISOCAT_2:8
for A, B being Category
for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] )
proof
let A, B be Category; ::_thesis: for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] )
let m be Morphism of (Functors (A,B)); ::_thesis: ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( F1 is_naturally_transformable_to F2 & dom m = F1 & cod m = F2 & m = [[F1,F2],t] )
( Hom ((dom m),(cod m)) <> {} & m is Morphism of dom m, cod m ) by CAT_1:2, CAT_1:4;
then consider F, F1 being Functor of A,B, t being natural_transformation of F,F1 such that
A1: ( dom m = F & cod m = F1 ) and
A2: m = [[F,F1],t] by NATTRA_1:34;
take F ; ::_thesis: ex F2 being Functor of A,B ex t being natural_transformation of F,F2 st
( F is_naturally_transformable_to F2 & dom m = F & cod m = F2 & m = [[F,F2],t] )
take F1 ; ::_thesis: ex t being natural_transformation of F,F1 st
( F is_naturally_transformable_to F1 & dom m = F & cod m = F1 & m = [[F,F1],t] )
take t ; ::_thesis: ( F is_naturally_transformable_to F1 & dom m = F & cod m = F1 & m = [[F,F1],t] )
the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17;
hence F is_naturally_transformable_to F1 by A2, NATTRA_1:32; ::_thesis: ( dom m = F & cod m = F1 & m = [[F,F1],t] )
thus ( dom m = F & cod m = F1 & m = [[F,F1],t] ) by A1, A2; ::_thesis: verum
end;
begin
definition
let A, B be Category;
let a be Object of A;
funca |-> B -> Functor of Functors (A,B),B means :Def1: :: ISOCAT_2:def 1
for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
it . [[F1,F2],t] = t . a;
existence
ex b1 being Functor of Functors (A,B),B st
for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
b1 . [[F1,F2],t] = t . a
proof
defpred S1[ set , set ] means for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = t . a;
A1: the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17;
A2: now__::_thesis:_for_x_being_Element_of_NatTrans_(A,B)_ex_b_being_Morphism_of_B_st_S1[x,b]
let x be Element of NatTrans (A,B); ::_thesis: ex b being Morphism of B st S1[x,b]
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A3: x = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by NATTRA_1:def_16;
reconsider b = t . a as Morphism of B ;
take b = b; ::_thesis: S1[x,b]
thus S1[x,b] ::_thesis: verum
proof
let F19, F29 be Functor of A,B; ::_thesis: for t being natural_transformation of F19,F29 st x = [[F19,F29],t] holds
b = t . a
let t9 be natural_transformation of F19,F29; ::_thesis: ( x = [[F19,F29],t9] implies b = t9 . a )
assume A4: x = [[F19,F29],t9] ; ::_thesis: b = t9 . a
then [F1,F2] = [F19,F29] by A3, XTUPLE_0:1;
then ( F1 = F19 & F2 = F29 ) by XTUPLE_0:1;
hence b = t9 . a by A3, A4, XTUPLE_0:1; ::_thesis: verum
end;
end;
consider f being Function of (NatTrans (A,B)), the carrier' of B such that
A5: for x being Element of NatTrans (A,B) holds S1[x,f . x] from FUNCT_2:sch_3(A2);
A6: the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17;
then reconsider ff = f as Function of the carrier' of (Functors (A,B)), the carrier' of B ;
A7: now__::_thesis:_for_c_being_Object_of_(Functors_(A,B))_ex_d_being_Element_of_the_carrier_of_B_st_f_._(id_c)_=_id_d
let c be Object of (Functors (A,B)); ::_thesis: ex d being Element of the carrier of B st f . (id c) = id d
reconsider F = c as Functor of A,B by Th7;
take d = F . a; ::_thesis: f . (id c) = id d
A8: [[F,F],(id F)] is Morphism of (Functors (A,B)) by A6, NATTRA_1:def_16;
thus f . (id c) = f . [[F,F],(id F)] by NATTRA_1:def_17
.= (id F) . a by A5, A6, A8
.= id d by NATTRA_1:20 ; ::_thesis: verum
end;
A9: now__::_thesis:_for_m1,_m2_being_Morphism_of_(Functors_(A,B))_st_[m2,m1]_in_dom_the_Comp_of_(Functors_(A,B))_holds_
ff_._(m2_(*)_m1)_=_(ff_._m2)_(*)_(ff_._m1)
let m1, m2 be Morphism of (Functors (A,B)); ::_thesis: ( [m2,m1] in dom the Comp of (Functors (A,B)) implies ff . (m2 (*) m1) = (ff . m2) (*) (ff . m1) )
assume A10: [m2,m1] in dom the Comp of (Functors (A,B)) ; ::_thesis: ff . (m2 (*) m1) = (ff . m2) (*) (ff . m1)
reconsider m19 = m1, m29 = m2 as Element of NatTrans (A,B) by NATTRA_1:def_17;
consider F, F1 being Functor of A,B, t being natural_transformation of F,F1 such that
A11: F is_naturally_transformable_to F1 and
dom m1 = F and
cod m1 = F1 and
A12: m1 = [[F,F1],t] by Th8;
A13: Hom ((F . a),(F1 . a)) <> {} by A11, ISOCAT_1:25;
A14: f . m19 = t . a by A5, A12;
consider F19, F2 being Functor of A,B, t9 being natural_transformation of F19,F2 such that
A15: F19 is_naturally_transformable_to F2 and
dom m2 = F19 and
cod m2 = F2 and
A16: m2 = [[F19,F2],t9] by Th8;
A17: F19 = dom m2 by A16, NATTRA_1:33
.= cod m1 by A10, CAT_1:15
.= F1 by A12, NATTRA_1:33 ;
then reconsider t9 = t9 as natural_transformation of F1,F2 ;
A18: Hom ((F1 . a),(F2 . a)) <> {} by A15, A17, ISOCAT_1:25;
A19: f . m29 = t9 . a by A5, A16, A17;
A20: m2 (*) m1 = [[F,F2],(t9 `*` t)] by A12, A16, A17, NATTRA_1:36;
thus ff . (m2 (*) m1) = (t9 `*` t) . a by A5, A6, A20
.= (t9 . a) * (t . a) by A11, A15, A17, NATTRA_1:25
.= (t9 . a) (*) (t . a) by A13, A18, CAT_1:def_13
.= (ff . m2) (*) (ff . m1) by A14, A19 ; ::_thesis: verum
end;
now__::_thesis:_for_m_being_Morphism_of_(Functors_(A,B))_holds_
(_f_._(id_(dom_m))_=_id_(dom_(ff_._m))_&_f_._(id_(cod_m))_=_id_(cod_(ff_._m))_)
let m be Morphism of (Functors (A,B)); ::_thesis: ( f . (id (dom m)) = id (dom (ff . m)) & f . (id (cod m)) = id (cod (ff . m)) )
reconsider m9 = m as Element of NatTrans (A,B) by NATTRA_1:def_17;
consider F, F1 being Functor of A,B, t being natural_transformation of F,F1 such that
A21: F is_naturally_transformable_to F1 and
A22: dom m = F and
A23: cod m = F1 and
A24: m = [[F,F1],t] by Th8;
A25: Hom ((F . a),(F1 . a)) <> {} by A21, ISOCAT_1:25;
A26: [[F,F],(id F)] is Morphism of (Functors (A,B)) by A6, NATTRA_1:def_16;
thus f . (id (dom m)) = f . [[F,F],(id F)] by A22, NATTRA_1:def_17
.= (id F) . a by A5, A6, A26
.= id (F . a) by NATTRA_1:20
.= id (dom (t . a)) by A25, CAT_1:5
.= id (dom (f . m9)) by A5, A24
.= id (dom (ff . m)) ; ::_thesis: f . (id (cod m)) = id (cod (ff . m))
A27: [[F1,F1],(id F1)] is Morphism of (Functors (A,B)) by A6, NATTRA_1:def_16;
thus f . (id (cod m)) = f . [[F1,F1],(id F1)] by A23, NATTRA_1:def_17
.= (id F1) . a by A5, A6, A27
.= id (F1 . a) by NATTRA_1:20
.= id (cod (t . a)) by A25, CAT_1:5
.= id (cod (f . m9)) by A5, A24
.= id (cod (ff . m)) ; ::_thesis: verum
end;
then reconsider f = f as Functor of Functors (A,B),B by A7, A9, CAT_1:def_21;
take f ; ::_thesis: for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f . [[F1,F2],t] = t . a
let F1, F2 be Functor of A,B; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f . [[F1,F2],t] = t . a
let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies f . [[F1,F2],t] = t . a )
assume F1 is_naturally_transformable_to F2 ; ::_thesis: f . [[F1,F2],t] = t . a
then [[F1,F2],t] is Morphism of (Functors (A,B)) by A1, NATTRA_1:32;
hence f . [[F1,F2],t] = t . a by A5, A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functor of Functors (A,B),B st ( for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
b1 . [[F1,F2],t] = t . a ) & ( for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
b2 . [[F1,F2],t] = t . a ) holds
b1 = b2
proof
let f1, f2 be Functor of Functors (A,B),B; ::_thesis: ( ( for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f1 . [[F1,F2],t] = t . a ) & ( for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f2 . [[F1,F2],t] = t . a ) implies f1 = f2 )
assume that
A28: for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f1 . [[F1,F2],t] = t . a and
A29: for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
f2 . [[F1,F2],t] = t . a ; ::_thesis: f1 = f2
now__::_thesis:_for_c_being_Morphism_of_(Functors_(A,B))_holds_f1_._c_=_f2_._c
let c be Morphism of (Functors (A,B)); ::_thesis: f1 . c = f2 . c
the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17;
then consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A30: ( c = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by NATTRA_1:def_15;
thus f1 . c = t . a by A28, A30
.= f2 . c by A29, A30 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines |-> ISOCAT_2:def_1_:_
for A, B being Category
for a being Object of A
for b4 being Functor of Functors (A,B),B holds
( b4 = a |-> B iff for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
b4 . [[F1,F2],t] = t . a );
theorem :: ISOCAT_2:9
for A being Category
for o, m being set holds Functors ((1Cat (o,m)),A) ~= A
proof
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_set_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 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_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, NATTRA_1:def_7;
then A9: Hom ((F1 . a),(F2 . a)) <> {} by NATTRA_1:def_2;
A10: F19 is_transformable_to F29 by A5, NATTRA_1:def_7;
then A11: Hom ((F19 . a),(F29 . a)) <> {} by NATTRA_1:def_2;
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 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 ;
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 by NATTRA_1:def_2;
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, NATTRA_1:def_2;
then A36: F1 is_naturally_transformable_to F2 by A27, NATTRA_1:def_7;
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
end;
begin
theorem Th10: :: ISOCAT_2:10
for A, B, C being Category
for F being Functor of [:A,B:],C
for a being Object of A
for b being Object of B holds (F ?- a) . b = F . [a,b]
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for a being Object of A
for b being Object of B holds (F ?- a) . b = F . [a,b]
let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A
for b being Object of B holds (F ?- a) . b = F . [a,b]
let a be Object of A; ::_thesis: for b being Object of B holds (F ?- a) . b = F . [a,b]
let b be Object of B; ::_thesis: (F ?- a) . b = F . [a,b]
thus (F ?- a) . b = (Obj F) . (a,b) by CAT_2:37
.= F . [a,b] ; ::_thesis: verum
end;
theorem Th11: :: ISOCAT_2:11
for A, B being Category
for a1, a2 being Object of A
for b1, b2 being Object of B holds
( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )
proof
let A, B be Category; ::_thesis: for a1, a2 being Object of A
for b1, b2 being Object of B holds
( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )
let a1, a2 be Object of A; ::_thesis: for b1, b2 being Object of B holds
( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )
let b1, b2 be Object of B; ::_thesis: ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )
Hom ([a1,b1],[a2,b2]) = [:(Hom (a1,a2)),(Hom (b1,b2)):] by CAT_2:32;
hence ( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} ) by ZFMISC_1:90; ::_thesis: verum
end;
theorem Th12: :: ISOCAT_2:12
for A, B being Category
for a1, a2 being Object of A
for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds
for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
proof
let A, B be Category; ::_thesis: for a1, a2 being Object of A
for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds
for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let a1, a2 be Object of A; ::_thesis: for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds
for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let b1, b2 be Object of B; ::_thesis: ( Hom ([a1,b1],[a2,b2]) <> {} implies for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) )
assume A1: Hom ([a1,b1],[a2,b2]) <> {} ; ::_thesis: for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let f be Morphism of A; ::_thesis: for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let g be Morphism of B; ::_thesis: ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
thus ( [f,g] is Morphism of [a1,b1],[a2,b2] implies ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) ::_thesis: ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] )
proof
assume [f,g] is Morphism of [a1,b1],[a2,b2] ; ::_thesis: ( f is Morphism of a1,a2 & g is Morphism of b1,b2 )
then A2: [f,g] in Hom ([a1,b1],[a2,b2]) by A1, CAT_1:def_5;
Hom ([a1,b1],[a2,b2]) = [:(Hom (a1,a2)),(Hom (b1,b2)):] by CAT_2:32;
then ( f in Hom (a1,a2) & g in Hom (b1,b2) ) by A2, ZFMISC_1:87;
hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) by CAT_1:def_5; ::_thesis: verum
end;
( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) by A1, Th11;
hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] ) by CAT_2:33; ::_thesis: verum
end;
theorem Th13: :: ISOCAT_2:13
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )
let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a ) )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2
for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )
then A2: F1 is_transformable_to F2 by NATTRA_1:def_7;
let u be natural_transformation of F1,F2; ::_thesis: for a being Object of A holds
( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a )
let a be Object of A; ::_thesis: ( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a )
reconsider t = u as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
A3: F1 ?- a is_transformable_to F2 ?- a
proof
let b be Object of B; :: according to NATTRA_1:def_2 ::_thesis: not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {}
( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th10;
hence not Hom (((F1 ?- a) . b),((F2 ?- a) . b)) = {} by A2, NATTRA_1:def_2; ::_thesis: verum
end;
A4: now__::_thesis:_for_b_being_Object_of_B_holds_((curry_t)_._a)_._b_in_Hom_(((F1_?-_a)_._b),((F2_?-_a)_._b))
let b be Object of B; ::_thesis: ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b))
A5: ( (F1 ?- a) . b = F1 . [a,b] & (F2 ?- a) . b = F2 . [a,b] ) by Th10;
A6: Hom (((F1 ?- a) . b),((F2 ?- a) . b)) <> {} by A3, NATTRA_1:def_2;
((curry t) . a) . b = t . (a,b) by FUNCT_5:69
.= u . [a,b] by A2, NATTRA_1:def_5 ;
hence ((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A5, A6, CAT_1:def_5; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Object_of_B_holds_((curry_t)_._a)_._b_is_Morphism_of_(F1_?-_a)_._b,(F2_?-_a)_._b
let b be Object of B; ::_thesis: ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b
((curry t) . a) . b in Hom (((F1 ?- a) . b),((F2 ?- a) . b)) by A4;
hence ((curry t) . a) . b is Morphism of (F1 ?- a) . b,(F2 ?- a) . b by CAT_1:def_5; ::_thesis: verum
end;
then reconsider s = (curry t) . a as transformation of F1 ?- a,F2 ?- a by A3, NATTRA_1:def_3;
A7: now__::_thesis:_for_b1,_b2_being_Object_of_B_st_Hom_(b1,b2)_<>_{}_holds_
for_f_being_Morphism_of_b1,b2_holds_(s_._b2)_*_((F1_?-_a)_/._f)_=_((F2_?-_a)_/._f)_*_(s_._b1)
let b1, b2 be Object of B; ::_thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1) )
assume A8: Hom (b1,b2) <> {} ; ::_thesis: for f being Morphism of b1,b2 holds (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1)
A9: Hom (((F1 ?- a) . b1),((F1 ?- a) . b2)) <> {} by A8, CAT_1:84;
let f be Morphism of b1,b2; ::_thesis: (s . b2) * ((F1 ?- a) /. f) = ((F2 ?- a) /. f) * (s . b1)
A10: Hom (a,a) <> {} ;
then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A8, CAT_2:33;
A11: Hom ([a,b1],[a,b2]) <> {} by A8, A10, Th11;
then A12: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:84;
A13: s . b1 = ((curry t) . a) . b1 by A3, NATTRA_1:def_5
.= t . (a,b1) by FUNCT_5:69
.= u . [a,b1] by A2, NATTRA_1:def_5 ;
A14: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2, NATTRA_1:def_2;
A15: Hom (((F2 ?- a) . b1),((F2 ?- a) . b2)) <> {} by A8, CAT_1:84;
A16: ( (F1 ?- a) . b1 = F1 . [a,b1] & (F2 ?- a) . b1 = F2 . [a,b1] ) by Th10;
A17: ( (F1 ?- a) . b2 = F1 . [a,b2] & (F2 ?- a) . b2 = F2 . [a,b2] ) by Th10;
A18: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2, NATTRA_1:def_2;
A19: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A11, CAT_1:84;
s . b2 = ((curry t) . a) . b2 by A3, NATTRA_1:def_5
.= t . (a,b2) by FUNCT_5:69
.= u . [a,b2] by A2, NATTRA_1:def_5 ;
hence (s . b2) * ((F1 ?- a) /. f) = (u . [a,b2]) (*) ((F1 ?- a) /. f) by A14, A9, A17, CAT_1:def_13
.= (u . [a,b2]) (*) ((F1 ?- a) . f) by A8, CAT_3:def_10
.= (u . [a,b2]) (*) (F1 . ((id a),f)) by CAT_2:36
.= (u . [a,b2]) (*) (F1 /. g) by A11, CAT_3:def_10
.= (u . [a,b2]) * (F1 /. g) by A12, A14, CAT_1:def_13
.= (F2 /. g) * (u . [a,b1]) by A1, A11, NATTRA_1:def_8
.= (F2 /. g) (*) (u . [a,b1]) by A18, A19, CAT_1:def_13
.= (F2 . ((id a),f)) (*) (u . [a,b1]) by A11, CAT_3:def_10
.= ((F2 ?- a) . f) (*) (u . [a,b1]) by CAT_2:36
.= ((F2 ?- a) /. f) (*) (s . b1) by A8, A13, CAT_3:def_10
.= ((F2 ?- a) /. f) * (s . b1) by A18, A15, A16, CAT_1:def_13 ;
::_thesis: verum
end;
hence F1 ?- a is_naturally_transformable_to F2 ?- a by A3, NATTRA_1:def_7; ::_thesis: (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a
hence (curry u) . a is natural_transformation of F1 ?- a,F2 ?- a by A7, NATTRA_1:def_8; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
func curry (F,f) -> Function of the carrier' of B, the carrier' of C equals :: ISOCAT_2:def 2
(curry F) . f;
coherence
(curry F) . f is Function of the carrier' of B, the carrier' of C
proof
reconsider F = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
(curry F) . f is Function of the carrier' of B, the carrier' of C ;
hence (curry F) . f is Function of the carrier' of B, the carrier' of C ; ::_thesis: verum
end;
end;
:: deftheorem defines curry ISOCAT_2:def_2_:_
for A, B, C being Category
for F being Functor of [:A,B:],C
for f being Morphism of A holds curry (F,f) = (curry F) . f;
theorem Th14: :: ISOCAT_2:14
for A, B being Category
for a1, a2 being Object of A
for b1, b2 being Object of B
for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
proof
let A, B be Category; ::_thesis: for a1, a2 being Object of A
for b1, b2 being Object of B
for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let a1, a2 be Object of A; ::_thesis: for b1, b2 being Object of B
for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let b1, b2 be Object of B; ::_thesis: for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let f be Morphism of A; ::_thesis: for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let g be Morphism of B; ::_thesis: ( f in Hom (a1,a2) & g in Hom (b1,b2) implies [f,g] in Hom ([a1,b1],[a2,b2]) )
assume ( f in Hom (a1,a2) & g in Hom (b1,b2) ) ; ::_thesis: [f,g] in Hom ([a1,b1],[a2,b2])
then [f,g] in [:(Hom (a1,a2)),(Hom (b1,b2)):] by ZFMISC_1:87;
hence [f,g] in Hom ([a1,b1],[a2,b2]) by CAT_2:32; ::_thesis: verum
end;
theorem Th15: :: ISOCAT_2:15
for A, B, C being Category
for F being Functor of [:A,B:],C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )
let F be Functor of [:A,B:],C; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )
let a1, a2 be Object of A; ::_thesis: ( Hom (a1,a2) <> {} implies for f being Morphism of a1,a2 holds
( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 ) )
assume A1: Hom (a1,a2) <> {} ; ::_thesis: for f being Morphism of a1,a2 holds
( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 )
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
let f be Morphism of a1,a2; ::_thesis: ( F ?- a1 is_naturally_transformable_to F ?- a2 & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 )
reconsider Ff = (curry G) . f as Function of the carrier' of B, the carrier' of C ;
A2: now__::_thesis:_for_b_being_Object_of_B_holds_((curry_(F,f))_*_(IdMap_B))_._b_in_Hom_(((F_?-_a1)_._b),((F_?-_a2)_._b))
let b be Object of B; ::_thesis: ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b))
( f in Hom (a1,a2) & id b in Hom (b,b) ) by A1, CAT_1:def_5;
then [f,(id b)] in Hom ([a1,b],[a2,b]) by Th14;
then A3: F . (f,(id b)) in Hom ((F . [a1,b]),(F . [a2,b])) by CAT_1:81;
A4: id b = (IdMap B) . b by ISOCAT_1:def_12;
( (F ?- a1) . b = F . [a1,b] & (F ?- a2) . b = F . [a2,b] ) by Th10;
then Ff . (id b) in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A3, FUNCT_5:69;
hence ((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by FUNCT_2:15, A4; ::_thesis: verum
end;
A5: F ?- a1 is_transformable_to F ?- a2
proof
let b be Object of B; :: according to NATTRA_1:def_2 ::_thesis: not Hom (((F ?- a1) . b),((F ?- a2) . b)) = {}
thus not Hom (((F ?- a1) . b),((F ?- a2) . b)) = {} by A2; ::_thesis: verum
end;
reconsider FfI = (curry (F,f)) * (IdMap B) as Function of the carrier of B, the carrier' of C ;
now__::_thesis:_for_b_being_Object_of_B_holds_FfI_._b_is_Morphism_of_(F_?-_a1)_._b,(F_?-_a2)_._b
let b be Object of B; ::_thesis: FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b
((curry (F,f)) * (IdMap B)) . b in Hom (((F ?- a1) . b),((F ?- a2) . b)) by A2;
hence FfI . b is Morphism of (F ?- a1) . b,(F ?- a2) . b by CAT_1:def_5; ::_thesis: verum
end;
then reconsider t = (curry (F,f)) * (IdMap B) as transformation of F ?- a1,F ?- a2 by A5, NATTRA_1:def_3;
A6: now__::_thesis:_for_b1,_b2_being_Object_of_B_st_Hom_(b1,b2)_<>_{}_holds_
for_g_being_Morphism_of_b1,b2_holds_(t_._b2)_*_((F_?-_a1)_/._g)_=_((F_?-_a2)_/._g)_*_(t_._b1)
reconsider ida1 = id a1, ida2 = id a2 as Morphism of A ;
A7: Hom (a1,a1) <> {} ;
A8: Hom (a2,a2) <> {} ;
let b1, b2 be Object of B; ::_thesis: ( Hom (b1,b2) <> {} implies for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1) )
assume A9: Hom (b1,b2) <> {} ; ::_thesis: for g being Morphism of b1,b2 holds (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1)
A10: Hom (((F ?- a2) . b1),((F ?- a2) . b2)) <> {} by A9, CAT_1:84;
let g be Morphism of b1,b2; ::_thesis: (t . b2) * ((F ?- a1) /. g) = ((F ?- a2) /. g) * (t . b1)
reconsider idb1 = id b1, idb2 = id b2 as Morphism of B ;
A11: Hom (b1,b1) <> {} ;
A12: dom (id b2) = b2
.= cod g by A9, CAT_1:5 ;
Hom (b2,b2) <> {} ;
then A13: [(f (*) ida1),(idb2 (*) g)] = [(f (*) ida1),((id b2) * g)] by A9, CAT_1:def_13
.= [(f (*) ida1),g] by A9, CAT_1:28
.= [(f * (id a1)),g] by A1, A7, CAT_1:def_13
.= [f,g] by A1, CAT_1:29
.= [((id a2) * f),g] by A1, CAT_1:28
.= [(ida2 (*) f),g] by A1, A8, CAT_1:def_13
.= [(ida2 (*) f),(g * (id b1))] by A9, CAT_1:29
.= [(ida2 (*) f),(g (*) idb1)] by A9, A11, CAT_1:def_13 ;
A14: ( Hom (((F ?- a1) . b2),((F ?- a2) . b2)) <> {} & t . b2 = FfI . b2 ) by A5, NATTRA_1:def_2, NATTRA_1:def_5;
A15: cod (id a1) = a1
.= dom f by A1, CAT_1:5 ;
then A16: cod [(id a1),g] = [(dom f),(cod g)] by CAT_2:28
.= dom [f,(id b2)] by A12, CAT_2:28 ;
A17: ( Hom (((F ?- a1) . b1),((F ?- a2) . b1)) <> {} & t . b1 = FfI . b1 ) by A5, NATTRA_1:def_2, NATTRA_1:def_5;
A18: dom g = b1 by A9, CAT_1:5
.= cod (id b1) ;
A19: dom (id a2) = a2
.= cod f by A1, CAT_1:5 ;
then A20: dom [(id a2),g] = [(cod f),(dom g)] by CAT_2:28
.= cod [f,(id b1)] by A18, CAT_2:28 ;
A21: id b2 = (IdMap B) . b2 by ISOCAT_1:def_12;
A22: id b1 = (IdMap B) . b1 by ISOCAT_1:def_12;
Hom (((F ?- a1) . b1),((F ?- a1) . b2)) <> {} by A9, CAT_1:84;
hence (t . b2) * ((F ?- a1) /. g) = (FfI . b2) (*) ((F ?- a1) /. g) by A14, CAT_1:def_13
.= (Ff . (id b2)) (*) ((F ?- a1) /. g) by FUNCT_2:15, A21
.= (F . (f,(id b2))) (*) ((F ?- a1) /. g) by FUNCT_5:69
.= (F . [f,(id b2)]) (*) ((F ?- a1) . g) by A9, CAT_3:def_10
.= (F . (f,(id b2))) (*) (F . ((id a1),g)) by CAT_2:36
.= F . ([f,(id b2)] (*) [(id a1),g]) by A16, CAT_1:64
.= F . [(f (*) ida1),(idb2 (*) g)] by A15, A12, CAT_2:29
.= F . ([ida2,g] (*) [f,idb1]) by A19, A18, A13, CAT_2:29
.= (F . ((id a2),g)) (*) (F . [f,(id b1)]) by A20, CAT_1:64
.= ((F ?- a2) . g) (*) (F . [f,(id b1)]) by CAT_2:36
.= ((F ?- a2) /. g) (*) (F . (f,(id b1))) by A9, CAT_3:def_10
.= ((F ?- a2) /. g) (*) (Ff . (id b1)) by FUNCT_5:69
.= ((F ?- a2) /. g) (*) (FfI . b1) by FUNCT_2:15, A22
.= ((F ?- a2) /. g) * (t . b1) by A10, A17, CAT_1:def_13 ;
::_thesis: verum
end;
hence F ?- a1 is_naturally_transformable_to F ?- a2 by A5, NATTRA_1:def_7; ::_thesis: (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2
hence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a1,F ?- a2 by A6, NATTRA_1:def_8; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
funcF ?- f -> natural_transformation of F ?- (dom f),F ?- (cod f) equals :: ISOCAT_2:def 3
(curry (F,f)) * (IdMap B);
coherence
(curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f)
proof
( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:2, CAT_1:4;
hence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f) by Th15; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines ?- ISOCAT_2:def_3_:_
for A, B, C being Category
for F being Functor of [:A,B:],C
for f being Morphism of A holds F ?- f = (curry (F,f)) * (IdMap B);
theorem Th16: :: ISOCAT_2:16
for A, B, C being Category
for F being Functor of [:A,B:],C
for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
let F be Functor of [:A,B:],C; ::_thesis: for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
let g be Morphism of A; ::_thesis: F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
Hom ((dom g),(cod g)) <> {} by CAT_1:2;
hence F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th15; ::_thesis: verum
end;
theorem Th17: :: ISOCAT_2:17
for A, B, C being Category
for F being Functor of [:A,B:],C
for f being Morphism of A
for b being Object of B holds (F ?- f) . b = F . (f,(id b))
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for f being Morphism of A
for b being Object of B holds (F ?- f) . b = F . (f,(id b))
let F be Functor of [:A,B:],C; ::_thesis: for f being Morphism of A
for b being Object of B holds (F ?- f) . b = F . (f,(id b))
let f be Morphism of A; ::_thesis: for b being Object of B holds (F ?- f) . b = F . (f,(id b))
let b be Object of B; ::_thesis: (F ?- f) . b = F . (f,(id b))
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
reconsider Ff = (curry G) . f as Function of the carrier' of B, the carrier' of C ;
A1: id b = (IdMap B) . b by ISOCAT_1:def_12;
F ?- (dom f) is_naturally_transformable_to F ?- (cod f) by Th16;
then F ?- (dom f) is_transformable_to F ?- (cod f) by NATTRA_1:def_7;
hence (F ?- f) . b = ((curry (F,f)) * (IdMap B)) . b by NATTRA_1:def_5
.= Ff . (id b) by FUNCT_2:15, A1
.= F . (f,(id b)) by FUNCT_5:69 ;
::_thesis: verum
end;
theorem Th18: :: ISOCAT_2:18
for A, B, C being Category
for F being Functor of [:A,B:],C
for a being Object of A holds id (F ?- a) = F ?- (id a)
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for a being Object of A holds id (F ?- a) = F ?- (id a)
let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A holds id (F ?- a) = F ?- (id a)
let a be Object of A; ::_thesis: id (F ?- a) = F ?- (id a)
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
reconsider Ff = (curry G) . (id a) as Function of the carrier' of B, the carrier' of C ;
reconsider I = F ?- (id a) as transformation of F ?- a,F ?- a ;
now__::_thesis:_for_b_being_Object_of_B_holds_I_._b_=_id_((F_?-_a)_._b)
let b be Object of B; ::_thesis: I . b = id ((F ?- a) . b)
A1: id b = (IdMap B) . b by ISOCAT_1:def_12;
thus I . b = Ff . (id b) by FUNCT_2:15, A1
.= F . ((id a),(id b)) by FUNCT_5:69
.= F . (id [a,b]) by CAT_2:31
.= id (F . [a,b]) by CAT_1:71
.= id ((F ?- a) . b) by Th10 ; ::_thesis: verum
end;
hence id (F ?- a) = F ?- (id a) by NATTRA_1:def_4; ::_thesis: verum
end;
theorem Th19: :: ISOCAT_2:19
for A, B, C being Category
for F being Functor of [:A,B:],C
for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
let F be Functor of [:A,B:],C; ::_thesis: for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
let g, f be Morphism of A; ::_thesis: ( dom g = cod f implies for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t )
assume A1: dom g = cod f ; ::_thesis: for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t
A2: F ?- (dom f) is_naturally_transformable_to F ?- (dom g) by A1, Th16;
then A3: F ?- (dom f) is_transformable_to F ?- (dom g) by NATTRA_1:def_7;
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
reconsider Fgf = (curry G) . (g (*) f), Ff = (curry G) . f, Fg = (curry G) . g as Function of the carrier' of B, the carrier' of C ;
let t be natural_transformation of F ?- (dom f),F ?- (dom g); ::_thesis: ( t = F ?- f implies F ?- (g (*) f) = (F ?- g) `*` t )
assume A4: t = F ?- f ; ::_thesis: F ?- (g (*) f) = (F ?- g) `*` t
reconsider s = t as transformation of F ?- (dom f),F ?- (dom g) ;
A5: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th16;
then A6: F ?- (dom g) is_transformable_to F ?- (cod g) by NATTRA_1:def_7;
F ?- (dom (g (*) f)) is_naturally_transformable_to F ?- (cod (g (*) f)) by Th16;
then A7: F ?- (dom (g (*) f)) is_transformable_to F ?- (cod (g (*) f)) by NATTRA_1:def_7;
A8: now__::_thesis:_for_b_being_Object_of_B_holds_(F_?-_(g_(*)_f))_._b_=_((F_?-_g)_`*`_s)_._b
let b be Object of B; ::_thesis: (F ?- (g (*) f)) . b = ((F ?- g) `*` s) . b
A9: Hom (b,b) <> {} ;
A10: id b = (IdMap B) . b by ISOCAT_1:def_12;
A11: (F ?- g) . b = ((curry (F,g)) * (IdMap B)) . b by A6, NATTRA_1:def_5
.= Fg . (id b) by FUNCT_2:15, A10
.= F . (g,(id b)) by FUNCT_5:69 ;
dom (id b) = b
.= cod (id b) ;
then A12: dom [g,(id b)] = [(cod f),(cod (id b))] by A1, CAT_2:28
.= cod [f,(id b)] by CAT_2:28 ;
A13: ( Hom (((F ?- (dom g)) . b),((F ?- (cod g)) . b)) <> {} & Hom (((F ?- (dom f)) . b),((F ?- (dom g)) . b)) <> {} ) by A3, A6, NATTRA_1:def_2;
A14: (F ?- f) . b = ((curry (F,f)) * (IdMap B)) . b by A1, A3, NATTRA_1:def_5
.= Ff . (id b) by FUNCT_2:15, A10
.= F . (f,(id b)) by FUNCT_5:69 ;
thus (F ?- (g (*) f)) . b = ((curry (F,(g (*) f))) * (IdMap B)) . b by A7, NATTRA_1:def_5
.= Fgf . (id b) by FUNCT_2:15, A10
.= F . ((g (*) f),(id b)) by FUNCT_5:69
.= F . [(g (*) f),((id b) * (id b))]
.= F . [(g (*) f),((id b) (*) (id b))] by A9, CAT_1:def_13
.= F . ([g,(id b)] (*) [f,(id b)]) by A12, CAT_2:30
.= ((F ?- g) . b) (*) (s . b) by A1, A4, A11, A14, A12, CAT_1:64
.= ((F ?- g) . b) * (s . b) by A13, CAT_1:def_13
.= ((F ?- g) `*` s) . b by A3, A6, NATTRA_1:def_6 ; ::_thesis: verum
end;
( cod (g (*) f) = cod g & dom (g (*) f) = dom f ) by A1, CAT_1:17;
then F ?- (g (*) f) = (F ?- g) `*` s by A3, A6, A8, NATTRA_1:18, NATTRA_1:19;
hence F ?- (g (*) f) = (F ?- g) `*` t by A2, A5, NATTRA_1:def_9; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F be Functor of [:A,B:],C;
func export F -> Functor of A, Functors (B,C) means :Def4: :: ISOCAT_2:def 4
for f being Morphism of A holds it . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)];
existence
ex b1 being Functor of A, Functors (B,C) st
for f being Morphism of A holds b1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]
proof
defpred S1[ set , set ] means for f being Morphism of A st $1 = f holds
$2 = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)];
A1: now__::_thesis:_for_m_being_set_st_m_in_the_carrier'_of_A_holds_
ex_o_being_set_st_
(_o_in_the_carrier'_of_(Functors_(B,C))_&_S1[m,o]_)
let m be set ; ::_thesis: ( m in the carrier' of A implies ex o being set st
( o in the carrier' of (Functors (B,C)) & S1[m,o] ) )
assume m in the carrier' of A ; ::_thesis: ex o being set st
( o in the carrier' of (Functors (B,C)) & S1[m,o] )
then reconsider g = m as Morphism of A ;
take o = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)]; ::_thesis: ( o in the carrier' of (Functors (B,C)) & S1[m,o] )
F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th16;
then o in NatTrans (B,C) by NATTRA_1:32;
hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def_17; ::_thesis: S1[m,o]
thus S1[m,o] ; ::_thesis: verum
end;
consider G being Function of the carrier' of A, the carrier' of (Functors (B,C)) such that
A2: for m being set st m in the carrier' of A holds
S1[m,G . m] from FUNCT_2:sch_1(A1);
G is Functor of A, Functors (B,C)
proof
thus for c being Object of A ex d being Object of (Functors (B,C)) st G . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of A holds
( G . (id (dom b1)) = id (dom (G . b1)) & G . (id (cod b1)) = id (cod (G . b1)) ) ) & ( for b1, b2 being Element of the carrier' of A holds
( not dom b2 = cod b1 or G . (b2 (*) b1) = (G . b2) (*) (G . b1) ) ) )
proof
let c be Object of A; ::_thesis: ex d being Object of (Functors (B,C)) st G . (id c) = id d
reconsider d = F ?- c as Object of (Functors (B,C)) by Th7;
take d ; ::_thesis: G . (id c) = id d
thus G . (id c) = [[(F ?- c),(F ?- c)],(F ?- (id c))] by A2
.= [[(F ?- c),(F ?- c)],(id (F ?- c))] by Th18
.= id d by NATTRA_1:def_17 ; ::_thesis: verum
end;
thus for f being Morphism of A holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of A holds
( not dom b2 = cod b1 or G . (b2 (*) b1) = (G . b2) (*) (G . b1) )
proof
let f be Element of the carrier' of A; ::_thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
reconsider d = F ?- (dom f), c = F ?- (cod f) as Object of (Functors (B,C)) by Th7;
A3: G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2;
thus G . (id (dom f)) = [[(F ?- (dom f)),(F ?- (dom f))],(F ?- (id (dom f)))] by A2
.= [[(F ?- (dom f)),(F ?- (dom f))],(id (F ?- (dom f)))] by Th18
.= id d by NATTRA_1:def_17
.= id (dom (G . f)) by A3, NATTRA_1:33 ; ::_thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = [[(F ?- (cod f)),(F ?- (cod f))],(F ?- (id (cod f)))] by A2
.= [[(F ?- (cod f)),(F ?- (cod f))],(id (F ?- (cod f)))] by Th18
.= id c by NATTRA_1:def_17
.= id (cod (G . f)) by A3, NATTRA_1:33 ; ::_thesis: verum
end;
let f, g be Morphism of A; ::_thesis: ( not dom g = cod f or G . (g (*) f) = (G . g) (*) (G . f) )
assume A4: dom g = cod f ; ::_thesis: G . (g (*) f) = (G . g) (*) (G . f)
then reconsider t = F ?- f as natural_transformation of F ?- (dom f),F ?- (dom g) ;
A5: ( cod (g (*) f) = cod g & dom (g (*) f) = dom f ) by A4, CAT_1:17;
A6: F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th16;
( the carrier' of (Functors (B,C)) = NatTrans (B,C) & F ?- (dom f) is_naturally_transformable_to F ?- (cod f) ) by Th16, NATTRA_1:def_17;
then reconsider gg = [[(F ?- (dom g)),(F ?- (cod g))],(F ?- g)], ff = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] as Morphism of (Functors (B,C)) by A6, NATTRA_1:32;
A7: G . f = ff by A2;
thus G . (g (*) f) = [[(F ?- (dom (g (*) f))),(F ?- (cod (g (*) f)))],(F ?- (g (*) f))] by A2
.= [[(F ?- (dom (g (*) f))),(F ?- (cod (g (*) f)))],((F ?- g) `*` t)] by A4, Th19
.= gg (*) ff by A4, A5, NATTRA_1:36
.= (G . g) (*) (G . f) by A2, A7 ; ::_thesis: verum
end;
then reconsider G = G as Functor of A, Functors (B,C) ;
take G ; ::_thesis: for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]
thus for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functor of A, Functors (B,C) st ( for f being Morphism of A holds b1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds b2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) holds
b1 = b2
proof
let G1, G2 be Functor of A, Functors (B,C); ::_thesis: ( ( for f being Morphism of A holds G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds G2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) implies G1 = G2 )
assume that
A8: for f being Morphism of A holds G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] and
A9: for f being Morphism of A holds G2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ; ::_thesis: G1 = G2
now__::_thesis:_for_f_being_Morphism_of_A_holds_G1_._f_=_G2_._f
let f be Morphism of A; ::_thesis: G1 . f = G2 . f
thus G1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A8
.= G2 . f by A9 ; ::_thesis: verum
end;
hence G1 = G2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines export ISOCAT_2:def_4_:_
for A, B, C being Category
for F being Functor of [:A,B:],C
for b5 being Functor of A, Functors (B,C) holds
( b5 = export F iff for f being Morphism of A holds b5 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] );
Lm1: for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let t be transformation of F1,F2; ::_thesis: for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let a be Object of A; ::_thesis: t . a in Hom ((F1 . a),(F2 . a))
Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2;
hence t . a in Hom ((F1 . a),(F2 . a)) by CAT_1:def_5; ::_thesis: verum
end;
theorem Th20: :: ISOCAT_2:20
for A, B, C being Category
for F being Functor of [:A,B:],C
for a being Object of A holds (export F) . a = F ?- a
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for a being Object of A holds (export F) . a = F ?- a
let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A holds (export F) . a = F ?- a
let a be Object of A; ::_thesis: (export F) . a = F ?- a
reconsider o = F ?- a as Object of (Functors (B,C)) by Th7;
reconsider i = id a as Morphism of A ;
(export F) . i = [[(F ?- a),(F ?- a)],(F ?- (id a))] by Def4
.= [[(F ?- a),(F ?- a)],(id (F ?- a))] by Th18
.= id o by NATTRA_1:def_17 ;
hence (export F) . a = F ?- a by CAT_1:67; ::_thesis: verum
end;
theorem Th21: :: ISOCAT_2:21
for A, B, C being Category
for F being Functor of [:A,B:],C
for a being Object of A holds (export F) . a is Functor of B,C
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C
for a being Object of A holds (export F) . a is Functor of B,C
let F be Functor of [:A,B:],C; ::_thesis: for a being Object of A holds (export F) . a is Functor of B,C
let a be Object of A; ::_thesis: (export F) . a is Functor of B,C
(export F) . a = F ?- a by Th20;
hence (export F) . a is Functor of B,C ; ::_thesis: verum
end;
theorem Th22: :: ISOCAT_2:22
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds
F1 = F2
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds
F1 = F2
let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( export F1 = export F2 implies F1 = F2 )
assume A1: export F1 = export F2 ; ::_thesis: F1 = F2
now__::_thesis:_for_fg_being_Morphism_of_[:A,B:]_holds_F1_._fg_=_F2_._fg
let fg be Morphism of [:A,B:]; ::_thesis: F1 . fg = F2 . fg
consider f being Morphism of A, g being Morphism of B such that
A2: fg = [f,g] by CAT_2:27;
A3: ( dom (id (cod f)) = cod f & dom g = cod (id (dom g)) ) ;
A4: fg = [((id (cod f)) (*) f),g] by A2, Th5
.= [((id (cod f)) (*) f),(g (*) (id (dom g)))] by Th6
.= [(id (cod f)),g] (*) [f,(id (dom g))] by A3, CAT_2:29 ;
A5: [[(F1 ?- (dom f)),(F1 ?- (cod f))],(F1 ?- f)] = (export F2) . f by A1, Def4
.= [[(F2 ?- (dom f)),(F2 ?- (cod f))],(F2 ?- f)] by Def4 ;
then A6: [(F1 ?- (dom f)),(F1 ?- (cod f))] = [(F2 ?- (dom f)),(F2 ?- (cod f))] by XTUPLE_0:1;
then A7: F1 ?- (dom f) = F2 ?- (dom f) by XTUPLE_0:1;
A8: F1 ?- (cod f) = F2 ?- (cod f) by A6, XTUPLE_0:1;
then A9: F1 . ((id (cod f)),g) = (F2 ?- (cod f)) . g by CAT_2:36
.= F2 . ((id (cod f)),g) by CAT_2:36 ;
A10: cod [f,(id (dom g))] = [(cod f),(cod (id (dom g)))] by CAT_2:28
.= [(cod f),(dom g)]
.= [(dom (id (cod f))),(dom g)]
.= dom [(id (cod f)),g] by CAT_2:28 ;
F1 . (f,(id (dom g))) = (F1 ?- f) . (dom g) by Th17
.= (F2 ?- f) . (dom g) by A5, A7, A8, XTUPLE_0:1
.= F2 . (f,(id (dom g))) by Th17 ;
hence F1 . fg = (F2 . [(id (cod f)),g]) (*) (F2 . [f,(id (dom g))]) by A4, A9, A10, CAT_1:64
.= F2 . fg by A4, A10, CAT_1:64 ;
::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th23: :: ISOCAT_2:23
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds
( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
then A2: F1 is_transformable_to F2 by NATTRA_1:def_7;
let t be natural_transformation of F1,F2; ::_thesis: ( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
A3: now__::_thesis:_for_a_being_Object_of_A
for_S1,_S2_being_Functor_of_B,C_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_holds_
for_b_being_Object_of_B_holds_((curry_s)_._a)_._b_in_Hom_((S1_._b),(S2_._b))
let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b))
let S1, S2 be Functor of B,C; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) )
assume that
A4: S1 = (export F1) . a and
A5: S2 = (export F2) . a ; ::_thesis: for b being Object of B holds ((curry s) . a) . b in Hom ((S1 . b),(S2 . b))
let b be Object of B; ::_thesis: ((curry s) . a) . b in Hom ((S1 . b),(S2 . b))
A6: S2 . b = (F2 ?- a) . b by A5, Th20
.= F2 . [a,b] by Th10 ;
A7: ((curry s) . a) . b = s . (a,b) by FUNCT_5:69
.= t . [a,b] by A2, NATTRA_1:def_5 ;
S1 . b = (F1 ?- a) . b by A4, Th20
.= F1 . [a,b] by Th10 ;
hence ((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A2, A6, A7, Lm1; ::_thesis: verum
end;
A8: now__::_thesis:_for_a_being_Object_of_A
for_S1,_S2_being_Functor_of_B,C_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_holds_
S1_is_transformable_to_S2
let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
S1 is_transformable_to S2
let S1, S2 be Functor of B,C; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies S1 is_transformable_to S2 )
assume ( S1 = (export F1) . a & S2 = (export F2) . a ) ; ::_thesis: S1 is_transformable_to S2
then for b being Object of B holds Hom ((S1 . b),(S2 . b)) <> {} by A3;
hence S1 is_transformable_to S2 by NATTRA_1:def_2; ::_thesis: verum
end;
A9: now__::_thesis:_for_a_being_Object_of_A
for_S1,_S2_being_Functor_of_B,C
for_T_being_transformation_of_S1,S2_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_&_T_=_(curry_s)_._a_holds_
for_b1,_b2_being_Object_of_B_st_Hom_(b1,b2)_<>_{}_holds_
for_f_being_Morphism_of_b1,b2_holds_(T_._b2)_*_(S1_/._f)_=_(S2_/._f)_*_(T_._b1)
let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C
for T being transformation of S1,S2 st S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a holds
for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1)
let S1, S2 be Functor of B,C; ::_thesis: for T being transformation of S1,S2 st S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a holds
for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1)
let T be transformation of S1,S2; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a & T = (curry s) . a implies for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) )
assume that
A10: S1 = (export F1) . a and
A11: S2 = (export F2) . a and
A12: T = (curry s) . a ; ::_thesis: for b1, b2 being Object of B st Hom (b1,b2) <> {} holds
for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1)
let b1, b2 be Object of B; ::_thesis: ( Hom (b1,b2) <> {} implies for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1) )
assume A13: Hom (b1,b2) <> {} ; ::_thesis: for f being Morphism of b1,b2 holds (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1)
A14: Hom ((S1 . b1),(S1 . b2)) <> {} by A13, CAT_1:84;
A15: T . b2 = T . b2 by A8, A10, A11, NATTRA_1:def_5
.= s . (a,b2) by A12, FUNCT_5:69
.= t . [a,b2] by A2, NATTRA_1:def_5 ;
A16: Hom ((F1 . [a,b2]),(F2 . [a,b2])) <> {} by A2, NATTRA_1:def_2;
let f be Morphism of b1,b2; ::_thesis: (T . b2) * (S1 /. f) = (S2 /. f) * (T . b1)
A17: Hom (a,a) <> {} ;
then reconsider g = [(id a),f] as Morphism of [a,b1],[a,b2] by A13, CAT_2:33;
A18: Hom ([a,b1],[a,b2]) <> {} by A13, A17, Th11;
then A19: Hom ((F1 . [a,b1]),(F1 . [a,b2])) <> {} by CAT_1:84;
A20: S1 is_transformable_to S2 by A8, A10, A11;
then A21: Hom ((S1 . b1),(S2 . b1)) <> {} by NATTRA_1:def_2;
A22: T . b1 = T . b1 by A8, A10, A11, NATTRA_1:def_5
.= s . (a,b1) by A12, FUNCT_5:69
.= t . [a,b1] by A2, NATTRA_1:def_5 ;
A23: Hom ((F1 . [a,b1]),(F2 . [a,b1])) <> {} by A2, NATTRA_1:def_2;
A24: Hom ((S1 . b2),(S2 . b2)) <> {} by A20, NATTRA_1:def_2;
A25: Hom ((S2 . b1),(S2 . b2)) <> {} by A13, CAT_1:84;
A26: S2 /. f = (F2 ?- a) /. f by A11, Th20
.= (F2 ?- a) /. f by A13, CAT_3:def_10
.= F2 . ((id a),f) by CAT_2:36
.= F2 /. g by A18, CAT_3:def_10 ;
A27: Hom ((F2 . [a,b1]),(F2 . [a,b2])) <> {} by A18, CAT_1:84;
A28: S1 /. f = (F1 ?- a) /. f by A10, Th20
.= (F1 ?- a) /. f by A13, CAT_3:def_10
.= F1 . ((id a),f) by CAT_2:36
.= F1 /. g by A18, CAT_3:def_10 ;
thus (T . b2) * (S1 /. f) = (T . b2) (*) (S1 /. f) by A14, A24, CAT_1:def_13
.= (t . [a,b2]) * (F1 /. g) by A19, A16, A15, A28, CAT_1:def_13
.= (F2 /. g) * (t . [a,b1]) by A1, A18, NATTRA_1:def_8
.= (S2 /. f) (*) (T . b1) by A27, A23, A22, A26, CAT_1:def_13
.= (S2 /. f) * (T . b1) by A25, A21, CAT_1:def_13 ; ::_thesis: verum
end;
defpred S1[ set , set ] means for f being Object of A
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s & $1 = f holds
$2 = [[((export F1) . f),((export F2) . f)],((curry s) . f)];
A29: now__::_thesis:_for_a_being_Object_of_A
for_S1,_S2_being_Functor_of_B,C_st_S1_=_(export_F1)_._a_&_S2_=_(export_F2)_._a_holds_
(curry_s)_._a_is_transformation_of_S1,S2
let a be Object of A; ::_thesis: for S1, S2 being Functor of B,C st S1 = (export F1) . a & S2 = (export F2) . a holds
(curry s) . a is transformation of S1,S2
let S1, S2 be Functor of B,C; ::_thesis: ( S1 = (export F1) . a & S2 = (export F2) . a implies (curry s) . a is transformation of S1,S2 )
assume A30: ( S1 = (export F1) . a & S2 = (export F2) . a ) ; ::_thesis: (curry s) . a is transformation of S1,S2
thus (curry s) . a is transformation of S1,S2 ::_thesis: verum
proof
thus S1 is_transformable_to S2 by A8, A30; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of B holds ((curry s) . a) . b1 is Morphism of S1 . b1,S2 . b1
let b be Object of B; ::_thesis: ((curry s) . a) . b is Morphism of S1 . b,S2 . b
((curry s) . a) . b in Hom ((S1 . b),(S2 . b)) by A3, A30;
hence ((curry s) . a) . b is Morphism of S1 . b,S2 . b by CAT_1:def_5; ::_thesis: verum
end;
end;
A31: now__::_thesis:_for_m_being_set_st_m_in_the_carrier_of_A_holds_
ex_o_being_set_st_
(_o_in_the_carrier'_of_(Functors_(B,C))_&_S1[m,o]_)
let m be set ; ::_thesis: ( m in the carrier of A implies ex o being set st
( o in the carrier' of (Functors (B,C)) & S1[m,o] ) )
assume m in the carrier of A ; ::_thesis: ex o being set st
( o in the carrier' of (Functors (B,C)) & S1[m,o] )
then reconsider a = m as Object of A ;
reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th21;
take o = [[((export F1) . a),((export F2) . a)],((curry s) . a)]; ::_thesis: ( o in the carrier' of (Functors (B,C)) & S1[m,o] )
reconsider T = (curry s) . a as transformation of S1,S2 by A29;
A32: S1 is_naturally_transformable_to S2
proof
thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of S1,S2 st
for b2, b3 being Element of the carrier of B holds
( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (S1 /. b4) = (S2 /. b4) * (b1 . b2) )
take T ; ::_thesis: for b1, b2 being Element of the carrier of B holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) )
thus for b1, b2 being Element of the carrier of B holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) ) by A9; ::_thesis: verum
end;
for a, b being Object of B st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (T . b) * (S1 /. f) = (S2 /. f) * (T . a) by A9;
then T is natural_transformation of S1,S2 by A32, NATTRA_1:def_8;
then o in NatTrans (B,C) by A32, NATTRA_1:32;
hence o in the carrier' of (Functors (B,C)) by NATTRA_1:def_17; ::_thesis: S1[m,o]
thus S1[m,o] ; ::_thesis: verum
end;
consider G being Function of the carrier of A, the carrier' of (Functors (B,C)) such that
A33: for m being set st m in the carrier of A holds
S1[m,G . m] from FUNCT_2:sch_1(A31);
A34: now__::_thesis:_for_a_being_Object_of_A_holds_G_._a_in_Hom_(((export_F1)_._a),((export_F2)_._a))
let a be Object of A; ::_thesis: G . a in Hom (((export F1) . a),((export F2) . a))
reconsider S1 = (export F1) . a, S2 = (export F2) . a as Functor of B,C by Th21;
reconsider T = (curry s) . a as transformation of S1,S2 by A29;
A35: G . a = [[S1,S2],T] by A33;
A36: S1 is_naturally_transformable_to S2
proof
thus S1 is_transformable_to S2 by A8; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of S1,S2 st
for b2, b3 being Element of the carrier of B holds
( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (S1 /. b4) = (S2 /. b4) * (b1 . b2) )
take T ; ::_thesis: for b1, b2 being Element of the carrier of B holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) )
thus for b1, b2 being Element of the carrier of B holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (T . b2) * (S1 /. b3) = (S2 /. b3) * (T . b1) ) by A9; ::_thesis: verum
end;
for a, b being Object of B st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (T . b) * (S1 /. f) = (S2 /. f) * (T . a) by A9;
then T is natural_transformation of S1,S2 by A36, NATTRA_1:def_8;
then ( dom (G . a) = S1 & cod (G . a) = S2 ) by A35, NATTRA_1:33;
hence G . a in Hom (((export F1) . a),((export F2) . a)) ; ::_thesis: verum
end;
then A37: for a being Object of A holds Hom (((export F1) . a),((export F2) . a)) <> {} ;
G is transformation of export F1, export F2
proof
thus export F1 is_transformable_to export F2 by A37, NATTRA_1:def_2; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of A holds G . b1 is Morphism of (export F1) . b1,(export F2) . b1
let a be Object of A; ::_thesis: G . a is Morphism of (export F1) . a,(export F2) . a
G . a in Hom (((export F1) . a),((export F2) . a)) by A34;
hence G . a is Morphism of (export F1) . a,(export F2) . a by CAT_1:def_5; ::_thesis: verum
end;
then reconsider G = G as transformation of export F1, export F2 ;
A38: export F1 is_transformable_to export F2 by A37, NATTRA_1:def_2;
A39: now__::_thesis:_for_a,_b_being_Object_of_A_st_Hom_(a,b)_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(G_._b)_*_((export_F1)_/._f)_=_((export_F2)_/._f)_*_(G_._a)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (G . b) * ((export F1) /. f) = ((export F2) /. f) * (G . a) )
assume A40: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (G . b) * ((export F1) /. f) = ((export F2) /. f) * (G . a)
A41: Hom (((export F2) . a),((export F2) . b)) <> {} by A40, CAT_1:84;
reconsider S1 = (export F1) . a, S2 = (export F2) . a, S3 = (export F1) . b, S4 = (export F2) . b as Functor of B,C by Th21;
let f be Morphism of a,b; ::_thesis: (G . b) * ((export F1) /. f) = ((export F2) /. f) * (G . a)
A42: F2 ?- a = (export F2) . a by Th20;
A43: F1 ?- a = (export F1) . a by Th20;
then reconsider T12 = (curry s) . a as natural_transformation of S1,S2 by A1, A42, Th13;
A44: F2 ?- b = (export F2) . b by Th20;
then A45: F2 ?- (cod f) = (export F2) . b by A40, CAT_1:5;
then reconsider T24 = F2 ?- f as natural_transformation of S2,S4 by A40, A42, CAT_1:5;
A46: G . a = G . a by A38, NATTRA_1:def_5
.= [[S1,S2],T12] by A33 ;
A47: F1 ?- b = (export F1) . b by Th20;
then reconsider T34 = (curry s) . b as natural_transformation of S3,S4 by A1, A44, Th13;
A48: S3 is_naturally_transformable_to S4 by A1, A47, A44, Th13;
then A49: S3 is_transformable_to S4 by NATTRA_1:def_7;
A50: F1 ?- (cod f) = (export F1) . b by A40, A47, CAT_1:5;
then reconsider T13 = F1 ?- f as natural_transformation of S1,S3 by A40, A43, CAT_1:5;
A51: G . b = G . b by A38, NATTRA_1:def_5
.= [[S3,S4],T34] by A33 ;
A52: S1 is_naturally_transformable_to S2 by A1, A42, A43, Th13;
then A53: S1 is_transformable_to S2 by NATTRA_1:def_7;
reconsider g = f as Morphism of A ;
A54: Hom (((export F1) . a),((export F2) . a)) <> {} by A34;
F2 ?- (dom f) = (export F2) . a by A40, A42, CAT_1:5;
then A55: (export F2) . g = [[S2,S4],T24] by A45, Def4;
A56: Hom (((export F1) . a),((export F1) . b)) <> {} by A40, CAT_1:84;
A57: S2 is_naturally_transformable_to S4 by A40, A42, A44, Th15;
then A58: S2 is_transformable_to S4 by NATTRA_1:def_7;
A59: S1 is_naturally_transformable_to S3 by A40, A47, A43, Th15;
then A60: S1 is_transformable_to S3 by NATTRA_1:def_7;
now__::_thesis:_for_c_being_Object_of_B_holds_(T34_`*`_T13)_._c_=_(T24_`*`_T12)_._c
reconsider FF1 = F1, FF2 = F2 as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
let c be Object of B; ::_thesis: (T34 `*` T13) . c = (T24 `*` T12) . c
A61: Hom ((F1 . [a,c]),(F2 . [a,c])) <> {} by A2, NATTRA_1:def_2;
A62: Hom ((F1 . [b,c]),(F2 . [b,c])) <> {} by A2, NATTRA_1:def_2;
A63: ( Hom ((S3 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S3 . c)) <> {} ) by A60, A49, NATTRA_1:def_2;
A64: ( Hom ((S2 . c),(S4 . c)) <> {} & Hom ((S1 . c),(S2 . c)) <> {} ) by A53, A58, NATTRA_1:def_2;
A65: t . [b,c] = s . (b,c) by A2, NATTRA_1:def_5
.= ((curry s) . b) . c by FUNCT_5:69
.= T34 . c by A49, NATTRA_1:def_5 ;
A66: t . [a,c] = s . (a,c) by A2, NATTRA_1:def_5
.= ((curry s) . a) . c by FUNCT_5:69
.= T12 . c by A53, NATTRA_1:def_5 ;
A67: Hom (c,c) <> {} ;
then reconsider fi = [f,(id c)] as Morphism of [a,c],[b,c] by A40, CAT_2:33;
A68: Hom ([a,c],[b,c]) <> {} by A40, A67, Th11;
then A69: Hom ((F2 . [a,c]),(F2 . [b,c])) <> {} by CAT_1:84;
A70: id c = (IdMap B) . c by ISOCAT_1:def_12;
A71: F1 /. fi = FF1 . (f,(id c)) by A68, CAT_3:def_10
.= (curry (F1,f)) . (id c) by FUNCT_5:69
.= (F1 ?- f) . c by FUNCT_2:15, A70
.= T13 . c by A60, NATTRA_1:def_5 ;
A72: F2 /. fi = FF2 . (f,(id c)) by A68, CAT_3:def_10
.= (curry (F2,f)) . (id c) by FUNCT_5:69
.= (F2 ?- f) . c by FUNCT_2:15, A70
.= T24 . c by A58, NATTRA_1:def_5 ;
A73: Hom ((F1 . [a,c]),(F1 . [b,c])) <> {} by A68, CAT_1:84;
thus (T34 `*` T13) . c = (T34 . c) * (T13 . c) by A59, A48, NATTRA_1:25
.= (t . [b,c]) (*) (F1 /. fi) by A63, A71, A65, CAT_1:def_13
.= (t . [b,c]) * (F1 /. fi) by A62, A73, CAT_1:def_13
.= (F2 /. fi) * (t . [a,c]) by A1, A68, NATTRA_1:def_8
.= (F2 /. fi) (*) (t . [a,c]) by A61, A69, CAT_1:def_13
.= (T24 . c) * (T12 . c) by A64, A72, A66, CAT_1:def_13
.= (T24 `*` T12) . c by A52, A57, NATTRA_1:25 ; ::_thesis: verum
end;
then A74: T34 `*` T13 = T24 `*` T12 by A53, A58, NATTRA_1:18, NATTRA_1:19;
F1 ?- (dom f) = (export F1) . a by A40, A43, CAT_1:5;
then A75: (export F1) . g = [[S1,S3],T13] by A50, Def4;
Hom (((export F1) . b),((export F2) . b)) <> {} by A34;
hence (G . b) * ((export F1) /. f) = (G . b) (*) ((export F1) /. f) by A56, CAT_1:def_13
.= (G . b) (*) ((export F1) . g) by A40, CAT_3:def_10
.= [[S1,S4],(T34 `*` T13)] by A75, A51, NATTRA_1:36
.= ((export F2) /. g) (*) (G . a) by A55, A46, A74, NATTRA_1:36
.= ((export F2) /. f) (*) (G . a) by A40, CAT_3:def_10
.= ((export F2) /. f) * (G . a) by A54, A41, CAT_1:def_13 ;
::_thesis: verum
end;
A76: export F1 is_transformable_to export F2 by A37, NATTRA_1:def_2;
hence export F1 is_naturally_transformable_to export F2 by A39, NATTRA_1:def_7; ::_thesis: ex G being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
export F1 is_naturally_transformable_to export F2 by A39, A76, NATTRA_1:def_7;
then reconsider G = G as natural_transformation of export F1, export F2 by A39, NATTRA_1:def_8;
take G ; ::_thesis: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; ::_thesis: ( t = s implies for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
assume A77: t = s ; ::_thesis: for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let a be Object of A; ::_thesis: G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
thus G . a = G . a by A38, NATTRA_1:def_5
.= [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A33, A77 ; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, F2 be Functor of [:A,B:],C;
assume B1: F1 is_naturally_transformable_to F2 ;
let t be natural_transformation of F1,F2;
func export t -> natural_transformation of export F1, export F2 means :Def5: :: ISOCAT_2:def 5
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds it . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)];
existence
ex b1 being natural_transformation of export F1, export F2 st
for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds b1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by B1, Th23;
uniqueness
for b1, b2 being natural_transformation of export F1, export F2 st ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds b1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds b2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) holds
b1 = b2
proof
reconsider s = t as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
let T1, T2 be natural_transformation of export F1, export F2; ::_thesis: ( ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds T2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) implies T1 = T2 )
assume that
A1: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] and
A2: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds T2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ; ::_thesis: T1 = T2
A3: now__::_thesis:_for_a_being_Object_of_A_holds_T1_._a_=_T2_._a
let a be Object of A; ::_thesis: T1 . a = T2 . a
T1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A1;
hence T1 . a = T2 . a by A2; ::_thesis: verum
end;
export F1 is_naturally_transformable_to export F2 by B1, Th23;
then export F1 is_transformable_to export F2 by NATTRA_1:def_7;
hence T1 = T2 by A3, NATTRA_1:19; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines export ISOCAT_2:def_5_:_
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2
for b7 being natural_transformation of export F1, export F2 holds
( b7 = export t iff for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds
for a being Object of A holds b7 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] );
theorem Th24: :: ISOCAT_2:24
for A, B, C being Category
for F being Functor of [:A,B:],C holds id (export F) = export (id F)
proof
let A, B, C be Category; ::_thesis: for F being Functor of [:A,B:],C holds id (export F) = export (id F)
let F be Functor of [:A,B:],C; ::_thesis: id (export F) = export (id F)
reconsider s = id F as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
now__::_thesis:_for_a_being_Object_of_A_holds_(id_(export_F))_._a_=_(export_(id_F))_._a
let a be Object of A; ::_thesis: (id (export F)) . a = (export (id F)) . a
reconsider ff = (export F) . a as Functor of B,C by Th7;
A1: now__::_thesis:_for_b_being_Object_of_B_holds_(id_ff)_._b_=_((curry_s)_._a)_._b
let b be Object of B; ::_thesis: (id ff) . b = ((curry s) . a) . b
thus (id ff) . b = (id ff) . b by NATTRA_1:def_5
.= id (ff . b) by NATTRA_1:20
.= ff . (id b) by CAT_1:71
.= (F ?- a) . (id b) by Th20
.= F . ((id a),(id b)) by CAT_2:36
.= F . (id [a,b]) by CAT_2:31
.= id (F . [a,b]) by CAT_1:71
.= (id F) . [a,b] by NATTRA_1:20
.= (id F) . (a,b) by NATTRA_1:def_5
.= ((curry s) . a) . b by FUNCT_5:69 ; ::_thesis: verum
end;
thus (id (export F)) . a = id ((export F) . a) by NATTRA_1:20
.= [[ff,ff],(id ff)] by NATTRA_1:def_17
.= [[((export F) . a),((export F) . a)],((curry s) . a)] by A1, FUNCT_2:63
.= (export (id F)) . a by Def5 ; ::_thesis: verum
end;
hence id (export F) = export (id F) by NATTRA_1:19; ::_thesis: verum
end;
theorem Th25: :: ISOCAT_2:25
for A, B, C being Category
for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
proof
let A, B, C be Category; ::_thesis: for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
let F1, F2, F3 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_naturally_transformable_to F3 ; ::_thesis: for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
A3: F2 is_transformable_to F3 by A2, NATTRA_1:def_7;
let t1 be natural_transformation of F1,F2; ::_thesis: for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)
let t2 be natural_transformation of F2,F3; ::_thesis: export (t2 `*` t1) = (export t2) `*` (export t1)
A4: F1 is_transformable_to F2 by A1, NATTRA_1:def_7;
A5: export F1 is_naturally_transformable_to export F2 by A1, Th23;
then A6: export F1 is_transformable_to export F2 by NATTRA_1:def_7;
A7: export F2 is_naturally_transformable_to export F3 by A2, Th23;
then A8: export F2 is_transformable_to export F3 by NATTRA_1:def_7;
A9: F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1:23;
then A10: F1 is_transformable_to F3 by NATTRA_1:def_7;
now__::_thesis:_for_a_being_Object_of_A_holds_(export_(t2_`*`_t1))_._a_=_((export_t2)_`*`_(export_t1))_._a
let a be Object of A; ::_thesis: (export (t2 `*` t1)) . a = ((export t2) `*` (export t1)) . a
reconsider S1 = (export F1) . a, S2 = (export F2) . a, S3 = (export F3) . a as Functor of B,C by Th7;
reconsider s1 = t1, s2 = t2, s3 = t2 `*` t1 as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
A11: S2 = F2 ?- a by Th20;
A12: S3 = F3 ?- a by Th20;
then reconsider T2 = (curry s2) . a as natural_transformation of S2,S3 by A2, A11, Th13;
A13: S2 is_naturally_transformable_to S3 by A2, A11, A12, Th13;
then A14: S2 is_transformable_to S3 by NATTRA_1:def_7;
A15: S1 = F1 ?- a by Th20;
then reconsider T1 = (curry s1) . a as natural_transformation of S1,S2 by A1, A11, Th13;
A16: ( (export t2) . a = [[S2,S3],T2] & (export t1) . a = [[S1,S2],T1] ) by A1, A2, Def5;
A17: S1 is_naturally_transformable_to S2 by A1, A15, A11, Th13;
then S1 is_naturally_transformable_to S3 by A13, NATTRA_1:23;
then A18: S1 is_transformable_to S3 by NATTRA_1:def_7;
reconsider T3 = (curry s3) . a as natural_transformation of S1,S3 by A9, A15, A12, Th13;
A19: ( Hom (((export F1) . a),((export F2) . a)) <> {} & Hom (((export F2) . a),((export F3) . a)) <> {} ) by A6, A8, NATTRA_1:def_2;
A20: S1 is_transformable_to S2 by A17, NATTRA_1:def_7;
now__::_thesis:_for_b_being_Object_of_B_holds_T3_._b_=_(T2_`*`_T1)_._b
let b be Object of B; ::_thesis: T3 . b = (T2 `*` T1) . b
A21: ( Hom ((F1 . [a,b]),(F2 . [a,b])) <> {} & Hom ((F2 . [a,b]),(F3 . [a,b])) <> {} ) by A4, A3, NATTRA_1:def_2;
A22: ( Hom ((S1 . b),(S2 . b)) <> {} & Hom ((S2 . b),(S3 . b)) <> {} ) by A20, A14, NATTRA_1:def_2;
A23: T1 . b = T1 . b by A20, NATTRA_1:def_5
.= s1 . (a,b) by FUNCT_5:69
.= t1 . [a,b] by A4, NATTRA_1:def_5 ;
A24: T2 . b = T2 . b by A14, NATTRA_1:def_5
.= s2 . (a,b) by FUNCT_5:69
.= t2 . [a,b] by A3, NATTRA_1:def_5 ;
thus T3 . b = T3 . b by A18, NATTRA_1:def_5
.= s3 . (a,b) by FUNCT_5:69
.= (t2 `*` t1) . [a,b] by A10, NATTRA_1:def_5
.= (t2 . [a,b]) * (t1 . [a,b]) by A1, A2, NATTRA_1:25
.= (T2 . b) (*) (T1 . b) by A21, A24, A23, CAT_1:def_13
.= (T2 . b) * (T1 . b) by A22, CAT_1:def_13
.= (T2 `*` T1) . b by A17, A13, NATTRA_1:25 ; ::_thesis: verum
end;
then A25: T3 = T2 `*` T1 by A18, NATTRA_1:19;
thus (export (t2 `*` t1)) . a = [[S1,S3],T3] by A9, Def5
.= ((export t2) . a) (*) ((export t1) . a) by A16, A25, NATTRA_1:36
.= ((export t2) . a) * ((export t1) . a) by A19, CAT_1:def_13
.= ((export t2) `*` (export t1)) . a by A5, A7, NATTRA_1:25 ; ::_thesis: verum
end;
hence export (t2 `*` t1) = (export t2) `*` (export t1) by A6, A8, NATTRA_1:18, NATTRA_1:19; ::_thesis: verum
end;
theorem Th26: :: ISOCAT_2:26
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2
let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2 )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds
t1 = t2
then A2: F1 is_transformable_to F2 by NATTRA_1:def_7;
let t1, t2 be natural_transformation of F1,F2; ::_thesis: ( export t1 = export t2 implies t1 = t2 )
assume A3: export t1 = export t2 ; ::_thesis: t1 = t2
now__::_thesis:_for_ab_being_Object_of_[:A,B:]_holds_t1_._ab_=_t2_._ab
reconsider s1 = t1, s2 = t2 as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;
let ab be Object of [:A,B:]; ::_thesis: t1 . ab = t2 . ab
consider a being Object of A, b being Object of B such that
A4: ab = [a,b] by DOMAIN_1:1;
[[((export F1) . a),((export F2) . a)],((curry s1) . a)] = (export t1) . a by A1, Def5
.= [[((export F1) . a),((export F2) . a)],((curry s2) . a)] by A1, A3, Def5 ;
then A5: (curry s1) . a = (curry s2) . a by XTUPLE_0:1;
thus t1 . ab = s1 . (a,b) by A2, A4, NATTRA_1:def_5
.= ((curry s2) . a) . b by A5, FUNCT_5:69
.= s2 . (a,b) by FUNCT_5:69
.= t2 . ab by A2, A4, NATTRA_1:def_5 ; ::_thesis: verum
end;
hence t1 = t2 by A1, ISOCAT_1:26; ::_thesis: verum
end;
theorem Th27: :: ISOCAT_2:27
for A, B, C being Category
for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F
proof
let A, B, C be Category; ::_thesis: for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F
let G be Functor of A, Functors (B,C); ::_thesis: ex F being Functor of [:A,B:],C st G = export F
defpred S1[ set , set ] means for f being Morphism of A
for g being Morphism of B st $1 = [f,g] holds
for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
$2 = (t . (cod g)) (*) (f1 . g);
A1: now__::_thesis:_for_m_being_set_st_m_in_the_carrier'_of_[:A,B:]_holds_
ex_o_being_set_st_
(_o_in_the_carrier'_of_C_&_S1[m,o]_)
let m be set ; ::_thesis: ( m in the carrier' of [:A,B:] implies ex o being set st
( o in the carrier' of C & S1[m,o] ) )
assume m in the carrier' of [:A,B:] ; ::_thesis: ex o being set st
( o in the carrier' of C & S1[m,o] )
then consider m1 being Morphism of A, m2 being Morphism of B such that
A2: m = [m1,m2] by CAT_2:27;
consider F1, F2 being Functor of B,C, t1 being natural_transformation of F1,F2 such that
F1 is_naturally_transformable_to F2 and
dom (G . m1) = F1 and
cod (G . m1) = F2 and
A3: G . m1 = [[F1,F2],t1] by Th8;
reconsider o = (t1 . (cod m2)) (*) (F1 . m2) as set ;
take o = o; ::_thesis: ( o in the carrier' of C & S1[m,o] )
thus o in the carrier' of C ; ::_thesis: S1[m,o]
thus S1[m,o] ::_thesis: verum
proof
let f be Morphism of A; ::_thesis: for g being Morphism of B st m = [f,g] holds
for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g)
let g be Morphism of B; ::_thesis: ( m = [f,g] implies for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g) )
assume A4: m = [f,g] ; ::_thesis: for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g)
then A5: g = m2 by A2, XTUPLE_0:1;
let f1, f2 be Functor of B,C; ::_thesis: for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g)
let t be natural_transformation of f1,f2; ::_thesis: ( G . f = [[f1,f2],t] implies o = (t . (cod g)) (*) (f1 . g) )
assume A6: G . f = [[f1,f2],t] ; ::_thesis: o = (t . (cod g)) (*) (f1 . g)
A7: f = m1 by A2, A4, XTUPLE_0:1;
then [F1,F2] = [f1,f2] by A3, A6, XTUPLE_0:1;
then ( F1 = f1 & F2 = f2 ) by XTUPLE_0:1;
hence o = (t . (cod g)) (*) (f1 . g) by A3, A7, A5, A6, XTUPLE_0:1; ::_thesis: verum
end;
end;
consider F being Function of the carrier' of [:A,B:], the carrier' of C such that
A8: for m being set st m in the carrier' of [:A,B:] holds
S1[m,F . m] from FUNCT_2:sch_1(A1);
F is Functor of [:A,B:],C
proof
thus for ab being Object of [:A,B:] ex c being Object of C st F . (id ab) = id c :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of [:A,B:] holds
( F . (id (dom b1)) = id (dom (F . b1)) & F . (id (cod b1)) = id (cod (F . b1)) ) ) & ( for b1, b2 being Element of the carrier' of [:A,B:] holds
( not dom b2 = cod b1 or F . (b2 (*) b1) = (F . b2) (*) (F . b1) ) ) )
proof
let ab be Object of [:A,B:]; ::_thesis: ex c being Object of C st F . (id ab) = id c
consider a being Object of A, b being Object of B such that
A9: ab = [a,b] by CAT_2:25;
reconsider H = G . a as Functor of B,C by Th7;
take H . b ; ::_thesis: F . (id ab) = id (H . b)
A10: Hom ((H . b),(H . b)) <> {} ;
A11: G . (id a) = id (G . a) by CAT_1:71
.= [[H,H],(id H)] by NATTRA_1:def_17 ;
id ab = [(id a),(id b)] by A9, CAT_2:31;
hence F . (id ab) = ((id H) . (cod (id b))) (*) (H . (id b)) by A8, A11
.= ((id H) . (cod (id b))) (*) (id (H . b)) by CAT_1:71
.= ((id H) . b) (*) (id (H . b)) by CAT_1:58
.= (id (H . b)) (*) (id (H . b)) by NATTRA_1:20
.= (id (H . b)) * (id (H . b)) by A10, CAT_1:def_13
.= id (H . b) ;
::_thesis: verum
end;
thus for f being Morphism of [:A,B:] holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of [:A,B:] holds
( not dom b2 = cod b1 or F . (b2 (*) b1) = (F . b2) (*) (F . b1) )
proof
let f be Morphism of [:A,B:]; ::_thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
consider f1 being Morphism of A, f2 being Morphism of B such that
A12: f = [f1,f2] by CAT_2:27;
reconsider H = G . (dom f1) as Functor of B,C by Th7;
A13: Hom ((dom (H . f2)),(dom (H . f2))) <> {} ;
A14: ( id (G . (dom f1)) = [[H,H],(id H)] & G . (id (dom f1)) = id (G . (dom f1)) ) by CAT_1:71, NATTRA_1:def_17;
consider F1, F2 being Functor of B,C, t being natural_transformation of F1,F2 such that
A15: F1 is_naturally_transformable_to F2 and
A16: dom (G . f1) = F1 and
A17: cod (G . f1) = F2 and
A18: G . f1 = [[F1,F2],t] by Th8;
A19: F1 . (cod f2) = cod (F1 . f2) by CAT_1:72;
Hom ((F1 . (cod f2)),(F2 . (cod f2))) <> {} by A15, ISOCAT_1:25;
then A20: dom (t . (cod f2)) = cod (F1 . f2) by A19, CAT_1:5;
A21: F1 = H by A16, CAT_1:72;
id (dom f) = id [(dom f1),(dom f2)] by A12, CAT_2:28
.= [(id (dom f1)),(id (dom f2))] by CAT_2:31 ;
hence F . (id (dom f)) = ((id H) . (cod (id (dom f2)))) (*) (H . (id (dom f2))) by A8, A14
.= ((id H) . (cod (id (dom f2)))) (*) (id (H . (dom f2))) by CAT_1:71
.= ((id H) . (cod (id (dom f2)))) (*) (id (dom (H . f2))) by CAT_1:72
.= ((id H) . (dom f2)) (*) (id (dom (H . f2))) by CAT_1:58
.= (id (H . (dom f2))) (*) (id (dom (H . f2))) by NATTRA_1:20
.= (id (dom (H . f2))) (*) (id (dom (H . f2))) by CAT_1:72
.= (id (dom (H . f2))) * (id (dom (H . f2))) by A13, CAT_1:def_13
.= id (dom (F1 . f2)) by A21
.= id (dom ((t . (cod f2)) (*) (F1 . f2))) by A20, CAT_1:17
.= id (dom (F . f)) by A8, A12, A18 ;
::_thesis: F . (id (cod f)) = id (cod (F . f))
reconsider H = G . (cod f1) as Functor of B,C by Th7;
A22: F2 = H by A17, CAT_1:72;
A23: Hom ((cod (H . f2)),(cod (H . f2))) <> {} ;
A24: id (cod f) = id [(cod f1),(cod f2)] by A12, CAT_2:28
.= [(id (cod f1)),(id (cod f2))] by CAT_2:31 ;
A25: Hom ((F1 . (cod f2)),(F2 . (cod f2))) <> {} by A15, ISOCAT_1:25;
F1 . (cod f2) = cod (F1 . f2) by CAT_1:72;
then A26: dom (t . (cod f2)) = cod (F1 . f2) by A25, CAT_1:5;
( id (G . (cod f1)) = [[H,H],(id H)] & G . (id (cod f1)) = id (G . (cod f1)) ) by CAT_1:71, NATTRA_1:def_17;
hence F . (id (cod f)) = ((id H) . (cod (id (cod f2)))) (*) (H . (id (cod f2))) by A8, A24
.= ((id H) . (cod (id (cod f2)))) (*) (id (H . (cod f2))) by CAT_1:71
.= ((id H) . (cod (id (cod f2)))) (*) (id (cod (H . f2))) by CAT_1:72
.= ((id H) . (cod f2)) (*) (id (cod (H . f2))) by CAT_1:58
.= (id (H . (cod f2))) (*) (id (cod (H . f2))) by NATTRA_1:20
.= (id (cod (H . f2))) (*) (id (cod (H . f2))) by CAT_1:72
.= (id (cod (H . f2))) * (id (cod (H . f2))) by A23, CAT_1:def_13
.= id (cod (H . f2))
.= id (F2 . (cod f2)) by A22, CAT_1:72
.= id (cod (t . (cod f2))) by A25, CAT_1:5
.= id (cod ((t . (cod f2)) (*) (F1 . f2))) by A26, CAT_1:17
.= id (cod (F . f)) by A8, A12, A18 ;
::_thesis: verum
end;
let f, g be Morphism of [:A,B:]; ::_thesis: ( not dom g = cod f or F . (g (*) f) = (F . g) (*) (F . f) )
assume A27: dom g = cod f ; ::_thesis: F . (g (*) f) = (F . g) (*) (F . f)
consider g1 being Morphism of A, g2 being Morphism of B such that
A28: g = [g1,g2] by CAT_2:27;
reconsider g29 = g2 as Morphism of dom g2, cod g2 by CAT_1:4;
consider f1 being Morphism of A, f2 being Morphism of B such that
A29: f = [f1,f2] by CAT_2:27;
A30: [(cod f1),(cod f2)] = cod f by A29, CAT_2:28;
consider G1, G2 being Functor of B,C, s being natural_transformation of G1,G2 such that
A31: G1 is_naturally_transformable_to G2 and
A32: dom (G . g1) = G1 and
cod (G . g1) = G2 and
A33: G . g1 = [[G1,G2],s] by Th8;
consider F1, F2 being Functor of B,C, t being natural_transformation of F1,F2 such that
A34: F1 is_naturally_transformable_to F2 and
dom (G . f1) = F1 and
A35: cod (G . f1) = F2 and
A36: G . f1 = [[F1,F2],t] by Th8;
A37: F . f = (t . (cod f2)) (*) (F1 . f2) by A8, A29, A36;
A38: [(dom g1),(dom g2)] = dom g by A28, CAT_2:28;
then A39: cod f1 = dom g1 by A27, A30, XTUPLE_0:1;
then reconsider s = s as natural_transformation of F2,G2 by A35, A32, CAT_1:64;
A40: cod f2 = dom g2 by A27, A30, A38, XTUPLE_0:1;
then A41: g (*) f = [(g1 (*) f1),(g2 (*) f2)] by A29, A28, A39, CAT_2:29;
reconsider f29 = f2 as Morphism of dom f2, dom g2 by A40, CAT_1:4;
A42: cod (g2 (*) f2) = cod g2 by A40, CAT_1:17;
A43: Hom ((dom f2),(dom g2)) <> {} by A40, CAT_1:2;
then A44: Hom ((F1 . (dom f2)),(F1 . (dom g2))) <> {} by CAT_1:84;
A45: Hom ((F1 . (dom g2)),(F2 . (dom g2))) <> {} by A34, ISOCAT_1:25;
then A46: Hom ((F1 . (dom f2)),(F2 . (dom g2))) <> {} by A44, CAT_1:24;
A47: Hom ((dom g2),(cod g2)) <> {} by CAT_1:2;
then A48: F1 /. g2 = F1 /. g29 by CAT_3:def_10;
A49: F2 = G1 by A35, A32, A39, CAT_1:64;
then A50: Hom ((F2 . (cod g2)),(G2 . (cod g2))) <> {} by A31, ISOCAT_1:25;
A51: G1 /. g2 = F2 /. g29 by A49, A47, CAT_3:def_10;
A52: Hom ((F2 . (dom g2)),(F2 . (cod g2))) <> {} by A47, CAT_1:84;
then A53: Hom ((F2 . (dom g2)),(G2 . (cod g2))) <> {} by A50, CAT_1:24;
A54: Hom ((F1 . (dom g2)),(F1 . (cod g2))) <> {} by A47, CAT_1:84;
then A55: Hom ((F1 . (dom f2)),(F1 . (cod g2))) <> {} by A44, CAT_1:24;
A56: Hom ((F1 . (cod g2)),(F2 . (cod g2))) <> {} by A34, ISOCAT_1:25;
then A57: Hom ((F1 . (cod g2)),(G2 . (cod g2))) <> {} by A50, CAT_1:24;
A58: F1 /. f2 = F1 /. f29 by A43, CAT_3:def_10;
G . (g1 (*) f1) = (G . g1) (*) (G . f1) by A39, CAT_1:64
.= [[F1,G2],(s `*` t)] by A36, A33, A49, NATTRA_1:36 ;
hence F . (g (*) f) = ((s `*` t) . (cod (g2 (*) f2))) (*) (F1 . (g2 (*) f2)) by A8, A41
.= ((s . (cod g2)) * (t . (cod g2))) (*) (F1 . (g2 (*) f2)) by A34, A31, A49, A42, NATTRA_1:25
.= ((s . (cod g2)) * (t . (cod g2))) (*) ((F1 /. g2) (*) (F1 /. f2)) by A40, CAT_1:64
.= ((s . (cod g2)) * (t . (cod g2))) (*) ((F1 /. g29) * (F1 /. f29)) by A44, A54, A48, A58, CAT_1:def_13
.= ((s . (cod g2)) * (t . (cod g2))) * ((F1 /. g29) * (F1 /. f29)) by A55, A57, CAT_1:def_13
.= (s . (cod g2)) * ((t . (cod g2)) * ((F1 /. g29) * (F1 /. f29))) by A50, A56, A55, CAT_1:25
.= (s . (cod g2)) * (((t . (cod g2)) * (F1 /. g29)) * (F1 /. f29)) by A56, A44, A54, CAT_1:25
.= (s . (cod g2)) * (((F2 /. g29) * (t . (dom g2))) * (F1 /. f29)) by A34, A47, NATTRA_1:def_8
.= (s . (cod g2)) * ((F2 /. g29) * ((t . (dom g2)) * (F1 /. f29))) by A44, A52, A45, CAT_1:25
.= ((s . (cod g2)) * (F2 /. g29)) * ((t . (dom g2)) * (F1 /. f29)) by A50, A52, A46, CAT_1:25
.= ((s . (cod g2)) * (F2 /. g29)) (*) ((t . (dom g2)) * (F1 /. f29)) by A46, A53, CAT_1:def_13
.= ((s . (cod g2)) * (F2 /. g29)) (*) ((t . (cod f2)) (*) (F1 . f2)) by A40, A44, A45, A58, CAT_1:def_13
.= ((s . (cod g2)) (*) (G1 /. g2)) (*) ((t . (cod f2)) (*) (F1 . f2)) by A50, A52, A51, CAT_1:def_13
.= (F . g) (*) (F . f) by A8, A28, A33, A49, A37 ;
::_thesis: verum
end;
then reconsider F = F as Functor of [:A,B:],C ;
take F ; ::_thesis: G = export F
now__::_thesis:_for_f_being_Morphism_of_A_holds_G_._f_=_[[(F_?-_(dom_f)),(F_?-_(cod_f))],(F_?-_f)]
let f be Morphism of A; ::_thesis: G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]
consider f1, f2 being Functor of B,C, t being natural_transformation of f1,f2 such that
A59: f1 is_naturally_transformable_to f2 and
A60: dom (G . f) = f1 and
A61: cod (G . f) = f2 and
A62: G . f = [[f1,f2],t] by Th8;
now__::_thesis:_for_g_being_Morphism_of_B_holds_(F_?-_(dom_f))_._g_=_f1_._g
let g be Morphism of B; ::_thesis: (F ?- (dom f)) . g = f1 . g
A63: dom (id (cod g)) = cod g ;
A64: f1 = G . (dom f) by A60, CAT_1:72;
A65: G . (id (dom f)) = id (G . (dom f)) by CAT_1:71
.= [[f1,f1],(id f1)] by A64, NATTRA_1:def_17 ;
thus (F ?- (dom f)) . g = F . ((id (dom f)),g) by CAT_2:36
.= F . [(id (dom f)),g]
.= ((id f1) . (cod g)) (*) (f1 . g) by A8, A65
.= (id (f1 . (cod g))) (*) (f1 . g) by NATTRA_1:20
.= (f1 . (id (cod g))) (*) (f1 . g) by CAT_1:71
.= f1 . ((id (cod g)) (*) g) by A63, CAT_1:64
.= f1 . g by CAT_1:21 ; ::_thesis: verum
end;
then A66: f1 = F ?- (dom f) by FUNCT_2:63;
now__::_thesis:_for_g_being_Morphism_of_B_holds_(F_?-_(cod_f))_._g_=_f2_._g
let g be Morphism of B; ::_thesis: (F ?- (cod f)) . g = f2 . g
A67: dom (id (cod g)) = cod g ;
A68: f2 = G . (cod f) by A61, CAT_1:72;
A69: G . (id (cod f)) = id (G . (cod f)) by CAT_1:71
.= [[f2,f2],(id f2)] by A68, NATTRA_1:def_17 ;
thus (F ?- (cod f)) . g = F . ((id (cod f)),g) by CAT_2:36
.= F . [(id (cod f)),g]
.= ((id f2) . (cod g)) (*) (f2 . g) by A8, A69
.= (id (f2 . (cod g))) (*) (f2 . g) by NATTRA_1:20
.= (f2 . (id (cod g))) (*) (f2 . g) by CAT_1:71
.= f2 . ((id (cod g)) (*) g) by A67, CAT_1:64
.= f2 . g by CAT_1:21 ; ::_thesis: verum
end;
then A70: f2 = F ?- (cod f) by FUNCT_2:63;
now__::_thesis:_for_b_being_Object_of_B_holds_(F_?-_f)_._b_=_t_._b
let b be Object of B; ::_thesis: (F ?- f) . b = t . b
A71: Hom ((f1 . b),(f1 . b)) <> {} ;
A72: Hom ((f1 . b),(f2 . b)) <> {} by A59, ISOCAT_1:25;
thus (F ?- f) . b = F . (f,(id b)) by Th17
.= F . [f,(id b)]
.= (t . (cod (id b))) (*) (f1 . (id b)) by A8, A62
.= (t . (cod (id b))) (*) (id (f1 . b)) by CAT_1:71
.= (t . b) (*) (id (f1 . b)) by CAT_1:58
.= (t . b) * (id (f1 . b)) by A72, A71, CAT_1:def_13
.= t . b by A72, CAT_1:29 ; ::_thesis: verum
end;
hence G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] by A59, A62, A66, A70, ISOCAT_1:26; ::_thesis: verum
end;
hence G = export F by Def4; ::_thesis: verum
end;
theorem Th28: :: ISOCAT_2:28
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds
for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds
for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( export F1 is_naturally_transformable_to export F2 implies for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) )
assume A1: export F1 is_naturally_transformable_to export F2 ; ::_thesis: for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
let t be natural_transformation of export F1, export F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
defpred S1[ set , set ] means for a being Object of A st $1 = a holds
t . a = [[((export F1) . a),((export F2) . a)],$2];
A2: now__::_thesis:_for_o_being_set_st_o_in_the_carrier_of_A_holds_
ex_m_being_set_st_
(_m_in_Funcs_(_the_carrier_of_B,_the_carrier'_of_C)_&_S1[o,m]_)
let o be set ; ::_thesis: ( o in the carrier of A implies ex m being set st
( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] ) )
assume o in the carrier of A ; ::_thesis: ex m being set st
( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] )
then reconsider a9 = o as Object of A ;
consider f1, f2 being Functor of B,C, tau being natural_transformation of f1,f2 such that
f1 is_naturally_transformable_to f2 and
A3: dom (t . a9) = f1 and
A4: ( cod (t . a9) = f2 & t . a9 = [[f1,f2],tau] ) by Th8;
reconsider m = tau as set ;
take m = m; ::_thesis: ( m in Funcs ( the carrier of B, the carrier' of C) & S1[o,m] )
thus m in Funcs ( the carrier of B, the carrier' of C) by FUNCT_2:8; ::_thesis: S1[o,m]
thus S1[o,m] ::_thesis: verum
proof
let a be Object of A; ::_thesis: ( o = a implies t . a = [[((export F1) . a),((export F2) . a)],m] )
assume A5: o = a ; ::_thesis: t . a = [[((export F1) . a),((export F2) . a)],m]
export F1 is_transformable_to export F2 by A1, NATTRA_1:def_7;
then A6: Hom (((export F1) . a),((export F2) . a)) <> {} by NATTRA_1:def_2;
then (export F1) . a = f1 by A3, A5, CAT_1:5;
hence t . a = [[((export F1) . a),((export F2) . a)],m] by A4, A5, A6, CAT_1:5; ::_thesis: verum
end;
end;
consider t9 being Function of the carrier of A,(Funcs ( the carrier of B, the carrier' of C)) such that
A7: for o being set st o in the carrier of A holds
S1[o,t9 . o] from FUNCT_2:sch_1(A2);
reconsider u9 = uncurry t9 as Function of the carrier of [:A,B:], the carrier' of C ;
A8: now__::_thesis:_for_ab_being_Object_of_[:A,B:]_holds_u9_._ab_in_Hom_((F1_._ab),(F2_._ab))
let ab be Object of [:A,B:]; ::_thesis: u9 . ab in Hom ((F1 . ab),(F2 . ab))
consider a being Object of A, b being Object of B such that
A9: ab = [a,b] by DOMAIN_1:1;
( (export F1) . a = F1 ?- a & (export F2) . a = F2 ?- a ) by Th20;
then t . a = [[(F1 ?- a),(F2 ?- a)],(t9 . a)] by A7;
then [[(F1 ?- a),(F2 ?- a)],(t9 . a)] in the carrier' of (Functors (B,C)) ;
then [[(F1 ?- a),(F2 ?- a)],(t9 . a)] in NatTrans (B,C) by NATTRA_1:def_17;
then consider G1, G2 being Functor of B,C, t99 being natural_transformation of G1,G2 such that
A10: [[(F1 ?- a),(F2 ?- a)],(t9 . a)] = [[G1,G2],t99] and
A11: G1 is_naturally_transformable_to G2 by NATTRA_1:def_15;
A12: G1 is_transformable_to G2 by A11, NATTRA_1:def_7;
A13: [(F1 ?- a),(F2 ?- a)] = [G1,G2] by A10, XTUPLE_0:1;
A14: F1 . [a,b] = (F1 ?- a) . b by Th10
.= G1 . b by A13, XTUPLE_0:1 ;
A15: Hom ((G1 . b),(G2 . b)) <> {} by A11, ISOCAT_1:25;
A16: F2 . [a,b] = (F2 ?- a) . b by Th10
.= G2 . b by A13, XTUPLE_0:1 ;
u9 . (a,b) = (t9 . a) . b by Th2
.= t99 . b by A10, XTUPLE_0:1
.= t99 . b by A12, NATTRA_1:def_5 ;
hence u9 . ab in Hom ((F1 . ab),(F2 . ab)) by A9, A14, A16, A15, CAT_1:def_5; ::_thesis: verum
end;
A17: F1 is_transformable_to F2
proof
let a be Object of [:A,B:]; :: according to NATTRA_1:def_2 ::_thesis: not Hom ((F1 . a),(F2 . a)) = {}
thus not Hom ((F1 . a),(F2 . a)) = {} by A8; ::_thesis: verum
end;
u9 is transformation of F1,F2
proof
thus F1 is_transformable_to F2 by A17; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of [:A,B:] holds u9 . b1 is Morphism of F1 . b1,F2 . b1
let a be Object of [:A,B:]; ::_thesis: u9 . a is Morphism of F1 . a,F2 . a
u9 . a in Hom ((F1 . a),(F2 . a)) by A8;
hence u9 . a is Morphism of F1 . a,F2 . a by CAT_1:def_5; ::_thesis: verum
end;
then reconsider u = u9 as transformation of F1,F2 ;
A18: now__::_thesis:_for_ab1,_ab2_being_Object_of_[:A,B:]_st_Hom_(ab1,ab2)_<>_{}_holds_
for_f_being_Morphism_of_ab1,ab2_holds_(u_._ab2)_*_(F1_/._f)_=_(F2_/._f)_*_(u_._ab1)
reconsider FF1 = F1, FF2 = F2 as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
let ab1, ab2 be Object of [:A,B:]; ::_thesis: ( Hom (ab1,ab2) <> {} implies for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1) )
assume A19: Hom (ab1,ab2) <> {} ; ::_thesis: for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1)
A20: Hom ((F2 . ab1),(F2 . ab2)) <> {} by A19, CAT_1:84;
consider a2 being Object of A, b2 being Object of B such that
A21: ab2 = [a2,b2] by DOMAIN_1:1;
( (export F1) . a2 = F1 ?- a2 & (export F2) . a2 = F2 ?- a2 ) by Th20;
then t . a2 = [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] by A7;
then [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in the carrier' of (Functors (B,C)) ;
then [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in NatTrans (B,C) by NATTRA_1:def_17;
then consider G2, H2 being Functor of B,C, t2 being natural_transformation of G2,H2 such that
A22: [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] = [[G2,H2],t2] and
A23: G2 is_naturally_transformable_to H2 by NATTRA_1:def_15;
A24: ( t9 . a2 = t2 & G2 is_transformable_to H2 ) by A22, A23, NATTRA_1:def_7, XTUPLE_0:1;
consider a1 being Object of A, b1 being Object of B such that
A25: ab1 = [a1,b1] by DOMAIN_1:1;
( (export F1) . a1 = F1 ?- a1 & (export F2) . a1 = F2 ?- a1 ) by Th20;
then t . a1 = [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] by A7;
then [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in the carrier' of (Functors (B,C)) ;
then [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in NatTrans (B,C) by NATTRA_1:def_17;
then consider G1, H1 being Functor of B,C, t1 being natural_transformation of G1,H1 such that
A26: [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] = [[G1,H1],t1] and
A27: G1 is_naturally_transformable_to H1 by NATTRA_1:def_15;
A28: ( t9 . a1 = t1 & G1 is_transformable_to H1 ) by A26, A27, NATTRA_1:def_7, XTUPLE_0:1;
A29: u . ab1 = u9 . (a1,b1) by A17, A25, NATTRA_1:def_5
.= (t9 . a1) . b1 by Th2
.= t1 . b1 by A28, NATTRA_1:def_5 ;
A30: Hom ((G1 . b2),(H1 . b2)) <> {} by A27, ISOCAT_1:25;
A31: Hom ((F1 . ab1),(F1 . ab2)) <> {} by A19, CAT_1:84;
A32: Hom ((F1 . ab2),(F2 . ab2)) <> {} by A17, NATTRA_1:def_2;
( (export F2) . a1 = F2 ?- a1 & (export F1) . a1 = F1 ?- a1 ) by Th20;
then A33: t . a1 = [[G1,H1],t1] by A7, A26;
A34: Hom ((G1 . b1),(H1 . b1)) <> {} by A27, ISOCAT_1:25;
( (export F1) . a2 = F1 ?- a2 & (export F2) . a2 = F2 ?- a2 ) by Th20;
then A35: t . a2 = [[G2,H2],t2] by A7, A22;
A36: Hom (((export F1) . a2),((export F2) . a2)) <> {} by A1, ISOCAT_1:25;
A37: Hom (((export F1) . a1),((export F2) . a1)) <> {} by A1, ISOCAT_1:25;
let f be Morphism of ab1,ab2; ::_thesis: (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1)
consider g being Morphism of A, h being Morphism of B such that
A38: f = [g,h] by DOMAIN_1:1;
reconsider g = g as Morphism of a1,a2 by A19, A25, A21, A38, Th12;
A39: Hom (a1,a2) <> {} by A19, A25, A21, Th11;
then A40: ( dom g = a1 & cod g = a2 ) by CAT_1:5;
reconsider h = h as Morphism of b1,b2 by A19, A25, A21, A38, Th12;
reconsider g9 = g as Morphism of A ;
reconsider h9 = h as Morphism of B ;
reconsider f9 = f as Morphism of [:A,B:] ;
A41: dom (id b2) = b2 ;
Hom (a1,a1) <> {} ;
then A42: g9 (*) (id a1) = g * (id a1) by A39, CAT_1:def_13
.= g by A39, CAT_1:29 ;
A43: dom g = a1 by A39, CAT_1:5;
A44: Hom (((export F2) . a1),((export F2) . a2)) <> {} by A39, CAT_1:84;
reconsider e1 = (export F1) /. g, e2 = (export F2) /. g as Morphism of (Functors (B,C)) ;
A45: Hom ((F1 . ab1),(F2 . ab1)) <> {} by A17, NATTRA_1:def_2;
A46: Hom (b1,b2) <> {} by A19, A25, A21, Th11;
then A47: Hom ((G1 . b1),(G1 . b2)) <> {} by CAT_1:84;
A48: [(F1 ?- a1),(F2 ?- a1)] = [G1,H1] by A26, XTUPLE_0:1;
then A49: F2 ?- a1 = H1 by XTUPLE_0:1;
then A50: H1 /. h = (F2 ?- a1) /. h by A46, CAT_3:def_10
.= F2 . ((id a1),h) by CAT_2:36 ;
A51: [(F1 ?- a2),(F2 ?- a2)] = [G2,H2] by A22, XTUPLE_0:1;
then A52: F2 ?- a2 = H2 by XTUPLE_0:1;
then A53: Hom ((H1 . b2),(H2 . b2)) <> {} by A49, A40, Th16, ISOCAT_1:25;
A54: F1 ?- a2 = G2 by A51, XTUPLE_0:1;
then reconsider v1 = F1 ?- g as natural_transformation of G1,G2 by A48, A40, XTUPLE_0:1;
A55: Hom (((export F1) . a1),((export F1) . a2)) <> {} by A39, CAT_1:84;
( cod (id a1) = a1 & cod h = b2 ) by A46, CAT_1:5;
then A56: cod [(id a1),h] = [a1,b2] by CAT_2:28
.= dom [g,(id b2)] by A43, A41, CAT_2:28 ;
reconsider v2 = F2 ?- g as natural_transformation of H1,H2 by A48, A52, A40, XTUPLE_0:1;
A57: (export F2) . g9 = [[H1,H2],v2] by A49, A52, A40, Def4;
A58: id b2 = (IdMap B) . b2 by ISOCAT_1:def_12;
A59: H1 is_naturally_transformable_to H2 by A49, A52, A40, Th16;
then H1 is_transformable_to H2 by NATTRA_1:def_7;
then A60: v2 . b2 = ((curry (F2,g)) * (IdMap B)) . b2 by NATTRA_1:def_5
.= (curry (F2,g)) . ((IdMap B) . b2) by FUNCT_2:15
.= F2 . (g,(id b2)) by FUNCT_5:69, A58 ;
A61: F1 ?- a1 = G1 by A48, XTUPLE_0:1;
then A62: G1 /. h = (F1 ?- a1) /. h by A46, CAT_3:def_10
.= F1 . ((id a1),h) by CAT_2:36 ;
(export F1) . g9 = [[G1,G2],v1] by A61, A54, A40, Def4;
then [[G1,H2],(t2 `*` v1)] = (t . a2) (*) ((export F1) . g9) by A35, NATTRA_1:36
.= (t . a2) (*) e1 by A39, CAT_3:def_10
.= (t . a2) * ((export F1) /. g) by A55, A36, CAT_1:def_13
.= ((export F2) /. g) * (t . a1) by A1, A39, NATTRA_1:def_8
.= e2 (*) (t . a1) by A44, A37, CAT_1:def_13
.= ((export F2) . g9) (*) (t . a1) by A39, CAT_3:def_10
.= [[G1,H2],(v2 `*` t1)] by A57, A33, NATTRA_1:36 ;
then A63: t2 `*` v1 = v2 `*` t1 by XTUPLE_0:1;
A64: id b2 = (IdMap B) . b2 by ISOCAT_1:def_12;
A65: G1 is_naturally_transformable_to G2 by A61, A54, A40, Th16;
then G1 is_transformable_to G2 by NATTRA_1:def_7;
then A66: v1 . b2 = ((curry (F1,g)) * (IdMap B)) . b2 by NATTRA_1:def_5
.= (curry (F1,g)) . ((IdMap B) . b2) by FUNCT_2:15
.= F1 . (g,(id b2)) by FUNCT_5:69, A64 ;
A67: u . ab2 = u9 . (a2,b2) by A17, A21, NATTRA_1:def_5
.= (t9 . a2) . b2 by Th2
.= t2 . b2 by A24, NATTRA_1:def_5 ;
A68: Hom ((G2 . b2),(H2 . b2)) <> {} by A23, ISOCAT_1:25;
Hom (b2,b2) <> {} ;
then (id b2) (*) h9 = (id b2) * h by A46, CAT_1:def_13
.= h by A46, CAT_1:28 ;
then A69: f = [g,(id b2)] (*) [(id a1),h] by A38, A42, A56, CAT_2:30;
A70: Hom ((H1 . b1),(H1 . b2)) <> {} by A46, CAT_1:84;
then A71: Hom ((H1 . b1),(H2 . b2)) <> {} by A53, CAT_1:24;
A72: F2 /. f = F2 /. f9 by A19, CAT_3:def_10
.= (v2 . b2) (*) (H1 /. h) by A56, A69, A60, A50, CAT_1:64
.= (v2 . b2) * (H1 /. h) by A53, A70, CAT_1:def_13 ;
A73: Hom ((G1 . b2),(G2 . b2)) <> {} by A61, A54, A40, Th16, ISOCAT_1:25;
then A74: Hom ((G1 . b1),(G2 . b2)) <> {} by A47, CAT_1:24;
F1 /. f = F1 /. f9 by A19, CAT_3:def_10
.= (v1 . b2) (*) (G1 /. h) by A56, A69, A66, A62, CAT_1:64
.= (v1 . b2) * (G1 /. h) by A73, A47, CAT_1:def_13 ;
hence (u . ab2) * (F1 /. f) = (t2 . b2) (*) ((v1 . b2) * (G1 /. h)) by A31, A32, A67, CAT_1:def_13
.= (t2 . b2) * ((v1 . b2) * (G1 /. h)) by A68, A74, CAT_1:def_13
.= ((t2 . b2) * (v1 . b2)) * (G1 /. h) by A68, A73, A47, CAT_1:25
.= ((v2 `*` t1) . b2) * (G1 /. h) by A23, A65, A63, NATTRA_1:25
.= ((v2 . b2) * (t1 . b2)) * (G1 /. h) by A27, A59, NATTRA_1:25
.= (v2 . b2) * ((t1 . b2) * (G1 /. h)) by A47, A53, A30, CAT_1:25
.= (v2 . b2) * ((H1 /. h) * (t1 . b1)) by A27, A46, NATTRA_1:def_8
.= ((v2 . b2) * (H1 /. h)) * (t1 . b1) by A53, A70, A34, CAT_1:25
.= (F2 /. f) (*) (u . ab1) by A34, A71, A29, A72, CAT_1:def_13
.= (F2 /. f) * (u . ab1) by A45, A20, CAT_1:def_13 ;
::_thesis: verum
end;
hence A75: F1 is_naturally_transformable_to F2 by A17, NATTRA_1:def_7; ::_thesis: ex u being natural_transformation of F1,F2 st t = export u
then reconsider u = u as natural_transformation of F1,F2 by A18, NATTRA_1:def_8;
take u ; ::_thesis: t = export u
now__::_thesis:_for_s_being_Function_of_[:_the_carrier_of_A,_the_carrier_of_B:],_the_carrier'_of_C_st_u_=_s_holds_
for_a_being_Object_of_A_holds_t_._a_=_[[((export_F1)_._a),((export_F2)_._a)],((curry_s)_._a)]
let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; ::_thesis: ( u = s implies for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
assume A76: u = s ; ::_thesis: for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let a be Object of A; ::_thesis: t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
t9 = curry u9 by Th1;
hence t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A7, A76; ::_thesis: verum
end;
hence t = export u by A75, Def5; ::_thesis: verum
end;
definition
let A, B, C be Category;
func export (A,B,C) -> Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) means :Def6: :: ISOCAT_2:def 6
for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds it . [[F1,F2],t] = [[(export F1),(export F2)],(export t)];
existence
ex b1 being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) st
for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
proof
defpred S1[ set , set ] means for F1, F2 being Functor of [:A,B:],C
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = [[(export F1),(export F2)],(export t)];
A1: now__::_thesis:_for_o_being_set_st_o_in_the_carrier'_of_(Functors_([:A,B:],C))_holds_
ex_m_being_set_st_
(_m_in_the_carrier'_of_(Functors_(A,(Functors_(B,C))))_&_S1[o,m]_)
let o be set ; ::_thesis: ( o in the carrier' of (Functors ([:A,B:],C)) implies ex m being set st
( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] ) )
assume o in the carrier' of (Functors ([:A,B:],C)) ; ::_thesis: ex m being set st
( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] )
then o in NatTrans ([:A,B:],C) by NATTRA_1:def_17;
then consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
A2: o = [[F1,F2],t] and
A3: F1 is_naturally_transformable_to F2 by NATTRA_1:def_16;
take m = [[(export F1),(export F2)],(export t)]; ::_thesis: ( m in the carrier' of (Functors (A,(Functors (B,C)))) & S1[o,m] )
export F1 is_naturally_transformable_to export F2 by A3, Th23;
then m in NatTrans (A,(Functors (B,C))) by NATTRA_1:def_16;
hence m in the carrier' of (Functors (A,(Functors (B,C)))) by NATTRA_1:def_17; ::_thesis: S1[o,m]
thus S1[o,m] ::_thesis: verum
proof
let F19, F29 be Functor of [:A,B:],C; ::_thesis: for t being natural_transformation of F19,F29 st o = [[F19,F29],t] holds
m = [[(export F19),(export F29)],(export t)]
let t9 be natural_transformation of F19,F29; ::_thesis: ( o = [[F19,F29],t9] implies m = [[(export F19),(export F29)],(export t9)] )
assume A4: o = [[F19,F29],t9] ; ::_thesis: m = [[(export F19),(export F29)],(export t9)]
then [F1,F2] = [F19,F29] by A2, XTUPLE_0:1;
then ( F1 = F19 & F2 = F29 ) by XTUPLE_0:1;
hence m = [[(export F19),(export F29)],(export t9)] by A2, A4, XTUPLE_0:1; ::_thesis: verum
end;
end;
consider FF being Function of the carrier' of (Functors ([:A,B:],C)), the carrier' of (Functors (A,(Functors (B,C)))) such that
A5: for o being set st o in the carrier' of (Functors ([:A,B:],C)) holds
S1[o,FF . o] from FUNCT_2:sch_1(A1);
FF is Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C)))
proof
thus for c being Object of (Functors ([:A,B:],C)) ex d being Object of (Functors (A,(Functors (B,C)))) st FF . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of (Functors ([:A,B:],C)) holds
( FF . (id (dom b1)) = id (dom (FF . b1)) & FF . (id (cod b1)) = id (cod (FF . b1)) ) ) & ( for b1, b2 being Element of the carrier' of (Functors ([:A,B:],C)) holds
( not dom b2 = cod b1 or FF . (b2 (*) b1) = (FF . b2) (*) (FF . b1) ) ) )
proof
let c be Object of (Functors ([:A,B:],C)); ::_thesis: ex d being Object of (Functors (A,(Functors (B,C)))) st FF . (id c) = id d
reconsider F = c as Functor of [:A,B:],C by Th7;
reconsider d = export F as Object of (Functors (A,(Functors (B,C)))) by Th7;
take d ; ::_thesis: FF . (id c) = id d
A6: id (export F) = export (id F) by Th24;
id c = [[F,F],(id F)] by NATTRA_1:def_17;
hence FF . (id c) = [[(export F),(export F)],(export (id F))] by A5
.= id d by A6, NATTRA_1:def_17 ;
::_thesis: verum
end;
thus for f being Morphism of (Functors ([:A,B:],C)) holds
( FF . (id (dom f)) = id (dom (FF . f)) & FF . (id (cod f)) = id (cod (FF . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of (Functors ([:A,B:],C)) holds
( not dom b2 = cod b1 or FF . (b2 (*) b1) = (FF . b2) (*) (FF . b1) )
proof
let f be Morphism of (Functors ([:A,B:],C)); ::_thesis: ( FF . (id (dom f)) = id (dom (FF . f)) & FF . (id (cod f)) = id (cod (FF . f)) )
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
F1 is_naturally_transformable_to F2 and
A7: dom f = F1 and
A8: cod f = F2 and
A9: f = [[F1,F2],t] by Th8;
A10: FF . f = [[(export F1),(export F2)],(export t)] by A5, A9;
then A11: dom (FF . f) = export F1 by NATTRA_1:33;
id (dom f) = [[F1,F1],(id F1)] by A7, NATTRA_1:def_17;
hence FF . (id (dom f)) = [[(export F1),(export F1)],(export (id F1))] by A5
.= [[(export F1),(export F1)],(id (export F1))] by Th24
.= id (dom (FF . f)) by A11, NATTRA_1:def_17 ;
::_thesis: FF . (id (cod f)) = id (cod (FF . f))
A12: cod (FF . f) = export F2 by A10, NATTRA_1:33;
id (cod f) = [[F2,F2],(id F2)] by A8, NATTRA_1:def_17;
hence FF . (id (cod f)) = [[(export F2),(export F2)],(export (id F2))] by A5
.= [[(export F2),(export F2)],(id (export F2))] by Th24
.= id (cod (FF . f)) by A12, NATTRA_1:def_17 ;
::_thesis: verum
end;
let f, g be Morphism of (Functors ([:A,B:],C)); ::_thesis: ( not dom g = cod f or FF . (g (*) f) = (FF . g) (*) (FF . f) )
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
A13: F1 is_naturally_transformable_to F2 and
dom f = F1 and
A14: cod f = F2 and
A15: f = [[F1,F2],t] by Th8;
A16: FF . f = [[(export F1),(export F2)],(export t)] by A5, A15;
consider G1, G2 being Functor of [:A,B:],C, u being natural_transformation of G1,G2 such that
A17: G1 is_naturally_transformable_to G2 and
A18: dom g = G1 and
cod g = G2 and
A19: g = [[G1,G2],u] by Th8;
assume A20: dom g = cod f ; ::_thesis: FF . (g (*) f) = (FF . g) (*) (FF . f)
then reconsider u = u as natural_transformation of F2,G2 by A14, A18;
g (*) f = [[F1,G2],(u `*` t)] by A14, A15, A18, A19, A20, NATTRA_1:36;
then A21: FF . (g (*) f) = [[(export F1),(export G2)],(export (u `*` t))] by A5;
( FF . g = [[(export F2),(export G2)],(export u)] & (export u) `*` (export t) = export (u `*` t) ) by A5, A13, A14, A17, A18, A19, A20, Th25;
hence FF . (g (*) f) = (FF . g) (*) (FF . f) by A16, A21, NATTRA_1:36; ::_thesis: verum
end;
then reconsider FF = FF as Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) ;
take FF ; ::_thesis: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
let F1, F2 be Functor of [:A,B:],C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] )
assume A22: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
let t be natural_transformation of F1,F2; ::_thesis: FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
[[F1,F2],t] in NatTrans ([:A,B:],C) by A22, NATTRA_1:32;
then [[F1,F2],t] in the carrier' of (Functors ([:A,B:],C)) by NATTRA_1:def_17;
hence FF . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] by A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) st ( for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) & ( for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) holds
b1 = b2
proof
let IT1, IT2 be Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))); ::_thesis: ( ( for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) & ( for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) implies IT1 = IT2 )
assume that
A23: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] and
A24: for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ; ::_thesis: IT1 = IT2
now__::_thesis:_for_f_being_Morphism_of_(Functors_([:A,B:],C))_holds_IT1_._f_=_IT2_._f
let f be Morphism of (Functors ([:A,B:],C)); ::_thesis: IT1 . f = IT2 . f
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
A25: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A26: f = [[F1,F2],t] by Th8;
thus IT1 . f = [[(export F1),(export F2)],(export t)] by A23, A25, A26
.= IT2 . f by A24, A25, A26 ; ::_thesis: verum
end;
hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines export ISOCAT_2:def_6_:_
for A, B, C being Category
for b4 being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) holds
( b4 = export (A,B,C) iff for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b4 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] );
registration
let A, B, C be Category;
cluster export (A,B,C) -> isomorphic ;
coherence
export (A,B,C) is isomorphic
proof
thus export (A,B,C) is one-to-one :: according to ISOCAT_1:def_3 ::_thesis: rng (export (A,B,C)) = the carrier' of (Functors (A,(Functors (B,C))))
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (export (A,B,C)) or not x2 in dom (export (A,B,C)) or not (export (A,B,C)) . x1 = (export (A,B,C)) . x2 or x1 = x2 )
assume x1 in dom (export (A,B,C)) ; ::_thesis: ( not x2 in dom (export (A,B,C)) or not (export (A,B,C)) . x1 = (export (A,B,C)) . x2 or x1 = x2 )
then reconsider f1 = x1 as Morphism of (Functors ([:A,B:],C)) ;
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
A1: F1 is_naturally_transformable_to F2 and
dom f1 = F1 and
cod f1 = F2 and
A2: f1 = [[F1,F2],t] by Th8;
assume x2 in dom (export (A,B,C)) ; ::_thesis: ( not (export (A,B,C)) . x1 = (export (A,B,C)) . x2 or x1 = x2 )
then reconsider f2 = x2 as Morphism of (Functors ([:A,B:],C)) ;
consider G1, G2 being Functor of [:A,B:],C, u being natural_transformation of G1,G2 such that
A3: G1 is_naturally_transformable_to G2 and
dom f2 = G1 and
cod f2 = G2 and
A4: f2 = [[G1,G2],u] by Th8;
assume (export (A,B,C)) . x1 = (export (A,B,C)) . x2 ; ::_thesis: x1 = x2
then A5: [[(export F1),(export F2)],(export t)] = (export (A,B,C)) . [[G1,G2],u] by A1, A2, A4, Def6
.= [[(export G1),(export G2)],(export u)] by A3, Def6 ;
then A6: [(export F1),(export F2)] = [(export G1),(export G2)] by XTUPLE_0:1;
then export F1 = export G1 by XTUPLE_0:1;
then A7: F1 = G1 by Th22;
export F2 = export G2 by A6, XTUPLE_0:1;
then A8: F2 = G2 by Th22;
export u = export t by A5, XTUPLE_0:1;
hence x1 = x2 by A1, A2, A4, A7, A8, Th26; ::_thesis: verum
end;
thus rng (export (A,B,C)) c= the carrier' of (Functors (A,(Functors (B,C)))) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of (Functors (A,(Functors (B,C)))) c= rng (export (A,B,C))
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in the carrier' of (Functors (A,(Functors (B,C)))) or m in rng (export (A,B,C)) )
assume m in the carrier' of (Functors (A,(Functors (B,C)))) ; ::_thesis: m in rng (export (A,B,C))
then reconsider f = m as Morphism of (Functors (A,(Functors (B,C)))) ;
consider F1, F2 being Functor of A, Functors (B,C), t being natural_transformation of F1,F2 such that
A9: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A10: f = [[F1,F2],t] by Th8;
consider G1 being Functor of [:A,B:],C such that
A11: F1 = export G1 by Th27;
consider G2 being Functor of [:A,B:],C such that
A12: F2 = export G2 by Th27;
consider u being natural_transformation of G1,G2 such that
A13: t = export u by A9, A11, A12, Th28;
A14: G1 is_naturally_transformable_to G2 by A9, A11, A12, Th28;
then ( dom (export (A,B,C)) = the carrier' of (Functors ([:A,B:],C)) & [[G1,G2],u] in NatTrans ([:A,B:],C) ) by FUNCT_2:def_1, NATTRA_1:32;
then A15: [[G1,G2],u] in dom (export (A,B,C)) by NATTRA_1:def_17;
(export (A,B,C)) . [[G1,G2],u] = f by A10, A11, A12, A14, A13, Def6;
hence m in rng (export (A,B,C)) by A15, FUNCT_1:def_3; ::_thesis: verum
end;
end;
theorem :: ISOCAT_2:29
for A, B, C being Category holds Functors ([:A,B:],C) ~= Functors (A,(Functors (B,C)))
proof
let A, B, C be Category; ::_thesis: Functors ([:A,B:],C) ~= Functors (A,(Functors (B,C)))
take export (A,B,C) ; :: according to ISOCAT_1:def_4 ::_thesis: export (A,B,C) is isomorphic
thus export (A,B,C) is isomorphic ; ::_thesis: verum
end;
begin
theorem Th30: :: ISOCAT_2:30
for A, B, C being Category
for F1, F2 being Functor of A,B
for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds G * t = G * t
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B
for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds G * t = G * t
let F1, F2 be Functor of A,B; ::_thesis: for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds G * t = G * t
let G be Functor of B,C; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds G * t = G * t )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds G * t = G * t
then A2: F1 is_transformable_to F2 by NATTRA_1:def_7;
let t be natural_transformation of F1,F2; ::_thesis: G * t = G * t
thus G * t = G * t by A1, ISOCAT_1:def_7
.= G * t by A2, ISOCAT_1:def_5 ; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F be Functor of A,B;
let G be Functor of A,C;
:: original: <:
redefine func<:F,G:> -> Functor of A,[:B,C:];
coherence
<:F,G:> is Functor of A,[:B,C:]
proof
thus <:F,G:> is Functor of A,[:B,C:] ; ::_thesis: verum
end;
end;
definition
let A, B, C be Category;
let F be Functor of A,[:B,C:];
func Pr1 F -> Functor of A,B equals :: ISOCAT_2:def 7
(pr1 (B,C)) * F;
correctness
coherence
(pr1 (B,C)) * F is Functor of A,B;
;
func Pr2 F -> Functor of A,C equals :: ISOCAT_2:def 8
(pr2 (B,C)) * F;
correctness
coherence
(pr2 (B,C)) * F is Functor of A,C;
;
end;
:: deftheorem defines Pr1 ISOCAT_2:def_7_:_
for A, B, C being Category
for F being Functor of A,[:B,C:] holds Pr1 F = (pr1 (B,C)) * F;
:: deftheorem defines Pr2 ISOCAT_2:def_8_:_
for A, B, C being Category
for F being Functor of A,[:B,C:] holds Pr2 F = (pr2 (B,C)) * F;
theorem Th31: :: ISOCAT_2:31
for A, B, C being Category
for F being Functor of A,B
for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
let F be Functor of A,B; ::_thesis: for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
let G be Functor of A,C; ::_thesis: ( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
thus Pr1 <:F,G:> = (pr1 ( the carrier' of B, the carrier' of C)) * <:F,G:>
.= F by FUNCT_3:62 ; ::_thesis: Pr2 <:F,G:> = G
thus Pr2 <:F,G:> = (pr2 ( the carrier' of B, the carrier' of C)) * <:F,G:>
.= G by FUNCT_3:62 ; ::_thesis: verum
end;
theorem Th32: :: ISOCAT_2:32
for A, B, C being Category
for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds
F = G
proof
let A, B, C be Category; ::_thesis: for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds
F = G
let F, G be Functor of A,[:B,C:]; ::_thesis: ( Pr1 F = Pr1 G & Pr2 F = Pr2 G implies F = G )
reconsider f = F, g = G as Function of the carrier' of A,[: the carrier' of B, the carrier' of C:] ;
assume Pr1 F = Pr1 G ; ::_thesis: ( not Pr2 F = Pr2 G or F = G )
then A1: (pr1 ( the carrier' of B, the carrier' of C)) * f = Pr1 G
.= (pr1 ( the carrier' of B, the carrier' of C)) * g ;
assume Pr2 F = Pr2 G ; ::_thesis: F = G
then (pr2 ( the carrier' of B, the carrier' of C)) * f = Pr2 G
.= (pr2 ( the carrier' of B, the carrier' of C)) * g ;
hence F = G by A1, FUNCT_3:80; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, F2 be Functor of A,[:B,C:];
let t be natural_transformation of F1,F2;
func Pr1 t -> natural_transformation of Pr1 F1, Pr1 F2 equals :: ISOCAT_2:def 9
(pr1 (B,C)) * t;
coherence
(pr1 (B,C)) * t is natural_transformation of Pr1 F1, Pr1 F2 ;
func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals :: ISOCAT_2:def 10
(pr2 (B,C)) * t;
coherence
(pr2 (B,C)) * t is natural_transformation of Pr2 F1, Pr2 F2 ;
end;
:: deftheorem defines Pr1 ISOCAT_2:def_9_:_
for A, B, C being Category
for F1, F2 being Functor of A,[:B,C:]
for t being natural_transformation of F1,F2 holds Pr1 t = (pr1 (B,C)) * t;
:: deftheorem defines Pr2 ISOCAT_2:def_10_:_
for A, B, C being Category
for F1, F2 being Functor of A,[:B,C:]
for t being natural_transformation of F1,F2 holds Pr2 t = (pr2 (B,C)) * t;
theorem Th33: :: ISOCAT_2:33
for A, B, C being Category
for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
proof
let A, B, C be Category; ::_thesis: for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
let F1, F2, G1, G2 be Functor of A,[:B,C:]; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; ::_thesis: for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
let s be natural_transformation of F1,F2; ::_thesis: for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
let t be natural_transformation of G1,G2; ::_thesis: ( Pr1 s = Pr1 t & Pr2 s = Pr2 t implies s = t )
assume that
A3: Pr1 s = Pr1 t and
A4: Pr2 s = Pr2 t ; ::_thesis: s = t
reconsider S = s, T = t as Function of the carrier of A,[: the carrier' of B, the carrier' of C:] ;
A5: (pr2 ( the carrier' of B, the carrier' of C)) * S = (pr2 (B,C)) * S
.= Pr2 s by A1, Th30
.= (pr2 (B,C)) * T by A2, A4, Th30
.= (pr2 ( the carrier' of B, the carrier' of C)) * T ;
(pr1 ( the carrier' of B, the carrier' of C)) * S = (pr1 (B,C)) * S
.= Pr1 s by A1, Th30
.= (pr1 (B,C)) * T by A2, A3, Th30
.= (pr1 ( the carrier' of B, the carrier' of C)) * T ;
hence s = t by A5, FUNCT_3:80; ::_thesis: verum
end;
Lm2: for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] )
assume that
A1: F1 is_transformable_to G1 and
A2: F2 is_transformable_to G2 ; ::_thesis: for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let t1 be transformation of F1,G1; ::_thesis: for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let t2 be transformation of F2,G2; ::_thesis: for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let a be Object of A; ::_thesis: <:t1,t2:> . a = [(t1 . a),(t2 . a)]
reconsider s1 = t1 as Function of the carrier of A, the carrier' of B ;
reconsider s2 = t2 as Function of the carrier of A, the carrier' of C ;
thus <:t1,t2:> . a = [(s1 . a),(s2 . a)] by FUNCT_3:59
.= [(t1 . a),(s2 . a)] by A1, NATTRA_1:def_5
.= [(t1 . a),(t2 . a)] by A2, NATTRA_1:def_5 ; ::_thesis: verum
end;
theorem Th34: :: ISOCAT_2:34
for A, B, C being Category
for F being Functor of A,B
for G being Functor of A,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)] by FUNCT_3:59;
theorem Th35: :: ISOCAT_2:35
for A, B, C being Category
for F being Functor of A,B
for G being Functor of A,C
for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G being Functor of A,C
for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let F be Functor of A,B; ::_thesis: for G being Functor of A,C
for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let G be Functor of A,C; ::_thesis: for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let a be Object of A; ::_thesis: <:F,G:> . a = [(F . a),(G . a)]
<:F,G:> . (id a) = [(F . (id a)),(G . (id a))] by FUNCT_3:59
.= [(id (F . a)),(G . (id a))] by CAT_1:71
.= [(id (F . a)),(id (G . a))] by CAT_1:71
.= id [(F . a),(G . a)] by CAT_2:31 ;
hence <:F,G:> . a = [(F . a),(G . a)] by CAT_1:70; ::_thesis: verum
end;
Lm3: for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) )
assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; ::_thesis: for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
let t1 be transformation of F1,G1; ::_thesis: for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
let t2 be transformation of F2,G2; ::_thesis: for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
let a be Object of A; ::_thesis: <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))
A2: ( t1 . a in Hom ((F1 . a),(G1 . a)) & t2 . a in Hom ((F2 . a),(G2 . a)) ) by A1, ISOCAT_1:4;
A3: ( [(F1 . a),(F2 . a)] = <:F1,F2:> . a & [(G1 . a),(G2 . a)] = <:G1,G2:> . a ) by Th35;
[(t1 . a),(t2 . a)] = <:t1,t2:> . a by A1, Lm2;
hence <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) by A2, A3, Th14; ::_thesis: verum
end;
theorem Th36: :: ISOCAT_2:36
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
<:F1,F2:> is_transformable_to <:G1,G2:>
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
<:F1,F2:> is_transformable_to <:G1,G2:>
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
<:F1,F2:> is_transformable_to <:G1,G2:>
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies <:F1,F2:> is_transformable_to <:G1,G2:> )
assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; ::_thesis: <:F1,F2:> is_transformable_to <:G1,G2:>
let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: not Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) = {}
thus not Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) = {} by A1, Lm3; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, G1 be Functor of A,B;
let F2, G2 be Functor of A,C;
assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ;
let t1 be transformation of F1,G1;
let t2 be transformation of F2,G2;
func<:t1,t2:> -> transformation of <:F1,F2:>,<:G1,G2:> equals :Def11: :: ISOCAT_2:def 11
<:t1,t2:>;
coherence
<:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:>
proof
reconsider t = <:t1,t2:> as Function of the carrier of A, the carrier' of [:B,C:] ;
t is transformation of <:F1,F2:>,<:G1,G2:>
proof
thus <:F1,F2:> is_transformable_to <:G1,G2:> by A1, Th36; :: according to NATTRA_1:def_3 ::_thesis: for b1 being Element of the carrier of A holds t . b1 is Morphism of <:F1,F2:> . b1,<:G1,G2:> . b1
let a be Object of A; ::_thesis: t . a is Morphism of <:F1,F2:> . a,<:G1,G2:> . a
t . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) by A1, Lm3;
hence t . a is Morphism of <:F1,F2:> . a,<:G1,G2:> . a by CAT_1:def_5; ::_thesis: verum
end;
hence <:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:> ; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines <: ISOCAT_2:def_11_:_
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;
theorem Th37: :: ISOCAT_2:37
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] )
assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; ::_thesis: for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let t1 be transformation of F1,G1; ::_thesis: for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let t2 be transformation of F2,G2; ::_thesis: for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let a be Object of A; ::_thesis: <:t1,t2:> . a = [(t1 . a),(t2 . a)]
reconsider s1 = t1 as Function of the carrier of A, the carrier' of B ;
reconsider s2 = t2 as Function of the carrier of A, the carrier' of C ;
thus <:t1,t2:> . a = <:t1,t2:> . a by A1, Th36, NATTRA_1:def_5
.= <:s1,s2:> . a by A1, Def11
.= [(t1 . a),(t2 . a)] by A1, Lm2 ; ::_thesis: verum
end;
Lm4: for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) )
assume that
A1: F1 is_naturally_transformable_to G1 and
A2: F2 is_naturally_transformable_to G2 ; ::_thesis: for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
let t1 be natural_transformation of F1,G1; ::_thesis: for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
let t2 be natural_transformation of F2,G2; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) )
assume A3: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
A4: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84;
let f be Morphism of a,b; ::_thesis: (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)
A5: ( (t1 . b) * (F1 /. f) = (G1 /. f) * (t1 . a) & (t2 . b) * (F2 /. f) = (G2 /. f) * (t2 . a) ) by A1, A2, A3, NATTRA_1:def_8;
A6: ( G1 /. f = G1 . f & G2 /. f = G2 . f ) by A3, CAT_3:def_10;
A7: <:G1,G2:> /. f = <:G1,G2:> . f by A3, CAT_3:def_10
.= [(G1 /. f),(G2 /. f)] by A6, A3, Th34 ;
A8: ( F1 /. f = F1 . f & F2 /. f = F2 . f ) by A3, CAT_3:def_10;
A9: <:F1,F2:> /. f = <:F1,F2:> . f by A3, CAT_3:def_10
.= [(F1 /. f),(F2 /. f)] by A3, Th34, A8 ;
A10: F2 is_transformable_to G2 by A2, NATTRA_1:def_7;
then A11: Hom ((F2 . b),(G2 . b)) <> {} by NATTRA_1:def_2;
A12: F1 is_transformable_to G1 by A1, NATTRA_1:def_7;
then A13: <:t1,t2:> . b = [(t1 . b),(t2 . b)] by A10, Th37;
A14: <:t1,t2:> . a = [(t1 . a),(t2 . a)] by A12, A10, Th37;
A15: Hom ((G2 . a),(G2 . b)) <> {} by A3, CAT_1:84;
A16: <:F1,F2:> is_transformable_to <:G1,G2:> by A12, A10, Th36;
then A17: Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) <> {} by NATTRA_1:def_2;
A18: Hom ((<:G1,G2:> . a),(<:G1,G2:> . b)) <> {} by A3, CAT_1:84;
A19: Hom ((G1 . a),(G1 . b)) <> {} by A3, CAT_1:84;
A20: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;
then A21: (t2 . b) * (F2 /. f) = (t2 . b) (*) (F2 /. f) by A11, CAT_1:def_13;
A22: Hom ((F2 . a),(G2 . a)) <> {} by A10, NATTRA_1:def_2;
then A23: (G2 /. f) * (t2 . a) = (G2 /. f) (*) (t2 . a) by A15, CAT_1:def_13;
A24: cod (t2 . a) = G2 . a by A22, CAT_1:5
.= dom (G2 /. f) by A15, CAT_1:5 ;
A25: Hom ((F1 . b),(G1 . b)) <> {} by A12, NATTRA_1:def_2;
then A26: dom (t1 . b) = F1 . b by CAT_1:5
.= cod (F1 /. f) by A4, CAT_1:5 ;
A27: Hom ((F1 . a),(G1 . a)) <> {} by A12, NATTRA_1:def_2;
then A28: (G1 /. f) * (t1 . a) = (G1 /. f) (*) (t1 . a) by A19, CAT_1:def_13;
A29: cod (t1 . a) = G1 . a by A27, CAT_1:5
.= dom (G1 /. f) by A19, CAT_1:5 ;
A30: dom (t2 . b) = F2 . b by A11, CAT_1:5
.= cod (F2 /. f) by A20, CAT_1:5 ;
A31: (t1 . b) * (F1 /. f) = (t1 . b) (*) (F1 /. f) by A25, A4, CAT_1:def_13;
A32: Hom ((<:F1,F2:> . b),(<:G1,G2:> . b)) <> {} by A16, NATTRA_1:def_2;
Hom ((<:F1,F2:> . a),(<:F1,F2:> . b)) <> {} by A3, CAT_1:84;
hence (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:t1,t2:> . b) (*) (<:F1,F2:> /. f) by A32, CAT_1:def_13
.= [((G1 /. f) * (t1 . a)),((G2 /. f) * (t2 . a))] by A5, A13, A9, A26, A30, A31, A21, CAT_2:29
.= (<:G1,G2:> /. f) (*) (<:t1,t2:> . a) by A28, A23, A29, A24, A7, A14, CAT_2:29
.= (<:G1,G2:> /. f) * (<:t1,t2:> . a) by A17, A18, CAT_1:def_13 ;
::_thesis: verum
end;
theorem Th38: :: ISOCAT_2:38
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
<:F1,F2:> is_naturally_transformable_to <:G1,G2:>
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
<:F1,F2:> is_naturally_transformable_to <:G1,G2:>
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
<:F1,F2:> is_naturally_transformable_to <:G1,G2:>
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies <:F1,F2:> is_naturally_transformable_to <:G1,G2:> )
assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; ::_thesis: <:F1,F2:> is_naturally_transformable_to <:G1,G2:>
( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) by A1, NATTRA_1:def_7;
hence <:F1,F2:> is_transformable_to <:G1,G2:> by Th36; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of <:F1,F2:>,<:G1,G2:> st
for b2, b3 being Element of the carrier of A holds
( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * (<:F1,F2:> /. b4) = (<:G1,G2:> /. b4) * (b1 . b2) )
set t1 = the natural_transformation of F1,G1;
set t2 = the natural_transformation of F2,G2;
take <: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> ; ::_thesis: for b1, b2 being Element of the carrier of A holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b2) * (<:F1,F2:> /. b3) = (<:G1,G2:> /. b3) * (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b1) )
thus for b1, b2 being Element of the carrier of A holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b2) * (<:F1,F2:> /. b3) = (<:G1,G2:> /. b3) * (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b1) ) by A1, Lm4; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, G1 be Functor of A,B;
let F2, G2 be Functor of A,C;
assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ;
let t1 be natural_transformation of F1,G1;
let t2 be natural_transformation of F2,G2;
func<:t1,t2:> -> natural_transformation of <:F1,F2:>,<:G1,G2:> equals :Def12: :: ISOCAT_2:def 12
<:t1,t2:>;
coherence
<:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:>
proof
( <:F1,F2:> is_naturally_transformable_to <:G1,G2:> & ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) ) ) by A1, Lm4, Th38;
hence <:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:> by NATTRA_1:def_8; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines <: ISOCAT_2:def_12_:_
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;
theorem Th39: :: ISOCAT_2:39
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
proof
let A, B, C be Category; ::_thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
let F1, G1 be Functor of A,B; ::_thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
let F2, G2 be Functor of A,C; ::_thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) )
assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; ::_thesis: for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
A2: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) by A1, NATTRA_1:def_7;
let t1 be natural_transformation of F1,G1; ::_thesis: for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
let t2 be natural_transformation of F2,G2; ::_thesis: ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
reconsider s = t1 as Function of the carrier of A, the carrier' of B ;
<:F1,F2:> is_naturally_transformable_to <:G1,G2:> by A1, Th38;
then A3: <:F1,F2:> is_transformable_to <:G1,G2:> by NATTRA_1:def_7;
thus Pr1 <:t1,t2:> = (pr1 (B,C)) * <:t1,t2:> by A1, Th38, ISOCAT_1:def_7
.= (pr1 (B,C)) * <:t1,t2:> by A3, ISOCAT_1:def_5
.= (pr1 (B,C)) * <:t1,t2:> by A1, Def12
.= (pr1 (B,C)) * <:s,t2:> by A2, Def11
.= (pr1 ( the carrier' of B, the carrier' of C)) * <:s,t2:>
.= t1 by FUNCT_3:62 ; ::_thesis: Pr2 <:t1,t2:> = t2
thus Pr2 <:t1,t2:> = (pr2 (B,C)) * <:t1,t2:> by A1, Th38, ISOCAT_1:def_7
.= (pr2 (B,C)) * <:t1,t2:> by A3, ISOCAT_1:def_5
.= (pr2 (B,C)) * <:t1,t2:> by A1, Def12
.= (pr2 (B,C)) * <:s,t2:> by A2, Def11
.= (pr2 ( the carrier' of B, the carrier' of C)) * <:s,t2:>
.= t2 by FUNCT_3:62 ; ::_thesis: verum
end;
definition
let A, B, C be Category;
func distribute (A,B,C) -> Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] means :Def13: :: ISOCAT_2:def 13
for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds it . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]];
existence
ex b1 being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] st
for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
proof
defpred S1[ set , set ] means for F1, F2 being Functor of A,[:B,C:]
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]];
A1: now__::_thesis:_for_f_being_Morphism_of_(Functors_(A,[:B,C:]))_ex_g_being_Element_of_the_carrier'_of_[:(Functors_(A,B)),(Functors_(A,C)):]_st_S1[f,g]
let f be Morphism of (Functors (A,[:B,C:])); ::_thesis: ex g being Element of the carrier' of [:(Functors (A,B)),(Functors (A,C)):] st S1[f,g]
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A2: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A3: f = [[F1,F2],s] by Th8;
( the carrier' of (Functors (A,C)) = NatTrans (A,C) & Pr2 F1 is_naturally_transformable_to Pr2 F2 ) by A2, ISOCAT_1:22, NATTRA_1:def_17;
then reconsider PPr2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by NATTRA_1:32;
( the carrier' of (Functors (A,B)) = NatTrans (A,B) & Pr1 F1 is_naturally_transformable_to Pr1 F2 ) by A2, ISOCAT_1:22, NATTRA_1:def_17;
then reconsider PPr1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by NATTRA_1:32;
take g = [PPr1,PPr2]; ::_thesis: S1[f,g]
thus S1[f,g] ::_thesis: verum
proof
let G1, G2 be Functor of A,[:B,C:]; ::_thesis: for t being natural_transformation of G1,G2 st f = [[G1,G2],t] holds
g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
let t be natural_transformation of G1,G2; ::_thesis: ( f = [[G1,G2],t] implies g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] )
assume A4: f = [[G1,G2],t] ; ::_thesis: g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
then [G1,G2] = [F1,F2] by A3, XTUPLE_0:1;
then A5: ( G1 = F1 & G2 = F2 ) by XTUPLE_0:1;
t = s by A3, A4, XTUPLE_0:1;
hence g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] by A5; ::_thesis: verum
end;
end;
consider IT being Function of the carrier' of (Functors (A,[:B,C:])), the carrier' of [:(Functors (A,B)),(Functors (A,C)):] such that
A6: for f being Morphism of (Functors (A,[:B,C:])) holds S1[f,IT . f] from FUNCT_2:sch_3(A1);
IT is Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):]
proof
thus for c being Object of (Functors (A,[:B,C:])) ex d being Object of [:(Functors (A,B)),(Functors (A,C)):] st IT . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for b1 being Element of the carrier' of (Functors (A,[:B,C:])) holds
( IT . (id (dom b1)) = id (dom (IT . b1)) & IT . (id (cod b1)) = id (cod (IT . b1)) ) ) & ( for b1, b2 being Element of the carrier' of (Functors (A,[:B,C:])) holds
( not dom b2 = cod b1 or IT . (b2 (*) b1) = (IT . b2) (*) (IT . b1) ) ) )
proof
let c be Object of (Functors (A,[:B,C:])); ::_thesis: ex d being Object of [:(Functors (A,B)),(Functors (A,C)):] st IT . (id c) = id d
reconsider F = c as Functor of A,[:B,C:] by Th7;
reconsider d2 = Pr2 F as Object of (Functors (A,C)) by Th7;
reconsider d1 = Pr1 F as Object of (Functors (A,B)) by Th7;
take [d1,d2] ; ::_thesis: IT . (id c) = id [d1,d2]
Pr1 (id F) = id (Pr1 F) by ISOCAT_1:33;
then A7: id d1 = [[(Pr1 F),(Pr1 F)],(Pr1 (id F))] by NATTRA_1:def_17;
Pr2 (id F) = id (Pr2 F) by ISOCAT_1:33;
then A8: id d2 = [[(Pr2 F),(Pr2 F)],(Pr2 (id F))] by NATTRA_1:def_17;
id c = [[F,F],(id F)] by NATTRA_1:def_17;
hence IT . (id c) = [(id d1),(id d2)] by A6, A7, A8
.= id [d1,d2] by CAT_2:31 ;
::_thesis: verum
end;
A9: the carrier' of (Functors (A,C)) = NatTrans (A,C) by NATTRA_1:def_17;
A10: the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def_17;
thus for f being Morphism of (Functors (A,[:B,C:])) holds
( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) ) ::_thesis: for b1, b2 being Element of the carrier' of (Functors (A,[:B,C:])) holds
( not dom b2 = cod b1 or IT . (b2 (*) b1) = (IT . b2) (*) (IT . b1) )
proof
let f be Morphism of (Functors (A,[:B,C:])); ::_thesis: ( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) )
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A11: F1 is_naturally_transformable_to F2 and
A12: dom f = F1 and
A13: cod f = F2 and
A14: f = [[F1,F2],s] by Th8;
Pr1 F1 is_naturally_transformable_to Pr1 F2 by A11, ISOCAT_1:22;
then reconsider f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A10, NATTRA_1:32;
( dom f1 = Pr1 F1 & Pr1 (id F1) = id (Pr1 F1) ) by ISOCAT_1:33, NATTRA_1:33;
then A15: id (dom f1) = [[(Pr1 F1),(Pr1 F1)],(Pr1 (id F1))] by NATTRA_1:def_17;
Pr2 F1 is_naturally_transformable_to Pr2 F2 by A11, ISOCAT_1:22;
then reconsider f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A9, NATTRA_1:32;
( dom f2 = Pr2 F1 & Pr2 (id F1) = id (Pr2 F1) ) by ISOCAT_1:33, NATTRA_1:33;
then A16: id (dom f2) = [[(Pr2 F1),(Pr2 F1)],(Pr2 (id F1))] by NATTRA_1:def_17;
id (dom f) = [[F1,F1],(id F1)] by A12, NATTRA_1:def_17;
hence IT . (id (dom f)) = [(id (dom f1)),(id (dom f2))] by A6, A15, A16
.= id [(dom f1),(dom f2)] by CAT_2:31
.= id (dom [f1,f2]) by CAT_2:28
.= id (dom (IT . f)) by A6, A14 ;
::_thesis: IT . (id (cod f)) = id (cod (IT . f))
( cod f1 = Pr1 F2 & Pr1 (id F2) = id (Pr1 F2) ) by ISOCAT_1:33, NATTRA_1:33;
then A17: id (cod f1) = [[(Pr1 F2),(Pr1 F2)],(Pr1 (id F2))] by NATTRA_1:def_17;
( cod f2 = Pr2 F2 & Pr2 (id F2) = id (Pr2 F2) ) by ISOCAT_1:33, NATTRA_1:33;
then A18: id (cod f2) = [[(Pr2 F2),(Pr2 F2)],(Pr2 (id F2))] by NATTRA_1:def_17;
id (cod f) = [[F2,F2],(id F2)] by A13, NATTRA_1:def_17;
hence IT . (id (cod f)) = [(id (cod f1)),(id (cod f2))] by A6, A17, A18
.= id [(cod f1),(cod f2)] by CAT_2:31
.= id (cod [f1,f2]) by CAT_2:28
.= id (cod (IT . f)) by A6, A14 ;
::_thesis: verum
end;
let f, g be Morphism of (Functors (A,[:B,C:])); ::_thesis: ( not dom g = cod f or IT . (g (*) f) = (IT . g) (*) (IT . f) )
assume A19: dom g = cod f ; ::_thesis: IT . (g (*) f) = (IT . g) (*) (IT . f)
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A20: F1 is_naturally_transformable_to F2 and
dom f = F1 and
A21: cod f = F2 and
A22: f = [[F1,F2],s] by Th8;
consider G1, G2 being Functor of A,[:B,C:], t being natural_transformation of G1,G2 such that
A23: G1 is_naturally_transformable_to G2 and
A24: dom g = G1 and
cod g = G2 and
A25: g = [[G1,G2],t] by Th8;
reconsider t = t as natural_transformation of F2,G2 by A19, A21, A24;
A26: g (*) f = [[F1,G2],(t `*` s)] by A19, A21, A22, A24, A25, NATTRA_1:36;
A27: Pr2 F1 is_naturally_transformable_to Pr2 F2 by A20, ISOCAT_1:22;
Pr2 F2 is_naturally_transformable_to Pr2 G2 by A19, A21, A23, A24, ISOCAT_1:22;
then reconsider g2 = [[(Pr2 F2),(Pr2 G2)],(Pr2 t)], f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A9, A27, NATTRA_1:32;
A28: g2 (*) f2 = [[(Pr2 F1),(Pr2 G2)],((Pr2 t) `*` (Pr2 s))] by NATTRA_1:36
.= [[(Pr2 F1),(Pr2 G2)],(Pr2 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1:27 ;
A29: dom g2 = Pr2 F2 by NATTRA_1:33
.= cod f2 by NATTRA_1:33 ;
A30: Pr1 F1 is_naturally_transformable_to Pr1 F2 by A20, ISOCAT_1:22;
Pr1 F2 is_naturally_transformable_to Pr1 G2 by A19, A21, A23, A24, ISOCAT_1:22;
then reconsider g1 = [[(Pr1 F2),(Pr1 G2)],(Pr1 t)], f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A10, A30, NATTRA_1:32;
A31: dom g1 = Pr1 F2 by NATTRA_1:33
.= cod f1 by NATTRA_1:33 ;
A32: IT . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A6, A22;
g1 (*) f1 = [[(Pr1 F1),(Pr1 G2)],((Pr1 t) `*` (Pr1 s))] by NATTRA_1:36
.= [[(Pr1 F1),(Pr1 G2)],(Pr1 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1:27 ;
hence IT . (g (*) f) = [(g1 (*) f1),(g2 (*) f2)] by A6, A28, A26
.= [g1,g2] (*) [f1,f2] by A31, A29, CAT_2:29
.= (IT . g) (*) (IT . f) by A6, A19, A21, A24, A25, A32 ;
::_thesis: verum
end;
then reconsider IT = IT as Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] ;
take IT ; ::_thesis: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
let F1, F2 be Functor of A,[:B,C:]; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] )
assume A33: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
let t be natural_transformation of F1,F2; ::_thesis: IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
set f = [[F1,F2],t];
[[F1,F2],t] in NatTrans (A,[:B,C:]) by A33, NATTRA_1:32;
then reconsider f = [[F1,F2],t] as Morphism of (Functors (A,[:B,C:])) by NATTRA_1:def_17;
thus IT . [[F1,F2],t] = IT . f
.= [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] by A6 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] st ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) & ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) holds
b1 = b2
proof
let IT1, IT2 be Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):]; ::_thesis: ( ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) & ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) implies IT1 = IT2 )
assume that
A34: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] and
A35: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ; ::_thesis: IT1 = IT2
now__::_thesis:_for_f_being_Morphism_of_(Functors_(A,[:B,C:]))_holds_IT1_._f_=_IT2_._f
let f be Morphism of (Functors (A,[:B,C:])); ::_thesis: IT1 . f = IT2 . f
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A36: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A37: f = [[F1,F2],s] by Th8;
thus IT1 . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A34, A36, A37
.= IT2 . f by A35, A36, A37 ; ::_thesis: verum
end;
hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines distribute ISOCAT_2:def_13_:_
for A, B, C being Category
for b4 being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] holds
( b4 = distribute (A,B,C) iff for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b4 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] );
registration
let A, B, C be Category;
cluster distribute (A,B,C) -> isomorphic ;
coherence
distribute (A,B,C) is isomorphic
proof
thus distribute (A,B,C) is one-to-one :: according to ISOCAT_1:def_3 ::_thesis: rng (distribute (A,B,C)) = the carrier' of [:(Functors (A,B)),(Functors (A,C)):]
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (distribute (A,B,C)) or not x2 in dom (distribute (A,B,C)) or not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 )
assume x1 in dom (distribute (A,B,C)) ; ::_thesis: ( not x2 in dom (distribute (A,B,C)) or not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 )
then reconsider f1 = x1 as Morphism of (Functors (A,[:B,C:])) ;
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A1: F1 is_naturally_transformable_to F2 and
dom f1 = F1 and
cod f1 = F2 and
A2: f1 = [[F1,F2],s] by Th8;
assume x2 in dom (distribute (A,B,C)) ; ::_thesis: ( not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 )
then reconsider f2 = x2 as Morphism of (Functors (A,[:B,C:])) ;
consider G1, G2 being Functor of A,[:B,C:], t being natural_transformation of G1,G2 such that
A3: G1 is_naturally_transformable_to G2 and
dom f2 = G1 and
cod f2 = G2 and
A4: f2 = [[G1,G2],t] by Th8;
assume (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 ; ::_thesis: x1 = x2
then A5: [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] = (distribute (A,B,C)) . [[G1,G2],t] by A1, A2, A4, Def13
.= [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] by A3, Def13 ;
then A6: [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] = [[(Pr1 G1),(Pr1 G2)],(Pr1 t)] by XTUPLE_0:1;
A7: [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] = [[(Pr2 G1),(Pr2 G2)],(Pr2 t)] by A5, XTUPLE_0:1;
then A8: Pr2 s = Pr2 t by XTUPLE_0:1;
A9: [(Pr2 F1),(Pr2 F2)] = [(Pr2 G1),(Pr2 G2)] by A7, XTUPLE_0:1;
then A10: Pr2 F1 = Pr2 G1 by XTUPLE_0:1;
A11: [(Pr1 F1),(Pr1 F2)] = [(Pr1 G1),(Pr1 G2)] by A6, XTUPLE_0:1;
then Pr1 F1 = Pr1 G1 by XTUPLE_0:1;
then A12: F1 = G1 by A10, Th32;
Pr1 s = Pr1 t by A6, XTUPLE_0:1;
then A13: s = t by A1, A3, A8, Th33;
A14: Pr2 F2 = Pr2 G2 by A9, XTUPLE_0:1;
Pr1 F2 = Pr1 G2 by A11, XTUPLE_0:1;
hence x1 = x2 by A2, A4, A14, A13, A12, Th32; ::_thesis: verum
end;
thus rng (distribute (A,B,C)) c= the carrier' of [:(Functors (A,B)),(Functors (A,C)):] ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of [:(Functors (A,B)),(Functors (A,C)):] c= rng (distribute (A,B,C))
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in the carrier' of [:(Functors (A,B)),(Functors (A,C)):] or o in rng (distribute (A,B,C)) )
assume o in the carrier' of [:(Functors (A,B)),(Functors (A,C)):] ; ::_thesis: o in rng (distribute (A,B,C))
then consider o1 being Morphism of (Functors (A,B)), o2 being Morphism of (Functors (A,C)) such that
A15: o = [o1,o2] by CAT_2:27;
consider G1, G2 being Functor of A,C, t being natural_transformation of G1,G2 such that
A16: G1 is_naturally_transformable_to G2 and
dom o2 = G1 and
cod o2 = G2 and
A17: o2 = [[G1,G2],t] by Th8;
consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that
A18: F1 is_naturally_transformable_to F2 and
dom o1 = F1 and
cod o1 = F2 and
A19: o1 = [[F1,F2],s] by Th8;
set f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>];
A20: <:F1,G1:> is_naturally_transformable_to <:F2,G2:> by A18, A16, Th38;
then [[<:F1,G1:>,<:F2,G2:>],<:s,t:>] in NatTrans (A,[:B,C:]) by NATTRA_1:32;
then reconsider f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>] as Morphism of (Functors (A,[:B,C:])) by NATTRA_1:def_17;
A21: ( Pr1 <:F1,G1:> = F1 & Pr1 <:F2,G2:> = F2 ) by Th31;
A22: ( Pr2 <:F1,G1:> = G1 & Pr2 <:F2,G2:> = G2 ) by Th31;
( Pr1 <:s,t:> = s & Pr2 <:s,t:> = t ) by A18, A16, Th39;
then (distribute (A,B,C)) . f = o by A15, A19, A17, A20, A21, A22, Def13;
hence o in rng (distribute (A,B,C)) by FUNCT_2:112; ::_thesis: verum
end;
end;
theorem :: ISOCAT_2:40
for A, B, C being Category holds Functors (A,[:B,C:]) ~= [:(Functors (A,B)),(Functors (A,C)):]
proof
let A, B, C be Category; ::_thesis: Functors (A,[:B,C:]) ~= [:(Functors (A,B)),(Functors (A,C)):]
take distribute (A,B,C) ; :: according to ISOCAT_1:def_4 ::_thesis: distribute (A,B,C) is isomorphic
thus distribute (A,B,C) is isomorphic ; ::_thesis: verum
end;