:: ISOCAT_1 semantic presentation
begin
theorem :: ISOCAT_1:1
canceled;
theorem :: ISOCAT_1:2
canceled;
theorem Th3: :: ISOCAT_1:3
for B, A being Category
for F being Functor of A,B
for a, b being Object of A
for f being Morphism of a,b st f is invertible holds
F /. f is invertible
proof
let B, A be Category; ::_thesis: for F being Functor of A,B
for a, b being Object of A
for f being Morphism of a,b st f is invertible holds
F /. f is invertible
let F be Functor of A,B; ::_thesis: for a, b being Object of A
for f being Morphism of a,b st f is invertible holds
F /. f is invertible
let a, b be Object of A; ::_thesis: for f being Morphism of a,b st f is invertible holds
F /. f is invertible
let f be Morphism of a,b; ::_thesis: ( f is invertible implies F /. f is invertible )
assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for b1 being Morphism of b,a holds
( not f * b1 = id b or not b1 * f = id a ) or F /. f is invertible )
given g being Morphism of b,a such that A2: f * g = id b and
A3: g * f = id a ; ::_thesis: F /. f is invertible
A4: dom g = b by A1, CAT_1:5
.= cod f by A1, CAT_1:5 ;
A5: cod g = a by A1, CAT_1:5
.= dom f by A1, CAT_1:5 ;
A6: cod f = b by A1, CAT_1:5;
A7: dom f = a by A1, CAT_1:5;
A8: f (*) g = id (cod f) by A2, A1, A6, CAT_1:def_13;
A9: g (*) f = id (dom f) by A3, A1, A7, CAT_1:def_13;
thus A10: ( Hom ((F . a),(F . b)) <> {} & Hom ((F . b),(F . a)) <> {} ) by A1, CAT_1:84; :: according to CAT_1:def_16 ::_thesis: ex b1 being Morphism of F . b,F . a st
( (F /. f) * b1 = id (F . b) & b1 * (F /. f) = id (F . a) )
take F /. g ; ::_thesis: ( (F /. f) * (F /. g) = id (F . b) & (F /. g) * (F /. f) = id (F . a) )
A11: F /. f = F . f by A1, CAT_3:def_10;
A12: F /. g = F . g by A1, CAT_3:def_10;
thus (F /. f) * (F /. g) = (F . f) (*) (F . g) by A10, A11, A12, CAT_1:def_13
.= F . (f (*) g) by A5, CAT_1:64
.= id (cod (F /. f)) by A8, A11, CAT_1:63
.= id (F . b) by A10, CAT_1:5 ; ::_thesis: (F /. g) * (F /. f) = id (F . a)
thus (F /. g) * (F /. f) = (F . g) (*) (F . f) by A10, A11, A12, CAT_1:def_13
.= F . (g (*) f) by A4, CAT_1:64
.= id (dom (F /. f)) by A9, A11, CAT_1:63
.= id (F . a) by A10, CAT_1:5 ; ::_thesis: verum
end;
theorem Th4: :: ISOCAT_1:4
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let t be transformation of F1,F2; ::_thesis: for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let a be Object of A; ::_thesis: t . a in Hom ((F1 . a),(F2 . a))
Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2;
hence t . a in Hom ((F1 . a),(F2 . a)) by CAT_1:def_5; ::_thesis: verum
end;
theorem Th5: :: ISOCAT_1:5
for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
let G1, G2 be Functor of B,C; ::_thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1 * F1 is_transformable_to G2 * F2 )
assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_transformable_to G2 ; ::_thesis: G1 * F1 is_transformable_to G2 * F2
let a be Object of A; :: according to NATTRA_1:def_2 ::_thesis: not Hom (((G1 * F1) . a),((G2 * F2) . a)) = {}
Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2;
then A3: Hom ((G1 . (F1 . a)),(G1 . (F2 . a))) <> {} by CAT_1:84;
A4: ( G1 . (F1 . a) = (G1 * F1) . a & G2 . (F2 . a) = (G2 * F2) . a ) by CAT_1:76;
Hom ((G1 . (F2 . a)),(G2 . (F2 . a))) <> {} by A2, NATTRA_1:def_2;
hence not Hom (((G1 * F1) . a),((G2 * F2) . a)) = {} by A4, A3, CAT_1:24; ::_thesis: verum
end;
theorem Th6: :: ISOCAT_1:6
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 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic
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 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic )
assume F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic
let t be transformation of F1,F2; ::_thesis: ( t is invertible implies for a being Object of A holds F1 . a,F2 . a are_isomorphic )
assume A1: t is invertible ; ::_thesis: for a being Object of A holds F1 . a,F2 . a are_isomorphic
let a be Object of A; ::_thesis: F1 . a,F2 . a are_isomorphic
take t . a ; :: according to CAT_1:def_20 ::_thesis: t . a is invertible
thus t . a is invertible by A1, NATTRA_1:def_10; ::_thesis: verum
end;
definition
let C, D be Category;
redefine mode Functor of C,D means :: ISOCAT_1:def 1
( ( for c being Object of C ex d being Object of D st it . (id c) = id d ) & ( for f being Morphism of C holds
( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
it . (g (*) f) = (it . g) (*) (it . f) ) );
compatibility
for b1 being M2( bool [: the carrier' of C, the carrier' of D:]) holds
( b1 is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) & ( for f being Morphism of C holds
( b1 . (id (dom f)) = id (dom (b1 . f)) & b1 . (id (cod f)) = id (cod (b1 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b1 . (g (*) f) = (b1 . g) (*) (b1 . f) ) ) ) by CAT_1:61, CAT_1:62, CAT_1:63, CAT_1:64;
end;
:: deftheorem defines Functor ISOCAT_1:def_1_:_
for C, D being Category
for b3 being M2( bool [: the carrier' of b1, the carrier' of b2:]) holds
( b3 is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b3 . (id c) = id d ) & ( for f being Morphism of C holds
( b3 . (id (dom f)) = id (dom (b3 . f)) & b3 . (id (cod f)) = id (cod (b3 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b3 . (g (*) f) = (b3 . g) (*) (b3 . f) ) ) );
theorem Th7: :: ISOCAT_1:7
for B, A being Category
for F being Functor of A,B st F is isomorphic holds
for g being Morphism of B ex f being Morphism of A st F . f = g
proof
let B, A be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds
for g being Morphism of B ex f being Morphism of A st F . f = g
let F be Functor of A,B; ::_thesis: ( F is isomorphic implies for g being Morphism of B ex f being Morphism of A st F . f = g )
assume A1: F is isomorphic ; ::_thesis: for g being Morphism of B ex f being Morphism of A st F . f = g
let g be Morphism of B; ::_thesis: ex f being Morphism of A st F . f = g
rng F = the carrier' of B by A1, CAT_1:def_25;
then consider f being set such that
A2: f in dom F and
A3: F . f = g by FUNCT_1:def_3;
reconsider f = f as Morphism of A by A2;
take f ; ::_thesis: F . f = g
thus F . f = g by A3; ::_thesis: verum
end;
theorem Th8: :: ISOCAT_1:8
for B, A being Category
for F being Functor of A,B st F is isomorphic holds
for b being Object of B ex a being Object of A st F . a = b
proof
let B, A be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds
for b being Object of B ex a being Object of A st F . a = b
let F be Functor of A,B; ::_thesis: ( F is isomorphic implies for b being Object of B ex a being Object of A st F . a = b )
assume A1: F is isomorphic ; ::_thesis: for b being Object of B ex a being Object of A st F . a = b
let b be Object of B; ::_thesis: ex a being Object of A st F . a = b
rng (Obj F) = the carrier of B by A1, CAT_1:def_25;
then consider a being set such that
A2: a in dom (Obj F) and
A3: (Obj F) . a = b by FUNCT_1:def_3;
reconsider a = a as Object of A by A2;
take a ; ::_thesis: F . a = b
thus F . a = b by A3; ::_thesis: verum
end;
theorem Th9: :: ISOCAT_1:9
for A, B being Category
for F being Functor of A,B st F is one-to-one holds
Obj F is one-to-one
proof
let A, B be Category; ::_thesis: for F being Functor of A,B st F is one-to-one holds
Obj F is one-to-one
let F be Functor of A,B; ::_thesis: ( F is one-to-one implies Obj F is one-to-one )
assume A1: F is one-to-one ; ::_thesis: Obj F is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (Obj F) or not x2 in dom (Obj F) or not (Obj F) . x1 = (Obj F) . x2 or x1 = x2 )
assume ( x1 in dom (Obj F) & x2 in dom (Obj F) ) ; ::_thesis: ( not (Obj F) . x1 = (Obj F) . x2 or x1 = x2 )
then reconsider a1 = x1, a2 = x2 as Object of A ;
assume (Obj F) . x1 = (Obj F) . x2 ; ::_thesis: x1 = x2
then F . a1 = F . a2 ;
then A2: F . (id a1) = id (F . a2) by CAT_1:71
.= F . (id a2) by CAT_1:71 ;
dom F = the carrier' of A by FUNCT_2:def_1;
then id a1 = id a2 by A1, A2, FUNCT_1:def_4;
hence x1 = x2 by CAT_1:59; ::_thesis: verum
end;
definition
let A, B be Category;
let F be Functor of A,B;
assume A1: F is isomorphic ;
funcF " -> Functor of B,A equals :Def2: :: ISOCAT_1:def 2
F " ;
coherence
F " is Functor of B,A
proof
A2: F is one-to-one by A1, CAT_1:def_25;
rng F = the carrier' of B by A1, CAT_1:def_25;
then reconsider G = F " as Function of the carrier' of B, the carrier' of A by A2, FUNCT_2:25;
A3: dom F = the carrier' of A by FUNCT_2:def_1;
A4: Obj F is one-to-one by A2, Th9;
G is Functor of B,A
proof
thus for c being Object of B ex d being Object of A st G . (id c) = id d :: according to ISOCAT_1:def_1 ::_thesis: ( ( for f being Morphism of B holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
G . (g (*) f) = (G . g) (*) (G . f) ) )
proof
let b be Object of B; ::_thesis: ex d being Object of A st G . (id b) = id d
consider a being Object of A such that
A5: F . a = b by A1, Th8;
take a ; ::_thesis: G . (id b) = id a
thus G . (id b) = G . (F . (id a)) by A5, CAT_1:71
.= id a by A2, A3, FUNCT_1:34 ; ::_thesis: verum
end;
thus for f being Morphism of B holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ::_thesis: for f, g being Morphism of B st dom g = cod f holds
G . (g (*) f) = (G . g) (*) (G . f)
proof
let f be Morphism of B; ::_thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
consider g being Morphism of A such that
A6: f = F . g by A1, Th7;
thus G . (id (dom f)) = G . (id (F . (dom g))) by A6, CAT_1:72
.= G . (F . (id (dom g))) by CAT_1:71
.= id (dom g) by A2, A3, FUNCT_1:34
.= id (dom (G . f)) by A2, A3, A6, FUNCT_1:34 ; ::_thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = G . (id (F . (cod g))) by A6, CAT_1:72
.= G . (F . (id (cod g))) by CAT_1:71
.= id (cod g) by A2, A3, FUNCT_1:34
.= id (cod (G . f)) by A2, A3, A6, FUNCT_1:34 ; ::_thesis: verum
end;
let f, g be Morphism of B; ::_thesis: ( dom g = cod f implies G . (g (*) f) = (G . g) (*) (G . f) )
A7: dom (Obj F) = the carrier of A by FUNCT_2:def_1;
assume A8: dom g = cod f ; ::_thesis: G . (g (*) f) = (G . g) (*) (G . f)
consider f9 being Morphism of A such that
A9: f = F . f9 by A1, Th7;
consider g9 being Morphism of A such that
A10: g = F . g9 by A1, Th7;
(Obj F) . (dom g9) = F . (dom g9)
.= cod f by A10, A8, CAT_1:72
.= F . (cod f9) by A9, CAT_1:72
.= (Obj F) . (cod f9) ;
then dom g9 = cod f9 by A4, A7, FUNCT_1:def_4;
hence G . (g (*) f) = G . (F . (g9 (*) f9)) by A9, A10, CAT_1:64
.= g9 (*) f9 by A2, A3, FUNCT_1:34
.= g9 (*) (G . f) by A2, A3, A9, FUNCT_1:34
.= (G . g) (*) (G . f) by A2, A3, A10, FUNCT_1:34 ;
::_thesis: verum
end;
hence F " is Functor of B,A ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines " ISOCAT_1:def_2_:_
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
F " = F " ;
definition
let A, B be Category;
let F be Functor of A,B;
redefine attr F is isomorphic means :Def3: :: ISOCAT_1:def 3
( F is one-to-one & rng F = the carrier' of B );
compatibility
( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) )
proof
thus ( F is isomorphic implies ( F is one-to-one & rng F = the carrier' of B ) ) by CAT_1:def_25; ::_thesis: ( F is one-to-one & rng F = the carrier' of B implies F is isomorphic )
assume that
A1: F is one-to-one and
A2: rng F = the carrier' of B ; ::_thesis: F is isomorphic
thus ( F is one-to-one & rng F = the carrier' of B ) by A1, A2; :: according to CAT_1:def_25 ::_thesis: rng (Obj F) = the carrier of B
thus rng (Obj F) c= the carrier of B ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of B c= rng (Obj F)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of B or x in rng (Obj F) )
assume x in the carrier of B ; ::_thesis: x in rng (Obj F)
then reconsider d = x as Object of B ;
consider f being set such that
A3: f in dom F and
A4: id d = F . f by A2, FUNCT_1:def_3;
reconsider f = f as Morphism of A by A3;
reconsider c = id (dom f) as Morphism of A ;
F . c = id (dom (id d)) by A4, CAT_1:63
.= id d ;
then ( dom (Obj F) = the carrier of A & (Obj F) . (dom f) = d ) by CAT_1:67, FUNCT_2:def_1;
hence x in rng (Obj F) by FUNCT_1:def_3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines isomorphic ISOCAT_1:def_3_:_
for A, B being Category
for F being Functor of A,B holds
( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) );
theorem Th10: :: ISOCAT_1:10
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
F " is isomorphic
proof
let A, B be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds
F " is isomorphic
let F be Functor of A,B; ::_thesis: ( F is isomorphic implies F " is isomorphic )
assume F is isomorphic ; ::_thesis: F " is isomorphic
then A1: ( F is one-to-one & F " = F " ) by Def2, CAT_1:def_25;
hence F " is one-to-one by FUNCT_1:40; :: according to ISOCAT_1:def_3 ::_thesis: rng (F ") = the carrier' of A
thus rng (F ") = dom F by A1, FUNCT_1:33
.= the carrier' of A by FUNCT_2:def_1 ; ::_thesis: verum
end;
theorem :: ISOCAT_1:11
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
(Obj F) " = Obj (F ")
proof
let A, B be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds
(Obj F) " = Obj (F ")
let F be Functor of A,B; ::_thesis: ( F is isomorphic implies (Obj F) " = Obj (F ") )
assume A1: F is isomorphic ; ::_thesis: (Obj F) " = Obj (F ")
then A2: F is one-to-one by Def3;
A3: rng (Obj F) = the carrier of B by A1, CAT_1:def_25;
then reconsider G = (Obj F) " as Function of the carrier of B, the carrier of A by A2, Th9, FUNCT_2:25;
A4: Obj F is one-to-one by A2, Th9;
now__::_thesis:_for_b_being_Object_of_B_holds_G_._b_=_(Obj_(F_"))_._b
let b be Object of B; ::_thesis: G . b = (Obj (F ")) . b
F . (id (G . b)) = id ((Obj F) . (G . b)) by CAT_1:68
.= id b by A3, A4, FUNCT_1:35 ;
then id (G . b) = (F ") . (id b) by A2, FUNCT_2:26
.= (F ") . (id b) by A1, Def2 ;
hence G . b = (Obj (F ")) . b by CAT_1:67; ::_thesis: verum
end;
hence (Obj F) " = Obj (F ") by FUNCT_2:63; ::_thesis: verum
end;
theorem :: ISOCAT_1:12
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
(F ") " = F
proof
let A, B be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds
(F ") " = F
let F be Functor of A,B; ::_thesis: ( F is isomorphic implies (F ") " = F )
reconsider f = F as Function of the carrier' of A, the carrier' of B ;
reconsider g = F " as Function of the carrier' of B, the carrier' of A ;
assume A1: F is isomorphic ; ::_thesis: (F ") " = F
then A2: F is one-to-one by CAT_1:def_25;
thus (F ") " = g " by A1, Def2, Th10
.= (f ") " by A1, Def2
.= F by A2, FUNCT_1:43 ; ::_thesis: verum
end;
theorem Th13: :: ISOCAT_1:13
for B, A being Category
for F being Functor of A,B st F is isomorphic holds
( F * (F ") = id B & (F ") * F = id A )
proof
let B, A be Category; ::_thesis: for F being Functor of A,B st F is isomorphic holds
( F * (F ") = id B & (F ") * F = id A )
let F be Functor of A,B; ::_thesis: ( F is isomorphic implies ( F * (F ") = id B & (F ") * F = id A ) )
reconsider f = F as Function of the carrier' of A, the carrier' of B ;
A1: dom f = the carrier' of A by FUNCT_2:def_1;
assume A2: F is isomorphic ; ::_thesis: ( F * (F ") = id B & (F ") * F = id A )
then A3: F is one-to-one by Def3;
A4: rng f = the carrier' of B by A2, Def3;
thus F * (F ") = f * (f ") by A2, Def2
.= id B by A3, A4, FUNCT_1:39 ; ::_thesis: (F ") * F = id A
thus (F ") * F = (f ") * f by A2, Def2
.= id A by A3, A1, FUNCT_1:39 ; ::_thesis: verum
end;
theorem Th14: :: ISOCAT_1:14
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st F is isomorphic & G is isomorphic holds
G * F is isomorphic
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,C st F is isomorphic & G is isomorphic holds
G * F is isomorphic
let F be Functor of A,B; ::_thesis: for G being Functor of B,C st F is isomorphic & G is isomorphic holds
G * F is isomorphic
let G be Functor of B,C; ::_thesis: ( F is isomorphic & G is isomorphic implies G * F is isomorphic )
assume that
A1: F is one-to-one and
A2: rng F = the carrier' of B and
A3: G is one-to-one and
A4: rng G = the carrier' of C ; :: according to ISOCAT_1:def_3 ::_thesis: G * F is isomorphic
thus G * F is one-to-one by A1, A3, FUNCT_1:24; :: according to ISOCAT_1:def_3 ::_thesis: rng (G * F) = the carrier' of C
dom G = the carrier' of B by FUNCT_2:def_1;
hence rng (G * F) = the carrier' of C by A2, A4, RELAT_1:28; ::_thesis: verum
end;
definition
let A, B be Category;
predA,B are_isomorphic means :: ISOCAT_1:def 4
ex F being Functor of A,B st F is isomorphic ;
reflexivity
for A being Category ex F being Functor of A,A st F is isomorphic
proof
let A be Category; ::_thesis: ex F being Functor of A,A st F is isomorphic
id A is isomorphic by CAT_1:80;
hence ex F being Functor of A,A st F is isomorphic ; ::_thesis: verum
end;
symmetry
for A, B being Category st ex F being Functor of A,B st F is isomorphic holds
ex F being Functor of B,A st F is isomorphic
proof
let A, B be Category; ::_thesis: ( ex F being Functor of A,B st F is isomorphic implies ex F being Functor of B,A st F is isomorphic )
given F being Functor of A,B such that A1: F is isomorphic ; ::_thesis: ex F being Functor of B,A st F is isomorphic
take F " ; ::_thesis: F " is isomorphic
thus F " is isomorphic by A1, Th10; ::_thesis: verum
end;
end;
:: deftheorem defines are_isomorphic ISOCAT_1:def_4_:_
for A, B being Category holds
( A,B are_isomorphic iff ex F being Functor of A,B st F is isomorphic );
notation
let A, B be Category;
synonym A ~= B for A,B are_isomorphic ;
end;
theorem :: ISOCAT_1:15
for A, B, C being Category st A ~= B & B ~= C holds
A ~= C
proof
let A, B, C be Category; ::_thesis: ( A ~= B & B ~= C implies A ~= C )
given F1 being Functor of A,B such that A1: F1 is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: ( not B ~= C or A ~= C )
given F2 being Functor of B,C such that A2: F2 is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: A ~= C
take F2 * F1 ; :: according to ISOCAT_1:def_4 ::_thesis: F2 * F1 is isomorphic
thus F2 * F1 is isomorphic by A1, A2, Th14; ::_thesis: verum
end;
theorem :: ISOCAT_1:16
for A being Category
for o, m being set holds [:(1Cat (o,m)),A:] ~= A
proof
let A be Category; ::_thesis: for o, m being set holds [:(1Cat (o,m)),A:] ~= A
let o, m be set ; ::_thesis: [:(1Cat (o,m)),A:] ~= A
take F = pr2 ((1Cat (o,m)),A); :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic
set X = [: the carrier' of (1Cat (o,m)), the carrier' of A:];
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_[:_the_carrier'_of_(1Cat_(o,m)),_the_carrier'_of_A:]_&_x2_in_[:_the_carrier'_of_(1Cat_(o,m)),_the_carrier'_of_A:]_&_F_._x1_=_F_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 implies x1 = x2 )
assume x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] ; ::_thesis: ( x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 implies x1 = x2 )
then consider x11, x12 being set such that
A1: x11 in the carrier' of (1Cat (o,m)) and
A2: x12 in the carrier' of A and
A3: x1 = [x11,x12] by ZFMISC_1:def_2;
assume x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] ; ::_thesis: ( F . x1 = F . x2 implies x1 = x2 )
then consider x21, x22 being set such that
A4: x21 in the carrier' of (1Cat (o,m)) and
A5: x22 in the carrier' of A and
A6: x2 = [x21,x22] by ZFMISC_1:def_2;
reconsider f11 = x11, f21 = x21 as Morphism of (1Cat (o,m)) by A1, A4;
assume A7: F . x1 = F . x2 ; ::_thesis: x1 = x2
reconsider f12 = x12, f22 = x22 as Morphism of A by A2, A5;
A8: f11 = m by TARSKI:def_1
.= f21 by TARSKI:def_1 ;
f12 = F . (f11,f12) by FUNCT_3:def_5
.= F . (f21,f22) by A3, A6, A7
.= f22 by FUNCT_3:def_5 ;
hence x1 = x2 by A3, A6, A8; ::_thesis: verum
end;
hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of A
thus rng F = the carrier' of A by FUNCT_3:46; ::_thesis: verum
end;
theorem :: ISOCAT_1:17
for A, B being Category holds [:A,B:] ~= [:B,A:]
proof
let A, B be Category; ::_thesis: [:A,B:] ~= [:B,A:]
take F = <:(pr2 (A,B)),(pr1 (A,B)):>; :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic
A1: ( dom (pr1 (A,B)) = the carrier' of [:A,B:] & dom (pr2 (A,B)) = the carrier' of [:A,B:] ) by FUNCT_2:def_1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_[:_the_carrier'_of_A,_the_carrier'_of_B:]_&_x2_in_[:_the_carrier'_of_A,_the_carrier'_of_B:]_&_F_._x1_=_F_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in [: the carrier' of A, the carrier' of B:] & x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 implies x1 = x2 )
assume x1 in [: the carrier' of A, the carrier' of B:] ; ::_thesis: ( x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 implies x1 = x2 )
then consider x11, x12 being set such that
A2: x11 in the carrier' of A and
A3: x12 in the carrier' of B and
A4: x1 = [x11,x12] by ZFMISC_1:def_2;
assume x2 in [: the carrier' of A, the carrier' of B:] ; ::_thesis: ( F . x1 = F . x2 implies x1 = x2 )
then consider x21, x22 being set such that
A5: x21 in the carrier' of A and
A6: x22 in the carrier' of B and
A7: x2 = [x21,x22] by ZFMISC_1:def_2;
reconsider f12 = x12, f22 = x22 as Morphism of B by A3, A6;
reconsider f11 = x11, f21 = x21 as Morphism of A by A2, A5;
A8: [f21,f22] in the carrier' of [:A,B:] ;
assume A9: F . x1 = F . x2 ; ::_thesis: x1 = x2
A10: [f11,f12] in the carrier' of [:A,B:] ;
A11: [f12,f11] = [f12,((pr1 (A,B)) . (f11,f12))] by FUNCT_3:def_4
.= [((pr2 (A,B)) . (f11,f12)),((pr1 (A,B)) . (f11,f12))] by FUNCT_3:def_5
.= F . (f21,f22) by A1, A4, A7, A10, A9, FUNCT_3:49
.= [((pr2 (A,B)) . (f21,f22)),((pr1 (A,B)) . (f21,f22))] by A1, A8, FUNCT_3:49
.= [f22,((pr1 (A,B)) . (f21,f22))] by FUNCT_3:def_5
.= [f22,f21] by FUNCT_3:def_4 ;
then x12 = x22 by XTUPLE_0:1;
hence x1 = x2 by A4, A7, A11, XTUPLE_0:1; ::_thesis: verum
end;
hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of [:B,A:]
thus rng F c= the carrier' of [:B,A:] ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of [:B,A:] c= rng F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of [:B,A:] or x in rng F )
assume x in the carrier' of [:B,A:] ; ::_thesis: x in rng F
then consider x1, x2 being set such that
A12: x1 in the carrier' of B and
A13: x2 in the carrier' of A and
A14: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Morphism of A by A13;
reconsider x1 = x1 as Morphism of B by A12;
F . [x2,x1] = [((pr2 (A,B)) . (x2,x1)),((pr1 (A,B)) . (x2,x1))] by A1, FUNCT_3:49
.= [x1,((pr1 (A,B)) . (x2,x1))] by FUNCT_3:def_5
.= [x1,x2] by FUNCT_3:def_4 ;
hence x in rng F by A14, FUNCT_2:4; ::_thesis: verum
end;
theorem :: ISOCAT_1:18
for A, B, C being Category holds [:[:A,B:],C:] ~= [:A,[:B,C:]:]
proof
let A, B, C be Category; ::_thesis: [:[:A,B:],C:] ~= [:A,[:B,C:]:]
set X = (pr1 (A,B)) * (pr1 ([:A,B:],C));
set Y = <:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):>;
take F = <:((pr1 (A,B)) * (pr1 ([:A,B:],C))),<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):>:>; :: according to ISOCAT_1:def_4 ::_thesis: F is isomorphic
A1: ( dom (pr2 ([:A,B:],C)) = the carrier' of [:[:A,B:],C:] & dom ((pr2 (A,B)) * (pr1 ([:A,B:],C))) = the carrier' of [:[:A,B:],C:] ) by FUNCT_2:def_1;
A2: ( dom ((pr1 (A,B)) * (pr1 ([:A,B:],C))) = the carrier' of [:[:A,B:],C:] & dom <:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> = the carrier' of [:[:A,B:],C:] ) by FUNCT_2:def_1;
now__::_thesis:_for_x,_y_being_set_st_x_in_[:[:_the_carrier'_of_A,_the_carrier'_of_B:],_the_carrier'_of_C:]_&_y_in_[:[:_the_carrier'_of_A,_the_carrier'_of_B:],_the_carrier'_of_C:]_&_F_._x_=_F_._y_holds_
x_=_y
let x, y be set ; ::_thesis: ( x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y implies x = y )
assume x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] ; ::_thesis: ( y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y implies x = y )
then consider x1, x2 being set such that
A3: x1 in [: the carrier' of A, the carrier' of B:] and
A4: x2 in the carrier' of C and
A5: x = [x1,x2] by ZFMISC_1:def_2;
assume y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] ; ::_thesis: ( F . x = F . y implies x = y )
then consider y1, y2 being set such that
A6: y1 in [: the carrier' of A, the carrier' of B:] and
A7: y2 in the carrier' of C and
A8: y = [y1,y2] by ZFMISC_1:def_2;
reconsider f2 = x2, g2 = y2 as Morphism of C by A4, A7;
assume A9: F . x = F . y ; ::_thesis: x = y
consider x11, x12 being set such that
A10: x11 in the carrier' of A and
A11: x12 in the carrier' of B and
A12: x1 = [x11,x12] by A3, ZFMISC_1:def_2;
consider y11, y12 being set such that
A13: y11 in the carrier' of A and
A14: y12 in the carrier' of B and
A15: y1 = [y11,y12] by A6, ZFMISC_1:def_2;
reconsider f12 = x12, g12 = y12 as Morphism of B by A11, A14;
reconsider f11 = x11, g11 = y11 as Morphism of A by A10, A13;
A16: [f11,[f12,f2]] = [((pr1 (A,B)) . (f11,f12)),[f12,f2]] by FUNCT_3:def_4
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([f11,f12],f2))),[f12,f2]] by FUNCT_3:def_4
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . [[f11,f12],f2])),[f12,f2]]
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . ([f11,f12],f2)),[f12,f2]] by FUNCT_2:15
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[((pr2 (A,B)) . (f11,f12)),f2]] by FUNCT_3:def_5
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([f11,f12],f2))),f2]] by FUNCT_3:def_4
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),f2]] by FUNCT_2:15
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),((pr2 ([:A,B:],C)) . ([f11,f12],f2))]] by FUNCT_3:def_5
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[f11,f12],f2])] by A1, FUNCT_3:49
.= F . [[g11,g12],g2] by A2, A5, A12, A8, A15, A9, FUNCT_3:49
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[g11,g12],g2])] by A2, FUNCT_3:49
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),((pr2 ([:A,B:],C)) . ([g11,g12],g2))]] by A1, FUNCT_3:49
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),g2]] by FUNCT_3:def_5
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([g11,g12],g2))),g2]] by FUNCT_2:15
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[((pr2 (A,B)) . (g11,g12)),g2]] by FUNCT_3:def_4
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[g12,g2]] by FUNCT_3:def_5
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([g11,g12],g2))),[g12,g2]] by FUNCT_2:15
.= [((pr1 (A,B)) . (g11,g12)),[g12,g2]] by FUNCT_3:def_4
.= [g11,[g12,g2]] by FUNCT_3:def_4 ;
then [x12,x2] = [y12,y2] by XTUPLE_0:1;
then ( x12 = y12 & x2 = y2 ) by XTUPLE_0:1;
hence x = y by A5, A12, A8, A15, A16, XTUPLE_0:1; ::_thesis: verum
end;
hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def_3 ::_thesis: rng F = the carrier' of [:A,[:B,C:]:]
thus rng F c= the carrier' of [:A,[:B,C:]:] ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier' of [:A,[:B,C:]:] c= rng F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of [:A,[:B,C:]:] or x in rng F )
assume x in the carrier' of [:A,[:B,C:]:] ; ::_thesis: x in rng F
then consider x1, x2 being set such that
A17: x1 in the carrier' of A and
A18: x2 in the carrier' of [:B,C:] and
A19: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1 as Morphism of A by A17;
consider x21, x22 being set such that
A20: x21 in the carrier' of B and
A21: x22 in the carrier' of C and
A22: x2 = [x21,x22] by A18, ZFMISC_1:def_2;
reconsider x22 = x22 as Morphism of C by A21;
reconsider x21 = x21 as Morphism of B by A20;
F . [[x1,x21],x22] = [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[x1,x21],x22]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by A2, FUNCT_3:49
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([x1,x21],x22))),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_2:15
.= [((pr1 (A,B)) . (x1,x21)),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_3:def_4
.= [x1,(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_3:def_4
.= [x1,[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[x1,x21],x22]),((pr2 ([:A,B:],C)) . [[x1,x21],x22])]] by A1, FUNCT_3:49
.= [x1,[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([x1,x21],x22))),((pr2 ([:A,B:],C)) . [[x1,x21],x22])]] by FUNCT_2:15
.= [x1,[((pr2 (A,B)) . (x1,x21)),((pr2 ([:A,B:],C)) . ([x1,x21],x22))]] by FUNCT_3:def_4
.= [x1,[x21,((pr2 ([:A,B:],C)) . ([x1,x21],x22))]] by FUNCT_3:def_5
.= [x1,[x21,x22]] by FUNCT_3:def_5 ;
hence x in rng F by A19, A22, FUNCT_2:4; ::_thesis: verum
end;
theorem :: ISOCAT_1:19
for A, B, C, D being Category st A ~= B & C ~= D holds
[:A,C:] ~= [:B,D:]
proof
let A, B, C, D be Category; ::_thesis: ( A ~= B & C ~= D implies [:A,C:] ~= [:B,D:] )
given F being Functor of A,B such that A1: F is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: ( not C ~= D or [:A,C:] ~= [:B,D:] )
A2: F is one-to-one by A1, Def3;
given G being Functor of C,D such that A3: G is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: [:A,C:] ~= [:B,D:]
take [:F,G:] ; :: according to ISOCAT_1:def_4 ::_thesis: [:F,G:] is isomorphic
G is one-to-one by A3, Def3;
hence [:F,G:] is one-to-one by A2; :: according to ISOCAT_1:def_3 ::_thesis: rng [:F,G:] = the carrier' of [:B,D:]
thus rng [:F,G:] = [:(rng F),(rng G):] by FUNCT_3:67
.= [: the carrier' of B,(rng G):] by A1, Def3
.= the carrier' of [:B,D:] by A3, Def3 ; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, F2 be Functor of A,B;
assume B1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let G be Functor of B,C;
funcG * t -> transformation of G * F1,G * F2 equals :Def5: :: ISOCAT_1:def 5
G * t;
coherence
G * t is transformation of G * F1,G * F2
proof
reconsider Gt = G * t as Function of the carrier of A, the carrier' of C ;
Gt is transformation of G * F1,G * F2
proof
thus G * F1 is_transformable_to G * F2 by B1, Th5; :: according to NATTRA_1:def_3 ::_thesis: for b1 being M2( the carrier of A) holds Gt . b1 is Morphism of (G * F1) . b1,(G * F2) . b1
let a be Object of A; ::_thesis: Gt . a is Morphism of (G * F1) . a,(G * F2) . a
A1: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76;
t . a in Hom ((F1 . a),(F2 . a)) by B1, Th4;
then A2: G . (t . a) in Hom (((G * F1) . a),((G * F2) . a)) by A1, CAT_1:81;
Gt . a = G . (t . a) by FUNCT_2:15
.= G . (t . a) by B1, NATTRA_1:def_5 ;
hence Gt . a is Morphism of (G * F1) . a,(G * F2) . a by A2, CAT_1:def_5; ::_thesis: verum
end;
hence G * t is transformation of G * F1,G * F2 ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def5 defines * ISOCAT_1:def_5_:_
for A, B, C 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 G being Functor of B,C holds G * t = G * t;
definition
let A, B, C be Category;
let G1, G2 be Functor of B,C;
assume B1: G1 is_transformable_to G2 ;
let F be Functor of A,B;
let t be transformation of G1,G2;
funct * F -> transformation of G1 * F,G2 * F equals :Def6: :: ISOCAT_1:def 6
t * (Obj F);
coherence
t * (Obj F) is transformation of G1 * F,G2 * F
proof
reconsider tF = t * (Obj F) as Function of the carrier of A, the carrier' of C ;
tF is transformation of G1 * F,G2 * F
proof
thus G1 * F is_transformable_to G2 * F by B1, Th5; :: according to NATTRA_1:def_3 ::_thesis: for b1 being M2( the carrier of A) holds tF . b1 is Morphism of (G1 * F) . b1,(G2 * F) . b1
let a be Object of A; ::_thesis: tF . a is Morphism of (G1 * F) . a,(G2 * F) . a
A1: G1 . (F . a) = (G1 * F) . a by CAT_1:76;
tF . a = t . ((Obj F) . a) by FUNCT_2:15
.= t . (F . a) by B1, NATTRA_1:def_5 ;
hence tF . a is Morphism of (G1 * F) . a,(G2 * F) . a by A1, CAT_1:76; ::_thesis: verum
end;
hence t * (Obj F) is transformation of G1 * F,G2 * F ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def6 defines * ISOCAT_1:def_6_:_
for A, B, C being Category
for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds
for F being Functor of A,B
for t being transformation of G1,G2 holds t * F = t * (Obj F);
theorem Th20: :: ISOCAT_1:20
for B, C, A being Category
for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds
for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
proof
let B, C, A be Category; ::_thesis: for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds
for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let G1, G2 be Functor of B,C; ::_thesis: ( G1 is_transformable_to G2 implies for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a) )
assume A1: G1 is_transformable_to G2 ; ::_thesis: for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let F be Functor of A,B; ::_thesis: for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let t be transformation of G1,G2; ::_thesis: for a being Object of A holds (t * F) . a = t . (F . a)
let a be Object of A; ::_thesis: (t * F) . a = t . (F . a)
thus (t * F) . a = (t * F) . a by A1, Th5, NATTRA_1:def_5
.= (t * (Obj F)) . a by A1, Def6
.= t . ((Obj F) . a) by FUNCT_2:15
.= t . (F . a) by A1, NATTRA_1:def_5 ; ::_thesis: verum
end;
theorem Th21: :: ISOCAT_1:21
for A, B, C 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 G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a) )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let t be transformation of F1,F2; ::_thesis: for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let G be Functor of B,C; ::_thesis: for a being Object of A holds (G * t) . a = G /. (t . a)
let a be Object of A; ::_thesis: (G * t) . a = G /. (t . a)
A2: Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2;
thus (G * t) . a = (G * t) . a by A1, Th5, NATTRA_1:def_5
.= (G * t) . a by A1, Def5
.= G . (t . a) by FUNCT_2:15
.= G . (t . a) by A1, NATTRA_1:def_5
.= G /. (t . a) by A2, CAT_3:def_10 ; ::_thesis: verum
end;
theorem Th22: :: ISOCAT_1:22
for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
G1 * F1 is_naturally_transformable_to G2 * F2
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
G1 * F1 is_naturally_transformable_to G2 * F2
let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
G1 * F1 is_naturally_transformable_to G2 * F2
let G1, G2 be Functor of B,C; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies G1 * F1 is_naturally_transformable_to G2 * F2 )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; ::_thesis: G1 * F1 is_naturally_transformable_to G2 * F2
set t1 = the natural_transformation of F1,F2;
set t2 = the natural_transformation of G1,G2;
A3: G1 is_transformable_to G2 by A2, NATTRA_1:def_7;
A4: F1 is_transformable_to F2 by A1, NATTRA_1:def_7;
hence A5: G1 * F1 is_transformable_to G2 * F2 by A3, Th5; :: according to NATTRA_1:def_7 ::_thesis: ex b1 being transformation of G1 * F1,G2 * F2 st
for b2, b3 being M2( the carrier of A) holds
( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * ((G1 * F1) /. b4) = ((G2 * F2) /. b4) * (b1 . b2) )
take t = ( the natural_transformation of G1,G2 * F2) `*` (G1 * the natural_transformation of F1,F2); ::_thesis: for b1, b2 being M2( the carrier of A) holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (t . b2) * ((G1 * F1) /. b3) = ((G2 * F2) /. b3) * (t . b1) )
let a, b be Object of A; ::_thesis: ( Hom (a,b) = {} or for b1 being Morphism of a,b holds (t . b) * ((G1 * F1) /. b1) = ((G2 * F2) /. b1) * (t . a) )
A6: Hom ((G1 . (F2 . b)),(G2 . (F2 . b))) <> {} by A3, NATTRA_1:def_2;
A7: Hom (((G1 * F1) . a),((G2 * F2) . a)) <> {} by A5, NATTRA_1:def_2;
A8: G1 * F1 is_transformable_to G1 * F2 by A4, Th5;
then A9: Hom (((G1 * F1) . b),((G1 * F2) . b)) <> {} by NATTRA_1:def_2;
A10: Hom (((G1 * F1) . b),((G2 * F2) . b)) <> {} by A5, NATTRA_1:def_2;
assume A11: Hom (a,b) <> {} ; ::_thesis: for b1 being Morphism of a,b holds (t . b) * ((G1 * F1) /. b1) = ((G2 * F2) /. b1) * (t . a)
then A12: Hom (((G2 * F2) . a),((G2 * F2) . b)) <> {} by CAT_1:84;
A13: Hom ((F1 . b),(F2 . b)) <> {} by A4, NATTRA_1:def_2;
then A14: Hom ((G1 . (F1 . b)),(G1 . (F2 . b))) <> {} by CAT_1:84;
then A15: Hom ((G1 . (F1 . b)),(G2 . (F2 . b))) <> {} by A6, CAT_1:24;
A16: G1 * F2 is_transformable_to G2 * F2 by A3, Th5;
then A17: Hom (((G1 * F2) . b),((G2 * F2) . b)) <> {} by NATTRA_1:def_2;
A18: Hom (((G1 * F1) . a),((G1 * F2) . a)) <> {} by A8, NATTRA_1:def_2;
A19: Hom (((G1 * F2) . a),((G2 * F2) . a)) <> {} by A16, NATTRA_1:def_2;
A20: Hom ((F1 . a),(F2 . a)) <> {} by A4, NATTRA_1:def_2;
then A21: Hom ((G1 . (F1 . a)),(G1 . (F2 . a))) <> {} by CAT_1:84;
let f be Morphism of a,b; ::_thesis: (t . b) * ((G1 * F1) /. f) = ((G2 * F2) /. f) * (t . a)
A22: Hom ((F2 . a),(F2 . b)) <> {} by A11, CAT_1:84;
then A23: Hom ((G1 . (F2 . a)),(G1 . (F2 . b))) <> {} by CAT_1:84;
A24: Hom ((F1 . a),(F1 . b)) <> {} by A11, CAT_1:84;
then A25: Hom ((G1 . (F1 . a)),(G1 . (F1 . b))) <> {} by CAT_1:84;
A26: Hom ((G1 . (F2 . a)),(G2 . (F2 . a))) <> {} by A3, NATTRA_1:def_2;
then A27: Hom ((G1 . (F1 . a)),(G2 . (F2 . a))) <> {} by A21, CAT_1:24;
A28: Hom ((G2 . (F2 . a)),(G2 . (F2 . b))) <> {} by A22, CAT_1:84;
Hom (((G1 * F1) . a),((G1 * F1) . b)) <> {} by A11, CAT_1:84;
hence (t . b) * ((G1 * F1) /. f) = (t . b) (*) ((G1 * F1) /. f) by A10, CAT_1:def_13
.= (t . b) (*) (G1 /. (F1 /. f)) by A11, NATTRA_1:11
.= ((( the natural_transformation of G1,G2 * F2) . b) * ((G1 * the natural_transformation of F1,F2) . b)) (*) (G1 /. (F1 /. f)) by A8, A16, NATTRA_1:def_6
.= ((( the natural_transformation of G1,G2 * F2) . b) (*) ((G1 * the natural_transformation of F1,F2) . b)) (*) (G1 /. (F1 /. f)) by A17, A9, CAT_1:def_13
.= ((( the natural_transformation of G1,G2 * F2) . b) (*) (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A4, Th21
.= (( the natural_transformation of G1,G2 . (F2 . b)) (*) (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A3, Th20
.= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A6, A14, CAT_1:def_13
.= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ( the natural_transformation of F1,F2 . b))) * (G1 /. (F1 /. f)) by A25, A15, CAT_1:def_13
.= ( the natural_transformation of G1,G2 . (F2 . b)) * ((G1 /. ( the natural_transformation of F1,F2 . b)) * (G1 /. (F1 /. f))) by A6, A14, A25, CAT_1:25
.= ( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. (( the natural_transformation of F1,F2 . b) * (F1 /. f))) by A13, A24, NATTRA_1:13
.= ( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ((F2 /. f) * ( the natural_transformation of F1,F2 . a))) by A1, A11, NATTRA_1:def_8
.= ( the natural_transformation of G1,G2 . (F2 . b)) * ((G1 /. (F2 /. f)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A22, A20, NATTRA_1:13
.= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. (F2 /. f))) * (G1 /. ( the natural_transformation of F1,F2 . a)) by A6, A23, A21, CAT_1:25
.= ((G2 /. (F2 /. f)) * ( the natural_transformation of G1,G2 . (F2 . a))) * (G1 /. ( the natural_transformation of F1,F2 . a)) by A2, A22, NATTRA_1:def_8
.= (G2 /. (F2 /. f)) * (( the natural_transformation of G1,G2 . (F2 . a)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A21, A28, A26, CAT_1:25
.= (G2 /. (F2 /. f)) (*) (( the natural_transformation of G1,G2 . (F2 . a)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A28, A27, CAT_1:def_13
.= (G2 /. (F2 /. f)) (*) (( the natural_transformation of G1,G2 . (F2 . a)) (*) (G1 /. ( the natural_transformation of F1,F2 . a))) by A21, A26, CAT_1:def_13
.= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) (*) (G1 /. ( the natural_transformation of F1,F2 . a))) by A3, Th20
.= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) (*) ((G1 * the natural_transformation of F1,F2) . a)) by A4, Th21
.= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) * ((G1 * the natural_transformation of F1,F2) . a)) by A19, A18, CAT_1:def_13
.= (G2 /. (F2 /. f)) (*) (t . a) by A8, A16, NATTRA_1:def_6
.= ((G2 * F2) /. f) (*) (t . a) by A11, NATTRA_1:11
.= ((G2 * F2) /. f) * (t . a) by A7, A12, CAT_1:def_13 ;
::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, F2 be Functor of A,B;
assume B1: F1 is_naturally_transformable_to F2 ;
let t be natural_transformation of F1,F2;
let G be Functor of B,C;
funcG * t -> natural_transformation of G * F1,G * F2 equals :Def7: :: ISOCAT_1:def 7
G * t;
coherence
G * t is natural_transformation of G * F1,G * F2
proof
A1: F1 is_transformable_to F2 by B1, NATTRA_1:def_7;
G * t is natural_transformation of G * F1,G * F2
proof
thus G * F1 is_naturally_transformable_to G * F2 by B1, Th22; :: according to NATTRA_1:def_8 ::_thesis: for b1, b2 being M2( the carrier of A) holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds ((G * t) . b2) * ((G * F1) /. b3) = ((G * F2) /. b3) * ((G * t) . b1) )
then A2: G * F1 is_transformable_to G * F2 by NATTRA_1:def_7;
let a, b be Object of A; ::_thesis: ( Hom (a,b) = {} or for b1 being Morphism of a,b holds ((G * t) . b) * ((G * F1) /. b1) = ((G * F2) /. b1) * ((G * t) . a) )
assume A3: Hom (a,b) <> {} ; ::_thesis: for b1 being Morphism of a,b holds ((G * t) . b) * ((G * F1) /. b1) = ((G * F2) /. b1) * ((G * t) . a)
A4: Hom (((G * F1) . a),((G * F1) . b)) <> {} by A3, CAT_1:84;
A5: Hom (((G * F2) . a),((G * F2) . b)) <> {} by A3, CAT_1:84;
A6: Hom (((G * F1) . a),((G * F2) . a)) <> {} by A2, NATTRA_1:def_2;
let f be Morphism of a,b; ::_thesis: ((G * t) . b) * ((G * F1) /. f) = ((G * F2) /. f) * ((G * t) . a)
A7: Hom ((F1 . b),(F2 . b)) <> {} by A1, NATTRA_1:def_2;
then A8: Hom ((G . (F1 . b)),(G . (F2 . b))) <> {} by CAT_1:84;
A9: Hom ((F1 . a),(F2 . a)) <> {} by A1, NATTRA_1:def_2;
then A10: Hom ((G . (F1 . a)),(G . (F2 . a))) <> {} by CAT_1:84;
A11: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;
then A12: Hom ((G . (F2 . a)),(G . (F2 . b))) <> {} by CAT_1:84;
A13: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84;
then A14: Hom ((G . (F1 . a)),(G . (F1 . b))) <> {} by CAT_1:84;
Hom (((G * F1) . b),((G * F2) . b)) <> {} by A2, NATTRA_1:def_2;
hence ((G * t) . b) * ((G * F1) /. f) = ((G * t) . b) (*) ((G * F1) /. f) by A4, CAT_1:def_13
.= ((G * t) . b) (*) (G /. (F1 /. f)) by A3, NATTRA_1:11
.= (G /. (t . b)) (*) (G /. (F1 /. f)) by A1, Th21
.= (G /. (t . b)) * (G /. (F1 /. f)) by A8, A14, CAT_1:def_13
.= G /. ((t . b) * (F1 /. f)) by A7, A13, NATTRA_1:13
.= G /. ((F2 /. f) * (t . a)) by B1, A3, NATTRA_1:def_8
.= (G /. (F2 /. f)) * (G /. (t . a)) by A9, A11, NATTRA_1:13
.= (G /. (F2 /. f)) (*) (G /. (t . a)) by A12, A10, CAT_1:def_13
.= (G /. (F2 /. f)) (*) ((G * t) . a) by A1, Th21
.= ((G * F2) /. f) (*) ((G * t) . a) by A3, NATTRA_1:11
.= ((G * F2) /. f) * ((G * t) . a) by A6, A5, CAT_1:def_13 ;
::_thesis: verum
end;
hence G * t is natural_transformation of G * F1,G * F2 ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def7 defines * ISOCAT_1:def_7_:_
for A, B, C 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
for G being Functor of B,C holds G * t = G * t;
theorem Th23: :: ISOCAT_1:23
for A, B, C 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
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
proof
let A, B, C 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
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a) )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
then A2: F1 is_transformable_to F2 by NATTRA_1:def_7;
let t be natural_transformation of F1,F2; ::_thesis: for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let G be Functor of B,C; ::_thesis: for a being Object of A holds (G * t) . a = G /. (t . a)
let a be Object of A; ::_thesis: (G * t) . a = G /. (t . a)
thus (G * t) . a = (G * t) . a by A1, Def7
.= G /. (t . a) by A2, Th21 ; ::_thesis: verum
end;
definition
let A, B, C be Category;
let G1, G2 be Functor of B,C;
assume B1: G1 is_naturally_transformable_to G2 ;
let F be Functor of A,B;
let t be natural_transformation of G1,G2;
funct * F -> natural_transformation of G1 * F,G2 * F equals :Def8: :: ISOCAT_1:def 8
t * F;
coherence
t * F is natural_transformation of G1 * F,G2 * F
proof
A1: G1 is_transformable_to G2 by B1, NATTRA_1:def_7;
t * F is natural_transformation of G1 * F,G2 * F
proof
thus G1 * F is_naturally_transformable_to G2 * F by B1, Th22; :: according to NATTRA_1:def_8 ::_thesis: for b1, b2 being M2( the carrier of A) holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds ((t * F) . b2) * ((G1 * F) /. b3) = ((G2 * F) /. b3) * ((t * F) . b1) )
then A2: G1 * F is_transformable_to G2 * F by NATTRA_1:def_7;
let a, b be Object of A; ::_thesis: ( Hom (a,b) = {} or for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b1) = ((G2 * F) /. b1) * ((t * F) . a) )
A3: Hom (((G1 * F) . b),((G2 * F) . b)) <> {} by A2, NATTRA_1:def_2;
A4: Hom (((G1 * F) . a),((G2 * F) . a)) <> {} by A2, NATTRA_1:def_2;
assume A5: Hom (a,b) <> {} ; ::_thesis: for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b1) = ((G2 * F) /. b1) * ((t * F) . a)
then A6: Hom (((G2 * F) . a),((G2 * F) . b)) <> {} by CAT_1:84;
let f be Morphism of a,b; ::_thesis: ((t * F) . b) * ((G1 * F) /. f) = ((G2 * F) /. f) * ((t * F) . a)
A7: Hom ((F . a),(F . b)) <> {} by A5, CAT_1:84;
then A8: Hom ((G1 . (F . a)),(G1 . (F . b))) <> {} by CAT_1:84;
A9: Hom ((G1 . (F . a)),(G2 . (F . a))) <> {} by A1, NATTRA_1:def_2;
A10: Hom ((G1 . (F . b)),(G2 . (F . b))) <> {} by A1, NATTRA_1:def_2;
A11: Hom ((G2 . (F . a)),(G2 . (F . b))) <> {} by A7, CAT_1:84;
Hom (((G1 * F) . a),((G1 * F) . b)) <> {} by A5, CAT_1:84;
hence ((t * F) . b) * ((G1 * F) /. f) = ((t * F) . b) (*) ((G1 * F) /. f) by A3, CAT_1:def_13
.= ((t * F) . b) (*) (G1 /. (F /. f)) by A5, NATTRA_1:11
.= (t . (F . b)) (*) (G1 /. (F /. f)) by A1, Th20
.= (t . (F . b)) * (G1 /. (F /. f)) by A10, A8, CAT_1:def_13
.= (G2 /. (F /. f)) * (t . (F . a)) by B1, A7, NATTRA_1:def_8
.= (G2 /. (F /. f)) (*) (t . (F . a)) by A11, A9, CAT_1:def_13
.= (G2 /. (F /. f)) (*) ((t * F) . a) by A1, Th20
.= ((G2 * F) /. f) (*) ((t * F) . a) by A5, NATTRA_1:11
.= ((G2 * F) /. f) * ((t * F) . a) by A6, A4, CAT_1:def_13 ;
::_thesis: verum
end;
hence t * F is natural_transformation of G1 * F,G2 * F ; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def8 defines * ISOCAT_1:def_8_:_
for A, B, C being Category
for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds
for F being Functor of A,B
for t being natural_transformation of G1,G2 holds t * F = t * F;
theorem Th24: :: ISOCAT_1:24
for B, C, A being Category
for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds
for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
proof
let B, C, A be Category; ::_thesis: for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds
for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let G1, G2 be Functor of B,C; ::_thesis: ( G1 is_naturally_transformable_to G2 implies for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a) )
assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
then A2: G1 is_transformable_to G2 by NATTRA_1:def_7;
let F be Functor of A,B; ::_thesis: for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let t be natural_transformation of G1,G2; ::_thesis: for a being Object of A holds (t * F) . a = t . (F . a)
let a be Object of A; ::_thesis: (t * F) . a = t . (F . a)
thus (t * F) . a = (t * F) . a by A1, Def8
.= t . (F . a) by A2, Th20 ; ::_thesis: verum
end;
theorem Th25: :: ISOCAT_1:25
for B, A being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {}
proof
let B, A be Category; ::_thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {}
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {}
let a be Object of A; ::_thesis: Hom ((F1 . a),(F2 . a)) <> {}
F1 is_transformable_to F2 by A1, NATTRA_1:def_7;
hence Hom ((F1 . a),(F2 . a)) <> {} by NATTRA_1:def_2; ::_thesis: verum
end;
theorem Th26: :: ISOCAT_1:26
for B, A being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t1, t2 being natural_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_naturally_transformable_to F2 holds
for t1, t2 being natural_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_naturally_transformable_to F2 implies for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2 )
assume F1 is_naturally_transformable_to F2 ; ::_thesis: for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
then F1 is_transformable_to F2 by NATTRA_1:def_7;
hence for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2 by NATTRA_1:19; ::_thesis: verum
end;
theorem Th27: :: ISOCAT_1:27
for C, A, B being Category
for F1, F2, F3 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
proof
let C, A, B be Category; ::_thesis: for F1, F2, F3 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let F1, F2, F3 be Functor of A,B; ::_thesis: for G being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let G be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let s be natural_transformation of F1,F2; ::_thesis: for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let s9 be natural_transformation of F2,F3; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies G * (s9 `*` s) = (G * s9) `*` (G * s) )
assume A1: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) ; ::_thesis: G * (s9 `*` s) = (G * s9) `*` (G * s)
then A2: ( G * F1 is_naturally_transformable_to G * F2 & G * F2 is_naturally_transformable_to G * F3 ) by Th22;
now__::_thesis:_for_a_being_Object_of_A_holds_(G_*_(s9_`*`_s))_._a_=_((G_*_s9)_`*`_(G_*_s))_._a
let a be Object of A; ::_thesis: (G * (s9 `*` s)) . a = ((G * s9) `*` (G * s)) . a
A3: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76;
A4: G . (F3 . a) = (G * F3) . a by CAT_1:76;
A5: ( Hom ((F1 . a),(F2 . a)) <> {} & Hom ((F2 . a),(F3 . a)) <> {} ) by A1, Th25;
A6: ( G /. (s9 . a) = (G * s9) . a & G /. (s . a) = (G * s) . a ) by A1, Th23;
thus (G * (s9 `*` s)) . a = G /. ((s9 `*` s) . a) by A1, Th23, NATTRA_1:23
.= G /. ((s9 . a) * (s . a)) by A1, NATTRA_1:25
.= (G /. (s9 . a)) * (G /. (s . a)) by A5, NATTRA_1:13
.= ((G * s9) `*` (G * s)) . a by A2, A6, A3, A4, NATTRA_1:25 ; ::_thesis: verum
end;
hence G * (s9 `*` s) = (G * s9) `*` (G * s) by A2, Th26, NATTRA_1:23; ::_thesis: verum
end;
theorem Th28: :: ISOCAT_1:28
for A, B, C being Category
for F being Functor of A,B
for G1, G2, G3 being Functor of B,C
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G1, G2, G3 being Functor of B,C
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let F be Functor of A,B; ::_thesis: for G1, G2, G3 being Functor of B,C
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let G1, G2, G3 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let t be natural_transformation of G1,G2; ::_thesis: for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let t9 be natural_transformation of G2,G3; ::_thesis: ( G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t9 `*` t) * F = (t9 * F) `*` (t * F) )
assume A1: ( G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 ) ; ::_thesis: (t9 `*` t) * F = (t9 * F) `*` (t * F)
then A2: ( G1 * F is_naturally_transformable_to G2 * F & G2 * F is_naturally_transformable_to G3 * F ) by Th22;
now__::_thesis:_for_a_being_Object_of_A_holds_((t9_`*`_t)_*_F)_._a_=_((t9_*_F)_`*`_(t_*_F))_._a
let a be Object of A; ::_thesis: ((t9 `*` t) * F) . a = ((t9 * F) `*` (t * F)) . a
A3: ( G1 . (F . a) = (G1 * F) . a & G2 . (F . a) = (G2 * F) . a ) by CAT_1:76;
A4: G3 . (F . a) = (G3 * F) . a by CAT_1:76;
A5: ( t9 . (F . a) = (t9 * F) . a & t . (F . a) = (t * F) . a ) by A1, Th24;
thus ((t9 `*` t) * F) . a = (t9 `*` t) . (F . a) by A1, Th24, NATTRA_1:23
.= (t9 . (F . a)) * (t . (F . a)) by A1, NATTRA_1:25
.= ((t9 * F) `*` (t * F)) . a by A2, A5, A3, A4, NATTRA_1:25 ; ::_thesis: verum
end;
hence (t9 `*` t) * F = (t9 * F) `*` (t * F) by A2, Th26, NATTRA_1:23; ::_thesis: verum
end;
theorem Th29: :: ISOCAT_1:29
for A, B, C, D being Category
for F being Functor of A,B
for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
proof
let A, B, C, D be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let F be Functor of A,B; ::_thesis: for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let G be Functor of B,C; ::_thesis: for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let H1, H2 be Functor of C,D; ::_thesis: for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let u be natural_transformation of H1,H2; ::_thesis: ( H1 is_naturally_transformable_to H2 implies (u * G) * F = u * (G * F) )
assume A1: H1 is_naturally_transformable_to H2 ; ::_thesis: (u * G) * F = u * (G * F)
A2: H1 * (G * F) = (H1 * G) * F by RELAT_1:36;
then reconsider v = u * (G * F) as natural_transformation of (H1 * G) * F,(H2 * G) * F by RELAT_1:36;
A3: H2 * (G * F) = (H2 * G) * F by RELAT_1:36;
A4: now__::_thesis:_for_a_being_Object_of_A_holds_((u_*_G)_*_F)_._a_=_v_._a
let a be Object of A; ::_thesis: ((u * G) * F) . a = v . a
thus ((u * G) * F) . a = (u * G) . (F . a) by A1, Th22, Th24
.= u . (G . (F . a)) by A1, Th24
.= u . ((G * F) . a) by CAT_1:76
.= v . a by A1, A2, A3, Th24 ; ::_thesis: verum
end;
H1 * G is_naturally_transformable_to H2 * G by A1, Th22;
hence (u * G) * F = u * (G * F) by A4, Th22, Th26; ::_thesis: verum
end;
theorem Th30: :: ISOCAT_1:30
for A, D, B, C being Category
for F being Functor of A,B
for G1, G2 being Functor of B,C
for H being Functor of C,D
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)
proof
let A, D, B, C be Category; ::_thesis: for F being Functor of A,B
for G1, G2 being Functor of B,C
for H being Functor of C,D
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)
let F be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C
for H being Functor of C,D
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)
let G1, G2 be Functor of B,C; ::_thesis: for H being Functor of C,D
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)
let H be Functor of C,D; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)
let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies (H * t) * F = H * (t * F) )
assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: (H * t) * F = H * (t * F)
A2: H * (G1 * F) = (H * G1) * F by RELAT_1:36;
then reconsider v = H * (t * F) as natural_transformation of (H * G1) * F,(H * G2) * F by RELAT_1:36;
A3: H * (G2 * F) = (H * G2) * F by RELAT_1:36;
A4: now__::_thesis:_for_a_being_Object_of_A_holds_((H_*_t)_*_F)_._a_=_v_._a
let a be Object of A; ::_thesis: ((H * t) * F) . a = v . a
A5: ( G1 . (F . a) = (G1 * F) . a & G2 . (F . a) = (G2 * F) . a ) by CAT_1:76;
thus ((H * t) * F) . a = (H * t) . (F . a) by A1, Th22, Th24
.= H /. (t . (F . a)) by A1, Th23
.= H /. ((t * F) . a) by A1, A5, Th24
.= v . a by A1, A2, A3, Th22, Th23 ; ::_thesis: verum
end;
H * G1 is_naturally_transformable_to H * G2 by A1, Th22;
hence (H * t) * F = H * (t * F) by A4, Th22, Th26; ::_thesis: verum
end;
theorem Th31: :: ISOCAT_1:31
for C, D, A, B being Category
for F1, F2 being Functor of A,B
for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
proof
let C, D, A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let F1, F2 be Functor of A,B; ::_thesis: for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let G be Functor of B,C; ::_thesis: for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let H be Functor of C,D; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies (H * G) * s = H * (G * s) )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: (H * G) * s = H * (G * s)
A2: H * (G * F1) = (H * G) * F1 by RELAT_1:36;
then reconsider v = H * (G * s) as natural_transformation of (H * G) * F1,(H * G) * F2 by RELAT_1:36;
A3: H * (G * F2) = (H * G) * F2 by RELAT_1:36;
now__::_thesis:_for_a_being_Object_of_A_holds_((H_*_G)_*_s)_._a_=_v_._a
let a be Object of A; ::_thesis: ((H * G) * s) . a = v . a
A4: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76;
A5: Hom ((F1 . a),(F2 . a)) <> {} by A1, Th25;
thus ((H * G) * s) . a = (H * G) /. (s . a) by A1, Th23
.= H /. (G /. (s . a)) by A5, NATTRA_1:11
.= H /. ((G * s) . a) by A1, A4, Th23
.= v . a by A1, A2, A3, Th22, Th23 ; ::_thesis: verum
end;
hence (H * G) * s = H * (G * s) by A1, Th22, Th26; ::_thesis: verum
end;
theorem Th32: :: ISOCAT_1:32
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C holds (id G) * F = id (G * F)
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,C holds (id G) * F = id (G * F)
let F be Functor of A,B; ::_thesis: for G being Functor of B,C holds (id G) * F = id (G * F)
let G be Functor of B,C; ::_thesis: (id G) * F = id (G * F)
now__::_thesis:_for_a_being_Object_of_A_holds_((id_G)_*_F)_._a_=_(id_(G_*_F))_._a
let a be Object of A; ::_thesis: ((id G) * F) . a = (id (G * F)) . a
thus ((id G) * F) . a = (id G) . (F . a) by Th24
.= id (G . (F . a)) by NATTRA_1:20
.= id ((G * F) . a) by CAT_1:76
.= (id (G * F)) . a by NATTRA_1:20 ; ::_thesis: verum
end;
hence (id G) * F = id (G * F) by Th26; ::_thesis: verum
end;
theorem Th33: :: ISOCAT_1:33
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C holds G * (id F) = id (G * F)
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,C holds G * (id F) = id (G * F)
let F be Functor of A,B; ::_thesis: for G being Functor of B,C holds G * (id F) = id (G * F)
let G be Functor of B,C; ::_thesis: G * (id F) = id (G * F)
now__::_thesis:_for_a_being_Object_of_A_holds_(G_*_(id_F))_._a_=_(id_(G_*_F))_._a
let a be Object of A; ::_thesis: (G * (id F)) . a = (id (G * F)) . a
thus (G * (id F)) . a = G /. ((id F) . a) by Th23
.= G /. (id (F . a)) by NATTRA_1:20
.= id (G . (F . a)) by NATTRA_1:15
.= id ((G * F) . a) by CAT_1:76
.= (id (G * F)) . a by NATTRA_1:20 ; ::_thesis: verum
end;
hence G * (id F) = id (G * F) by Th26; ::_thesis: verum
end;
theorem Th34: :: ISOCAT_1:34
for C, B being Category
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * (id B) = t
proof
let C, B be Category; ::_thesis: for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * (id B) = t
let G1, G2 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * (id B) = t
let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies t * (id B) = t )
assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: t * (id B) = t
A2: G1 * (id B) = G1 by FUNCT_2:17;
then reconsider s = t * (id B) as natural_transformation of G1,G2 by FUNCT_2:17;
A3: G2 * (id B) = G2 by FUNCT_2:17;
now__::_thesis:_for_b_being_Object_of_B_holds_s_._b_=_t_._b
let b be Object of B; ::_thesis: s . b = t . b
thus s . b = t . ((id B) . b) by A1, A2, A3, Th24
.= t . b by CAT_1:79 ; ::_thesis: verum
end;
hence t * (id B) = t by A1, Th26; ::_thesis: verum
end;
theorem Th35: :: ISOCAT_1:35
for A, B being Category
for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id B) * s = s
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id B) * s = s
let F1, F2 be Functor of A,B; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id B) * s = s
let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies (id B) * s = s )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: (id B) * s = s
A2: (id B) * F1 = F1 by FUNCT_2:17;
then reconsider t = (id B) * s as natural_transformation of F1,F2 by FUNCT_2:17;
A3: (id B) * F2 = F2 by FUNCT_2:17;
now__::_thesis:_for_a_being_Object_of_A_holds_t_._a_=_s_._a
let a be Object of A; ::_thesis: t . a = s . a
A4: Hom ((F1 . a),(F2 . a)) <> {} by A1, Th25;
thus t . a = (id B) /. (s . a) by A1, A2, A3, Th23
.= (id B) . (s . a) by A4, CAT_3:def_10
.= s . a by FUNCT_1:18 ; ::_thesis: verum
end;
hence (id B) * s = s by A1, Th26; ::_thesis: verum
end;
definition
let A, B, C be Category;
let F1, F2 be Functor of A,B;
let G1, G2 be Functor of B,C;
let s be natural_transformation of F1,F2;
let t be natural_transformation of G1,G2;
funct (#) s -> natural_transformation of G1 * F1,G2 * F2 equals :: ISOCAT_1:def 9
(t * F2) `*` (G1 * s);
correctness
coherence
(t * F2) `*` (G1 * s) is natural_transformation of G1 * F1,G2 * F2;
;
end;
:: deftheorem defines (#) ISOCAT_1:def_9_:_
for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 holds t (#) s = (t * F2) `*` (G1 * s);
theorem Th36: :: ISOCAT_1:36
for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
proof
let A, B, C be Category; ::_thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let G1, G2 be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let s be natural_transformation of F1,F2; ::_thesis: for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let t be natural_transformation of G1,G2; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies t (#) s = (G2 * s) `*` (t * F1) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; ::_thesis: t (#) s = (G2 * s) `*` (t * F1)
A3: ( G1 * F1 is_naturally_transformable_to G1 * F2 & G1 * F2 is_naturally_transformable_to G2 * F2 ) by A1, A2, Th22;
A4: ( G2 * F1 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G2 * F1 ) by A1, A2, Th22;
now__::_thesis:_for_a_being_Object_of_A_holds_((t_*_F2)_`*`_(G1_*_s))_._a_=_((G2_*_s)_`*`_(t_*_F1))_._a
let a be Object of A; ::_thesis: ((t * F2) `*` (G1 * s)) . a = ((G2 * s) `*` (t * F1)) . a
A5: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by CAT_1:76;
A6: (G2 * F2) . a = G2 . (F2 . a) by CAT_1:76;
A7: ( (G2 * s) . a = G2 /. (s . a) & (G1 * F1) . a = G1 . (F1 . a) ) by A1, Th23, CAT_1:76;
A8: ( Hom ((F1 . a),(F2 . a)) <> {} & (t * F1) . a = t . (F1 . a) ) by A1, A2, Th24, Th25;
A9: ( (G2 * F1) . a = G2 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by CAT_1:76;
( (t * F2) . a = t . (F2 . a) & (G1 * s) . a = G1 /. (s . a) ) by A1, A2, Th23, Th24;
hence ((t * F2) `*` (G1 * s)) . a = (t . (F2 . a)) * (G1 /. (s . a)) by A3, A5, A6, NATTRA_1:25
.= ((G2 * s) . a) * ((t * F1) . a) by A2, A8, A7, A9, NATTRA_1:def_8
.= ((G2 * s) `*` (t * F1)) . a by A4, NATTRA_1:25 ;
::_thesis: verum
end;
hence t (#) s = (G2 * s) `*` (t * F1) by A3, Th26, NATTRA_1:23; ::_thesis: verum
end;
theorem :: ISOCAT_1:37
for A, B being Category
for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id (id B)) (#) s = s
proof
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id (id B)) (#) s = s
let F1, F2 be Functor of A,B; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id (id B)) (#) s = s
let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies (id (id B)) (#) s = s )
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: (id (id B)) (#) s = s
then A2: (id B) * F1 is_naturally_transformable_to (id B) * F2 by Th22;
thus (id (id B)) (#) s = (id ((id B) * F2)) `*` ((id B) * s) by Th32
.= (id B) * s by A2, NATTRA_1:24
.= s by A1, Th35 ; ::_thesis: verum
end;
theorem :: ISOCAT_1:38
for C, B being Category
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t (#) (id (id B)) = t
proof
let C, B be Category; ::_thesis: for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t (#) (id (id B)) = t
let G1, G2 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t (#) (id (id B)) = t
let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies t (#) (id (id B)) = t )
assume A1: G1 is_naturally_transformable_to G2 ; ::_thesis: t (#) (id (id B)) = t
then A2: G1 * (id B) is_naturally_transformable_to G2 * (id B) by Th22;
thus t (#) (id (id B)) = (t * (id B)) `*` (id (G1 * (id B))) by Th33
.= t * (id B) by A2, NATTRA_1:24
.= t by A1, Th34 ; ::_thesis: verum
end;
theorem :: ISOCAT_1:39
for A, B, C, D being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
proof
let A, B, C, D be Category; ::_thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let F1, F2 be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C
for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let G1, G2 be Functor of B,C; ::_thesis: for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let H1, H2 be Functor of C,D; ::_thesis: for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let s be natural_transformation of F1,F2; ::_thesis: for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let t be natural_transformation of G1,G2; ::_thesis: for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
let u be natural_transformation of H1,H2; ::_thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 implies u (#) (t (#) s) = (u (#) t) (#) s )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 and
A3: H1 is_naturally_transformable_to H2 ; ::_thesis: u (#) (t (#) s) = (u (#) t) (#) s
A4: ( u * (G2 * F2) = (u * G2) * F2 & H1 * (t * F2) = (H1 * t) * F2 ) by A2, A3, Th29, Th30;
A5: H1 * G1 is_naturally_transformable_to H1 * G2 by A2, Th22;
then A6: (H1 * G1) * F2 is_naturally_transformable_to (H1 * G2) * F2 by Th22;
A7: ( H1 * (G1 * s) = (H1 * G1) * s & (H1 * G1) * F1 is_naturally_transformable_to (H1 * G1) * F2 ) by A1, Th22, Th31;
A8: ( (H1 * G1) * F1 = H1 * (G1 * F1) & (H1 * G1) * F2 = H1 * (G1 * F2) ) by RELAT_1:36;
A9: H1 * G2 is_naturally_transformable_to H2 * G2 by A3, Th22;
then A10: (H1 * G2) * F2 is_naturally_transformable_to (H2 * G2) * F2 by Th22;
A11: ( (H1 * G2) * F2 = H1 * (G2 * F2) & (H2 * G2) * F2 = H2 * (G2 * F2) ) by RELAT_1:36;
( G1 * F2 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G1 * F2 ) by A1, A2, Th22;
hence u (#) (t (#) s) = (u * (G2 * F2)) `*` ((H1 * (t * F2)) `*` (H1 * (G1 * s))) by Th27
.= (((u * G2) * F2) `*` ((H1 * t) * F2)) `*` ((H1 * G1) * s) by A8, A11, A4, A7, A6, A10, NATTRA_1:26
.= (u (#) t) (#) s by A5, A9, Th28 ;
::_thesis: verum
end;
theorem :: ISOCAT_1:40
for A, B, C being Category
for F being Functor of A,B
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * F = t (#) (id F)
proof
let A, B, C be Category; ::_thesis: for F being Functor of A,B
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * F = t (#) (id F)
let F be Functor of A,B; ::_thesis: for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * F = t (#) (id F)
let G1, G2 be Functor of B,C; ::_thesis: for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * F = t (#) (id F)
let t be natural_transformation of G1,G2; ::_thesis: ( G1 is_naturally_transformable_to G2 implies t * F = t (#) (id F) )
assume G1 is_naturally_transformable_to G2 ; ::_thesis: t * F = t (#) (id F)
then G1 * F is_naturally_transformable_to G2 * F by Th22;
hence t * F = (t * F) `*` (id (G1 * F)) by NATTRA_1:24
.= t (#) (id F) by Th33 ;
::_thesis: verum
end;
theorem :: ISOCAT_1:41
for C, A, B being Category
for F1, F2 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
proof
let C, A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
let F1, F2 be Functor of A,B; ::_thesis: for G being Functor of B,C
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
let G be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
let s be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 implies G * s = (id G) (#) s )
assume F1 is_naturally_transformable_to F2 ; ::_thesis: G * s = (id G) (#) s
then G * F1 is_naturally_transformable_to G * F2 by Th22;
hence G * s = (id (G * F2)) `*` (G * s) by NATTRA_1:24
.= (id G) (#) s by Th32 ;
::_thesis: verum
end;
theorem :: ISOCAT_1:42
for A, B, C being Category
for F1, F2, F3 being Functor of A,B
for G1, G2, G3 being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
proof
let A, B, C be Category; ::_thesis: for F1, F2, F3 being Functor of A,B
for G1, G2, G3 being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let F1, F2, F3 be Functor of A,B; ::_thesis: for G1, G2, G3 being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let G1, G2, G3 be Functor of B,C; ::_thesis: for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let s be natural_transformation of F1,F2; ::_thesis: for s9 being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let s9 be natural_transformation of F2,F3; ::_thesis: for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let t be natural_transformation of G1,G2; ::_thesis: for t9 being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
let t9 be natural_transformation of G2,G3; ::_thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_naturally_transformable_to F3 and
A3: G1 is_naturally_transformable_to G2 and
A4: G2 is_naturally_transformable_to G3 ; ::_thesis: (t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
A5: ( t9 (#) s9 = (G3 * s9) `*` (t9 * F2) & t (#) s = (G2 * s) `*` (t * F1) ) by A1, A2, A3, A4, Th36;
A6: G1 * F1 is_naturally_transformable_to G2 * F1 by A3, Th22;
A7: G2 * F1 is_naturally_transformable_to G2 * F2 by A1, Th22;
then A8: G1 * F1 is_naturally_transformable_to G2 * F2 by A6, NATTRA_1:23;
A9: G2 * F2 is_naturally_transformable_to G3 * F2 by A4, Th22;
A10: G1 is_naturally_transformable_to G3 by A3, A4, NATTRA_1:23;
then A11: G1 * F1 is_naturally_transformable_to G3 * F1 by Th22;
A12: G3 * F1 is_naturally_transformable_to G3 * F2 by A1, Th22;
A13: G2 * F1 is_naturally_transformable_to G3 * F1 by A4, Th22;
A14: G3 * F2 is_naturally_transformable_to G3 * F3 by A2, Th22;
F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1:23;
hence (t9 `*` t) (#) (s9 `*` s) = (G3 * (s9 `*` s)) `*` ((t9 `*` t) * F1) by A10, Th36
.= ((G3 * s9) `*` (G3 * s)) `*` ((t9 `*` t) * F1) by A1, A2, Th27
.= ((G3 * s9) `*` (G3 * s)) `*` ((t9 * F1) `*` (t * F1)) by A3, A4, Th28
.= (G3 * s9) `*` ((G3 * s) `*` ((t9 * F1) `*` (t * F1))) by A14, A12, A11, NATTRA_1:26
.= (G3 * s9) `*` (((G3 * s) `*` (t9 * F1)) `*` (t * F1)) by A12, A6, A13, NATTRA_1:26
.= (G3 * s9) `*` ((t9 (#) s) `*` (t * F1)) by A1, A4, Th36
.= (G3 * s9) `*` ((t9 * F2) `*` ((G2 * s) `*` (t * F1))) by A6, A9, A7, NATTRA_1:26
.= (t9 (#) s9) `*` (t (#) s) by A14, A9, A8, A5, NATTRA_1:26 ;
::_thesis: verum
end;
theorem Th43: :: ISOCAT_1:43
for A, B, C, D being Category
for F being Functor of A,B
for G being Functor of C,D
for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
proof
let A, B, C, D be Category; ::_thesis: for F being Functor of A,B
for G being Functor of C,D
for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
let F be Functor of A,B; ::_thesis: for G being Functor of C,D
for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
let G be Functor of C,D; ::_thesis: for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )
let I, J be Functor of B,C; ::_thesis: ( I ~= J implies ( G * I ~= G * J & I * F ~= J * F ) )
assume A1: I is_naturally_transformable_to J ; :: according to NATTRA_1:def_11 ::_thesis: ( for b1 being natural_transformation of I,J holds not b1 is invertible or ( G * I ~= G * J & I * F ~= J * F ) )
given t being natural_transformation of I,J such that A2: t is invertible ; ::_thesis: ( G * I ~= G * J & I * F ~= J * F )
thus G * I ~= G * J ::_thesis: I * F ~= J * F
proof
thus G * I is_naturally_transformable_to G * J by A1, Th22; :: according to NATTRA_1:def_11 ::_thesis: ex b1 being natural_transformation of G * I,G * J st b1 is invertible
take G * t ; ::_thesis: G * t is invertible
let b be Object of B; :: according to NATTRA_1:def_10 ::_thesis: (G * t) . b is invertible
A3: t . b is invertible by A2, NATTRA_1:def_10;
A4: ( G . (I . b) = (G * I) . b & G . (J . b) = (G * J) . b ) by CAT_1:76;
(G * t) . b = G /. (t . b) by A1, Th23;
hence (G * t) . b is invertible by A3, Th3, A4; ::_thesis: verum
end;
thus I * F is_naturally_transformable_to J * F by A1, Th22; :: according to NATTRA_1:def_11 ::_thesis: ex b1 being natural_transformation of I * F,J * F st b1 is invertible
take t * F ; ::_thesis: t * F is invertible
let a be Object of A; :: according to NATTRA_1:def_10 ::_thesis: (t * F) . a is invertible
A5: ( I . (F . a) = (I * F) . a & J . (F . a) = (J * F) . a ) by CAT_1:76;
(t * F) . a = t . (F . a) by A1, Th24;
hence (t * F) . a is invertible by A2, A5, NATTRA_1:def_10; ::_thesis: verum
end;
theorem Th44: :: ISOCAT_1:44
for A, B being Category
for F being Functor of A,B
for G being Functor of B,A
for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
proof
let A, B be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,A
for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
let F be Functor of A,B; ::_thesis: for G being Functor of B,A
for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
let G be Functor of B,A; ::_thesis: for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
let I be Functor of A,A; ::_thesis: ( I ~= id A implies ( F * I ~= F & I * G ~= G ) )
( F * (id A) = F & (id A) * G = G ) by FUNCT_2:17;
hence ( I ~= id A implies ( F * I ~= F & I * G ~= G ) ) by Th43; ::_thesis: verum
end;
definition
let A, B be Category;
predA is_equivalent_with B means :Def10: :: ISOCAT_1:def 10
ex F being Functor of A,B ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B );
reflexivity
for A being Category ex F, G being Functor of A,A st
( G * F ~= id A & F * G ~= id A )
proof
let A be Category; ::_thesis: ex F, G being Functor of A,A st
( G * F ~= id A & F * G ~= id A )
take id A ; ::_thesis: ex G being Functor of A,A st
( G * (id A) ~= id A & (id A) * G ~= id A )
take id A ; ::_thesis: ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A )
thus ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) by FUNCT_2:17; ::_thesis: verum
end;
symmetry
for A, B being Category st ex F being Functor of A,B ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B ) holds
ex F being Functor of B,A ex G being Functor of A,B st
( G * F ~= id B & F * G ~= id A ) ;
end;
:: deftheorem Def10 defines is_equivalent_with ISOCAT_1:def_10_:_
for A, B being Category holds
( A is_equivalent_with B iff ex F being Functor of A,B ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B ) );
notation
let A, B be Category;
synonym A,B are_equivalent for A is_equivalent_with B;
end;
theorem :: ISOCAT_1:45
for A, B being Category st A ~= B holds
A is_equivalent_with B
proof
let A, B be Category; ::_thesis: ( A ~= B implies A is_equivalent_with B )
given F being Functor of A,B such that A1: F is isomorphic ; :: according to ISOCAT_1:def_4 ::_thesis: A is_equivalent_with B
take F ; :: according to ISOCAT_1:def_10 ::_thesis: ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B )
take F " ; ::_thesis: ( (F ") * F ~= id A & F * (F ") ~= id B )
thus ( (F ") * F ~= id A & F * (F ") ~= id B ) by A1, Th13; ::_thesis: verum
end;
theorem Th46: :: ISOCAT_1:46
for A, B, C being Category st A,B are_equivalent & B,C are_equivalent holds
A,C are_equivalent
proof
let A, B, C be Category; ::_thesis: ( A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent )
given F1 being Functor of A,B, G1 being Functor of B,A such that A1: G1 * F1 ~= id A and
A2: F1 * G1 ~= id B ; :: according to ISOCAT_1:def_10 ::_thesis: ( not B,C are_equivalent or A,C are_equivalent )
given F2 being Functor of B,C, G2 being Functor of C,B such that A3: G2 * F2 ~= id B and
A4: F2 * G2 ~= id C ; :: according to ISOCAT_1:def_10 ::_thesis: A,C are_equivalent
take F2 * F1 ; :: according to ISOCAT_1:def_10 ::_thesis: ex G being Functor of C,A st
( G * (F2 * F1) ~= id A & (F2 * F1) * G ~= id C )
take G1 * G2 ; ::_thesis: ( (G1 * G2) * (F2 * F1) ~= id A & (F2 * F1) * (G1 * G2) ~= id C )
(G1 * G2) * F2 = G1 * (G2 * F2) by RELAT_1:36;
then A5: (G1 * G2) * F2 ~= G1 by A3, Th44;
(G1 * G2) * (F2 * F1) = ((G1 * G2) * F2) * F1 by RELAT_1:36;
then (G1 * G2) * (F2 * F1) ~= G1 * F1 by A5, Th43;
hence (G1 * G2) * (F2 * F1) ~= id A by A1, NATTRA_1:29; ::_thesis: (F2 * F1) * (G1 * G2) ~= id C
(F2 * F1) * G1 = F2 * (F1 * G1) by RELAT_1:36;
then A6: (F2 * F1) * G1 ~= F2 by A2, Th44;
(F2 * F1) * (G1 * G2) = ((F2 * F1) * G1) * G2 by RELAT_1:36;
then (F2 * F1) * (G1 * G2) ~= F2 * G2 by A6, Th43;
hence (F2 * F1) * (G1 * G2) ~= id C by A4, NATTRA_1:29; ::_thesis: verum
end;
definition
let A, B be Category;
assume A1: A,B are_equivalent ;
mode Equivalence of A,B -> Functor of A,B means :Def11: :: ISOCAT_1:def 11
ex G being Functor of B,A st
( G * it ~= id A & it * G ~= id B );
existence
ex b1 being Functor of A,B ex G being Functor of B,A st
( G * b1 ~= id A & b1 * G ~= id B ) by A1, Def10;
end;
:: deftheorem Def11 defines Equivalence ISOCAT_1:def_11_:_
for A, B being Category st A,B are_equivalent holds
for b3 being Functor of A,B holds
( b3 is Equivalence of A,B iff ex G being Functor of B,A st
( G * b3 ~= id A & b3 * G ~= id B ) );
theorem :: ISOCAT_1:47
for A being Category holds id A is Equivalence of A,A
proof
let A be Category; ::_thesis: id A is Equivalence of A,A
thus A is_equivalent_with A ; :: according to ISOCAT_1:def_11 ::_thesis: ex G being Functor of A,A st
( G * (id A) ~= id A & (id A) * G ~= id A )
take id A ; ::_thesis: ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A )
thus ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) by FUNCT_2:17; ::_thesis: verum
end;
theorem :: ISOCAT_1:48
for A, B, C being Category st A,B are_equivalent & B,C are_equivalent holds
for F being Equivalence of A,B
for G being Equivalence of B,C holds G * F is Equivalence of A,C
proof
let A, B, C be Category; ::_thesis: ( A,B are_equivalent & B,C are_equivalent implies for F being Equivalence of A,B
for G being Equivalence of B,C holds G * F is Equivalence of A,C )
assume that
A1: A,B are_equivalent and
A2: B,C are_equivalent ; ::_thesis: for F being Equivalence of A,B
for G being Equivalence of B,C holds G * F is Equivalence of A,C
let F be Equivalence of A,B; ::_thesis: for G being Equivalence of B,C holds G * F is Equivalence of A,C
let G be Equivalence of B,C; ::_thesis: G * F is Equivalence of A,C
thus A,C are_equivalent by A1, A2, Th46; :: according to ISOCAT_1:def_11 ::_thesis: ex G being Functor of C,A st
( G * (G * F) ~= id A & (G * F) * G ~= id C )
consider F9 being Functor of B,A such that
A3: F9 * F ~= id A and
A4: F * F9 ~= id B by A1, Def11;
(G * F) * F9 = G * (F * F9) by RELAT_1:36;
then A5: (G * F) * F9 ~= G by A4, Th44;
consider G9 being Functor of C,B such that
A6: G9 * G ~= id B and
A7: G * G9 ~= id C by A2, Def11;
take F9 * G9 ; ::_thesis: ( (F9 * G9) * (G * F) ~= id A & (G * F) * (F9 * G9) ~= id C )
(F9 * G9) * G = F9 * (G9 * G) by RELAT_1:36;
then A8: (F9 * G9) * G ~= F9 by A6, Th44;
(F9 * G9) * (G * F) = ((F9 * G9) * G) * F by RELAT_1:36;
then (F9 * G9) * (G * F) ~= F9 * F by A8, Th43;
hence (F9 * G9) * (G * F) ~= id A by A3, NATTRA_1:29; ::_thesis: (G * F) * (F9 * G9) ~= id C
(G * F) * (F9 * G9) = ((G * F) * F9) * G9 by RELAT_1:36;
then (G * F) * (F9 * G9) ~= G * G9 by A5, Th43;
hence (G * F) * (F9 * G9) ~= id C by A7, NATTRA_1:29; ::_thesis: verum
end;
theorem Th49: :: ISOCAT_1:49
for A, B being Category st A,B are_equivalent holds
for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )
proof
let A, B be Category; ::_thesis: ( A,B are_equivalent implies for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B ) )
assume A1: A,B are_equivalent ; ::_thesis: for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )
let F be Equivalence of A,B; ::_thesis: ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )
consider G being Functor of B,A such that
A2: ( G * F ~= id A & F * G ~= id B ) by A1, Def11;
G is Equivalence of B,A
proof
thus B,A are_equivalent by A1; :: according to ISOCAT_1:def_11 ::_thesis: ex G being Functor of A,B st
( G * G ~= id B & G * G ~= id A )
take F ; ::_thesis: ( F * G ~= id B & G * F ~= id A )
thus ( F * G ~= id B & G * F ~= id A ) by A2; ::_thesis: verum
end;
hence ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B ) by A2; ::_thesis: verum
end;
theorem Th50: :: ISOCAT_1:50
for A, B being Category
for F being Functor of A,B
for G being Functor of B,A st G * F ~= id A holds
F is faithful
proof
let A, B be Category; ::_thesis: for F being Functor of A,B
for G being Functor of B,A st G * F ~= id A holds
F is faithful
let F be Functor of A,B; ::_thesis: for G being Functor of B,A st G * F ~= id A holds
F is faithful
let G be Functor of B,A; ::_thesis: ( G * F ~= id A implies F is faithful )
assume G * F ~= id A ; ::_thesis: F is faithful
then A1: id A ~= G * F by NATTRA_1:28;
then A2: id A is_naturally_transformable_to G * F by NATTRA_1:def_11;
consider s being natural_transformation of id A,G * F such that
A3: s is invertible by A1, NATTRA_1:def_11;
thus F is faithful ::_thesis: verum
proof
let a, a9 be Object of A; :: according to CAT_1:def_27 ::_thesis: ( Hom (a,a9) = {} or for b1, b2 being Morphism of a,a9 holds
( not F . b1 = F . b2 or b1 = b2 ) )
assume A4: Hom (a,a9) <> {} ; ::_thesis: for b1, b2 being Morphism of a,a9 holds
( not F . b1 = F . b2 or b1 = b2 )
then A5: Hom (((id A) . a),((id A) . a9)) <> {} by CAT_1:84;
let f1, f2 be Morphism of a,a9; ::_thesis: ( not F . f1 = F . f2 or f1 = f2 )
assume A6: F . f1 = F . f2 ; ::_thesis: f1 = f2
A7: (G * F) /. f1 = (G * F) . f1 by A4, CAT_3:def_10
.= G . (F . f2) by A6, FUNCT_2:15
.= (G * F) . f2 by FUNCT_2:15
.= (G * F) /. f2 by A4, CAT_3:def_10 ;
A8: (s . a9) * ((id A) /. f1) = ((G * F) /. f1) * (s . a) by A2, A4, NATTRA_1:def_8
.= (s . a9) * ((id A) /. f2) by A2, A4, A7, NATTRA_1:def_8 ;
A9: Hom (((id A) . a9),((G * F) . a9)) <> {} by A2, Th25;
s . a9 is invertible by A3, NATTRA_1:def_10;
then A10: s . a9 is monic by CAT_1:43;
thus f1 = (id A) /. f1 by A4, NATTRA_1:16
.= (id A) /. f2 by A5, A9, A10, A8, CAT_1:31
.= f2 by A4, NATTRA_1:16 ; ::_thesis: verum
end;
end;
theorem :: ISOCAT_1:51
for A, B being Category st A,B are_equivalent holds
for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
proof
let A, B be Category; ::_thesis: ( A,B are_equivalent implies for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) )
assume A1: A,B are_equivalent ; ::_thesis: for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
let F be Equivalence of A,B; ::_thesis: ( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
consider G being Equivalence of B,A such that
A2: G * F ~= id A and
A3: F * G ~= id B by A1, Th49;
A4: id A ~= G * F by A2, NATTRA_1:28;
then A5: id A is_naturally_transformable_to G * F by NATTRA_1:def_11;
consider s being natural_transformation of id A,G * F such that
A6: s is invertible by A4, NATTRA_1:def_11;
A7: G is faithful by A3, Th50;
thus F is full ::_thesis: ( F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
proof
let a, a9 be Object of A; :: according to CAT_1:def_26 ::_thesis: ( Hom ((F . a),(F . a9)) = {} or for b1 being Morphism of F . a,F . a9 holds
( not Hom (a,a9) = {} & ex b2 being Morphism of a,a9 st b1 = F . b2 ) )
assume A8: Hom ((F . a),(F . a9)) <> {} ; ::_thesis: for b1 being Morphism of F . a,F . a9 holds
( not Hom (a,a9) = {} & ex b2 being Morphism of a,a9 st b1 = F . b2 )
reconsider f2 = s . a9 as Morphism of a9,(G * F) . a9 by CAT_1:79;
reconsider f1 = s . a as Morphism of a,(G * F) . a by CAT_1:79;
A9: s . a9 is invertible by A6, NATTRA_1:def_10;
A10: Hom (((id A) . a9),((G * F) . a9)) <> {} by A5, Th25;
let g be Morphism of F . a,F . a9; ::_thesis: ( not Hom (a,a9) = {} & ex b1 being Morphism of a,a9 st g = F . b1 )
A11: (G * F) . a = G . (F . a) by CAT_1:76;
then reconsider h = G /. g as Morphism of (G * F) . a,(G * F) . a9 by CAT_1:76;
A12: Hom (((id A) . a),((G * F) . a)) <> {} by A5, Th25;
(G * F) . a9 = G . (F . a9) by CAT_1:76;
then A13: Hom (((G * F) . a),((G * F) . a9)) <> {} by A8, A11, CAT_1:84;
then A14: Hom (((id A) . a),((G * F) . a9)) <> {} by A12, CAT_1:24;
s . a is invertible by A6, NATTRA_1:def_10;
then A15: s . a is epi by CAT_1:43;
G * F is_naturally_transformable_to id A by A2, NATTRA_1:def_11;
then A16: Hom (((G * F) . a9),((id A) . a9)) <> {} by Th25;
A17: ( (id A) . a = a & (id A) . a9 = a9 ) by CAT_1:79;
hence A18: Hom (a,a9) <> {} by A16, A14, CAT_1:24; ::_thesis: ex b1 being Morphism of a,a9 st g = F . b1
take f = (f2 ") * (h * f1); ::_thesis: g = F . f
A19: (id A) /. f = ((s . a9) ") * (h * (s . a)) by A17, A18, NATTRA_1:16;
h * (s . a) = (id ((G * F) . a9)) * (h * (s . a)) by A14, CAT_1:28
.= ((s . a9) * ((s . a9) ")) * (h * (s . a)) by A9, CAT_1:def_17
.= (s . a9) * ((id A) /. f) by A16, A14, A10, A19, CAT_1:25
.= ((G * F) /. f) * (s . a) by A5, A18, NATTRA_1:def_8 ;
then A20: h = (G * F) /. f by A12, A13, A15, CAT_1:36;
G . g = G /. g by A8, CAT_3:def_10
.= (G * F) . f by A18, A20, CAT_3:def_10
.= G . (F . f) by FUNCT_2:15
.= G . (F /. f) by A18, CAT_3:def_10 ;
hence g = F /. f by A7, A8, CAT_1:def_27
.= F . f by A18, CAT_3:def_10 ;
::_thesis: verum
end;
thus F is faithful by A2, Th50; ::_thesis: for b being Object of B ex a being Object of A st b,F . a are_isomorphic
let b be Object of B; ::_thesis: ex a being Object of A st b,F . a are_isomorphic
take G . b ; ::_thesis: b,F . (G . b) are_isomorphic
A21: ( F . (G . b) = (F * G) . b & (id B) . b = b ) by CAT_1:76, CAT_1:79;
A22: id B ~= F * G by A3, NATTRA_1:28;
then id B is_naturally_transformable_to F * G by NATTRA_1:def_11;
then A23: id B is_transformable_to F * G by NATTRA_1:def_7;
ex t being natural_transformation of id B,F * G st t is invertible by A22, NATTRA_1:def_11;
hence b,F . (G . b) are_isomorphic by A21, A23, Th6; ::_thesis: verum
end;
definition
let C be Category;
deffunc H1( Object of C) -> Morphism of $1,$1 = id $1;
func IdMap C -> Function of the carrier of C, the carrier' of C means :: ISOCAT_1:def 12
for o being Object of C holds it . o = id o;
existence
ex b1 being Function of the carrier of C, the carrier' of C st
for o being Object of C holds b1 . o = id o
proof
deffunc H2( Object of C) -> Morphism of $1,$1 = id $1;
consider f being Function of the carrier of C, the carrier' of C such that
A1: for o being Object of C holds f . o = H2(o) from FUNCT_2:sch_4();
take f ; ::_thesis: for o being Object of C holds f . o = id o
thus for o being Object of C holds f . o = id o by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the carrier of C, the carrier' of C st ( for o being Object of C holds b1 . o = id o ) & ( for o being Object of C holds b2 . o = id o ) holds
b1 = b2
proof
let F, G be Function of the carrier of C, the carrier' of C; ::_thesis: ( ( for o being Object of C holds F . o = id o ) & ( for o being Object of C holds G . o = id o ) implies F = G )
assume that
A2: for o being Object of C holds F . o = id o and
A3: for o being Object of C holds G . o = id o ; ::_thesis: F = G
let o be Object of C; :: according to FUNCT_2:def_8 ::_thesis: F . o = G . o
thus F . o = id o by A2
.= G . o by A3 ; ::_thesis: verum
end;
end;
:: deftheorem defines IdMap ISOCAT_1:def_12_:_
for C being Category
for b2 being Function of the carrier of C, the carrier' of C holds
( b2 = IdMap C iff for o being Object of C holds b2 . o = id o );