let C1, C2 be composable with_identities CategoryStr ; ( C1 ~= C2 implies RelOb C1, RelOb C2 are_isomorphic )
assume A1:
C1 ~= C2
; RelOb C1, RelOb C2 are_isomorphic
per cases
( C1 is empty or not C1 is empty )
;
suppose A4:
not
C1 is
empty
;
RelOb C1, RelOb C2 are_isomorphic then A5:
not
C2 is
empty
by A1, Th15;
consider F being
Functor of
C1,
C2,
G being
Functor of
C2,
C1 such that A6:
(
F is
covariant &
G is
covariant &
G (*) F = id C1 &
F (*) G = id C2 )
by A1, CAT_6:def 28;
F * G =
id C1
by A6, CAT_6:def 27
.=
id the
carrier of
C1
by STRUCT_0:def 4
;
then A7:
F is
one-to-one
by FUNCT_2:23;
set F1 =
F | (Ob C1);
A8:
dom F =
the
carrier of
C1
by A5, FUNCT_2:def 1
.=
Mor C1
by CAT_6:def 1
;
then A9:
dom (F | (Ob C1)) = Ob C1
by RELAT_1:62;
A10:
Ob C1 =
(Ob C1) \/ (Ob C1)
.=
(Ob C1) \/ (rng (RelOb C1))
by Th34
.=
(dom (RelOb C1)) \/ (rng (RelOb C1))
by Th34
.=
field (RelOb C1)
by RELAT_1:def 6
;
then A11:
dom (F | (Ob C1)) = field (RelOb C1)
by A8, RELAT_1:62;
for
y being
object st
y in rng (F | (Ob C1)) holds
y in Ob C2
then A15:
rng (F | (Ob C1)) c= Ob C2
by TARSKI:def 3;
for
y being
object st
y in Ob C2 holds
y in rng (F | (Ob C1))
proof
let y be
object ;
( y in Ob C2 implies y in rng (F | (Ob C1)) )
assume A16:
y in Ob C2
;
y in rng (F | (Ob C1))
set x =
G . y;
A17:
G * F = id C2
by A6, CAT_6:def 27;
A18:
y in Mor C2
by A16;
then A19:
y in the
carrier of
C2
by CAT_6:def 1;
y in dom (id the carrier of C2)
by A18, CAT_6:def 1;
then A20:
y in dom (G * F)
by A17, STRUCT_0:def 4;
then A21:
G . y in dom F
by FUNCT_1:11;
A22:
F . (G . y) =
(G * F) . y
by A20, FUNCT_1:12
.=
(id C2) . y
by A6, CAT_6:def 27
.=
(id the carrier of C2) . y
by STRUCT_0:def 4
.=
y
by A19, FUNCT_1:18
;
y in { g where g is morphism of C2 : ( g is identity & g in Mor C2 ) }
by A16, CAT_6:def 17;
then consider g being
morphism of
C2 such that A23:
(
y = g &
g is
identity &
g in Mor C2 )
;
A24:
G . y = G . g
by A23, A4, A1, Th15, CAT_6:def 21;
G . g is
identity
by A23, CAT_6:def 22, A6, CAT_6:def 25;
then
G . g in { f where f is morphism of C1 : ( f is identity & f in Mor C1 ) }
by A4;
then
G . y in Ob C1
by A24, CAT_6:def 17;
hence
y in rng (F | (Ob C1))
by A21, A22, FUNCT_1:50;
verum
end; then A25:
Ob C2 c= rng (F | (Ob C1))
by TARSKI:def 3;
then A26:
rng (F | (Ob C1)) = Ob C2
by A15, XBOOLE_0:def 10;
A27:
rng (F | (Ob C1)) =
(Ob C2) \/ (Ob C2)
by A25, A15, XBOOLE_0:def 10
.=
(Ob C2) \/ (rng (RelOb C2))
by Th34
.=
(dom (RelOb C2)) \/ (rng (RelOb C2))
by Th34
.=
field (RelOb C2)
by RELAT_1:def 6
;
A28:
F | (Ob C1) is
one-to-one
by A7, FUNCT_1:52;
for
a,
b being
object holds
(
[a,b] in RelOb C1 iff (
a in field (RelOb C1) &
b in field (RelOb C1) &
[((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ) )
proof
let a,
b be
object ;
( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 ) )
hereby ( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 implies [a,b] in RelOb C1 )
assume
[a,b] in RelOb C1
;
( a in field (RelOb C1) & b in field (RelOb C1) & [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 )then consider a1,
b1 being
Object of
C1 such that A29:
(
[a,b] = [a1,b1] & ex
f being
morphism of
C1 st
f in Hom (
a1,
b1) )
;
consider f being
morphism of
C1 such that A30:
f in Hom (
a1,
b1)
by A29;
A31:
(
a = a1 &
b = b1 )
by A29, XTUPLE_0:1;
not
Ob C1 is
empty
by A4;
then A32:
(
a1 in Ob C1 &
b1 in Ob C1 )
;
hence
(
a in field (RelOb C1) &
b in field (RelOb C1) )
by A10, A29, XTUPLE_0:1;
[((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2A33:
(F | (Ob C1)) . a = F . a1
by A31, A4, FUNCT_1:49;
A34:
(F | (Ob C1)) . b = F . b1
by A31, A4, FUNCT_1:49;
(
a in dom (F | (Ob C1)) &
b in dom (F | (Ob C1)) )
by A9, A29, XTUPLE_0:1, A32;
then reconsider a2 =
(F | (Ob C1)) . a,
b2 =
(F | (Ob C1)) . b as
Object of
C2 by A26, FUNCT_1:3;
(
dom f = a1 &
cod f = b1 )
by A30, A4, Th20;
then
(
dom (F . f) = F . a1 &
cod (F . f) = F . b1 )
by A4, A5, A6, CAT_6:32;
then
F . f in Hom (
a2,
b2)
by A33, A34, A5, Th20;
hence
[((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2
;
verum
end;
assume A35:
(
a in field (RelOb C1) &
b in field (RelOb C1) )
;
( not [((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2 or [a,b] in RelOb C1 )
assume
[((F | (Ob C1)) . a),((F | (Ob C1)) . b)] in RelOb C2
;
[a,b] in RelOb C1
then consider a2,
b2 being
Object of
C2 such that A36:
(
[((F | (Ob C1)) . a),((F | (Ob C1)) . b)] = [a2,b2] & ex
g being
morphism of
C2 st
g in Hom (
a2,
b2) )
;
consider g being
morphism of
C2 such that A37:
g in Hom (
a2,
b2)
by A36;
reconsider a1 =
a,
b1 =
b as
Object of
C1 by A10, A35;
A38:
F * G = id C1
by A6, CAT_6:def 27;
A39:
a in Mor C1
by A10, A35;
then A40:
a in the
carrier of
C1
by CAT_6:def 1;
a in dom (id the carrier of C1)
by A39, CAT_6:def 1;
then A41:
a in dom (F * G)
by A38, STRUCT_0:def 4;
A42:
G . a2 =
G . ((F | (Ob C1)) . a)
by A36, XTUPLE_0:1
.=
G . (F . a)
by A10, A35, FUNCT_1:49
.=
(F * G) . a
by A41, FUNCT_1:12
.=
(id C1) . a
by A6, CAT_6:def 27
.=
(id the carrier of C1) . a
by STRUCT_0:def 4
.=
a1
by A40, FUNCT_1:18
;
A43:
b in Mor C1
by A10, A35;
then A44:
b in the
carrier of
C1
by CAT_6:def 1;
b in dom (id the carrier of C1)
by A43, CAT_6:def 1;
then A45:
b in dom (F * G)
by A38, STRUCT_0:def 4;
A46:
G . b2 =
G . ((F | (Ob C1)) . b)
by A36, XTUPLE_0:1
.=
G . (F . b)
by A10, A35, FUNCT_1:49
.=
(F * G) . b
by A45, FUNCT_1:12
.=
(id C1) . b
by A6, CAT_6:def 27
.=
(id the carrier of C1) . b
by STRUCT_0:def 4
.=
b1
by A44, FUNCT_1:18
;
(
G . (dom g) = G . a2 &
G . (cod g) = G . b2 )
by A37, A5, Th20;
then
(
dom (G . g) = G . a2 &
cod (G . g) = G . b2 )
by A4, A5, A6, CAT_6:32;
then
G . g in Hom (
a1,
b1)
by A42, A46, A4, Th20;
hence
[a,b] in RelOb C1
;
verum
end; hence
RelOb C1,
RelOb C2 are_isomorphic
by A11, A27, A28, WELLORD1:def 7, WELLORD1:def 8;
verum end;