let A1, A2 be category; for F being covariant Functor of A1,A2
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F
let F be covariant Functor of A1,A2; for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F
let B1 be non empty subcategory of A1; for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F
let B2 be non empty subcategory of A2; ( F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) implies B1,B2 are_isomorphic_under F )
assume that
A1:
F is bijective
and
A2:
for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 )
and
A3:
for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> )
; B1,B2 are_isomorphic_under F
thus
B1,B2 are_isomorphic_under F
verumproof
deffunc H1(
Object of
B1,
Object of
B1,
Morphism of $1,$2)
-> M3(
<^((F | B1) . $1),((F | B1) . $2)^>) =
(F | B1) . $3;
deffunc H2(
Object of
B1)
-> M3( the
carrier of
A2) =
(F | B1) . $1;
A4:
(
F is
injective &
F is
surjective )
by A1;
A5:
for
a,
b being
Object of
B2 st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b ex
c,
d being
Object of
B1 ex
g being
Morphism of
c,
d st
(
a = H2(
c) &
b = H2(
d) &
<^c,d^> <> {} &
f = H1(
c,
d,
g) )
proof
A6:
the
carrier of
B2 c= the
carrier of
A2
by ALTCAT_2:def 11;
let a,
b be
Object of
B2;
( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) ) )
assume A7:
<^a,b^> <> {}
;
for f being Morphism of a,b ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
reconsider a1 =
a,
b1 =
b as
Object of
A2 by A6;
let f be
Morphism of
a,
b;
ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
A8:
(
<^a,b^> c= <^a1,b1^> &
f in <^a,b^> )
by A7, ALTCAT_2:31;
then reconsider f1 =
f as
Morphism of
a1,
b1 ;
consider c1,
d1 being
Object of
A1,
g1 being
Morphism of
c1,
d1 such that A9:
(
a1 = F . c1 &
b1 = F . d1 )
and A10:
<^c1,d1^> <> {}
and A11:
f1 = F . g1
by A4, A8, Th33;
reconsider c =
c1,
d =
d1 as
Object of
B1 by A2, A9;
reconsider g =
g1 as
Morphism of
c,
d by A3, A7, A9, A10, A11;
take
c
;
ex d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
take
d
;
ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
take
g
;
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
g1 in <^c,d^>
by A3, A7, A9, A10, A11;
hence
(
a = H2(
c) &
b = H2(
d) &
<^c,d^> <> {} &
f = H1(
c,
d,
g) )
by A9, A11, Th28, Th29;
verum
end;
A12:
the
carrier of
B1 c= the
carrier of
A1
by ALTCAT_2:def 11;
A14:
now for a, b being Object of B1 st <^a,b^> <> {} holds
for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b))let a,
b be
Object of
B1;
( <^a,b^> <> {} implies for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b)) )assume A15:
<^a,b^> <> {}
;
for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b))let f be
Morphism of
a,
b;
H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b))reconsider c =
a,
d =
b as
Object of
A1 by A12;
A16:
(
<^a,b^> c= <^c,d^> &
f in <^a,b^> )
by A15, ALTCAT_2:31;
then reconsider g =
f as
Morphism of
c,
d ;
reconsider a9 =
(F | B1) . a,
b9 =
(F | B1) . b as
Object of
B2 by A13;
A17:
(
(F | B1) . a = F . c &
(F | B1) . b = F . d )
by Th28;
(F | B1) . f = F . g
by A15, Th29;
then
(F | B1) . f in <^a9,b9^>
by A3, A16, A17;
hence
H1(
a,
b,
f)
in the
Arrows of
B2 . (
H2(
a),
H2(
b))
;
verum end;
thus
(
B1 is
subcategory of
A1 &
B2 is
subcategory of
A2 )
;
YELLOW20:def 4 ex G being covariant Functor of B1,B2 st
( G is bijective & ( for a9 being Object of B1
for a being Object of A1 st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of B1
for b, c being Object of A1 st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) )
A18:
(
F is
one-to-one &
F is
faithful &
F is
surjective )
by A4;
A19:
now for a, b being Object of B1 st <^a,b^> <> {} holds
for f, g being Morphism of a,b st H1(a,b,f) = H1(a,b,g) holds
f = glet a,
b be
Object of
B1;
( <^a,b^> <> {} implies for f, g being Morphism of a,b st H1(a,b,f) = H1(a,b,g) holds
f = g )assume A20:
<^a,b^> <> {}
;
for f, g being Morphism of a,b st H1(a,b,f) = H1(a,b,g) holds
f = greconsider a1 =
a,
b1 =
b as
Object of
A1 by A12;
let f,
g be
Morphism of
a,
b;
( H1(a,b,f) = H1(a,b,g) implies f = g )A21:
(
<^a,b^> c= <^a1,b1^> &
f in <^a,b^> )
by A20, ALTCAT_2:31;
reconsider f1 =
f,
g1 =
g as
Morphism of
a1,
b1 by A21;
assume
H1(
a,
b,
f)
= H1(
a,
b,
g)
;
f = gthen F . f1 =
(F | B1) . g
by A20, Th29
.=
F . g1
by A20, Th29
;
hence
f = g
by A18, A21, Th32;
verum end;
A22:
now for a, b, c being Object of B1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9let a,
b,
c be
Object of
B1;
( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9 )assume that A23:
<^a,b^> <> {}
and A24:
<^b,c^> <> {}
;
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9let f be
Morphism of
a,
b;
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9let g be
Morphism of
b,
c;
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9reconsider a1 =
a,
b1 =
b,
c1 =
c as
Object of
A1 by A12;
let a9,
b9,
c9 be
Object of
B2;
( a9 = H2(a) & b9 = H2(b) & c9 = H2(c) implies for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9 )assume that A25:
a9 = H2(
a)
and A26:
b9 = H2(
b)
and A27:
c9 = H2(
c)
;
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9let f9 be
Morphism of
a9,
b9;
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9let g9 be
Morphism of
b9,
c9;
( f9 = H1(a,b,f) & g9 = H1(b,c,g) implies H1(a,c,g * f) = g9 * f9 )assume that A28:
f9 = H1(
a,
b,
f)
and A29:
g9 = H1(
b,
c,
g)
;
H1(a,c,g * f) = g9 * f9A30:
b9 = F . b1
by A26, Th28;
A31:
(
<^b,c^> c= <^b1,c1^> &
g in <^b,c^> )
by A24, ALTCAT_2:31;
then reconsider g1 =
g as
Morphism of
b1,
c1 ;
A32:
c9 = F . c1
by A27, Th28;
A33:
(
<^a,b^> c= <^a1,b1^> &
f in <^a,b^> )
by A23, ALTCAT_2:31;
then reconsider f1 =
f as
Morphism of
a1,
b1 ;
A34:
a9 = F . a1
by A25, Th28;
A35:
g9 = F . g1
by A24, A29, Th29;
then A36:
g9 in <^b9,c9^>
by A3, A31, A30, A32;
A37:
f9 = F . f1
by A23, A28, Th29;
then A38:
f9 in <^a9,b9^>
by A3, A33, A34, A30;
(
<^a,c^> <> {} &
g * f = g1 * f1 )
by A23, A24, ALTCAT_1:def 2, ALTCAT_2:32;
then
(F | B1) . (g * f) = F . (g1 * f1)
by Th29;
hence H1(
a,
c,
g * f) =
(F . g1) * (F . f1)
by A33, A31, FUNCTOR0:def 23
.=
g9 * f9
by A34, A30, A32, A37, A35, A38, A36, ALTCAT_2:32
;
verum end;
A39:
now for a being Object of B1
for a9 being Object of B2 st a9 = H2(a) holds
H1(a,a, idm a) = idm a9let a be
Object of
B1;
for a9 being Object of B2 st a9 = H2(a) holds
H1(a,a, idm a) = idm a9let a9 be
Object of
B2;
( a9 = H2(a) implies H1(a,a, idm a) = idm a9 )assume A40:
a9 = H2(
a)
;
H1(a,a, idm a) = idm a9reconsider a1 =
a as
Object of
A1 by A12;
thus H1(
a,
a,
idm a) =
F . (idm a1)
by Th29, ALTCAT_2:34
.=
idm (F . a1)
by FUNCTOR2:1
.=
idm a9
by A40, Th28, ALTCAT_2:34
;
verum end;
consider G being
strict covariant Functor of
B1,
B2 such that A41:
for
a being
Object of
B1 holds
G . a = H2(
a)
and A42:
for
a,
b being
Object of
B1 st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
G . f = H1(
a,
b,
f)
from YELLOW18:sch 8(A13, A14, A22, A39);
take
G
;
( G is bijective & ( for a9 being Object of B1
for a being Object of A1 st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of B1
for b, c being Object of A1 st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) )
A43:
now for a, b being Object of B1 st H2(a) = H2(b) holds
a = blet a,
b be
Object of
B1;
( H2(a) = H2(b) implies a = b )reconsider a1 =
a,
b1 =
b as
Object of
A1 by A12;
assume
H2(
a)
= H2(
b)
;
a = bthen F . a1 =
(F | B1) . b
by Th28
.=
F . b1
by Th28
;
hence
a = b
by A18, Th31;
verum end;
thus
G is
bijective
from YELLOW18:sch 10(A41, A42, A43, A19, A5); ( ( for a9 being Object of B1
for a being Object of A1 st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of B1
for b, c being Object of A1 st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) )
let b,
c be
Object of
B1;
for b, c being Object of A1 st <^b,c^> <> {} & b = b & c = c holds
for f9 being Morphism of b,c
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . flet b1,
c1 be
Object of
A1;
( <^b,c^> <> {} & b = b1 & c = c1 implies for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
G . f9 = (Morph-Map (F,b1,c1)) . f )
assume that A45:
<^b,c^> <> {}
and A46:
(
b1 = b &
c1 = c )
;
for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
G . f9 = (Morph-Map (F,b1,c1)) . f
let f be
Morphism of
b,
c;
for f being Morphism of b1,c1 st f = f holds
G . f = (Morph-Map (F,b1,c1)) . flet f1 be
Morphism of
b1,
c1;
( f = f1 implies G . f = (Morph-Map (F,b1,c1)) . f1 )
assume A47:
f = f1
;
G . f = (Morph-Map (F,b1,c1)) . f1
A48:
(
<^b,c^> c= <^b1,c1^> &
f in <^b,c^> )
by A45, A46, ALTCAT_2:31;
then A49:
<^(F . b1),(F . c1)^> <> {}
by FUNCTOR0:def 18;
thus G . f =
(F | B1) . f
by A42, A45
.=
F . f1
by A45, A46, A47, Th29
.=
(Morph-Map (F,b1,c1)) . f1
by A48, A49, FUNCTOR0:def 15
;
verum
end;