let C1, C2, A, B be category; for P1 being Functor of A,C1
for P2 being Functor of A,C2
for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let P1 be Functor of A,C1; for P2 being Functor of A,C2
for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let P2 be Functor of A,C2; for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let Q1 be Functor of B,C1; for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let Q2 be Functor of B,C2; ( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 implies A ~= B )
assume A1:
( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant )
; ( not A,P1,P2 is_product_of C1,C2 or not B,Q1,Q2 is_product_of C1,C2 or A ~= B )
assume A2:
A,P1,P2 is_product_of C1,C2
; ( not B,Q1,Q2 is_product_of C1,C2 or A ~= B )
assume A3:
B,Q1,Q2 is_product_of C1,C2
; A ~= B
ex FF being Functor of A,B ex GG being Functor of B,A st
( FF is covariant & GG is covariant & GG (*) FF = id A & FF (*) GG = id B )
proof
consider FF being
Functor of
A,
B such that A4:
(
FF is
covariant &
Q1 (*) FF = P1 &
Q2 (*) FF = P2 & ( for
H1 being
Functor of
A,
B st
H1 is
covariant &
Q1 (*) H1 = P1 &
Q2 (*) H1 = P2 holds
FF = H1 ) )
by A1, A3, Def17;
consider GG being
Functor of
B,
A such that A5:
(
GG is
covariant &
P1 (*) GG = Q1 &
P2 (*) GG = Q2 & ( for
H1 being
Functor of
B,
A st
H1 is
covariant &
P1 (*) H1 = Q1 &
P2 (*) H1 = Q2 holds
GG = H1 ) )
by A1, A2, Def17;
take
FF
;
ex GG being Functor of B,A st
( FF is covariant & GG is covariant & GG (*) FF = id A & FF (*) GG = id B )
take
GG
;
( FF is covariant & GG is covariant & GG (*) FF = id A & FF (*) GG = id B )
thus
(
FF is
covariant &
GG is
covariant )
by A4, A5;
( GG (*) FF = id A & FF (*) GG = id B )
set G11 =
Q1 (*) FF;
set G12 =
Q2 (*) FF;
consider H1 being
Functor of
A,
A such that A6:
(
H1 is
covariant &
P1 (*) H1 = Q1 (*) FF &
P2 (*) H1 = Q2 (*) FF & ( for
H being
Functor of
A,
A st
H is
covariant &
P1 (*) H = Q1 (*) FF &
P2 (*) H = Q2 (*) FF holds
H1 = H ) )
by A1, A4, A2, Def17;
A7:
P1 (*) (GG (*) FF) = Q1 (*) FF
by A1, A4, A5, CAT_7:10;
A8:
P2 (*) (GG (*) FF) = Q2 (*) FF
by A1, A4, A5, CAT_7:10;
A9:
P1 (*) (id A) = Q1 (*) FF
by A1, A4, CAT_7:11;
A10:
P2 (*) (id A) = Q2 (*) FF
by A1, A4, CAT_7:11;
thus GG (*) FF =
H1
by A6, A7, A8, A4, A5, CAT_6:35
.=
id A
by A6, A9, A10
;
FF (*) GG = id B
set G21 =
P1 (*) GG;
set G22 =
P2 (*) GG;
consider H2 being
Functor of
B,
B such that A11:
(
H2 is
covariant &
Q1 (*) H2 = P1 (*) GG &
Q2 (*) H2 = P2 (*) GG & ( for
H being
Functor of
B,
B st
H is
covariant &
Q1 (*) H = P1 (*) GG &
Q2 (*) H = P2 (*) GG holds
H2 = H ) )
by A1, A5, A3, Def17;
A12:
Q1 (*) (FF (*) GG) = P1 (*) GG
by A1, A4, A5, CAT_7:10;
A13:
Q2 (*) (FF (*) GG) = P2 (*) GG
by A1, A4, A5, CAT_7:10;
A14:
Q1 (*) (id B) = P1 (*) GG
by A1, A5, CAT_7:11;
A15:
Q2 (*) (id B) = P2 (*) GG
by A1, A5, CAT_7:11;
thus FF (*) GG =
H2
by A11, A12, A13, A4, A5, CAT_6:35
.=
id B
by A11, A14, A15
;
verum
end;
hence
A ~= B
by CAT_6:def 28; verum