let A, B be category; for F, G being contravariant Functor of A,B st ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)
let F, G be contravariant Functor of A,B; ( ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) implies FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #) )
assume that
A1:
for a being Object of A holds F . a = G . a
and
A2:
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f
; FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)
the ObjectMap of F is Contravariant
by FUNCTOR0:def 13;
then consider ff being Function of the carrier of A, the carrier of B such that
A3:
the ObjectMap of F = ~ [:ff,ff:]
;
the ObjectMap of G is Contravariant
by FUNCTOR0:def 13;
then consider gg being Function of the carrier of A, the carrier of B such that
A4:
the ObjectMap of G = ~ [:gg,gg:]
;
now for a, b being Element of A holds the ObjectMap of F . (a,b) = the ObjectMap of G . (a,b)let a,
b be
Element of
A;
the ObjectMap of F . (a,b) = the ObjectMap of G . (a,b)reconsider x =
a,
y =
b as
Object of
A ;
A5:
dom ff = the
carrier of
A
by FUNCT_2:def 1;
A6:
dom gg = the
carrier of
A
by FUNCT_2:def 1;
A7:
dom [:ff,ff:] = [: the carrier of A, the carrier of A:]
by FUNCT_2:def 1;
then A8:
[b,a] in dom [:ff,ff:]
by ZFMISC_1:def 2;
A9:
dom [:gg,gg:] = [: the carrier of A, the carrier of A:]
by FUNCT_2:def 1;
then A10:
[b,a] in dom [:gg,gg:]
by ZFMISC_1:def 2;
A11:
[a,a] in dom [:gg,gg:]
by A9, ZFMISC_1:def 2;
A12:
[b,b] in dom [:gg,gg:]
by A9, ZFMISC_1:def 2;
A13:
the
ObjectMap of
F . (
x,
x)
= [:ff,ff:] . (
x,
x)
by A3, A7, A11, FUNCT_4:def 2;
A14:
the
ObjectMap of
F . (
y,
y)
= [:ff,ff:] . (
y,
y)
by A3, A7, A12, FUNCT_4:def 2;
A15:
the
ObjectMap of
G . (
x,
x)
= [:gg,gg:] . (
x,
x)
by A4, A11, FUNCT_4:def 2;
A16:
the
ObjectMap of
G . (
y,
y)
= [:gg,gg:] . (
y,
y)
by A4, A12, FUNCT_4:def 2;
A17:
the
ObjectMap of
F . (
x,
x)
= [(ff . x),(ff . x)]
by A5, A13, FUNCT_3:def 8;
A18:
the
ObjectMap of
F . (
y,
y)
= [(ff . y),(ff . y)]
by A5, A14, FUNCT_3:def 8;
A19:
the
ObjectMap of
G . (
x,
x)
= [(gg . x),(gg . x)]
by A6, A15, FUNCT_3:def 8;
A20:
the
ObjectMap of
G . (
y,
y)
= [(gg . y),(gg . y)]
by A6, A16, FUNCT_3:def 8;
A21:
F . x = ff . x
by A17;
A22:
F . y = ff . y
by A18;
A23:
G . x = gg . x
by A19;
A24:
G . y = gg . y
by A20;
A25:
F . x = G . x
by A1;
A26:
F . y = G . y
by A1;
thus the
ObjectMap of
F . (
a,
b) =
[:ff,ff:] . (
b,
a)
by A3, A8, FUNCT_4:def 2
.=
[(ff . b),(ff . a)]
by A5, FUNCT_3:def 8
.=
[:gg,gg:] . (
b,
a)
by A6, A21, A22, A23, A24, A25, A26, FUNCT_3:def 8
.=
the
ObjectMap of
G . (
a,
b)
by A4, A10, FUNCT_4:def 2
;
verum end;
then A27:
the ObjectMap of F = the ObjectMap of G
;
now for i being object st i in [: the carrier of A, the carrier of A:] holds
the MorphMap of F . i = the MorphMap of G . ilet i be
object ;
( i in [: the carrier of A, the carrier of A:] implies the MorphMap of F . i = the MorphMap of G . i )assume
i in [: the carrier of A, the carrier of A:]
;
the MorphMap of F . i = the MorphMap of G . ithen consider a,
b being
object such that A28:
a in the
carrier of
A
and A29:
b in the
carrier of
A
and A30:
i = [a,b]
by ZFMISC_1:def 2;
reconsider x =
a,
y =
b as
Object of
A by A28, A29;
A31:
(
<^x,y^> <> {} implies
<^(F . y),(F . x)^> <> {} )
by FUNCTOR0:def 19;
A32:
(
<^x,y^> <> {} implies
<^(G . y),(G . x)^> <> {} )
by FUNCTOR0:def 19;
A33:
dom (Morph-Map (F,x,y)) = <^x,y^>
by A31, FUNCT_2:def 1;
A34:
dom (Morph-Map (G,x,y)) = <^x,y^>
by A32, FUNCT_2:def 1;
now for z being object st z in <^x,y^> holds
(Morph-Map (F,x,y)) . z = (Morph-Map (G,x,y)) . zlet z be
object ;
( z in <^x,y^> implies (Morph-Map (F,x,y)) . z = (Morph-Map (G,x,y)) . z )assume A35:
z in <^x,y^>
;
(Morph-Map (F,x,y)) . z = (Morph-Map (G,x,y)) . zthen reconsider f =
z as
Morphism of
x,
y ;
thus (Morph-Map (F,x,y)) . z =
F . f
by A31, A35, FUNCTOR0:def 16
.=
G . f
by A2, A35
.=
(Morph-Map (G,x,y)) . z
by A32, A35, FUNCTOR0:def 16
;
verum end; hence
the
MorphMap of
F . i = the
MorphMap of
G . i
by A30, A33, A34;
verum end;
hence
FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)
by A27, PBOOLE:3; verum