let I be set ; :: thesis: for C being category
for A being ObjectsFamily of I,C
for C1, C2 being Object of C st C1 is A -CatProduct-like & C2 is A -CatProduct-like holds
C1,C2 are_iso
let C be category; :: thesis: for A being ObjectsFamily of I,C
for C1, C2 being Object of C st C1 is A -CatProduct-like & C2 is A -CatProduct-like holds
C1,C2 are_iso
let A be ObjectsFamily of I,C; :: thesis: for C1, C2 being Object of C st C1 is A -CatProduct-like & C2 is A -CatProduct-like holds
C1,C2 are_iso
let C1, C2 be Object of C; :: thesis: ( C1 is A -CatProduct-like & C2 is A -CatProduct-like implies C1,C2 are_iso )
assume that
A1: C1 is A -CatProduct-like and
A2: C2 is A -CatProduct-like ; :: thesis: C1,C2 are_iso
per cases ( I is empty or not I is empty ) ;
suppose I is empty ; :: thesis: C1,C2 are_iso
hence C1,C2 are_iso by A1, A2, ALTCAT_3:28; :: thesis: verum
end;
suppose not I is empty ; :: thesis: C1,C2 are_iso
then reconsider I = I as non empty set ;
reconsider A = A as ObjectsFamily of I,C ;
consider P1 being MorphismsFamily of C1,A such that
A3: P1 is feasible and
A4: P1 is projection-morphisms by A1;
consider P2 being MorphismsFamily of C2,A such that
A5: P2 is feasible and
A6: P2 is projection-morphisms by A2;
consider f1 being Morphism of C2,C1 such that
A7: f1 in <^C2,C1^> and
A8: for i being Element of I holds P2 . i = (P1 . i) * f1 and
for fa being Morphism of C2,C1 st ( for i being Element of I holds P2 . i = (P1 . i) * fa ) holds
f1 = fa by A4, A5;
consider g1 being Morphism of C1,C1 such that
g1 in <^C1,C1^> and
for i being Element of I holds P1 . i = (P1 . i) * g1 and
A9: for fa being Morphism of C1,C1 st ( for i being Element of I holds P1 . i = (P1 . i) * fa ) holds
g1 = fa by A3, A4;
consider f2 being Morphism of C1,C2 such that
A10: f2 in <^C1,C2^> and
A11: for i being Element of I holds P1 . i = (P2 . i) * f2 and
for fa being Morphism of C1,C2 st ( for i being Element of I holds P1 . i = (P2 . i) * fa ) holds
f2 = fa by A3, A6;
consider g2 being Morphism of C2,C2 such that
g2 in <^C2,C2^> and
for i being Element of I holds P2 . i = (P2 . i) * g2 and
A12: for fa being Morphism of C2,C2 st ( for i being Element of I holds P2 . i = (P2 . i) * fa ) holds
g2 = fa by A5, A6;
thus ( <^C1,C2^> <> {} & <^C2,C1^> <> {} ) by A7, A10; :: according to ALTCAT_3:def 6 :: thesis: ex b1 being Element of <^C1,C2^> st b1 is iso
take f2 ; :: thesis: f2 is iso
A13: f2 is retraction
proof
take f1 ; :: according to ALTCAT_3:def 2 :: thesis: f2 is_left_inverse_of f1
now :: thesis: for i being Element of I holds P2 . i = (P2 . i) * (idm C2)
let i be Element of I; :: thesis: P2 . i = (P2 . i) * (idm C2)
P2 . i in <^C2,(A . i)^> by A5;
hence P2 . i = (P2 . i) * (idm C2) by ALTCAT_1:def 17; :: thesis: verum
end;
then A14: g2 = idm C2 by A12;
now :: thesis: for i being Element of I holds (P2 . i) * (f2 * f1) = P2 . i
let i be Element of I; :: thesis: (P2 . i) * (f2 * f1) = P2 . i
P2 . i in <^C2,(A . i)^> by A5;
hence (P2 . i) * (f2 * f1) = ((P2 . i) * f2) * f1 by A7, A10, ALTCAT_1:21
.= (P1 . i) * f1 by A11
.= P2 . i by A8 ;
:: thesis: verum
end;
hence f2 * f1 = idm C2 by A14, A12; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
f2 is coretraction
proof
take f1 ; :: according to ALTCAT_3:def 3 :: thesis: f1 is_left_inverse_of f2
now :: thesis: for i being Element of I holds P1 . i = (P1 . i) * (idm C1)
let i be Element of I; :: thesis: P1 . i = (P1 . i) * (idm C1)
P1 . i in <^C1,(A . i)^> by A3;
hence P1 . i = (P1 . i) * (idm C1) by ALTCAT_1:def 17; :: thesis: verum
end;
then A15: g1 = idm C1 by A9;
now :: thesis: for i being Element of I holds (P1 . i) * (f1 * f2) = P1 . i
let i be Element of I; :: thesis: (P1 . i) * (f1 * f2) = P1 . i
P1 . i in <^C1,(A . i)^> by A3;
hence (P1 . i) * (f1 * f2) = ((P1 . i) * f1) * f2 by A7, A10, ALTCAT_1:21
.= (P2 . i) * f2 by A8
.= P1 . i by A11 ;
:: thesis: verum
end;
hence f1 * f2 = idm C1 by A15, A9; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
hence f2 is iso by A7, A10, A13, ALTCAT_3:6; :: thesis: verum
end;
end;