let A1, A2 be category; for F being contravariant 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 <^b2,a2^> ) ) holds
B1,B2 are_anti-isomorphic_under F
let F be contravariant 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 <^b2,a2^> ) ) holds
B1,B2 are_anti-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 <^b2,a2^> ) ) holds
B1,B2 are_anti-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 <^b2,a2^> ) ) implies B1,B2 are_anti-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 <^b2,a2^> )
; B1,B2 are_anti-isomorphic_under F
thus
B1,B2 are_anti-isomorphic_under F
verumproof
deffunc H1(
object of
B1,
object of
B1,
Morphism of $1,$2)
-> M2(
<^((F | B1) . $2),((F | B1) . $1)^>) =
(F | B1) . $3;
deffunc H2(
object of
B1)
-> M2( the
carrier of
A2) =
(F | B1) . $1;
A4:
(
F is
injective &
F is
surjective )
by A1, FUNCTOR0:def 35;
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
(
b = H2(
c) &
a = 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
( b = H2(c) & a = 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
( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
(
a in the
carrier of
B2 &
b in the
carrier of
B2 )
;
then 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
( b = H2(c) & a = 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:
(
b1 = F . c1 &
a1 = F . d1 )
and A10:
<^c1,d1^> <> {}
and A11:
f1 = F . g1
by A4, A8, Th37;
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
( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
take
d
;
ex g being Morphism of c,d st
( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
take
g
;
( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
g1 in <^c,d^>
by A3, A7, A9, A10, A11;
hence
(
b = H2(
c) &
a = H2(
d) &
<^c,d^> <> {} &
f = H1(
c,
d,
g) )
by A9, A11, Th29, Th31;
verum
end;
A12:
the
carrier of
B1 c= the
carrier of
A1
by ALTCAT_2:def 11;
A14:
now 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(b),H2(a)) )assume A15:
<^a,b^> <> {}
;
for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(b),H2(a))let f be
Morphism of
a,
b;
H1(a,b,f) in the Arrows of B2 . (H2(b),H2(a))
(
a in the
carrier of
B1 &
b in the
carrier of
B1 )
;
then 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 Th29;
(F | B1) . f = F . g
by A15, Th31;
then
(F | B1) . f in <^b9,a9^>
by A3, A16, A17;
hence
H1(
a,
b,
f)
in the
Arrows of
B2 . (
H2(
b),
H2(
a))
;
verum end;
thus
(
B1 is
subcategory of
A1 &
B2 is
subcategory of
A2 )
;
YELLOW20:def 5 ex G being contravariant 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, FUNCTOR0:def 33;
A19:
now let 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 = g
(
a in the
carrier of
B1 &
b in the
carrier of
B1 )
;
then reconsider 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;
g in <^a,b^>
by A20;
then 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, Th31
.=
F . g1
by A20, Th31
;
hence
f = g
by A18, A21, Th36;
verum end;
A22:
now let 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 b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9 )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 b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9let 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 b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9let 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 b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9A25:
c in the
carrier of
B1
;
(
a in the
carrier of
B1 &
b in the
carrier of
B1 )
;
then reconsider a1 =
a,
b1 =
b,
c1 =
c as
object of
A1 by A12, A25;
let a9,
b9,
c9 be
object of
B2;
( a9 = H2(a) & b9 = H2(b) & c9 = H2(c) implies for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9 )assume that A26:
a9 = H2(
a)
and A27:
b9 = H2(
b)
and A28:
c9 = H2(
c)
;
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9let f9 be
Morphism of
b9,
a9;
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9let g9 be
Morphism of
c9,
b9;
( f9 = H1(a,b,f) & g9 = H1(b,c,g) implies H1(a,c,g * f) = f9 * g9 )assume that A29:
f9 = H1(
a,
b,
f)
and A30:
g9 = H1(
b,
c,
g)
;
H1(a,c,g * f) = f9 * g9A31:
b9 = F . b1
by A27, Th29;
A32:
(
<^b,c^> c= <^b1,c1^> &
g in <^b,c^> )
by A24, ALTCAT_2:31;
then reconsider g1 =
g as
Morphism of
b1,
c1 ;
A33:
c9 = F . c1
by A28, Th29;
A34:
(
<^a,b^> c= <^a1,b1^> &
f in <^a,b^> )
by A23, ALTCAT_2:31;
then reconsider f1 =
f as
Morphism of
a1,
b1 ;
A35:
a9 = F . a1
by A26, Th29;
A36:
g9 = F . g1
by A24, A30, Th31;
then A37:
g9 in <^c9,b9^>
by A3, A32, A31, A33;
A38:
f9 = F . f1
by A23, A29, Th31;
then A39:
f9 in <^b9,a9^>
by A3, A34, A35, A31;
(
<^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 Th31;
hence H1(
a,
c,
g * f) =
(F . f1) * (F . g1)
by A34, A32, FUNCTOR0:def 24
.=
f9 * g9
by A35, A31, A33, A38, A36, A39, A37, ALTCAT_2:32
;
verum end;
A40:
now let 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 A41:
a9 = H2(
a)
;
H1(a,a, idm a) = idm a9
a in the
carrier of
B1
;
then reconsider a1 =
a as
object of
A1 by A12;
thus H1(
a,
a,
idm a) =
F . (idm a1)
by Th31, ALTCAT_2:34
.=
idm (F . a1)
by ALTCAT_4:13
.=
idm a9
by A41, Th29, ALTCAT_2:34
;
verum end;
consider G being
strict contravariant Functor of
B1,
B2 such that A42:
for
a being
object of
B1 holds
G . a = H2(
a)
and A43:
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 9(A13, A14, A22, A40);
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 ) )
thus
G is
bijective
from YELLOW18:sch 12(A42, A43, A44, 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 A46:
<^b,c^> <> {}
and A47:
(
b = b1 &
c = c1 )
;
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 A48:
f = f1
;
G . f = (Morph-Map (F,b1,c1)) . f1
A49:
(
<^b,c^> c= <^b1,c1^> &
f in <^b,c^> )
by A46, A47, ALTCAT_2:31;
then A50:
<^(F . c1),(F . b1)^> <> {}
by FUNCTOR0:def 19;
thus G . f =
(F | B1) . f
by A43, A46
.=
F . f1
by A46, A47, A48, Th31
.=
(Morph-Map (F,b1,c1)) . f1
by A49, A50, FUNCTOR0:def 16
;
verum
end;