:: NATTRA_1 semantic presentation
begin
definition
let A1 be set ;
let B1 be non empty set ;
let f be Function of A1,B1;
let Y1 be Subset of A1;
:: original: |
redefine funcf | Y1 -> Function of Y1,B1;
coherence
f | Y1 is Function of Y1,B1 by FUNCT_2:32;
end;
theorem Th1: :: NATTRA_1:1
for B1, B2, A1, A2 being non empty set
for f being Function of A1,B1
for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
proof
let B1, B2, A1, A2 be non empty set ; ::_thesis: for f being Function of A1,B1
for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let f be Function of A1,B1; ::_thesis: for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let g be Function of A2,B2; ::_thesis: for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let Y1 be non empty Subset of A1; ::_thesis: for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let Y2 be non empty Subset of A2; ::_thesis: [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
now__::_thesis:_for_a_being_Element_of_[:Y1,Y2:]_holds_[:(f_|_Y1),(g_|_Y2):]_._a_=_([:f,g:]_|_[:Y1,Y2:])_._a
let a be Element of [:Y1,Y2:]; ::_thesis: [:(f | Y1),(g | Y2):] . a = ([:f,g:] | [:Y1,Y2:]) . a
consider a1 being Element of Y1, a2 being Element of Y2 such that
A1: a = [a1,a2] by DOMAIN_1:1;
A2: (g | Y2) . a2 = g . a2 by FUNCT_1:49;
A3: (f | Y1) . a1 = f . a1 by FUNCT_1:49;
thus [:(f | Y1),(g | Y2):] . a = [:(f | Y1),(g | Y2):] . (a1,a2) by A1
.= [(f . a1),(g . a2)] by A3, A2, FUNCT_3:75
.= [:f,g:] . (a1,a2) by FUNCT_3:75
.= ([:f,g:] | [:Y1,Y2:]) . a by A1, FUNCT_1:49 ; ::_thesis: verum
end;
hence [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] by FUNCT_2:63; ::_thesis: verum
end;
definition
let A, B be non empty set ;
let A1 be non empty Subset of A;
let B1 be non empty Subset of B;
let f be PartFunc of [:A1,A1:],A1;
let g be PartFunc of [:B1,B1:],B1;
:: original: |:
redefine func|:f,g:| -> PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:];
coherence
|:f,g:| is PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:] by FUNCT_4:59;
end;
theorem Th2: :: NATTRA_1:2
for A1, A2 being non empty set
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
proof
let A1, A2 be non empty set ; ::_thesis: for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let Y1 be non empty Subset of A1; ::_thesis: for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let Y2 be non empty Subset of A2; ::_thesis: for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let f be PartFunc of [:A1,A1:],A1; ::_thesis: for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let g be PartFunc of [:A2,A2:],A2; ::_thesis: for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
let F be PartFunc of [:Y1,Y1:],Y1; ::_thesis: ( F = f || Y1 implies for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:] )
assume A1: F = f || Y1 ; ::_thesis: for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
A2: dom F c= dom f by A1, RELAT_1:60;
let G be PartFunc of [:Y2,Y2:],Y2; ::_thesis: ( G = g || Y2 implies |:F,G:| = |:f,g:| || [:Y1,Y2:] )
assume A3: G = g || Y2 ; ::_thesis: |:F,G:| = |:f,g:| || [:Y1,Y2:]
set X = dom |:F,G:|;
A4: dom G c= dom g by A3, RELAT_1:60;
A5: dom |:F,G:| = dom (|:f,g:| || [:Y1,Y2:])
proof
thus dom |:F,G:| c= dom (|:f,g:| || [:Y1,Y2:]) :: according to XBOOLE_0:def_10 ::_thesis: dom (|:f,g:| || [:Y1,Y2:]) c= dom |:F,G:|
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom |:F,G:| or x in dom (|:f,g:| || [:Y1,Y2:]) )
assume x in dom |:F,G:| ; ::_thesis: x in dom (|:f,g:| || [:Y1,Y2:])
then consider x11, x21, x12, x22 being set such that
A6: x = [[x11,x12],[x21,x22]] and
A7: [x11,x21] in dom F and
A8: [x12,x22] in dom G by FUNCT_4:def_3;
A9: dom G c= [:Y2,Y2:] by A3, RELAT_1:58;
then A10: x12 in Y2 by A8, ZFMISC_1:87;
A11: x22 in Y2 by A8, A9, ZFMISC_1:87;
A12: dom F c= [:Y1,Y1:] by A1, RELAT_1:58;
then x21 in Y1 by A7, ZFMISC_1:87;
then A13: [x21,x22] in [:Y1,Y2:] by A11, ZFMISC_1:87;
x11 in Y1 by A7, A12, ZFMISC_1:87;
then [x11,x12] in [:Y1,Y2:] by A10, ZFMISC_1:87;
then A14: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A6, A13, ZFMISC_1:87;
x in dom |:f,g:| by A2, A4, A6, A7, A8, FUNCT_4:def_3;
then x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by A14, XBOOLE_0:def_4;
hence x in dom (|:f,g:| || [:Y1,Y2:]) by RELAT_1:61; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (|:f,g:| || [:Y1,Y2:]) or x in dom |:F,G:| )
A15: dom F = (dom f) /\ [:Y1,Y1:] by A1, RELAT_1:61;
assume x in dom (|:f,g:| || [:Y1,Y2:]) ; ::_thesis: x in dom |:F,G:|
then A16: x in (dom |:f,g:|) /\ [:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:61;
then A17: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by XBOOLE_0:def_4;
A18: dom G = (dom g) /\ [:Y2,Y2:] by A3, RELAT_1:61;
x in dom |:f,g:| by A16, XBOOLE_0:def_4;
then consider x11, x21, x12, x22 being set such that
A19: x = [[x11,x12],[x21,x22]] and
A20: [x11,x21] in dom f and
A21: [x12,x22] in dom g by FUNCT_4:def_3;
A22: [x21,x22] in [:Y1,Y2:] by A19, A17, ZFMISC_1:87;
then A23: x22 in Y2 by ZFMISC_1:87;
A24: [x11,x12] in [:Y1,Y2:] by A19, A17, ZFMISC_1:87;
then x12 in Y2 by ZFMISC_1:87;
then [x12,x22] in [:Y2,Y2:] by A23, ZFMISC_1:87;
then A25: [x12,x22] in dom G by A21, A18, XBOOLE_0:def_4;
A26: x21 in Y1 by A22, ZFMISC_1:87;
x11 in Y1 by A24, ZFMISC_1:87;
then [x11,x21] in [:Y1,Y1:] by A26, ZFMISC_1:87;
then [x11,x21] in dom F by A20, A15, XBOOLE_0:def_4;
hence x in dom |:F,G:| by A19, A25, FUNCT_4:def_3; ::_thesis: verum
end;
A27: now__::_thesis:_for_x_being_set_st_x_in_dom_|:F,G:|_holds_
|:F,G:|_._x_=_(|:f,g:|_||_[:Y1,Y2:])_._x
let x be set ; ::_thesis: ( x in dom |:F,G:| implies |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x )
assume A28: x in dom |:F,G:| ; ::_thesis: |:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x
then consider x11, x21, x12, x22 being set such that
A29: x = [[x11,x12],[x21,x22]] and
A30: [x11,x21] in dom F and
A31: [x12,x22] in dom G by FUNCT_4:def_3;
thus |:F,G:| . x = |:F,G:| . ([x11,x12],[x21,x22]) by A29
.= [(F . (x11,x21)),(G . (x12,x22))] by A30, A31, FUNCT_4:def_3
.= [(f . [x11,x21]),(G . [x12,x22])] by A1, A30, FUNCT_1:47
.= [(f . (x11,x21)),(g . (x12,x22))] by A3, A31, FUNCT_1:47
.= |:f,g:| . ([x11,x12],[x21,x22]) by A2, A4, A30, A31, FUNCT_4:def_3
.= (|:f,g:| || [:Y1,Y2:]) . x by A5, A28, A29, FUNCT_1:47 ; ::_thesis: verum
end;
then A32: for x being Element of [:[:Y1,Y2:],[:Y1,Y2:]:] st x in dom |:F,G:| holds
|:F,G:| . x = (|:f,g:| || [:Y1,Y2:]) . x ;
A33: rng (|:f,g:| || [:Y1,Y2:]) c= rng |:F,G:|
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (|:f,g:| || [:Y1,Y2:]) or x in rng |:F,G:| )
assume x in rng (|:f,g:| || [:Y1,Y2:]) ; ::_thesis: x in rng |:F,G:|
then consider y being set such that
A34: y in dom (|:f,g:| || [:Y1,Y2:]) and
A35: x = (|:f,g:| || [:Y1,Y2:]) . y by FUNCT_1:def_3;
x = |:F,G:| . y by A5, A27, A34, A35;
hence x in rng |:F,G:| by A5, A34, FUNCT_1:def_3; ::_thesis: verum
end;
rng |:F,G:| c= [:Y1,Y2:] by RELAT_1:def_19;
then rng (|:f,g:| || [:Y1,Y2:]) c= [:Y1,Y2:] by A33, XBOOLE_1:1;
then |:f,g:| || [:Y1,Y2:] is PartFunc of [:[:Y1,Y2:],[:Y1,Y2:]:],[:Y1,Y2:] by RELAT_1:def_18, A5, RELSET_1:4;
hence |:F,G:| = |:f,g:| || [:Y1,Y2:] by A5, A32, PARTFUN1:5; ::_thesis: verum
end;
theorem :: NATTRA_1:3
canceled;
theorem Th4: :: NATTRA_1:4
for o, m being set
for f, g being Morphism of (1Cat (o,m)) holds f = g
proof
let o, m be set ; ::_thesis: for f, g being Morphism of (1Cat (o,m)) holds f = g
let f, g be Morphism of (1Cat (o,m)); ::_thesis: f = g
f = m by TARSKI:def_1;
hence f = g by TARSKI:def_1; ::_thesis: verum
end;
theorem Th5: :: NATTRA_1:5
for A being Category
for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A
proof
let A be Category; ::_thesis: for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A
let a be Object of A; ::_thesis: [[(id a),(id a)],(id a)] in the Comp of A
A1: dom (id a) = a ;
A2: cod (id a) = a ;
then A3: [(id a),(id a)] in dom the Comp of A by A1, CAT_1:15;
(id a) (*) (id a) = id a by A1, CAT_1:22;
then the Comp of A . ((id a),(id a)) = id a by A1, A2, CAT_1:16;
hence [[(id a),(id a)],(id a)] in the Comp of A by A3, FUNCT_1:def_2; ::_thesis: verum
end;
theorem Th6: :: NATTRA_1:6
for o, m being set holds the Comp of (1Cat (o,m)) = {[[m,m],m]}
proof
let o, m be set ; ::_thesis: the Comp of (1Cat (o,m)) = {[[m,m],m]}
set A = 1Cat (o,m);
reconsider f = m as Morphism of (1Cat (o,m)) by TARSKI:def_1;
set a = the Object of (1Cat (o,m));
thus the Comp of (1Cat (o,m)) c= {[[m,m],m]} :: according to XBOOLE_0:def_10 ::_thesis: {[[m,m],m]} c= the Comp of (1Cat (o,m))
proof
set o9 = the Object of (1Cat (o,m));
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Comp of (1Cat (o,m)) or x in {[[m,m],m]} )
A1: dom (id the Object of (1Cat (o,m))) = the Object of (1Cat (o,m)) ;
A2: cod (id the Object of (1Cat (o,m))) = the Object of (1Cat (o,m)) ;
assume A3: x in the Comp of (1Cat (o,m)) ; ::_thesis: x in {[[m,m],m]}
then consider x1, x2 being set such that
A4: x = [x1,x2] by RELAT_1:def_1;
A5: x1 in dom the Comp of (1Cat (o,m)) by A3, A4, XTUPLE_0:def_12;
dom the Comp of (1Cat (o,m)) c= [: the carrier' of (1Cat (o,m)), the carrier' of (1Cat (o,m)):] by RELAT_1:def_18;
then consider x11, x12 being set such that
A6: x11 in the carrier' of (1Cat (o,m)) and
A7: x12 in the carrier' of (1Cat (o,m)) and
A8: x1 = [x11,x12] by A5, ZFMISC_1:def_2;
A9: x12 = id the Object of (1Cat (o,m)) by A7, Th4;
x11 = id the Object of (1Cat (o,m)) by A6, Th4;
then x2 = the Comp of (1Cat (o,m)) . ((id the Object of (1Cat (o,m))),(id the Object of (1Cat (o,m)))) by A3, A4, A5, A8, A9, FUNCT_1:def_2;
then x2 = (id the Object of (1Cat (o,m))) (*) (id the Object of (1Cat (o,m))) by A1, A2, CAT_1:16;
then A10: x2 = m by TARSKI:def_1;
A11: x12 = m by A7, TARSKI:def_1;
x11 = m by A6, TARSKI:def_1;
hence x in {[[m,m],m]} by A4, A8, A11, A10, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[[m,m],m]} or x in the Comp of (1Cat (o,m)) )
assume x in {[[m,m],m]} ; ::_thesis: x in the Comp of (1Cat (o,m))
then A12: x = [[m,m],m] by TARSKI:def_1;
f = id the Object of (1Cat (o,m)) by TARSKI:def_1;
hence x in the Comp of (1Cat (o,m)) by A12, Th5; ::_thesis: verum
end;
theorem Th7: :: NATTRA_1:7
for A being Category
for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A
proof
let A be Category; ::_thesis: for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A
let d be Object of A; ::_thesis: 1Cat (d,(id d)) is Subcategory of A
thus the carrier of (1Cat (d,(id d))) c= the carrier of A :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of (1Cat (d,(id d)))
for b3, b4 being Element of the carrier of A holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of (1Cat (d,(id d))) c= the Comp of A & ( for b1 being Element of the carrier of (1Cat (d,(id d)))
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in the carrier of (1Cat (d,(id d))) or b in the carrier of A )
assume b in the carrier of (1Cat (d,(id d))) ; ::_thesis: b in the carrier of A
then b = d by TARSKI:def_1;
hence b in the carrier of A ; ::_thesis: verum
end;
thus for a, b being Object of (1Cat (d,(id d)))
for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ::_thesis: ( the Comp of (1Cat (d,(id d))) c= the Comp of A & ( for b1 being Element of the carrier of (1Cat (d,(id d)))
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
proof
let a, b be Object of (1Cat (d,(id d))); ::_thesis: for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of A; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that
A1: a = a9 and
A2: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9)
A3: b9 = d by A2, TARSKI:def_1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9)
then A4: x = id d by TARSKI:def_1;
a9 = d by A1, TARSKI:def_1;
hence x in Hom (a9,b9) by A3, A4, CAT_1:27; ::_thesis: verum
end;
thus the Comp of (1Cat (d,(id d))) c= the Comp of A ::_thesis: for b1 being Element of the carrier of (1Cat (d,(id d)))
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Comp of (1Cat (d,(id d))) or x in the Comp of A )
assume x in the Comp of (1Cat (d,(id d))) ; ::_thesis: x in the Comp of A
then x in {[[(id d),(id d)],(id d)]} by Th6;
then x = [[(id d),(id d)],(id d)] by TARSKI:def_1;
hence x in the Comp of A by Th5; ::_thesis: verum
end;
let a be Object of (1Cat (d,(id d))); ::_thesis: for b1 being Element of the carrier of A holds
( not a = b1 or id a = id b1 )
let a9 be Object of A; ::_thesis: ( not a = a9 or id a = id a9 )
assume a = a9 ; ::_thesis: id a = id a9
then a9 = d by TARSKI:def_1;
hence id a = id a9 by TARSKI:def_1; ::_thesis: verum
end;
theorem Th8: :: NATTRA_1:8
for A being Category
for C being Subcategory of A holds
( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )
proof
let A be Category; ::_thesis: for C being Subcategory of A holds
( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )
let C be Subcategory of A; ::_thesis: ( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )
A1: dom the Source of A = the carrier' of A by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Source_of_C_holds_
the_Source_of_C_._x_=_the_Source_of_A_._x
let x be set ; ::_thesis: ( x in dom the Source of C implies the Source of C . x = the Source of A . x )
assume x in dom the Source of C ; ::_thesis: the Source of C . x = the Source of A . x
then reconsider m = x as Morphism of C by FUNCT_2:def_1;
reconsider m9 = m as Morphism of A by CAT_2:8;
thus the Source of C . x = dom m
.= dom m9 by CAT_2:9
.= the Source of A . x ; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Target_of_C_holds_
the_Target_of_C_._x_=_the_Target_of_A_._x
let x be set ; ::_thesis: ( x in dom the Target of C implies the Target of C . x = the Target of A . x )
assume x in dom the Target of C ; ::_thesis: the Target of C . x = the Target of A . x
then reconsider m = x as Morphism of C by FUNCT_2:def_1;
reconsider m9 = m as Morphism of A by CAT_2:8;
thus the Target of C . x = cod m
.= cod m9 by CAT_2:9
.= the Target of A . x ; ::_thesis: verum
end;
dom the Source of C = the carrier' of C by FUNCT_2:def_1;
then dom the Source of C = (dom the Source of A) /\ the carrier' of C by A1, CAT_2:7, XBOOLE_1:28;
hence the Source of C = the Source of A | the carrier' of C by A2, FUNCT_1:46; ::_thesis: ( the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )
A4: dom the Target of A = the carrier' of A by FUNCT_2:def_1;
dom the Target of C = the carrier' of C by FUNCT_2:def_1;
then dom the Target of C = (dom the Target of A) /\ the carrier' of C by A4, CAT_2:7, XBOOLE_1:28;
hence the Target of C = the Target of A | the carrier' of C by A3, FUNCT_1:46; ::_thesis: the Comp of C = the Comp of A || the carrier' of C
A5: dom the Comp of C = (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]
proof
the Comp of C c= the Comp of A by CAT_2:def_4;
then A6: dom the Comp of C c= dom the Comp of A by RELAT_1:11;
dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def_18;
hence dom the Comp of C c= (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] by A6, XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] c= dom the Comp of C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] or x in dom the Comp of C )
assume A7: x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] ; ::_thesis: x in dom the Comp of C
then x in [: the carrier' of C, the carrier' of C:] by XBOOLE_0:def_4;
then reconsider f = x `1 , g = x `2 as Morphism of C by MCART_1:10;
reconsider f9 = f, g9 = g as Morphism of A by CAT_2:8;
x in dom the Comp of A by A7, XBOOLE_0:def_4;
then A8: [f9,g9] in dom the Comp of A by MCART_1:21;
dom f = dom f9 by CAT_2:9
.= cod g9 by A8, CAT_1:15
.= cod g by CAT_2:9 ;
then [f,g] in dom the Comp of C by CAT_1:15;
hence x in dom the Comp of C by A7, MCART_1:21; ::_thesis: verum
end;
the Comp of C c= the Comp of A by CAT_2:def_4;
hence the Comp of C = the Comp of A | ((dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]) by A5, GRFUNC_1:23
.= ( the Comp of A | (dom the Comp of A)) | [: the carrier' of C, the carrier' of C:] by RELAT_1:71
.= the Comp of A || the carrier' of C ;
::_thesis: verum
end;
theorem Th9: :: NATTRA_1:9
for A being Category
for O being non empty Subset of the carrier of A
for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds
id o in M ) holds
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
proof
let A be Category; ::_thesis: for O being non empty Subset of the carrier of A
for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds
id o in M ) holds
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
let O be non empty Subset of the carrier of A; ::_thesis: for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds
id o in M ) holds
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
let M be non empty Subset of the carrier' of A; ::_thesis: ( ( for o being Element of A st o in O holds
id o in M ) implies for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A )
assume A1: for o being Element of A st o in O holds
id o in M ; ::_thesis: for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
let DOM, COD be Function of M,O; ::_thesis: ( DOM = the Source of A | M & COD = the Target of A | M implies for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A )
assume that
A2: DOM = the Source of A | M and
A3: COD = the Target of A | M ; ::_thesis: for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
let COMP be PartFunc of [:M,M:],M; ::_thesis: ( COMP = the Comp of A || M implies CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A )
assume A4: COMP = the Comp of A || M ; ::_thesis: CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
set C = CatStr(# O,M,DOM,COD,COMP #);
A5: now__::_thesis:_for_f_being_Morphism_of_A
for_g_being_Morphism_of_CatStr(#_O,M,DOM,COD,COMP_#)_st_f_=_g_holds_
(_dom_f_=_dom_g_&_cod_f_=_cod_g_)
let f be Morphism of A; ::_thesis: for g being Morphism of CatStr(# O,M,DOM,COD,COMP #) st f = g holds
( dom f = dom g & cod f = cod g )
let g be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( f = g implies ( dom f = dom g & cod f = cod g ) )
assume A6: f = g ; ::_thesis: ( dom f = dom g & cod f = cod g )
dom the Source of CatStr(# O,M,DOM,COD,COMP #) = the carrier' of CatStr(# O,M,DOM,COD,COMP #) by FUNCT_2:def_1;
hence dom f = dom g by A2, A6, FUNCT_1:47; ::_thesis: cod f = cod g
dom the Target of CatStr(# O,M,DOM,COD,COMP #) = the carrier' of CatStr(# O,M,DOM,COD,COMP #) by FUNCT_2:def_1;
hence cod f = cod g by A3, A6, FUNCT_1:47; ::_thesis: verum
end;
A7: dom the Comp of CatStr(# O,M,DOM,COD,COMP #) = (dom the Comp of A) /\ [: the carrier' of CatStr(# O,M,DOM,COD,COMP #), the carrier' of CatStr(# O,M,DOM,COD,COMP #):] by A4, RELAT_1:61;
A8: now__::_thesis:_for_f,_g_being_Morphism_of_CatStr(#_O,M,DOM,COD,COMP_#)_st_dom_g_=_cod_f_holds_
[g,f]_in_dom_the_Comp_of_CatStr(#_O,M,DOM,COD,COMP_#)
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) )
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def_3;
assume dom g = cod f ; ::_thesis: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #)
then dom g9 = cod f by A5
.= cod f9 by A5 ;
then A9: [g9,f9] in dom the Comp of A by CAT_1:def_6;
[g,f] in [: the carrier' of CatStr(# O,M,DOM,COD,COMP #), the carrier' of CatStr(# O,M,DOM,COD,COMP #):] by ZFMISC_1:87;
hence [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A7, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
A10: dom the Comp of CatStr(# O,M,DOM,COD,COMP #) c= dom the Comp of A by A4, RELAT_1:60;
A11: CatStr(# O,M,DOM,COD,COMP #) is Category-like
proof
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) ) )
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def_3;
thus ( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) implies dom g = cod f ) ::_thesis: ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) )
proof
assume A12: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) ; ::_thesis: dom g = cod f
thus dom g = dom g9 by A5
.= cod f9 by A10, A12, CAT_1:def_6
.= cod f by A5 ; ::_thesis: verum
end;
thus ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) ) by A8; ::_thesis: verum
end;
A13: CatStr(# O,M,DOM,COD,COMP #) is transitive
proof
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def_3;
assume A14: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
[g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A14, A11, CAT_1:def_6;
then A15: the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = g (*) f by CAT_1:def_1;
A16: dom g9 = cod f by A5, A14
.= cod f9 by A5 ;
then [g9,f9] in dom the Comp of A by CAT_1:def_6;
then A17: the Comp of A . (g9,f9) = g9 (*) f9 by CAT_1:def_1;
A18: the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = the Comp of A . (g9,f9) by A4, A8, A14, FUNCT_1:47;
thus dom (g (*) f) = dom (g9 (*) f9) by A5, A18, A15, A17
.= dom f9 by A16, CAT_1:def_7
.= dom f by A5 ; ::_thesis: cod (g (*) f) = cod g
thus cod (g (*) f) = cod (g9 (*) f9) by A5, A18, A15, A17
.= cod g9 by A16, CAT_1:def_7
.= cod g by A5 ; ::_thesis: verum
end;
A19: for f, g being Morphism of CatStr(# O,M,DOM,COD,COMP #) st cod g = dom f holds
for ff, gg being Morphism of A st ff = f & gg = g holds
f (*) g = ff (*) gg
proof
let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( cod g = dom f implies for ff, gg being Morphism of A st ff = f & gg = g holds
f (*) g = ff (*) gg )
assume A20: cod g = dom f ; ::_thesis: for ff, gg being Morphism of A st ff = f & gg = g holds
f (*) g = ff (*) gg
let ff, gg be Morphism of A; ::_thesis: ( ff = f & gg = g implies f (*) g = ff (*) gg )
assume A21: ( ff = f & gg = g ) ; ::_thesis: f (*) g = ff (*) gg
A22: cod gg = dom f by A20, A5, A21
.= dom ff by A5, A21 ;
[f,g] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A20, A11, CAT_1:def_6;
hence f (*) g = the Comp of CatStr(# O,M,DOM,COD,COMP #) . (f,g) by CAT_1:def_1
.= the Comp of A . (ff,gg) by A21, A4, A8, A20, FUNCT_1:47
.= ff (*) gg by A22, CAT_1:16 ;
::_thesis: verum
end;
A23: CatStr(# O,M,DOM,COD,COMP #) is associative
proof
let f, g, h be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
reconsider g9 = g, f9 = f, h9 = h as Morphism of A by TARSKI:def_3;
assume that
A24: dom h = cod g and
A25: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
reconsider gf = the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f), hg = the Comp of CatStr(# O,M,DOM,COD,COMP #) . [h,g] as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A8, A24, A25, PARTFUN1:4;
A26: dom h9 = cod g by A5, A24
.= cod g9 by A5 ;
then A27: [h9,g9] in dom the Comp of A by CAT_1:def_6;
A28: dom g9 = cod f by A5, A25
.= cod f9 by A5 ;
then A29: [g9,f9] in dom the Comp of A by CAT_1:def_6;
reconsider gf9 = g9 (*) f9, hg9 = h9 (*) g9 as Morphism of A ;
the Comp of CatStr(# O,M,DOM,COD,COMP #) . (h,g) = the Comp of A . (h9,g9) by A4, A8, A24, FUNCT_1:47;
then A30: hg = h9 (*) g9 by A27, CAT_1:def_1;
then A31: dom hg = dom hg9 by A5
.= dom g9 by A26, CAT_1:def_7
.= cod f by A5, A25 ;
the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = the Comp of A . (g9,f9) by A4, A8, A25, FUNCT_1:47;
then A32: gf = gf9 by A29, CAT_1:def_1;
A33: dom h = cod g9 by A5, A24
.= cod gf9 by A28, CAT_1:def_7
.= cod gf by A5, A32 ;
A34: h (*) g = h9 (*) g9 by A19, A24;
g (*) f = g9 (*) f9 by A19, A25;
hence h (*) (g (*) f) = h9 (*) (g9 (*) f9) by A19, A33, A32
.= (h9 (*) g9) (*) f9 by A26, A28, CAT_1:def_8
.= (h (*) g) (*) f by A19, A34, A30, A31 ;
::_thesis: verum
end;
A35: CatStr(# O,M,DOM,COD,COMP #) is reflexive
proof
let b be Object of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {}
reconsider b9 = b as Object of A by TARSKI:def_3;
reconsider ii = id b9 as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A1;
A36: cod ii = cod (id b9) by A5
.= b ;
dom ii = dom (id b9) by A5
.= b ;
then ii in Hom (b,b) by A36;
hence Hom (b,b) <> {} ; ::_thesis: verum
end;
A37: for a being Object of CatStr(# O,M,DOM,COD,COMP #)
for aa being Element of A st a = aa holds
for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds
for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
proof
let a be Object of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: for aa being Element of A st a = aa holds
for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds
for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let aa be Element of A; ::_thesis: ( a = aa implies for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds
for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) )
assume A38: a = aa ; ::_thesis: for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds
for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let m be Morphism of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( m = id aa implies for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) )
assume A39: m = id aa ; ::_thesis: for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let b be Object of CatStr(# O,M,DOM,COD,COMP #); ::_thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
reconsider bb = b as Object of A by TARSKI:def_3;
thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f )
proof
assume A40: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds f (*) m = f
let f be Morphism of a,b; ::_thesis: f (*) m = f
reconsider ff = f as Morphism of A by TARSKI:def_3;
dom f = a by A40, CAT_1:5;
then A41: dom ff = aa by A38, A5;
dom f = aa by A38, A40, CAT_1:5
.= cod (id aa)
.= cod m by A39, A5 ;
hence f (*) m = ff (*) (id aa) by A19, A39
.= f by A41, CAT_1:22 ;
::_thesis: verum
end;
thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ::_thesis: verum
proof
assume A42: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds m (*) f = f
let f be Morphism of b,a; ::_thesis: m (*) f = f
reconsider ff = f as Morphism of A by TARSKI:def_3;
cod f = a by A42, CAT_1:5;
then A43: cod ff = aa by A38, A5;
dom f = b by A42, CAT_1:5;
then dom ff = bb by A5;
then A44: ff in Hom (bb,aa) by A43;
then reconsider ff = ff as Morphism of bb,aa by CAT_1:def_5;
A45: Hom (aa,aa) <> {} ;
cod f = aa by A38, A42, CAT_1:5
.= dom (id aa)
.= dom m by A39, A5 ;
hence m (*) f = (id aa) (*) ff by A19, A39
.= (id aa) * ff by A44, A45, CAT_1:def_13
.= f by A44, CAT_1:28 ;
::_thesis: verum
end;
end;
CatStr(# O,M,DOM,COD,COMP #) is with_identities
proof
let a be Element of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of A by TARSKI:def_3;
reconsider m = id aa as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A1;
A46: cod m = cod (id aa) by A5
.= a ;
dom m = dom (id aa) by A5
.= a ;
then m in Hom (a,a) by A46;
then reconsider m = m as Morphism of a,a by CAT_1:def_5;
take m ; ::_thesis: for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) m = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds m (*) b2 = b2 ) )
thus for b1 being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) m = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds m (*) b2 = b2 ) ) by A37; ::_thesis: verum
end;
then reconsider C = CatStr(# O,M,DOM,COD,COMP #) as Category by A11, A13, A23, A35;
C is Subcategory of A
proof
thus the carrier of C c= the carrier of A ; :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of C
for b3, b4 being Element of the carrier of A holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
thus for a, b being Object of C
for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ::_thesis: ( the Comp of C c= the Comp of A & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
proof
let a, b be Object of C; ::_thesis: for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of A; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that
A47: a = a9 and
A48: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9)
then consider f being Morphism of C such that
A49: x = f and
A50: dom f = a and
A51: cod f = b ;
reconsider f9 = f as Morphism of A by TARSKI:def_3;
A52: cod f9 = b9 by A5, A48, A51;
dom f9 = a9 by A5, A47, A50;
hence x in Hom (a9,b9) by A49, A52; ::_thesis: verum
end;
thus the Comp of C c= the Comp of A by A4, RELAT_1:59; ::_thesis: for b1 being Element of the carrier of C
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of C; ::_thesis: for b1 being Element of the carrier of A holds
( not a = b1 or id a = id b1 )
let a9 be Object of A; ::_thesis: ( not a = a9 or id a = id a9 )
assume A53: a = a9 ; ::_thesis: id a = id a9
reconsider m = id a9 as Morphism of C by A1, A53;
A54: cod m = cod (id a9) by A5
.= a by A53 ;
dom m = dom (id a9) by A5
.= a by A53 ;
then m in Hom (a,a) by A54;
then reconsider m = m as Morphism of a,a by CAT_1:def_5;
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) by A53, A37;
hence id a = id a9 by CAT_1:def_12; ::_thesis: verum
end;
hence CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A ; ::_thesis: verum
end;
theorem Th10: :: NATTRA_1:10
for C being strict Category
for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds
A = C
proof
let C be strict Category; ::_thesis: for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds
A = C
let A be strict Subcategory of C; ::_thesis: ( the carrier of A = the carrier of C & the carrier' of A = the carrier' of C implies A = C )
assume that
A1: the carrier of A = the carrier of C and
A2: the carrier' of A = the carrier' of C ; ::_thesis: A = C
A3: dom the Target of C = the carrier' of C by FUNCT_2:def_1;
A4: dom the Source of C = the carrier' of C by FUNCT_2:def_1;
A5: the Target of A = the Target of C | the carrier' of A by Th8
.= the Target of C by A2, A3, RELAT_1:68 ;
A6: dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def_18;
A7: the Comp of A = the Comp of C || the carrier' of A by Th8
.= the Comp of C by A2, A6, RELAT_1:68 ;
the Source of A = the Source of C | the carrier' of A by Th8
.= the Source of C by A2, A4, RELAT_1:68 ;
hence A = C by A1, A2, A5, A7; ::_thesis: verum
end;
begin
definition
canceled;
end;
:: deftheorem NATTRA_1:def_1_:_
canceled;
theorem :: NATTRA_1:11
for B, C, A being Category
for F being Functor of A,B
for G being Functor of B,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
proof
let B, C, A be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
let F be Functor of A,B; ::_thesis: for G being Functor of B,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
let G be Functor of B,C; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
then A2: Hom ((F . a),(F . b)) <> {} by CAT_1:84;
let f be Morphism of a,b; ::_thesis: (G * F) /. f = G /. (F /. f)
thus (G * F) /. f = (G * F) . f by A1, CAT_3:def_10
.= G . (F . f) by FUNCT_2:15
.= G . (F /. f) by A1, CAT_3:def_10
.= G /. (F /. f) by A2, CAT_3:def_10 ; ::_thesis: verum
end;
theorem :: NATTRA_1:12
for A, B being Category
for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) holds
F1 = F2
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) holds
F1 = F2
let F1, F2 be Functor of A,B; ::_thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) implies F1 = F2 )
assume A1: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Morphism_of_A_holds_F1_._f_=_F2_._f
let f be Morphism of A; ::_thesis: F1 . f = F2 . f
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
set a = dom f;
set b = cod f;
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
hence F1 . f = F2 . f9 by A1
.= F2 . f ;
::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th13: :: NATTRA_1:13
for B, A being Category
for F being Functor of A,B
for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
proof
let B, A be Category; ::_thesis: for F being Functor of A,B
for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let F be Functor of A,B; ::_thesis: for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let a, b, c be Object of A; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let g be Morphism of b,c; ::_thesis: F /. (g * f) = (F /. g) * (F /. f)
A3: dom g = b by A2, CAT_1:5;
A4: cod f = b by A1, CAT_1:5;
A5: F /. g = F . g by A2, CAT_3:def_10;
A6: Hom ((F . a),(F . b)) <> {} by A1, CAT_1:84;
A7: F /. f = F . f by A1, CAT_3:def_10;
A8: Hom ((F . b),(F . c)) <> {} by A2, CAT_1:84;
Hom (a,c) <> {} by A1, A2, CAT_1:24;
hence F /. (g * f) = F . (g * f) by CAT_3:def_10
.= F . (g (*) f) by A1, A2, CAT_1:def_13
.= (F . g) (*) (F . f) by A3, A4, CAT_1:64
.= (F /. g) * (F /. f) by A6, A8, A5, A7, CAT_1:def_13 ;
::_thesis: verum
end;
theorem :: NATTRA_1:14
for A, B being Category
for F being Functor of A,B
for c being Object of A
for d being Object of B st F /. (id c) = id d holds
F . c = d
proof
let A, B be Category; ::_thesis: for F being Functor of A,B
for c being Object of A
for d being Object of B st F /. (id c) = id d holds
F . c = d
let F be Functor of A,B; ::_thesis: for c being Object of A
for d being Object of B st F /. (id c) = id d holds
F . c = d
let c be Object of A; ::_thesis: for d being Object of B st F /. (id c) = id d holds
F . c = d
let d be Object of B; ::_thesis: ( F /. (id c) = id d implies F . c = d )
A1: Hom (c,c) <> {} ;
assume F /. (id c) = id d ; ::_thesis: F . c = d
then F . (id c) = id d by A1, CAT_3:def_10;
hence F . c = d by CAT_1:70; ::_thesis: verum
end;
theorem Th15: :: NATTRA_1:15
for B, A being Category
for F being Functor of A,B
for a being Object of A holds F /. (id a) = id (F . a)
proof
let B, A be Category; ::_thesis: for F being Functor of A,B
for a being Object of A holds F /. (id a) = id (F . a)
let F be Functor of A,B; ::_thesis: for a being Object of A holds F /. (id a) = id (F . a)
let a be Object of A; ::_thesis: F /. (id a) = id (F . a)
Hom (a,a) <> {} ;
hence F /. (id a) = F . (id a) by CAT_3:def_10
.= id (F . a) by CAT_1:71 ;
::_thesis: verum
end;
theorem :: NATTRA_1:16
for A being Category
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (id A) /. f = f
proof
let A be Category; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (id A) /. f = f
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (id A) /. f = f )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (id A) /. f = f
let f be Morphism of a,b; ::_thesis: (id A) /. f = f
thus (id A) /. f = (id A) . f by A1, CAT_3:def_10
.= f by FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th17: :: NATTRA_1:17
for A being Category
for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds
( a = c & b = d )
proof
let A be Category; ::_thesis: for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds
( a = c & b = d )
let a, b, c, d be Object of A; ::_thesis: ( Hom (a,b) meets Hom (c,d) implies ( a = c & b = d ) )
assume Hom (a,b) meets Hom (c,d) ; ::_thesis: ( a = c & b = d )
then consider x being set such that
A1: x in Hom (a,b) and
A2: x in Hom (c,d) by XBOOLE_0:3;
reconsider x = x as Morphism of A by A1;
A3: cod x = b by A1, CAT_1:1;
dom x = a by A1, CAT_1:1;
hence ( a = c & b = d ) by A2, A3, CAT_1:1; ::_thesis: verum
end;
begin
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
predF1 is_transformable_to F2 means :Def2: :: NATTRA_1:def 2
for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ;
reflexivity
for F1 being Functor of A,B
for a being Object of A holds Hom ((F1 . a),(F1 . a)) <> {} ;
end;
:: deftheorem Def2 defines is_transformable_to NATTRA_1:def_2_:_
for A, B being Category
for F1, F2 being Functor of A,B holds
( F1 is_transformable_to F2 iff for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} );
theorem Th18: :: NATTRA_1:18
for A, B being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2
proof
let A, B be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2
let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2 )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ; ::_thesis: F is_transformable_to F2
let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: Hom ((F . a),(F2 . a)) <> {}
A3: Hom ((F1 . a),(F2 . a)) <> {} by A2, Def2;
Hom ((F . a),(F1 . a)) <> {} by A1, Def2;
hence Hom ((F . a),(F2 . a)) <> {} by A3, CAT_1:24; ::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
mode transformation of F1,F2 -> Function of the carrier of A, the carrier' of B means :Def3: :: NATTRA_1:def 3
for a being Object of A holds it . a is Morphism of F1 . a,F2 . a;
existence
ex b1 being Function of the carrier of A, the carrier' of B st
for a being Object of A holds b1 . a is Morphism of F1 . a,F2 . a
proof
deffunc H1( Object of A) -> Element of bool the carrier' of B = Hom ((F1 . $1),(F2 . $1));
A2: for a being Object of A holds the carrier' of B meets H1(a)
proof
let a be Object of A; ::_thesis: the carrier' of B meets H1(a)
set x = the Element of Hom ((F1 . a),(F2 . a));
A3: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2;
now__::_thesis:_ex_x_being_Element_of_Hom_((F1_._a),(F2_._a))_st_
(_x_in_the_carrier'_of_B_&_x_in_Hom_((F1_._a),(F2_._a))_)
take x = the Element of Hom ((F1 . a),(F2 . a)); ::_thesis: ( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) )
thus ( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) ) by A3, TARSKI:def_3; ::_thesis: verum
end;
hence the carrier' of B meets H1(a) by XBOOLE_0:3; ::_thesis: verum
end;
consider t being Function of the carrier of A, the carrier' of B such that
A4: for a being Object of A holds t . a in H1(a) from FUNCT_2:sch_10(A2);
take t ; ::_thesis: for a being Object of A holds t . a is Morphism of F1 . a,F2 . a
let a be Object of A; ::_thesis: t . a is Morphism of F1 . a,F2 . a
t . a in Hom ((F1 . a),(F2 . a)) by A4;
hence t . a is Morphism of F1 . a,F2 . a by CAT_1:def_5; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines transformation NATTRA_1:def_3_:_
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for b5 being Function of the carrier of A, the carrier' of B holds
( b5 is transformation of F1,F2 iff for a being Object of A holds b5 . a is Morphism of F1 . a,F2 . a );
definition
let A, B be Category;
let F be Functor of A,B;
func id F -> transformation of F,F means :Def4: :: NATTRA_1:def 4
for a being Object of A holds it . a = id (F . a);
existence
ex b1 being transformation of F,F st
for a being Object of A holds b1 . a = id (F . a)
proof
deffunc H1( Object of A) -> Morphism of F . $1,F . $1 = id (F . $1);
consider t being Function of the carrier of A, the carrier' of B such that
A1: for a being Object of A holds t . a = H1(a) from FUNCT_2:sch_4();
for a being Object of A holds t . a is Morphism of F . a,F . a
proof
let a be Object of A; ::_thesis: t . a is Morphism of F . a,F . a
t . a = id (F . a) by A1;
hence t . a is Morphism of F . a,F . a ; ::_thesis: verum
end;
then reconsider t = t as transformation of F,F by Def3;
take t ; ::_thesis: for a being Object of A holds t . a = id (F . a)
let a be Object of A; ::_thesis: t . a = id (F . a)
thus t . a = id (F . a) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being transformation of F,F st ( for a being Object of A holds b1 . a = id (F . a) ) & ( for a being Object of A holds b2 . a = id (F . a) ) holds
b1 = b2
proof
let it1, it2 be transformation of F,F; ::_thesis: ( ( for a being Object of A holds it1 . a = id (F . a) ) & ( for a being Object of A holds it2 . a = id (F . a) ) implies it1 = it2 )
assume that
A2: for a being Object of A holds it1 . a = id (F . a) and
A3: for a being Object of A holds it2 . a = id (F . a) ; ::_thesis: it1 = it2
now__::_thesis:_for_a_being_Object_of_A_holds_it1_._a_=_it2_._a
let a be Object of A; ::_thesis: it1 . a = it2 . a
thus it1 . a = id (F . a) by A2
.= it2 . a by A3 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines id NATTRA_1:def_4_:_
for A, B being Category
for F being Functor of A,B
for b4 being transformation of F,F holds
( b4 = id F iff for a being Object of A holds b4 . a = id (F . a) );
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let a be Object of A;
funct . a -> Morphism of F1 . a,F2 . a equals :Def5: :: NATTRA_1:def 5
t . a;
coherence
t . a is Morphism of F1 . a,F2 . a by A1, Def3;
end;
:: deftheorem Def5 defines . NATTRA_1:def_5_:_
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 = t . a;
definition
let A, B be Category;
let F, F1, F2 be Functor of A,B;
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ;
let t1 be transformation of F,F1;
let t2 be transformation of F1,F2;
funct2 `*` t1 -> transformation of F,F2 means :Def6: :: NATTRA_1:def 6
for a being Object of A holds it . a = (t2 . a) * (t1 . a);
existence
ex b1 being transformation of F,F2 st
for a being Object of A holds b1 . a = (t2 . a) * (t1 . a)
proof
deffunc H1( Object of A) -> Morphism of F . $1,F2 . $1 = (t2 . $1) * (t1 . $1);
consider t being Function of the carrier of A, the carrier' of B such that
A3: for a being Object of A holds t . a = H1(a) from FUNCT_2:sch_4();
A4: for a being Object of A holds t . a is Morphism of F . a,F2 . a
proof
let a be Object of A; ::_thesis: t . a is Morphism of F . a,F2 . a
t . a = (t2 . a) * (t1 . a) by A3;
hence t . a is Morphism of F . a,F2 . a ; ::_thesis: verum
end;
F is_transformable_to F2 by A1, A2, Th18;
then reconsider t9 = t as transformation of F,F2 by A4, Def3;
take t9 ; ::_thesis: for a being Object of A holds t9 . a = (t2 . a) * (t1 . a)
let a be Object of A; ::_thesis: t9 . a = (t2 . a) * (t1 . a)
thus t9 . a = t . a by A1, A2, Def5, Th18
.= (t2 . a) * (t1 . a) by A3 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being transformation of F,F2 st ( for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds b2 . a = (t2 . a) * (t1 . a) ) holds
b1 = b2
proof
let it1, it2 be transformation of F,F2; ::_thesis: ( ( for a being Object of A holds it1 . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds it2 . a = (t2 . a) * (t1 . a) ) implies it1 = it2 )
assume that
A5: for a being Object of A holds it1 . a = (t2 . a) * (t1 . a) and
A6: for a being Object of A holds it2 . a = (t2 . a) * (t1 . a) ; ::_thesis: it1 = it2
now__::_thesis:_for_a_being_Object_of_A_holds_it1_._a_=_it2_._a
let a be Object of A; ::_thesis: it1 . a = it2 . a
thus it1 . a = it1 . a by A1, A2, Def5, Th18
.= (t2 . a) * (t1 . a) by A5
.= it2 . a by A6
.= it2 . a by A1, A2, Def5, Th18 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines `*` NATTRA_1:def_6_:_
for A, B being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for b8 being transformation of F,F2 holds
( b8 = t2 `*` t1 iff for a being Object of A holds b8 . a = (t2 . a) * (t1 . a) );
theorem Th19: :: NATTRA_1:19
for B, A being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
proof
let B, A be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2 )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
let t1, t2 be transformation of F1,F2; ::_thesis: ( ( for a being Object of A holds t1 . a = t2 . a ) implies t1 = t2 )
assume A2: for a being Object of A holds t1 . a = t2 . a ; ::_thesis: t1 = t2
now__::_thesis:_for_a_being_Object_of_A_holds_t1_._a_=_t2_._a
let a be Object of A; ::_thesis: t1 . a = t2 . a
thus t1 . a = t1 . a by A1, Def5
.= t2 . a by A2
.= t2 . a by A1, Def5 ; ::_thesis: verum
end;
hence t1 = t2 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th20: :: NATTRA_1:20
for B, A being Category
for F being Functor of A,B
for a being Object of A holds (id F) . a = id (F . a)
proof
let B, A be Category; ::_thesis: for F being Functor of A,B
for a being Object of A holds (id F) . a = id (F . a)
let F be Functor of A,B; ::_thesis: for a being Object of A holds (id F) . a = id (F . a)
let a be Object of A; ::_thesis: (id F) . a = id (F . a)
thus (id F) . a = (id F) . a by Def5
.= id (F . a) by Def4 ; ::_thesis: verum
end;
theorem Th21: :: NATTRA_1:21
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 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
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 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t ) )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
let t be transformation of F1,F2; ::_thesis: ( (id F2) `*` t = t & t `*` (id F1) = t )
now__::_thesis:_for_a_being_Object_of_A_holds_((id_F2)_`*`_t)_._a_=_t_._a
let a be Object of A; ::_thesis: ((id F2) `*` t) . a = t . a
A2: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2;
thus ((id F2) `*` t) . a = ((id F2) . a) * (t . a) by A1, Def6
.= (id (F2 . a)) * (t . a) by Th20
.= t . a by A2, CAT_1:28 ; ::_thesis: verum
end;
hence (id F2) `*` t = t by A1, Th19; ::_thesis: t `*` (id F1) = t
now__::_thesis:_for_a_being_Object_of_A_holds_(t_`*`_(id_F1))_._a_=_t_._a
let a be Object of A; ::_thesis: (t `*` (id F1)) . a = t . a
A3: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2;
thus (t `*` (id F1)) . a = (t . a) * ((id F1) . a) by A1, Def6
.= (t . a) * (id (F1 . a)) by Th20
.= t . a by A3, CAT_1:29 ; ::_thesis: verum
end;
hence t `*` (id F1) = t by A1, Th19; ::_thesis: verum
end;
theorem Th22: :: NATTRA_1:22
for A, B being Category
for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
proof
let A, B be Category; ::_thesis: for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let F, F1, F2, F3 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 and
A3: F2 is_transformable_to F3 ; ::_thesis: for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t1 be transformation of F,F1; ::_thesis: for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t2 be transformation of F1,F2; ::_thesis: for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t3 be transformation of F2,F3; ::_thesis: (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
A4: F1 is_transformable_to F3 by A2, A3, Th18;
A5: F is_transformable_to F2 by A1, A2, Th18;
now__::_thesis:_for_a_being_Object_of_A_holds_((t3_`*`_t2)_`*`_t1)_._a_=_(t3_`*`_(t2_`*`_t1))_._a
let a be Object of A; ::_thesis: ((t3 `*` t2) `*` t1) . a = (t3 `*` (t2 `*` t1)) . a
A6: Hom ((F . a),(F1 . a)) <> {} by A1, Def2;
A7: Hom ((F1 . a),(F2 . a)) <> {} by A2, Def2;
A8: Hom ((F2 . a),(F3 . a)) <> {} by A3, Def2;
thus ((t3 `*` t2) `*` t1) . a = ((t3 `*` t2) . a) * (t1 . a) by A1, A4, Def6
.= ((t3 . a) * (t2 . a)) * (t1 . a) by A2, A3, Def6
.= (t3 . a) * ((t2 . a) * (t1 . a)) by A6, A7, A8, CAT_1:25
.= (t3 . a) * ((t2 `*` t1) . a) by A1, A2, Def6
.= (t3 `*` (t2 `*` t1)) . a by A3, A5, Def6 ; ::_thesis: verum
end;
hence (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) by A1, A4, Th18, Th19; ::_thesis: verum
end;
begin
Lm1: for B, A being Category
for F being Functor of A,B
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
proof
let B, A be Category; ::_thesis: for F being Functor of A,B
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
let F be Functor of A,B; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
let f be Morphism of a,b; ::_thesis: ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
A2: Hom (a,a) <> {} ;
A3: Hom (b,b) <> {} ;
thus ((id F) . b) * (F /. f) = (id (F . b)) * (F /. f) by Th20
.= (F /. (id b)) * (F /. f) by Th15
.= F /. ((id b) * f) by A1, A3, Th13
.= F /. f by A1, CAT_1:28
.= F /. (f * (id a)) by A1, CAT_1:29
.= (F /. f) * (F /. (id a)) by A1, A2, Th13
.= (F /. f) * (id (F . a)) by Th15
.= (F /. f) * ((id F) . a) by Th20 ; ::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
predF1 is_naturally_transformable_to F2 means :Def7: :: NATTRA_1:def 7
( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) );
reflexivity
for F1 being Functor of A,B holds
( F1 is_transformable_to F1 & ex t being transformation of F1,F1 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F1 /. f) * (t . a) )
proof
let F be Functor of A,B; ::_thesis: ( F is_transformable_to F & ex t being transformation of F,F st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) )
ex t being transformation of F,F st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a)
proof
take id F ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
thus for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) by Lm1; ::_thesis: verum
end;
hence ( F is_transformable_to F & ex t being transformation of F,F st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines is_naturally_transformable_to NATTRA_1:def_7_:_
for A, B being Category
for F1, F2 being Functor of A,B holds
( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) );
Lm2: for B, A being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
proof
let B, A be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ; ::_thesis: for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
let t1 be transformation of F,F1; ::_thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) implies for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )
assume A3: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ; ::_thesis: for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
let t2 be transformation of F1,F2; ::_thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) implies for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )
assume A4: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )
A5: Hom ((F . b),(F1 . b)) <> {} by A1, Def2;
A6: Hom ((F . a),(F1 . a)) <> {} by A1, Def2;
A7: Hom ((F1 . b),(F2 . b)) <> {} by A2, Def2;
A8: Hom ((F1 . a),(F2 . a)) <> {} by A2, Def2;
assume A9: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
then A10: Hom ((F . a),(F . b)) <> {} by CAT_1:84;
let f be Morphism of a,b; ::_thesis: ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
A11: Hom ((F2 . a),(F2 . b)) <> {} by A9, CAT_1:84;
A12: Hom ((F1 . a),(F1 . b)) <> {} by A9, CAT_1:84;
thus ((t2 `*` t1) . b) * (F /. f) = ((t2 . b) * (t1 . b)) * (F /. f) by A1, A2, Def6
.= (t2 . b) * ((t1 . b) * (F /. f)) by A10, A5, A7, CAT_1:25
.= (t2 . b) * ((F1 /. f) * (t1 . a)) by A3, A9
.= ((t2 . b) * (F1 /. f)) * (t1 . a) by A6, A7, A12, CAT_1:25
.= ((F2 /. f) * (t2 . a)) * (t1 . a) by A4, A9
.= (F2 /. f) * ((t2 . a) * (t1 . a)) by A6, A8, A11, CAT_1:25
.= (F2 /. f) * ((t2 `*` t1) . a) by A1, A2, Def6 ; ::_thesis: verum
end;
theorem Th23: :: NATTRA_1:23
for A, B being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2
proof
let A, B be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2
let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2 )
assume A1: F is_transformable_to F1 ; :: according to NATTRA_1:def_7 ::_thesis: ( for t being transformation of F,F1 ex a, b being Object of A st
( Hom (a,b) <> {} & not for f being Morphism of a,b holds (t . b) * (F /. f) = (F1 /. f) * (t . a) ) or not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 )
given t1 being transformation of F,F1 such that A2: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ; ::_thesis: ( not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 )
assume A3: F1 is_transformable_to F2 ; :: according to NATTRA_1:def_7 ::_thesis: ( for t being transformation of F1,F2 ex a, b being Object of A st
( Hom (a,b) <> {} & not for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) or F is_naturally_transformable_to F2 )
given t2 being transformation of F1,F2 such that A4: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ; ::_thesis: F is_naturally_transformable_to F2
thus F is_transformable_to F2 by A1, A3, Th18; :: according to NATTRA_1:def_7 ::_thesis: ex t being transformation of F,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F2 /. f) * (t . a)
take t2 `*` t1 ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
thus for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) by A1, A2, A3, A4, Lm2; ::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_naturally_transformable_to F2 ;
mode natural_transformation of F1,F2 -> transformation of F1,F2 means :Def8: :: NATTRA_1:def 8
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (it . b) * (F1 /. f) = (F2 /. f) * (it . a);
existence
ex b1 being transformation of F1,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (b1 . b) * (F1 /. f) = (F2 /. f) * (b1 . a) by A1, Def7;
end;
:: deftheorem Def8 defines natural_transformation NATTRA_1:def_8_:_
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for b5 being transformation of F1,F2 holds
( b5 is natural_transformation of F1,F2 iff for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (b5 . b) * (F1 /. f) = (F2 /. f) * (b5 . a) );
definition
let A, B be Category;
let F be Functor of A,B;
:: original: id
redefine func id F -> natural_transformation of F,F;
coherence
id F is natural_transformation of F,F
proof
thus F is_naturally_transformable_to F ; :: according to NATTRA_1:def_8 ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
thus for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) by Lm1; ::_thesis: verum
end;
end;
definition
let A, B be Category;
let F, F1, F2 be Functor of A,B;
assume that
B1: F is_naturally_transformable_to F1 and
B2: F1 is_naturally_transformable_to F2 ;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
funct2 `*` t1 -> natural_transformation of F,F2 equals :Def9: :: NATTRA_1:def 9
t2 `*` t1;
coherence
t2 `*` t1 is natural_transformation of F,F2
proof
A1: F is_naturally_transformable_to F2 by B1, B2, Th23;
A2: F1 is_transformable_to F2 by B2, Def7;
A3: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) by B2, Def8;
A4: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) by B1, Def8;
F is_transformable_to F1 by B1, Def7;
then for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) by A2, A4, A3, Lm2;
hence t2 `*` t1 is natural_transformation of F,F2 by A1, Def8; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines `*` NATTRA_1:def_9_:_
for A, B being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2 holds t2 `*` t1 = t2 `*` t1;
theorem Th24: :: NATTRA_1:24
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t ) )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )
then A2: F1 is_transformable_to F2 by Def7;
let t be natural_transformation of F1,F2; ::_thesis: ( (id F2) `*` t = t & t `*` (id F1) = t )
thus (id F2) `*` t = (id F2) `*` t by A1, Def9
.= t by A2, Th21 ; ::_thesis: t `*` (id F1) = t
thus t `*` (id F1) = t `*` (id F1) by A1, Def9
.= t by A2, Th21 ; ::_thesis: verum
end;
theorem Th25: :: NATTRA_1:25
for B, A being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)
proof
let B, A be Category; ::_thesis: for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)
let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a) )
assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2 ; ::_thesis: for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)
A3: F1 is_transformable_to F2 by A2, Def7;
let t1 be natural_transformation of F,F1; ::_thesis: for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)
let t2 be natural_transformation of F1,F2; ::_thesis: for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)
let a be Object of A; ::_thesis: (t2 `*` t1) . a = (t2 . a) * (t1 . a)
reconsider t19 = t1 as transformation of F,F1 ;
reconsider t29 = t2 as transformation of F1,F2 ;
A4: F is_transformable_to F1 by A1, Def7;
thus (t2 `*` t1) . a = (t29 `*` t19) . a by A1, A2, Def9
.= (t2 . a) * (t1 . a) by A4, A3, Def6 ; ::_thesis: verum
end;
theorem Th26: :: NATTRA_1:26
for A, B being Category
for F, F1, F2, F3 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
proof
let A, B be Category; ::_thesis: for F, F1, F2, F3 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let F, F1, F2, F3 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let t1 be natural_transformation of F1,F2; ::_thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) )
assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2 and
A3: F2 is_naturally_transformable_to F3 ; ::_thesis: for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A4: F is_naturally_transformable_to F2 by A1, A2, Th23;
A5: F2 is_transformable_to F3 by A3, Def7;
A6: F1 is_transformable_to F2 by A2, Def7;
let t3 be natural_transformation of F2,F3; ::_thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A7: F is_transformable_to F1 by A1, Def7;
F1 is_naturally_transformable_to F3 by A2, A3, Th23;
hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def9
.= (t3 `*` t1) `*` t by A2, A3, Def9
.= t3 `*` (t1 `*` t) by A7, A6, A5, Th22
.= t3 `*` (t1 `*` t) by A1, A2, Def9
.= t3 `*` (t1 `*` t) by A3, A4, Def9 ;
::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
let IT be transformation of F1,F2;
attrIT is invertible means :Def10: :: NATTRA_1:def 10
for a being Object of A holds IT . a is invertible ;
end;
:: deftheorem Def10 defines invertible NATTRA_1:def_10_:_
for A, B being Category
for F1, F2 being Functor of A,B
for IT being transformation of F1,F2 holds
( IT is invertible iff for a being Object of A holds IT . a is invertible );
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
predF1,F2 are_naturally_equivalent means :Def11: :: NATTRA_1:def 11
( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible );
reflexivity
for F1 being Functor of A,B holds
( F1 is_naturally_transformable_to F1 & ex t being natural_transformation of F1,F1 st t is invertible )
proof
let F be Functor of A,B; ::_thesis: ( F is_naturally_transformable_to F & ex t being natural_transformation of F,F st t is invertible )
thus F is_naturally_transformable_to F ; ::_thesis: ex t being natural_transformation of F,F st t is invertible
take id F ; ::_thesis: id F is invertible
let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (id F) . a is invertible
(id F) . a = id (F . a) by Th20;
hence (id F) . a is invertible by CAT_1:44; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines are_naturally_equivalent NATTRA_1:def_11_:_
for A, B being Category
for F1, F2 being Functor of A,B holds
( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ) );
notation
let A, B be Category;
let F1, F2 be Functor of A,B;
synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ;
end;
Lm3: for A, B being Category
for F1, F2 being Functor of A,B
for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds
F2 is_transformable_to F1
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds
F2 is_transformable_to F1
let F1, F2 be Functor of A,B; ::_thesis: for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds
F2 is_transformable_to F1
let t be transformation of F1,F2; ::_thesis: ( F1 is_transformable_to F2 & t is invertible implies F2 is_transformable_to F1 )
assume that
A1: F1 is_transformable_to F2 and
A2: for a being Object of A holds t . a is invertible ; :: according to NATTRA_1:def_10 ::_thesis: F2 is_transformable_to F1
let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: Hom ((F2 . a),(F1 . a)) <> {}
A3: t . a is invertible by A2;
Hom ((F1 . a),(F2 . a)) <> {} by A1, Def2;
hence Hom ((F2 . a),(F1 . a)) <> {} by A3, CAT_1:41; ::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume B1: F1 is_transformable_to F2 ;
let t1 be transformation of F1,F2;
assume B2: t1 is invertible ;
funct1 " -> transformation of F2,F1 means :Def12: :: NATTRA_1:def 12
for a being Object of A holds it . a = (t1 . a) " ;
existence
ex b1 being transformation of F2,F1 st
for a being Object of A holds b1 . a = (t1 . a) "
proof
deffunc H1( Object of A) -> Morphism of F2 . $1,F1 . $1 = (t1 . $1) " ;
consider t being Function of the carrier of A, the carrier' of B such that
A1: for a being Object of A holds t . a = H1(a) from FUNCT_2:sch_4();
A2: now__::_thesis:_for_a_being_Object_of_A_holds_t_._a_is_Morphism_of_F2_._a,F1_._a
let a be Object of A; ::_thesis: t . a is Morphism of F2 . a,F1 . a
t . a = (t1 . a) " by A1;
hence t . a is Morphism of F2 . a,F1 . a ; ::_thesis: verum
end;
F2 is_transformable_to F1 by B1, B2, Lm3;
then reconsider t = t as transformation of F2,F1 by A2, Def3;
take t ; ::_thesis: for a being Object of A holds t . a = (t1 . a) "
let a be Object of A; ::_thesis: t . a = (t1 . a) "
thus t . a = t . a by B1, B2, Def5, Lm3
.= (t1 . a) " by A1 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being transformation of F2,F1 st ( for a being Object of A holds b1 . a = (t1 . a) " ) & ( for a being Object of A holds b2 . a = (t1 . a) " ) holds
b1 = b2
proof
let t, t9 be transformation of F2,F1; ::_thesis: ( ( for a being Object of A holds t . a = (t1 . a) " ) & ( for a being Object of A holds t9 . a = (t1 . a) " ) implies t = t9 )
assume that
A3: for a being Object of A holds t . a = (t1 . a) " and
A4: for a being Object of A holds t9 . a = (t1 . a) " ; ::_thesis: t = t9
now__::_thesis:_for_a_being_Object_of_A_holds_t_._a_=_t9_._a
let a be Object of A; ::_thesis: t . a = t9 . a
thus t . a = (t1 . a) " by A3
.= t9 . a by A4 ; ::_thesis: verum
end;
hence t = t9 by B1, B2, Lm3, Th19; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines " NATTRA_1:def_12_:_
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1 being transformation of F1,F2 st t1 is invertible holds
for b6 being transformation of F2,F1 holds
( b6 = t1 " iff for a being Object of A holds b6 . a = (t1 . a) " );
Lm4: now__::_thesis:_for_A,_B_being_Category
for_F1,_F2_being_Functor_of_A,B
for_t1_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&_t1_is_invertible_holds_
for_a,_b_being_Object_of_A_st_Hom_(a,b)_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_((t1_")_._b)_*_(F2_/._f)_=_(F1_/._f)_*_((t1_")_._a)
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) )
assume A3: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
A4: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84;
let f be Morphism of a,b; ::_thesis: ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
A5: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;
A6: F1 is_transformable_to F2 by A1, Def7;
A7: Hom ((F1 . b),(F2 . b)) <> {} by Def2, A1, Def7;
A8: t1 . b is invertible by A2, Def10;
then A9: Hom ((F2 . b),(F1 . b)) <> {} by A7, CAT_1:41;
A10: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def7, Def2;
(F2 /. f) * (t1 . a) = (t1 . b) * (F1 /. f) by A1, A3, Def8;
then A11: (((t1 . b) ") * (F2 /. f)) * (t1 . a) = ((t1 . b) ") * ((t1 . b) * (F1 /. f)) by A10, A9, A5, CAT_1:25
.= (((t1 . b) ") * (t1 . b)) * (F1 /. f) by A4, A7, A9, CAT_1:25
.= (id (F1 . b)) * (F1 /. f) by A8, CAT_1:def_17
.= F1 /. f by A4, CAT_1:28 ;
A12: t1 . a is invertible by A2, Def10;
then A13: Hom ((F2 . a),(F1 . a)) <> {} by A10, CAT_1:41;
then A14: Hom ((F2 . a),(F1 . b)) <> {} by A4, CAT_1:24;
then ((t1 . b) ") * (F2 /. f) = (((t1 . b) ") * (F2 /. f)) * (id (F2 . a)) by CAT_1:29
.= (((t1 . b) ") * (F2 /. f)) * ((t1 . a) * ((t1 . a) ")) by A12, CAT_1:def_17
.= (F1 /. f) * ((t1 . a) ") by A10, A13, A14, A11, CAT_1:25 ;
hence ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 . a) ") by A2, A6, Def12
.= (F1 /. f) * ((t1 ") . a) by A2, A6, Def12 ;
::_thesis: verum
end;
Lm5: for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
F2 is_naturally_transformable_to F1
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
F2 is_naturally_transformable_to F1
let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
F2 is_naturally_transformable_to F1
let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies F2 is_naturally_transformable_to F1 )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: ( not t1 is invertible or F2 is_naturally_transformable_to F1 )
assume A2: t1 is invertible ; ::_thesis: F2 is_naturally_transformable_to F1
hence F2 is_transformable_to F1 by A1, Def7, Lm3; :: according to NATTRA_1:def_7 ::_thesis: ex t being transformation of F2,F1 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F2 /. f) = (F1 /. f) * (t . a)
take t1 " ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
thus for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) by A1, A2, Lm4; ::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
let t1 be natural_transformation of F1,F2;
assume that
B1: F1 is_naturally_transformable_to F2 and
B2: t1 is invertible ;
funct1 " -> natural_transformation of F2,F1 equals :Def13: :: NATTRA_1:def 13
t1 " ;
coherence
t1 " is natural_transformation of F2,F1
proof
A1: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) by B1, B2, Lm4;
F2 is_naturally_transformable_to F1 by B1, B2, Lm5;
hence t1 " is natural_transformation of F2,F1 by A1, Def8; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines " NATTRA_1:def_13_:_
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
t1 " = t1 " ;
theorem Th27: :: NATTRA_1:27
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a being Object of A holds (t1 ") . a = (t1 . a) "
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a being Object of A holds (t1 ") . a = (t1 . a) "
let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a being Object of A holds (t1 ") . a = (t1 . a) "
let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a being Object of A holds (t1 ") . a = (t1 . a) " )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible ; ::_thesis: for a being Object of A holds (t1 ") . a = (t1 . a) "
let a be Object of A; ::_thesis: (t1 ") . a = (t1 . a) "
A3: F1 is_transformable_to F2 by A1, Def7;
thus (t1 ") . a = (t1 ") . a by A1, A2, Def13
.= (t1 . a) " by A2, A3, Def12 ; ::_thesis: verum
end;
theorem :: NATTRA_1:28
for A, B being Category
for F1, F2 being Functor of A,B st F1 ~= F2 holds
F2 ~= F1
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 ~= F2 holds
F2 ~= F1
let F1, F2 be Functor of A,B; ::_thesis: ( F1 ~= F2 implies F2 ~= F1 )
assume A1: F1 is_naturally_transformable_to F2 ; :: according to NATTRA_1:def_11 ::_thesis: ( for t being natural_transformation of F1,F2 holds not t is invertible or F2 ~= F1 )
given t being natural_transformation of F1,F2 such that A2: t is invertible ; ::_thesis: F2 ~= F1
thus F2 is_naturally_transformable_to F1 by A1, A2, Lm5; :: according to NATTRA_1:def_11 ::_thesis: ex t being natural_transformation of F2,F1 st t is invertible
take t " ; ::_thesis: t " is invertible
let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t ") . a is invertible
(t ") . a = (t . a) " by A1, A2, Th27;
hence (t ") . a is invertible by A2, Def10, CAT_1:46; ::_thesis: verum
end;
theorem Th29: :: NATTRA_1:29
for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
F1 ~= F3
proof
let A, B be Category; ::_thesis: for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
F1 ~= F3
let F1, F2, F3 be Functor of A,B; ::_thesis: ( F1 ~= F2 & F2 ~= F3 implies F1 ~= F3 )
assume A1: F1 is_naturally_transformable_to F2 ; :: according to NATTRA_1:def_11 ::_thesis: ( for t being natural_transformation of F1,F2 holds not t is invertible or not F2 ~= F3 or F1 ~= F3 )
given t being natural_transformation of F1,F2 such that A2: t is invertible ; ::_thesis: ( not F2 ~= F3 or F1 ~= F3 )
assume A3: F2 is_naturally_transformable_to F3 ; :: according to NATTRA_1:def_11 ::_thesis: ( for t being natural_transformation of F2,F3 holds not t is invertible or F1 ~= F3 )
given t9 being natural_transformation of F2,F3 such that A4: t9 is invertible ; ::_thesis: F1 ~= F3
thus F1 is_naturally_transformable_to F3 by A1, A3, Th23; :: according to NATTRA_1:def_11 ::_thesis: ex t being natural_transformation of F1,F3 st t is invertible
take t9 `*` t ; ::_thesis: t9 `*` t is invertible
let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t9 `*` t) . a is invertible
A5: t9 . a is invertible by A4, Def10;
A6: t . a is invertible by A2, Def10;
(t9 `*` t) . a = (t9 . a) * (t . a) by A1, A3, Th25;
hence (t9 `*` t) . a is invertible by A5, A6, CAT_1:45; ::_thesis: verum
end;
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1,F2 are_naturally_equivalent ;
mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :Def14: :: NATTRA_1:def 14
it is invertible ;
existence
ex b1 being natural_transformation of F1,F2 st b1 is invertible by A1, Def11;
end;
:: deftheorem Def14 defines natural_equivalence NATTRA_1:def_14_:_
for A, B being Category
for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds
for b5 being natural_transformation of F1,F2 holds
( b5 is natural_equivalence of F1,F2 iff b5 is invertible );
theorem :: NATTRA_1:30
for A, B being Category
for F being Functor of A,B holds id F is natural_equivalence of F,F
proof
let A, B be Category; ::_thesis: for F being Functor of A,B holds id F is natural_equivalence of F,F
let F be Functor of A,B; ::_thesis: id F is natural_equivalence of F,F
thus F ~= F ; :: according to NATTRA_1:def_14 ::_thesis: id F is invertible
let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (id F) . a is invertible
(id F) . a = id (F . a) by Th20;
hence (id F) . a is invertible by CAT_1:44; ::_thesis: verum
end;
theorem :: NATTRA_1:31
for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
for t being natural_equivalence of F1,F2
for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3
proof
let A, B be Category; ::_thesis: for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
for t being natural_equivalence of F1,F2
for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3
let F1, F2, F3 be Functor of A,B; ::_thesis: ( F1 ~= F2 & F2 ~= F3 implies for t being natural_equivalence of F1,F2
for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3 )
assume that
A1: F1,F2 are_naturally_equivalent and
A2: F2,F3 are_naturally_equivalent ; ::_thesis: for t being natural_equivalence of F1,F2
for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3
let t be natural_equivalence of F1,F2; ::_thesis: for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3
let t9 be natural_equivalence of F2,F3; ::_thesis: t9 `*` t is natural_equivalence of F1,F3
thus F1,F3 are_naturally_equivalent by A1, A2, Th29; :: according to NATTRA_1:def_14 ::_thesis: t9 `*` t is invertible
let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t9 `*` t) . a is invertible
t9 is invertible by A2, Def14;
then A3: t9 . a is invertible by Def10;
t is invertible by A1, Def14;
then A4: t . a is invertible by Def10;
A5: F1 is_naturally_transformable_to F2 by A1, Def11;
A6: F2 is_naturally_transformable_to F3 by A2, Def11;
(t9 `*` t) . a = (t9 . a) * (t . a) by A5, A6, Th25;
hence (t9 `*` t) . a is invertible by A3, A4, CAT_1:45; ::_thesis: verum
end;
begin
definition
let A, B be Category;
mode NatTrans-DOMAIN of A,B -> non empty set means :Def15: :: NATTRA_1:def 15
for x being set st x in it holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 );
existence
ex b1 being non empty set st
for x being set st x in b1 holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
proof
set F = the Functor of A,B;
take {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} ; ::_thesis: for x being set st x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
let x be set ; ::_thesis: ( x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} implies ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
assume A1: x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} ; ::_thesis: ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
take the Functor of A,B ; ::_thesis: ex F2 being Functor of A,B ex t being natural_transformation of the Functor of A,B,F2 st
( x = [[ the Functor of A,B,F2],t] & the Functor of A,B is_naturally_transformable_to F2 )
take the Functor of A,B ; ::_thesis: ex t being natural_transformation of the Functor of A,B, the Functor of A,B st
( x = [[ the Functor of A,B, the Functor of A,B],t] & the Functor of A,B is_naturally_transformable_to the Functor of A,B )
take id the Functor of A,B ; ::_thesis: ( x = [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] & the Functor of A,B is_naturally_transformable_to the Functor of A,B )
thus ( x = [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] & the Functor of A,B is_naturally_transformable_to the Functor of A,B ) by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines NatTrans-DOMAIN NATTRA_1:def_15_:_
for A, B being Category
for b3 being non empty set holds
( b3 is NatTrans-DOMAIN of A,B iff for x being set st x in b3 holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) );
definition
let A, B be Category;
func NatTrans (A,B) -> NatTrans-DOMAIN of A,B means :Def16: :: NATTRA_1:def 16
for x being set holds
( x in it iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) );
existence
ex b1 being NatTrans-DOMAIN of A,B st
for x being set holds
( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
proof
set F = the Functor of A,B;
defpred S1[ set ] means ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( $1 = [[F1,F2],t] & F1 is_naturally_transformable_to F2 );
consider T being set such that
A1: for x being set holds
( x in T iff ( x in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] & S1[x] ) ) from XBOOLE_0:sch_1();
the Functor of A,B in Funct (A,B) by CAT_2:def_2;
then A2: [ the Functor of A,B, the Functor of A,B] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:87;
id the Functor of A,B in Funcs ( the carrier of A, the carrier' of B) by FUNCT_2:8;
then [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] by A2, ZFMISC_1:87;
then reconsider T = T as non empty set by A1;
for x being set st x in T holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by A1;
then reconsider T = T as NatTrans-DOMAIN of A,B by Def15;
take T ; ::_thesis: for x being set holds
( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
let x be set ; ::_thesis: ( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
thus ( x in T implies ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) by A1; ::_thesis: ( ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) implies x in T )
given F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A3: x = [[F1,F2],t] and
A4: F1 is_naturally_transformable_to F2 ; ::_thesis: x in T
A5: F2 in Funct (A,B) by CAT_2:def_2;
A6: t in Funcs ( the carrier of A, the carrier' of B) by FUNCT_2:8;
F1 in Funct (A,B) by CAT_2:def_2;
then [F1,F2] in [:(Funct (A,B)),(Funct (A,B)):] by A5, ZFMISC_1:87;
then x in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] by A3, A6, ZFMISC_1:87;
hence x in T by A1, A3, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being NatTrans-DOMAIN of A,B st ( for x being set holds
( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds
( x in b2 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) holds
b1 = b2
proof
let S, T be NatTrans-DOMAIN of A,B; ::_thesis: ( ( for x being set holds
( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds
( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) implies S = T )
assume that
A7: for x being set holds
( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) and
A8: for x being set holds
( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ; ::_thesis: S = T
now__::_thesis:_for_x_being_set_holds_
(_x_in_S_iff_x_in_T_)
let x be set ; ::_thesis: ( x in S iff x in T )
( x in S iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) by A7;
hence ( x in S iff x in T ) by A8; ::_thesis: verum
end;
hence S = T by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def16 defines NatTrans NATTRA_1:def_16_:_
for A, B being Category
for b3 being NatTrans-DOMAIN of A,B holds
( b3 = NatTrans (A,B) iff for x being set holds
( x in b3 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) );
theorem Th32: :: NATTRA_1:32
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) )
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) )
let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) )
let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) )
thus ( F1 is_naturally_transformable_to F2 implies [[F1,F2],t1] in NatTrans (A,B) ) by Def16; ::_thesis: ( [[F1,F2],t1] in NatTrans (A,B) implies F1 is_naturally_transformable_to F2 )
assume [[F1,F2],t1] in NatTrans (A,B) ; ::_thesis: F1 is_naturally_transformable_to F2
then consider F19, F29 being Functor of A,B, t being natural_transformation of F19,F29 such that
A1: [[F1,F2],t1] = [[F19,F29],t] and
A2: F19 is_naturally_transformable_to F29 by Def16;
A3: [F1,F2] = [F19,F29] by A1, XTUPLE_0:1;
then F1 = F19 by XTUPLE_0:1;
hence F1 is_naturally_transformable_to F2 by A2, A3, XTUPLE_0:1; ::_thesis: verum
end;
definition
let A, B be Category;
func Functors (A,B) -> strict Category means :Def17: :: NATTRA_1:def 17
( the carrier of it = Funct (A,B) & the carrier' of it = NatTrans (A,B) & ( for f being Morphism of it holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of it st dom g = cod f holds
[g,f] in dom the Comp of it ) & ( for f, g being Morphism of it st [g,f] in dom the Comp of it holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of it . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of it
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) );
existence
ex b1 being strict Category st
( the carrier of b1 = Funct (A,B) & the carrier' of b1 = NatTrans (A,B) & ( for f being Morphism of b1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds
[g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
proof
defpred S1[ set , set , set ] means ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( $2 = [[F,F1],t] & $1 = [[F1,F2],t1] & $3 = [[F,F2],(t1 `*` t)] );
deffunc H1( set ) -> set = ($1 `1) `1 ;
A1: now__::_thesis:_for_x,_y,_z1,_z2_being_set_st_x_in_NatTrans_(A,B)_&_y_in_NatTrans_(A,B)_&_S1[x,y,z1]_&_S1[x,y,z2]_holds_
z1_=_z2
let x, y, z1, z2 be set ; ::_thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume that
x in NatTrans (A,B) and
y in NatTrans (A,B) ; ::_thesis: ( S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume S1[x,y,z1] ; ::_thesis: ( S1[x,y,z2] implies z1 = z2 )
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A2: y = [[F,F1],t] and
A3: x = [[F1,F2],t1] and
A4: z1 = [[F,F2],(t1 `*` t)] ;
assume S1[x,y,z2] ; ::_thesis: z1 = z2
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A5: y = [[F9,F19],t9] and
A6: x = [[F19,F29],t19] and
A7: z2 = [[F9,F29],(t19 `*` t9)] ;
A8: t = t9 by A2, A5, XTUPLE_0:1;
[F1,F2] = [F19,F29] by A3, A6, XTUPLE_0:1;
then A9: F2 = F29 by XTUPLE_0:1;
A10: t1 = t19 by A3, A6, XTUPLE_0:1;
A11: [F,F1] = [F9,F19] by A2, A5, XTUPLE_0:1;
then F = F9 by XTUPLE_0:1;
hence z1 = z2 by A4, A7, A11, A8, A10, A9, XTUPLE_0:1; ::_thesis: verum
end;
A12: now__::_thesis:_for_x,_y,_z_being_set_st_x_in_NatTrans_(A,B)_&_y_in_NatTrans_(A,B)_&_S1[x,y,z]_holds_
z_in_NatTrans_(A,B)
let x, y, z be set ; ::_thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z] implies z in NatTrans (A,B) )
assume that
A13: x in NatTrans (A,B) and
A14: y in NatTrans (A,B) ; ::_thesis: ( S1[x,y,z] implies z in NatTrans (A,B) )
assume S1[x,y,z] ; ::_thesis: z in NatTrans (A,B)
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A15: y = [[F,F1],t] and
A16: x = [[F1,F2],t1] and
A17: z = [[F,F2],(t1 `*` t)] ;
A18: F1 is_naturally_transformable_to F2 by A13, A16, Th32;
F is_naturally_transformable_to F1 by A14, A15, Th32;
hence z in NatTrans (A,B) by A17, Th32, A18, Th23; ::_thesis: verum
end;
consider m being PartFunc of [:(NatTrans (A,B)),(NatTrans (A,B)):],(NatTrans (A,B)) such that
A19: for x, y being set holds
( [x,y] in dom m iff ( x in NatTrans (A,B) & y in NatTrans (A,B) & ex z being set st S1[x,y,z] ) ) and
A20: for x, y being set st [x,y] in dom m holds
S1[x,y,m . (x,y)] from BINOP_1:sch_5(A12, A1);
A21: now__::_thesis:_for_t_being_Element_of_NatTrans_(A,B)_holds_H1(t)_in_Funct_(A,B)
let t be Element of NatTrans (A,B); ::_thesis: H1(t) in Funct (A,B)
consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that
A22: t = [[F1,F2],s] and
F1 is_naturally_transformable_to F2 by Def16;
(t `1) `1 = [F1,F2] `1 by A22, MCART_1:7
.= F1 ;
hence H1(t) in Funct (A,B) by CAT_2:def_2; ::_thesis: verum
end;
consider d being Function of (NatTrans (A,B)),(Funct (A,B)) such that
A23: for t being Element of NatTrans (A,B) holds d . t = H1(t) from FUNCT_2:sch_8(A21);
deffunc H2( set ) -> set = ($1 `1) `2 ;
A24: now__::_thesis:_for_t_being_Element_of_NatTrans_(A,B)_holds_H2(t)_in_Funct_(A,B)
let t be Element of NatTrans (A,B); ::_thesis: H2(t) in Funct (A,B)
consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that
A25: t = [[F1,F2],s] and
F1 is_naturally_transformable_to F2 by Def16;
(t `1) `2 = [F1,F2] `2 by A25, MCART_1:7
.= F2 ;
hence H2(t) in Funct (A,B) by CAT_2:def_2; ::_thesis: verum
end;
consider c being Function of (NatTrans (A,B)),(Funct (A,B)) such that
A26: for t being Element of NatTrans (A,B) holds c . t = H2(t) from FUNCT_2:sch_8(A24);
deffunc H3( Element of Funct (A,B)) -> set = [[$1,$1],(id $1)];
A27: for F being Element of Funct (A,B) holds H3(F) in NatTrans (A,B) by Def16;
consider i being Function of (Funct (A,B)),(NatTrans (A,B)) such that
A28: for F being Element of Funct (A,B) holds i . F = H3(F) from FUNCT_2:sch_8(A27);
set C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #);
A29: now__::_thesis:_for_F,_F1,_F2_being_Functor_of_A,B
for_t_being_natural_transformation_of_F,F1
for_t1_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&_F_is_naturally_transformable_to_F1_holds_
m_._[[[F1,F2],t1],[[F,F1],t]]_=_[[F,F2],(t1_`*`_t)]
let F, F1, F2 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 implies m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] )
assume that
A30: F1 is_naturally_transformable_to F2 and
A31: F is_naturally_transformable_to F1 ; ::_thesis: m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
A32: [[F,F1],t] in NatTrans (A,B) by A31, Th32;
A33: S1[[[F1,F2],t1],[[F,F1],t],[[F,F2],(t1 `*` t)]] ;
[[F1,F2],t1] in NatTrans (A,B) by A30, Th32;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A34: [[F,F1],t] = [[F9,F19],t9] and
A35: [[F1,F2],t1] = [[F19,F29],t19] and
A36: m . ([[F1,F2],t1],[[F,F1],t]) = [[F9,F29],(t19 `*` t9)] by A20, A19, A32, A33;
A37: t = t9 by A34, XTUPLE_0:1;
[F1,F2] = [F19,F29] by A35, XTUPLE_0:1;
then A38: F2 = F29 by XTUPLE_0:1;
A39: t1 = t19 by A35, XTUPLE_0:1;
A40: [F,F1] = [F9,F19] by A34, XTUPLE_0:1;
then F = F9 by XTUPLE_0:1;
hence m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] by A36, A40, A37, A39, A38, XTUPLE_0:1; ::_thesis: verum
end;
A41: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is Category-like
proof
let f, g be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ) )
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A42: f = [[F19,F29],t9] and
A43: F19 is_naturally_transformable_to F29 by Def16;
thus ( [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) implies dom g = cod f ) ::_thesis: ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) )
proof
assume [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ; ::_thesis: dom g = cod f
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A44: f = [[F,F1],t] and
A45: g = [[F1,F2],t1] and
m . (g,f) = [[F,F2],(t1 `*` t)] by A20;
thus dom g = (g `1) `1 by A23
.= [F1,F2] `1 by A45, MCART_1:7
.= [F,F1] `2
.= (f `1) `2 by A44, MCART_1:7
.= cod f by A26 ; ::_thesis: verum
end;
assume A46: dom g = cod f ; ::_thesis: [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A47: g = [[F1,F2],t] and
A48: F1 is_naturally_transformable_to F2 by Def16;
A49: F1 = [F1,F2] `1
.= (g `1) `1 by A47, MCART_1:7
.= c . f by A23, A46
.= (f `1) `2 by A26
.= [F19,F29] `2 by A42, MCART_1:7
.= F29 ;
then reconsider t = t as natural_transformation of F29,F2 ;
m . [g,f] = [[F19,F2],(t `*` t9)] by A29, A47, A48, A42, A43, A49;
hence [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A19, A47, A42, A49; ::_thesis: verum
end;
A50: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is transitive
proof
let f, g be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A51: f = [[F19,F29],t9] and
A52: F19 is_naturally_transformable_to F29 by Def16;
assume dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
then A53: [g,f] in dom m by A41, CAT_1:def_6;
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A54: f = [[F,F1],t] and
A55: g = [[F1,F2],t1] and
A56: m . (g,f) = [[F,F2],(t1 `*` t)] by A20;
A57: m . (g,f) = g (*) f by A53, CAT_1:def_1;
A58: [F,F1] = [F19,F29] by A54, A51, XTUPLE_0:1;
then A59: F = F19 by XTUPLE_0:1;
A60: F1 = F29 by A58, XTUPLE_0:1;
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A61: g = [[F19,F29],t9] and
A62: F19 is_naturally_transformable_to F29 by Def16;
A63: [F1,F2] = [F19,F29] by A55, A61, XTUPLE_0:1;
then A64: F2 = F29 by XTUPLE_0:1;
F1 = F19 by A63, XTUPLE_0:1;
then reconsider x = [[F,F2],(t1 `*` t)] as Element of NatTrans (A,B) by Th32, A52, A59, A60, A62, A64, Th23;
thus dom (g (*) f) = (x `1) `1 by A23, A56, A57
.= [F,F2] `1 by MCART_1:7
.= ([[F,F1],t] `1) `1
.= dom f by A23, A54 ; ::_thesis: cod (g (*) f) = cod g
thus cod (g (*) f) = (x `1) `2 by A26, A56, A57
.= [F,F2] `2 by MCART_1:7
.= ([[F1,F2],t1] `1) `2
.= cod g by A26, A55 ; ::_thesis: verum
end;
A65: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is associative
proof
A66: for f, g being Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) iff dom g = cod f ) by A41, CAT_1:def_6;
let f, g, h be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
reconsider f9 = f, g9 = g, h9 = h as Element of NatTrans (A,B) ;
assume that
A67: dom h = cod g and
A68: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
[g9,f9] in dom m by A41, CAT_1:def_6, A68;
then consider F1, F19, F2 being Functor of A,B, t1 being natural_transformation of F1,F19, t2 being natural_transformation of F19,F2 such that
A69: f9 = [[F1,F19],t1] and
A70: g9 = [[F19,F2],t2] and
A71: m . (g9,f9) = [[F1,F2],(t2 `*` t1)] by A20;
[h9,g9] in dom m by A41, CAT_1:def_6, A67;
then consider F29, F3, F39 being Functor of A,B, t29 being natural_transformation of F29,F3, t3 being natural_transformation of F3,F39 such that
A72: g9 = [[F29,F3],t29] and
A73: h9 = [[F3,F39],t3] and
m . (h9,g9) = [[F29,F39],(t3 `*` t29)] by A20;
A74: [F29,F3] = [F19,F2] by A70, A72, XTUPLE_0:1;
then A75: g9 = [[F19,F3],t2] by A70, XTUPLE_0:1;
reconsider t2 = t2 as natural_transformation of F19,F3 by A74, XTUPLE_0:1;
A76: F2 = F3 by A74, XTUPLE_0:1;
then A77: F19 is_naturally_transformable_to F3 by A70, Th32;
A78: F3 is_naturally_transformable_to F39 by A73, Th32;
then A79: F19 is_naturally_transformable_to F39 by A77, Th23;
A80: F1 is_naturally_transformable_to F19 by A69, Th32;
then A81: F1 is_naturally_transformable_to F3 by A77, Th23;
A82: h (*) g = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g) by A66, A67, CAT_1:def_1;
A83: dom (h (*) g) = dom g by A50, CAT_1:def_7, A67;
A84: g (*) f = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f) by A66, A68, CAT_1:def_1;
cod (g (*) f) = cod g by A50, CAT_1:def_7, A68;
hence h (*) (g (*) f) = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f))) by A84, A66, A67, CAT_1:def_1
.= [[F1,F39],(t3 `*` (t2 `*` t1))] by A29, A71, A73, A76, A78, A81
.= [[F1,F39],((t3 `*` t2) `*` t1)] by A80, A77, A78, Th26
.= m . [[[F19,F39],(t3 `*` t2)],f9] by A29, A69, A80, A79
.= the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g)),f) by A29, A73, A75, A77, A78
.= (h (*) g) (*) f by A83, A82, A66, A68, CAT_1:def_1 ;
::_thesis: verum
end;
A85: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is reflexive
proof
let b be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {}
reconsider F = b as Functor of A,B by CAT_2:def_2;
reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16;
reconsider s = s as Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ;
A86: dom s = ([[F,F],(id F)] `1) `1 by A23
.= F ;
cod s = ([[F,F],(id F)] `1) `2 by A26
.= F ;
then s in Hom (b,b) by A86;
hence Hom (b,b) <> {} ; ::_thesis: verum
end;
A87: for a being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
for F being Functor of A,B st a = F holds
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
proof
let a be Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); ::_thesis: for F being Functor of A,B st a = F holds
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let F be Functor of A,B; ::_thesis: ( a = F implies for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) )
assume A88: a = F ; ::_thesis: for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let ii be Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); ::_thesis: ( ii = [[F,F],(id F)] implies for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) )
assume A89: ii = [[F,F],(id F)] ; ::_thesis: for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
let b be Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); ::_thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16;
A90: F in Funct (A,B) by CAT_2:def_2;
then A91: i . F = [[F,F],(id F)] by A28;
thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )
proof
assume A92: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds f (*) ii = f
let f be Morphism of a,b; ::_thesis: f (*) ii = f
reconsider f9 = f as Element of NatTrans (A,B) ;
A93: dom f = a by A92, CAT_1:5;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A94: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A95: F1 = [F1,F2] `1
.= (f9 `1) `1 by A94, MCART_1:7
.= dom f by A23
.= F by A92, CAT_1:5, A88 ;
then reconsider t = t as natural_transformation of F,F2 ;
S1[f9,s,[[F,F2],(t `*` (id F))]] by A94, A95;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A96: i . F = [[F9,F19],t9] and
A97: f9 = [[F19,F29],t19] and
A98: m . (f9,(i . F)) = [[F9,F29],(t19 `*` t9)] by A20, A91, A19;
A99: [F9,F19] = [F,F] by A96, A91, XTUPLE_0:1;
then A100: F9 = F by XTUPLE_0:1;
A101: F19 = F by A99, XTUPLE_0:1;
A102: F19 is_naturally_transformable_to F29 by A97, Th32;
A103: F29 = ([[F19,F29],t19] `1) `2
.= ([[F1,F2],t] `1) `2 by A97, A94
.= F2 ;
A104: t19 = [[F19,F29],t19] `2
.= [[F1,F2],t] `2 by A97, A94
.= t ;
A105: t19 `*` (id F19) = t19 by Th24, A102;
cod ii = ([[F,F],(id F)] `1) `2 by A89, A26
.= a by A88 ;
then [f,ii] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A41, CAT_1:def_6, A93;
hence f (*) ii = m . (f,ii) by CAT_1:def_1
.= f by A104, A105, A95, A103, XTUPLE_0:1, A96, A91, A100, A101, A98, A89, A94 ;
::_thesis: verum
end;
assume A106: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f
let f be Morphism of b,a; ::_thesis: ii (*) f = f
reconsider f9 = f as Element of NatTrans (A,B) ;
A107: cod f = a by A106, CAT_1:5;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A108: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A109: F2 = [F1,F2] `2
.= (f9 `1) `2 by A108, MCART_1:7
.= cod f by A26
.= F by A106, CAT_1:5, A88 ;
then reconsider t = t as natural_transformation of F1,F ;
S1[s,f9,[[F1,F],((id F) `*` t)]] by A108, A109;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A110: f9 = [[F9,F19],t9] and
A111: i . F = [[F19,F29],t19] and
A112: m . ((i . F),f9) = [[F9,F29],(t19 `*` t9)] by A20, A91, A19;
A113: t19 = id F by A111, XTUPLE_0:1, A91;
A114: [F19,F29] = [F,F] by A111, A91, XTUPLE_0:1;
then A115: F19 = F by XTUPLE_0:1;
A116: F9 is_naturally_transformable_to F19 by A110, Th32;
A117: F9 = ([[F9,F19],t9] `1) `1
.= ([[F1,F2],t] `1) `1 by A110, A108
.= F1 ;
A118: t9 = [[F9,F19],t9] `2
.= [[F1,F2],t] `2 by A110, A108
.= t ;
A119: (id F19) `*` t9 = t9 by Th24, A116;
dom ii = ([[F,F],(id F)] `1) `1 by A89, A23
.= a by A88 ;
then [ii,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A41, CAT_1:def_6, A107;
hence ii (*) f = m . (ii,f) by CAT_1:def_1
.= m . ((i . F),f9) by A89, A90, A28
.= [[F9,F29],((id F19) `*` t9)] by A113, A115, A114, XTUPLE_0:1, A112
.= f by A108, A118, A119, A114, A109, A117, XTUPLE_0:1 ;
::_thesis: verum
end;
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is with_identities
proof
let a be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider F = a as Functor of A,B by CAT_2:def_2;
reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16;
reconsider s = s as Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ;
A120: dom s = ([[F,F],(id F)] `1) `1 by A23
.= F ;
cod s = ([[F,F],(id F)] `1) `2 by A26
.= F ;
then s in Hom (a,a) by A120;
then reconsider s = s as Morphism of a,a by CAT_1:def_5;
take s ; ::_thesis: for b1 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) s = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds s (*) b2 = b2 ) )
thus for b1 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) s = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds s (*) b2 = b2 ) ) by A87; ::_thesis: verum
end;
then reconsider C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) as strict Category by A41, A50, A65, A85;
take C ; ::_thesis: ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) & ( for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) ) ; ::_thesis: ( ( for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) by A23, A26; ::_thesis: ( ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ::_thesis: ( ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
proof
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of C )
assume A121: dom g = cod f ; ::_thesis: [g,f] in dom the Comp of C
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A122: g = [[F19,F29],t9] and
F19 is_naturally_transformable_to F29 by Def16;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A123: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A124: F2 = ([[F1,F2],t] `1) `2
.= cod f by A26, A123
.= ([[F19,F29],t9] `1) `1 by A23, A122, A121
.= F19 ;
then reconsider t9 = t9 as natural_transformation of F2,F29 ;
S1[g,f,[[F1,F29],(t9 `*` t)]] by A123, A122, A124;
hence [g,f] in dom the Comp of C by A19; ::_thesis: verum
end;
thus for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ::_thesis: for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
proof
let f, g be Morphism of C; ::_thesis: ( [g,f] in dom the Comp of C implies ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) )
assume [g,f] in dom the Comp of C ; ::_thesis: ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] )
then ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . (g,f) = [[F,F2],(t1 `*` t)] ) by A20;
hence ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ; ::_thesis: verum
end;
let a be Object of C; ::_thesis: for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
let F be Functor of A,B; ::_thesis: ( F = a implies id a = [[F,F],(id F)] )
assume A125: a = F ; ::_thesis: id a = [[F,F],(id F)]
reconsider m = [[F,F],(id F)] as Element of NatTrans (A,B) by Def16;
reconsider m = m as Morphism of C ;
A126: dom m = ([[F,F],(id F)] `1) `1 by A23
.= F ;
cod m = ([[F,F],(id F)] `1) `2 by A26
.= F ;
then m in Hom (a,a) by A125, A126;
then reconsider m = m as Morphism of a,a by CAT_1:def_5;
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) by A125, A87;
hence id a = [[F,F],(id F)] by CAT_1:def_12; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Category st the carrier of b1 = Funct (A,B) & the carrier' of b1 = NatTrans (A,B) & ( for f being Morphism of b1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds
[g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) & the carrier of b2 = Funct (A,B) & the carrier' of b2 = NatTrans (A,B) & ( for f being Morphism of b2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b2 st dom g = cod f holds
[g,f] in dom the Comp of b2 ) & ( for f, g being Morphism of b2 st [g,f] in dom the Comp of b2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) holds
b1 = b2
proof
let C1, C2 be strict Category; ::_thesis: ( the carrier of C1 = Funct (A,B) & the carrier' of C1 = NatTrans (A,B) & ( for f being Morphism of C1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1 ) & ( for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) & the carrier of C2 = Funct (A,B) & the carrier' of C2 = NatTrans (A,B) & ( for f being Morphism of C2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2 ) & ( for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) implies C1 = C2 )
assume that
A127: the carrier of C1 = Funct (A,B) and
A128: the carrier' of C1 = NatTrans (A,B) and
A129: for f being Morphism of C1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) and
A130: for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1 and
A131: for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) and
for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] and
A132: the carrier of C2 = Funct (A,B) and
A133: the carrier' of C2 = NatTrans (A,B) and
A134: for f being Morphism of C2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) and
A135: for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2 and
A136: for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] ) and
for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ; ::_thesis: C1 = C2
A137: the Target of C1 = the Target of C2
proof
thus the carrier' of C1 = the carrier' of C2 by A128, A133; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier' of C1 holds the Target of C1 . b1 = the Target of C2 . b1
let a be Morphism of C1; ::_thesis: the Target of C1 . a = the Target of C2 . a
reconsider b = a as Morphism of C2 by A128, A133;
thus the Target of C1 . a = cod a
.= (a `1) `2 by A129
.= cod b by A134
.= the Target of C2 . a ; ::_thesis: verum
end;
A138: now__::_thesis:_(_dom_the_Comp_of_C1_=_dom_the_Comp_of_C2_&_(_for_x_being_set_st_x_in_dom_the_Comp_of_C1_holds_
the_Comp_of_C1_._x_=_the_Comp_of_C2_._x_)_)
reconsider S1 = dom the Comp of C1, S2 = dom the Comp of C2 as Subset of [: the carrier' of C1, the carrier' of C1:] by A128, A133, RELAT_1:def_18;
A139: now__::_thesis:_for_x_being_Element_of_[:_the_carrier'_of_C1,_the_carrier'_of_C1:]_holds_
(_x_in_S1_iff_x_in_S2_)
let x be Element of [: the carrier' of C1, the carrier' of C1:]; ::_thesis: ( x in S1 iff x in S2 )
A140: x = [(x `1),(x `2)] by MCART_1:21;
then reconsider f1 = x `2 , g1 = x `1 as Morphism of C1 by ZFMISC_1:87;
reconsider f2 = x `2 , g2 = x `1 as Morphism of C2 by A128, A133, A140, ZFMISC_1:87;
A141: now__::_thesis:_(_[g2,f2]_in_S2_implies_[g1,f1]_in_S1_)
assume [g2,f2] in S2 ; ::_thesis: [g1,f1] in S1
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A142: f2 = [[F,F1],t] and
A143: g2 = [[F1,F2],t1] and
the Comp of C2 . [g2,f2] = [[F,F2],(t1 `*` t)] by A136;
dom g1 = (g1 `1) `1 by A129
.= [F1,F2] `1 by A143, MCART_1:7
.= [F,F1] `2
.= (f2 `1) `2 by A142, MCART_1:7
.= cod f1 by A129 ;
hence [g1,f1] in S1 by A130; ::_thesis: verum
end;
now__::_thesis:_(_[g1,f1]_in_S1_implies_[g2,f2]_in_S2_)
assume [g1,f1] in S1 ; ::_thesis: [g2,f2] in S2
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A144: f1 = [[F,F1],t] and
A145: g1 = [[F1,F2],t1] and
the Comp of C1 . [g1,f1] = [[F,F2],(t1 `*` t)] by A131;
dom g2 = (g2 `1) `1 by A134
.= [F1,F2] `1 by A145, MCART_1:7
.= [F,F1] `2
.= (f1 `1) `2 by A144, MCART_1:7
.= cod f2 by A134 ;
hence [g2,f2] in S2 by A135; ::_thesis: verum
end;
hence ( x in S1 iff x in S2 ) by A141, MCART_1:21; ::_thesis: verum
end;
hence dom the Comp of C1 = dom the Comp of C2 by SUBSET_1:3; ::_thesis: for x being set st x in dom the Comp of C1 holds
the Comp of C1 . x = the Comp of C2 . x
let x be set ; ::_thesis: ( x in dom the Comp of C1 implies the Comp of C1 . x = the Comp of C2 . x )
assume A146: x in dom the Comp of C1 ; ::_thesis: the Comp of C1 . x = the Comp of C2 . x
dom the Comp of C1 c= [: the carrier' of C1, the carrier' of C1:] by RELAT_1:def_18;
then reconsider f = x `2 , g = x `1 as Morphism of C1 by A146, MCART_1:10;
A147: [g,f] = x by A146, MCART_1:21;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A148: f = [[F9,F19],t9] and
A149: g = [[F19,F29],t19] and
A150: the Comp of C2 . [g,f] = [[F9,F29],(t19 `*` t9)] by A128, A133, A136, A139, A146;
consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A151: f = [[F,F1],t] and
A152: g = [[F1,F2],t1] and
A153: the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] by A131, A146, A147;
A154: [F,F1] = [F9,F19] by A151, A148, XTUPLE_0:1;
then A155: F = F9 by XTUPLE_0:1;
[F1,F2] = [F19,F29] by A152, A149, XTUPLE_0:1;
then A156: F2 = F29 by XTUPLE_0:1;
A157: F1 = F19 by A154, XTUPLE_0:1;
t = t9 by A151, A148, XTUPLE_0:1;
hence the Comp of C1 . x = the Comp of C2 . x by A147, A152, A153, A149, A150, A155, A157, A156, XTUPLE_0:1; ::_thesis: verum
end;
the Source of C1 = the Source of C2
proof
thus the carrier' of C1 = the carrier' of C2 by A128, A133; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier' of C1 holds the Source of C1 . b1 = the Source of C2 . b1
let a be Morphism of C1; ::_thesis: the Source of C1 . a = the Source of C2 . a
reconsider b = a as Morphism of C2 by A128, A133;
thus the Source of C1 . a = dom a
.= (a `1) `1 by A129
.= dom b by A134
.= the Source of C2 . a ; ::_thesis: verum
end;
hence C1 = C2 by A127, A128, A132, A133, A137, A138, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines Functors NATTRA_1:def_17_:_
for A, B being Category
for b3 being strict Category holds
( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) & the carrier' of b3 = NatTrans (A,B) & ( for f being Morphism of b3 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b3 st dom g = cod f holds
[g,f] in dom the Comp of b3 ) & ( for f, g being Morphism of b3 st [g,f] in dom the Comp of b3 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b3 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b3
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) ) );
theorem Th33: :: NATTRA_1:33
for A, B being Category
for F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
proof
let A, B be Category; ::_thesis: for F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
let F, F1 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1
for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
let t be natural_transformation of F,F1; ::_thesis: for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
let f be Morphism of (Functors (A,B)); ::_thesis: ( f = [[F,F1],t] implies ( dom f = F & cod f = F1 ) )
assume A1: f = [[F,F1],t] ; ::_thesis: ( dom f = F & cod f = F1 )
thus dom f = (f `1) `1 by Def17
.= [F,F1] `1 by A1, MCART_1:7
.= F ; ::_thesis: cod f = F1
thus cod f = (f `1) `2 by Def17
.= [F,F1] `2 by A1, MCART_1:7
.= F1 ; ::_thesis: verum
end;
theorem :: NATTRA_1:34
for A, B being Category
for a, b being Object of (Functors (A,B))
for f being Morphism of a,b st Hom (a,b) <> {} holds
ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
proof
let A, B be Category; ::_thesis: for a, b being Object of (Functors (A,B))
for f being Morphism of a,b st Hom (a,b) <> {} holds
ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
let a, b be Object of (Functors (A,B)); ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] ) )
assume A1: Hom (a,b) <> {} ; ::_thesis: ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
the carrier' of (Functors (A,B)) = NatTrans (A,B) by Def17;
then consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A2: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
take F1 ; ::_thesis: ex F1 being Functor of A,B ex t being natural_transformation of F1,F1 st
( a = F1 & b = F1 & f = [[F1,F1],t] )
take F2 ; ::_thesis: ex t being natural_transformation of F1,F2 st
( a = F1 & b = F2 & f = [[F1,F2],t] )
take t ; ::_thesis: ( a = F1 & b = F2 & f = [[F1,F2],t] )
thus a = dom f by A1, CAT_1:5
.= F1 by A2, Th33 ; ::_thesis: ( b = F2 & f = [[F1,F2],t] )
thus b = cod f by A1, CAT_1:5
.= F2 by A2, Th33 ; ::_thesis: f = [[F1,F2],t]
thus f = [[F1,F2],t] by A2; ::_thesis: verum
end;
theorem Th35: :: NATTRA_1:35
for A, B being Category
for F2, F3, F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
proof
let A, B be Category; ::_thesis: for F2, F3, F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let F2, F3, F, F1 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let t be natural_transformation of F,F1; ::_thesis: for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let t9 be natural_transformation of F2,F3; ::_thesis: for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let f, g be Morphism of (Functors (A,B)); ::_thesis: ( f = [[F,F1],t] & g = [[F2,F3],t9] implies ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) )
assume that
A1: f = [[F,F1],t] and
A2: g = [[F2,F3],t9] ; ::_thesis: ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
thus ( [g,f] in dom the Comp of (Functors (A,B)) implies F1 = F2 ) ::_thesis: ( F1 = F2 implies [g,f] in dom the Comp of (Functors (A,B)) )
proof
assume [g,f] in dom the Comp of (Functors (A,B)) ; ::_thesis: F1 = F2
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A3: f = [[F9,F19],t9] and
A4: g = [[F19,F29],t19] and
the Comp of (Functors (A,B)) . [g,f] = [[F9,F29],(t19 `*` t9)] by Def17;
thus F1 = ([[F,F1],t] `1) `2
.= [F9,F19] `2 by A1, A3, MCART_1:7
.= ([[F19,F29],t19] `1) `1
.= [F2,F3] `1 by A2, A4, MCART_1:7
.= F2 ; ::_thesis: verum
end;
A5: cod f = F1 by A1, Th33;
dom g = F2 by A2, Th33;
hence ( F1 = F2 implies [g,f] in dom the Comp of (Functors (A,B)) ) by A5, Def17; ::_thesis: verum
end;
theorem :: NATTRA_1:36
for A, B being Category
for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
proof
let A, B be Category; ::_thesis: for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let F, F1, F2 be Functor of A,B; ::_thesis: for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let t1 be natural_transformation of F1,F2; ::_thesis: for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let f, g be Morphism of (Functors (A,B)); ::_thesis: ( f = [[F,F1],t] & g = [[F1,F2],t1] implies g (*) f = [[F,F2],(t1 `*` t)] )
assume that
A1: f = [[F,F1],t] and
A2: g = [[F1,F2],t1] ; ::_thesis: g (*) f = [[F,F2],(t1 `*` t)]
A3: [g,f] in dom the Comp of (Functors (A,B)) by A1, A2, Th35;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A4: f = [[F9,F19],t9] and
A5: g = [[F19,F29],t19] and
A6: the Comp of (Functors (A,B)) . (g,f) = [[F9,F29],(t19 `*` t9)] by Def17;
A7: t1 = t19 by A2, A5, XTUPLE_0:1;
A8: [F9,F19] = [F,F1] by A1, A4, XTUPLE_0:1;
then A9: F = F9 by XTUPLE_0:1;
[F19,F29] = [F1,F2] by A2, A5, XTUPLE_0:1;
then A10: F2 = F29 by XTUPLE_0:1;
A11: F1 = F19 by A8, XTUPLE_0:1;
t = t9 by A1, A4, XTUPLE_0:1;
hence g (*) f = [[F,F2],(t1 `*` t)] by A3, A6, A7, A9, A11, A10, CAT_1:def_1; ::_thesis: verum
end;
begin
definition
let C be Category;
attrC is discrete means :Def18: :: NATTRA_1:def 18
for f being Morphism of C ex a being Object of C st f = id a;
end;
:: deftheorem Def18 defines discrete NATTRA_1:def_18_:_
for C being Category holds
( C is discrete iff for f being Morphism of C ex a being Object of C st f = id a );
registration
cluster non empty non void V55() Category-like transitive associative reflexive with_identities discrete for CatStr ;
existence
ex b1 being Category st b1 is discrete
proof
set o = the set ;
take 1Cat ( the set , the set ) ; ::_thesis: 1Cat ( the set , the set ) is discrete
let f be Morphism of (1Cat ( the set , the set )); :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of (1Cat ( the set , the set )) st f = id a
set a = the Object of (1Cat ( the set , the set ));
take the Object of (1Cat ( the set , the set )) ; ::_thesis: f = id the Object of (1Cat ( the set , the set ))
thus f = the set by TARSKI:def_1
.= id the Object of (1Cat ( the set , the set )) by TARSKI:def_1 ; ::_thesis: verum
end;
end;
theorem Th37: :: NATTRA_1:37
for A being discrete Category
for a being Object of A holds Hom (a,a) = {(id a)}
proof
let A be discrete Category; ::_thesis: for a being Object of A holds Hom (a,a) = {(id a)}
let a be Object of A; ::_thesis: Hom (a,a) = {(id a)}
A1: Hom (a,a) <> {} ;
now__::_thesis:_for_g_being_Morphism_of_a,a_holds_id_a_=_g
let g be Morphism of a,a; ::_thesis: id a = g
consider a2 being Object of A such that
A2: g = id a2 by Def18;
a = dom g by A1, CAT_1:5
.= a2 by A2, CAT_1:58 ;
hence id a = g by A2; ::_thesis: verum
end;
hence Hom (a,a) = {(id a)} by CAT_1:8; ::_thesis: verum
end;
theorem Th38: :: NATTRA_1:38
for A being Category holds
( A is discrete iff ( ( for a being Object of A ex B being finite set st
( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom (a,b) = {} ) ) )
proof
let A be Category; ::_thesis: ( A is discrete iff ( ( for a being Object of A ex B being finite set st
( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom (a,b) = {} ) ) )
thus ( A is discrete implies ( ( for a being Object of A ex B being finite set st
( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom (a,b) = {} ) ) ) ::_thesis: ( ( for a being Object of A ex B being finite set st
( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom (a,b) = {} ) implies A is discrete )
proof
assume A1: A is discrete ; ::_thesis: ( ( for a being Object of A ex B being finite set st
( B = Hom (a,a) & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom (a,b) = {} ) )
hereby ::_thesis: for a, b being Object of A st a <> b holds
Hom (a,b) = {}
let a be Object of A; ::_thesis: ex B being finite set st
( B = Hom (a,a) & card B = 1 )
A2: Hom (a,a) = {(id a)} by A1, Th37;
then reconsider B = Hom (a,a) as finite set ;
take B = B; ::_thesis: ( B = Hom (a,a) & card B = 1 )
thus B = Hom (a,a) ; ::_thesis: card B = 1
thus card B = 1 by A2, CARD_1:30; ::_thesis: verum
end;
let a, b be Object of A; ::_thesis: ( a <> b implies Hom (a,b) = {} )
assume A3: a <> b ; ::_thesis: Hom (a,b) = {}
set m = the Element of Hom (a,b);
assume A4: Hom (a,b) <> {} ; ::_thesis: contradiction
then reconsider m = the Element of Hom (a,b) as Morphism of A by TARSKI:def_3;
consider c being Object of A such that
A5: m = id c by A1, Def18;
id c in Hom (c,c) by CAT_1:27;
then A6: Hom (c,c) meets Hom (a,b) by A4, A5, XBOOLE_0:3;
then c = a by Th17;
hence contradiction by A3, A6, Th17; ::_thesis: verum
end;
assume that
A7: for a being Object of A ex B being finite set st
( B = Hom (a,a) & card B = 1 ) and
A8: for a, b being Object of A st a <> b holds
Hom (a,b) = {} ; ::_thesis: A is discrete
let f be Morphism of A; :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of A st f = id a
ex B being finite set st
( B = Hom ((dom f),(dom f)) & card B = 1 ) by A7;
then consider x being set such that
A9: Hom ((dom f),(dom f)) = {x} by CARD_2:42;
take dom f ; ::_thesis: f = id (dom f)
A10: id (dom f) in Hom ((dom f),(dom f)) by CAT_1:27;
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then dom f = cod f by A8;
then f in Hom ((dom f),(dom f)) ;
then f = x by A9, TARSKI:def_1;
hence f = id (dom f) by A9, A10, TARSKI:def_1; ::_thesis: verum
end;
theorem Th39: :: NATTRA_1:39
for o, m being set holds 1Cat (o,m) is discrete
proof
let o, m be set ; ::_thesis: 1Cat (o,m) is discrete
let f be Morphism of (1Cat (o,m)); :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of (1Cat (o,m)) st f = id a
set a = the Object of (1Cat (o,m));
f = m by TARSKI:def_1
.= id the Object of (1Cat (o,m)) by TARSKI:def_1 ;
hence ex a being Object of (1Cat (o,m)) st f = id a ; ::_thesis: verum
end;
theorem :: NATTRA_1:40
for A being discrete Category
for C being Subcategory of A holds C is discrete
proof
let A be discrete Category; ::_thesis: for C being Subcategory of A holds C is discrete
let C be Subcategory of A; ::_thesis: C is discrete
let f be Morphism of C; :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of C st f = id a
reconsider f9 = f as Morphism of A by CAT_2:8;
take dom f ; ::_thesis: f = id (dom f)
consider a9 being Object of A such that
A1: f9 = id a9 by Def18;
dom f9 = a9 by A1, CAT_1:58;
then dom f = a9 by CAT_2:9;
hence f = id (dom f) by A1, CAT_2:def_4; ::_thesis: verum
end;
theorem :: NATTRA_1:41
for A, B being Category st A is discrete & B is discrete holds
[:A,B:] is discrete
proof
let A, B be Category; ::_thesis: ( A is discrete & B is discrete implies [:A,B:] is discrete )
assume that
A1: A is discrete and
A2: B is discrete ; ::_thesis: [:A,B:] is discrete
let f be Morphism of [:A,B:]; :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of [:A,B:] st f = id a
consider f1 being Morphism of A, f2 being Morphism of B such that
A3: f = [f1,f2] by DOMAIN_1:1;
consider b being Object of B such that
A4: f2 = id b by A2, Def18;
consider a being Object of A such that
A5: f1 = id a by A1, Def18;
take [a,b] ; ::_thesis: f = id [a,b]
thus f = id [a,b] by A3, A5, A4, CAT_2:31; ::_thesis: verum
end;
theorem Th42: :: NATTRA_1:42
for A being discrete Category
for B being Category
for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
proof
let A be discrete Category; ::_thesis: for B being Category
for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
let B be Category; ::_thesis: for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
let F1, F2 be Functor of B,A; ::_thesis: ( F1 is_transformable_to F2 implies F1 = F2 )
assume A1: F1 is_transformable_to F2 ; ::_thesis: F1 = F2
now__::_thesis:_for_m_being_Morphism_of_B_holds_F1_._m_=_F2_._m
let m be Morphism of B; ::_thesis: F1 . m = F2 . m
Hom ((F1 . (dom m)),(F2 . (dom m))) <> {} by A1, Def2;
then A2: F1 . (dom m) = F2 . (dom m) by Th38;
A3: m in Hom ((dom m),(cod m)) ;
then Hom ((F1 . (dom m)),(F1 . (cod m))) <> {} by CAT_1:81;
then F1 . (dom m) = F1 . (cod m) by Th38;
then A4: Hom ((F1 . (dom m)),(F1 . (cod m))) = {(id (F1 . (dom m)))} by Th37;
Hom ((F2 . (dom m)),(F2 . (cod m))) <> {} by A3, CAT_1:81;
then F2 . (dom m) = F2 . (cod m) by Th38;
then A5: Hom ((F2 . (dom m)),(F2 . (cod m))) = {(id (F2 . (dom m)))} by Th37;
F1 . m in Hom ((F1 . (dom m)),(F1 . (cod m))) by A3, CAT_1:81;
then A6: F1 . m = id (F1 . (dom m)) by A4, TARSKI:def_1;
F2 . m in Hom ((F2 . (dom m)),(F2 . (cod m))) by A3, CAT_1:81;
hence F1 . m = F2 . m by A2, A6, A5, TARSKI:def_1; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th43: :: NATTRA_1:43
for A being discrete Category
for B being Category
for F being Functor of B,A
for t being transformation of F,F holds t = id F
proof
let A be discrete Category; ::_thesis: for B being Category
for F being Functor of B,A
for t being transformation of F,F holds t = id F
let B be Category; ::_thesis: for F being Functor of B,A
for t being transformation of F,F holds t = id F
let F be Functor of B,A; ::_thesis: for t being transformation of F,F holds t = id F
let t be transformation of F,F; ::_thesis: t = id F
now__::_thesis:_for_a_being_Object_of_B_holds_t_._a_=_(id_F)_._a
let a be Object of B; ::_thesis: t . a = (id F) . a
A1: Hom ((F . a),(F . a)) = {(id (F . a))} by Th37;
t . a in Hom ((F . a),(F . a)) by CAT_1:def_5;
hence t . a = id (F . a) by A1, TARSKI:def_1
.= (id F) . a by Th20 ;
::_thesis: verum
end;
hence t = id F by Th19; ::_thesis: verum
end;
theorem :: NATTRA_1:44
for A, B being Category st A is discrete holds
Functors (B,A) is discrete
proof
let A, B be Category; ::_thesis: ( A is discrete implies Functors (B,A) is discrete )
assume A1: A is discrete ; ::_thesis: Functors (B,A) is discrete
let f be Morphism of (Functors (B,A)); :: according to NATTRA_1:def_18 ::_thesis: ex a being Object of (Functors (B,A)) st f = id a
f in the carrier' of (Functors (B,A)) ;
then f in NatTrans (B,A) by Def17;
then consider F1, F2 being Functor of B,A, t being natural_transformation of F1,F2 such that
A2: f = [[F1,F2],t] and
A3: F1 is_naturally_transformable_to F2 by Def16;
F1 in Funct (B,A) by CAT_2:def_2;
then reconsider a = F1 as Object of (Functors (B,A)) by Def17;
take a ; ::_thesis: f = id a
A4: F1 = F2 by A1, Th42, A3, Def7;
then t = id F1 by A1, Th43;
hence f = id a by A2, A4, Def17; ::_thesis: verum
end;
registration
let C be Category;
cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities discrete for Subcategory of C;
existence
ex b1 being Subcategory of C st
( b1 is strict & b1 is discrete )
proof
set c = the Object of C;
reconsider A = 1Cat ( the Object of C,(id the Object of C)) as Subcategory of C by Th7;
take A ; ::_thesis: ( A is strict & A is discrete )
thus ( A is strict & A is discrete ) by Th39; ::_thesis: verum
end;
end;
definition
let C be Category;
func IdCat C -> strict discrete Subcategory of C means :Def19: :: NATTRA_1:def 19
( the carrier of it = the carrier of C & the carrier' of it = { (id a) where a is Object of C : verum } );
existence
ex b1 being strict discrete Subcategory of C st
( the carrier of b1 = the carrier of C & the carrier' of b1 = { (id a) where a is Object of C : verum } )
proof
defpred S1[ Object of C] means verum;
deffunc H1( Object of C) -> Morphism of $1,$1 = id $1;
defpred S2[ Object of C] means H1($1) in the carrier' of C;
set M = { H1(a) where a is Object of C : S1[a] } ;
set N = { H1(a) where a is Object of C : S2[a] } ;
set N9 = { H1(a) where a is Object of C : ( H1(a) in the carrier' of C & S1[a] ) } ;
defpred S3[ Object of C] means ( H1($1) in the carrier' of C & S1[$1] );
set N99 = { H1(a) where a is Object of C : S3[a] } ;
set a = the Object of C;
A1: id the Object of C in { H1(a) where a is Object of C : S1[a] } ;
A2: for a being Object of C holds
( S2[a] iff S1[a] ) ;
A3: { H1(a) where a is Object of C : S2[a] } = { H1(a) where a is Object of C : S1[a] } from FRAENKEL:sch_3(A2);
A4: for a being Object of C holds
( S2[a] iff S3[a] ) ;
A5: { H1(a) where a is Object of C : S2[a] } = { H1(a) where a is Object of C : S3[a] } from FRAENKEL:sch_3(A4);
{ H1(a) where a is Object of C : ( H1(a) in the carrier' of C & S1[a] ) } c= the carrier' of C from FRAENKEL:sch_17();
then reconsider M = { H1(a) where a is Object of C : S1[a] } as non empty Subset of the carrier' of C by A3, A5, A1;
A6: rng ( the Comp of C || M) c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the Comp of C || M) or x in M )
assume x in rng ( the Comp of C || M) ; ::_thesis: x in M
then consider y being set such that
A7: y in dom ( the Comp of C || M) and
A8: x = ( the Comp of C || M) . y by FUNCT_1:def_3;
A9: y in (dom the Comp of C) /\ [:M,M:] by A7, RELAT_1:61;
then A10: y in dom the Comp of C by XBOOLE_0:def_4;
y in [:M,M:] by A9, XBOOLE_0:def_4;
then consider y1, y2 being set such that
A11: y1 in M and
A12: y2 in M and
A13: y = [y1,y2] by ZFMISC_1:84;
consider a1 being Object of C such that
A14: y1 = id a1 by A11;
A15: Hom (a1,a1) <> {} ;
consider a2 being Object of C such that
A16: y2 = id a2 by A12;
A17: a1 = dom (id a1)
.= cod (id a2) by A13, A14, A16, A10, CAT_1:15
.= a2 ;
id a1 = (id a1) * (id a1)
.= (id a1) (*) (id a2) by A15, A17, CAT_1:def_13
.= the Comp of C . ((id a1),(id a2)) by A13, A14, A16, A10, CAT_1:def_1
.= x by A8, A9, A13, A14, A16, FUNCT_1:48 ;
hence x in M ; ::_thesis: verum
end;
the Comp of C || M is PartFunc of [:M,M:], the carrier' of C by PARTFUN1:10;
then reconsider COMP = the Comp of C || M as PartFunc of [:M,M:],M by A6, RELSET_1:6;
A18: the carrier of C c= the carrier of C ;
for o being Element of C st o in the carrier of C holds
id o in M ;
then reconsider A = CatStr(# the carrier of C,M,( the Source of C | M),( the Target of C | M),COMP #) as Subcategory of C by Th9, A18;
now__::_thesis:_for_f_being_Morphism_of_A_ex_a_being_Element_of_A_st_f_=_id_a
let f be Morphism of A; ::_thesis: ex a being Element of A st f = id a
f in M ;
then consider a being Object of C such that
A19: f = id a ;
reconsider a = a as Element of A ;
take a = a; ::_thesis: f = id a
thus f = id a by A19, CAT_2:def_4; ::_thesis: verum
end;
then reconsider A = A as strict discrete Subcategory of C by Def18;
take A ; ::_thesis: ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } )
thus ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict discrete Subcategory of C st the carrier of b1 = the carrier of C & the carrier' of b1 = { (id a) where a is Object of C : verum } & the carrier of b2 = the carrier of C & the carrier' of b2 = { (id a) where a is Object of C : verum } holds
b1 = b2
proof
let It1, It2 be strict discrete Subcategory of C; ::_thesis: ( the carrier of It1 = the carrier of C & the carrier' of It1 = { (id a) where a is Object of C : verum } & the carrier of It2 = the carrier of C & the carrier' of It2 = { (id a) where a is Object of C : verum } implies It1 = It2 )
assume that
A20: the carrier of It1 = the carrier of C and
A21: the carrier' of It1 = { (id a) where a is Object of C : verum } and
A22: the carrier of It2 = the carrier of C and
A23: the carrier' of It2 = { (id a) where a is Object of C : verum } ; ::_thesis: It1 = It2
set M = the carrier' of It1;
A24: the Target of It2 = the Target of C | the carrier' of It1 by A21, A23, Th8;
A25: the Comp of It2 = the Comp of C || the carrier' of It1 by A21, A23, Th8;
A26: the Source of It1 = the Source of C | the carrier' of It1 by Th8;
A27: the Comp of It1 = the Comp of C || the carrier' of It1 by Th8;
the Target of It1 = the Target of C | the carrier' of It1 by Th8;
hence It1 = It2 by A20, A21, A22, A23, A26, A24, A27, A25, Th8; ::_thesis: verum
end;
end;
:: deftheorem Def19 defines IdCat NATTRA_1:def_19_:_
for C being Category
for b2 being strict discrete Subcategory of C holds
( b2 = IdCat C iff ( the carrier of b2 = the carrier of C & the carrier' of b2 = { (id a) where a is Object of C : verum } ) );
theorem Th45: :: NATTRA_1:45
for C being strict Category st C is discrete holds
IdCat C = C
proof
let C be strict Category; ::_thesis: ( C is discrete implies IdCat C = C )
assume A1: C is discrete ; ::_thesis: IdCat C = C
the carrier' of C c= { (id a) where a is Object of C : verum }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of C or x in { (id a) where a is Object of C : verum } )
assume x in the carrier' of C ; ::_thesis: x in { (id a) where a is Object of C : verum }
then ex a being Object of C st x = id a by A1, Def18;
hence x in { (id a) where a is Object of C : verum } ; ::_thesis: verum
end;
then A2: the carrier' of C c= the carrier' of (IdCat C) by Def19;
the carrier' of (IdCat C) c= the carrier' of C by CAT_2:7;
then the carrier' of (IdCat C) = the carrier' of C by A2, XBOOLE_0:def_10;
hence IdCat C = C by Def19, Th10; ::_thesis: verum
end;
theorem :: NATTRA_1:46
for C being Category holds IdCat (IdCat C) = IdCat C by Th45;
theorem :: NATTRA_1:47
for o, m being set holds IdCat (1Cat (o,m)) = 1Cat (o,m)
proof
let o, m be set ; ::_thesis: IdCat (1Cat (o,m)) = 1Cat (o,m)
1Cat (o,m) is discrete by Th39;
hence IdCat (1Cat (o,m)) = 1Cat (o,m) by Th45; ::_thesis: verum
end;
theorem :: NATTRA_1:48
for A, B being Category holds IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
proof
let A, B be Category; ::_thesis: IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
now__::_thesis:_(_[:_the_carrier_of_(IdCat_A),_the_carrier_of_(IdCat_B):]_=_the_carrier_of_(IdCat_[:A,B:])_&_the_carrier'_of_(IdCat_[:A,B:])_=_[:_the_carrier'_of_(IdCat_A),_the_carrier'_of_(IdCat_B):]_&_[:_the_Source_of_(IdCat_A),_the_Source_of_(IdCat_B):]_=_the_Source_of_(IdCat_[:A,B:])_&_[:_the_Target_of_(IdCat_A),_the_Target_of_(IdCat_B):]_=_the_Target_of_(IdCat_[:A,B:])_&_|:_the_Comp_of_(IdCat_A),_the_Comp_of_(IdCat_B):|_=_the_Comp_of_(IdCat_[:A,B:])_)
reconsider OA = the carrier of (IdCat A) as non empty Subset of the carrier of A by CAT_2:def_4;
set AB = { (id c) where c is Object of [:A,B:] : verum } ;
set MA = { (id a) where a is Object of A : verum } ;
set MB = { (id b) where b is Object of B : verum } ;
A1: { (id c) where c is Object of [:A,B:] : verum } = [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
proof
thus { (id c) where c is Object of [:A,B:] : verum } c= [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] :: according to XBOOLE_0:def_10 ::_thesis: [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] c= { (id c) where c is Object of [:A,B:] : verum }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (id c) where c is Object of [:A,B:] : verum } or x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] )
assume x in { (id c) where c is Object of [:A,B:] : verum } ; ::_thesis: x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
then consider c being Object of [:A,B:] such that
A2: x = id c ;
consider c1 being Object of A, c2 being Object of B such that
A3: c = [c1,c2] by DOMAIN_1:1;
A4: id c2 in { (id b) where b is Object of B : verum } ;
A5: id c1 in { (id a) where a is Object of A : verum } ;
id c = [(id c1),(id c2)] by A3, CAT_2:31;
hence x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] by A2, A5, A4, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] or x in { (id c) where c is Object of [:A,B:] : verum } )
assume x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] ; ::_thesis: x in { (id c) where c is Object of [:A,B:] : verum }
then consider x1, x2 being set such that
A6: x1 in { (id a) where a is Object of A : verum } and
A7: x2 in { (id b) where b is Object of B : verum } and
A8: x = [x1,x2] by ZFMISC_1:84;
consider a being Object of A such that
A9: x1 = id a by A6;
consider b being Object of B such that
A10: x2 = id b by A7;
id [a,b] = [(id a),(id b)] by CAT_2:31;
hence x in { (id c) where c is Object of [:A,B:] : verum } by A8, A9, A10; ::_thesis: verum
end;
reconsider OB = the carrier of (IdCat B) as non empty Subset of the carrier of B by CAT_2:def_4;
reconsider MB = the carrier' of (IdCat B) as non empty Subset of the carrier' of B by CAT_2:7;
reconsider MA = the carrier' of (IdCat A) as non empty Subset of the carrier' of A by CAT_2:7;
A11: the carrier of (IdCat B) = the carrier of B by Def19;
the carrier of (IdCat A) = the carrier of A by Def19;
hence [: the carrier of (IdCat A), the carrier of (IdCat B):] = the carrier of (IdCat [:A,B:]) by A11, Def19; ::_thesis: ( the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] & [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
A12: the Target of (IdCat B) = the Target of B | the carrier' of (IdCat B) by Th8;
A13: the Source of (IdCat B) = the Source of B | the carrier' of (IdCat B) by Th8;
A14: the carrier' of (IdCat B) = { (id b) where b is Object of B : verum } by Def19;
the carrier' of (IdCat A) = { (id a) where a is Object of A : verum } by Def19;
hence A15: the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] by A1, A14, Def19; ::_thesis: ( [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
the Source of (IdCat A) = the Source of A | the carrier' of (IdCat A) by Th8;
hence [: the Source of (IdCat A), the Source of (IdCat B):] = [: the Source of A, the Source of B:] | [:MA,MB:] by A13, Th1
.= the Source of (IdCat [:A,B:]) by A15, Th8 ;
::_thesis: ( [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
the Target of (IdCat A) = the Target of A | the carrier' of (IdCat A) by Th8;
hence [: the Target of (IdCat A), the Target of (IdCat B):] = [: the Target of A, the Target of B:] | [:MA,MB:] by A12, Th1
.= the Target of (IdCat [:A,B:]) by A15, Th8 ;
::_thesis: |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:])
A16: the Comp of (IdCat A) = the Comp of A || MA by Th8;
A17: the Comp of (IdCat B) = the Comp of B || MB by Th8;
|: the Comp of A, the Comp of B:| || [:MA,MB:] = the Comp of (IdCat [:A,B:]) by A15, Th8;
hence |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) by A16, A17, Th2; ::_thesis: verum
end;
hence IdCat [:A,B:] = [:(IdCat A),(IdCat B):] ; ::_thesis: verum
end;