let C, C1, C2, D be category; :: thesis: for F1 being Functor of C1,C
for F2 being Functor of C2,C
for P1 being Functor of D,C1
for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds
P2 is isomorphism
let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C
for P1 being Functor of D,C1
for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds
P2 is isomorphism
let F2 be Functor of C2,C; :: thesis: for P1 being Functor of D,C1
for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds
P2 is isomorphism
let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds
P2 is isomorphism
let P2 be Functor of D,C2; :: thesis: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism implies P2 is isomorphism )
assume A1: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant ) ; :: thesis: ( not D,P1,P2 is_pullback_of F1,F2 or not F1 is isomorphism or P2 is isomorphism )
assume A2: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: ( not F1 is isomorphism or P2 is isomorphism )
then A3: ( F1 (*) P1 = F2 (*) P2 & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) ) ) by A1, Def20;
assume A4: F1 is isomorphism ; :: thesis: P2 is isomorphism
consider G1 being Functor of C,C1 such that
A5: ( G1 is covariant & G1 (*) F1 = id C1 & F1 (*) G1 = id C ) by A4;
set G11 = G1 (*) F2;
set G22 = id C2;
A6: G1 (*) F2 is covariant by A5, A1, CAT_6:35;
A7: F1 (*) (G1 (*) F2) = (F1 (*) G1) (*) F2 by A5, A1, Th10
.= F2 by A5, A1, Th11
.= F2 (*) (id C2) by A1, Th11 ;
consider Q2 being Functor of C2,D such that
A8: ( Q2 is covariant & P1 (*) Q2 = G1 (*) F2 & P2 (*) Q2 = id C2 & ( for H1 being Functor of C2,D st H1 is covariant & P1 (*) H1 = G1 (*) F2 & P2 (*) H1 = id C2 holds
Q2 = H1 ) ) by A6, A2, A1, Def20, A7;
set G33 = (P1 (*) Q2) (*) P2;
A9: F2 (*) P2 is covariant by A1, CAT_6:35;
A10: (P1 (*) Q2) (*) P2 is covariant by A8, A6, A1, CAT_6:35;
F1 (*) ((P1 (*) Q2) (*) P2) = F1 (*) (G1 (*) (F2 (*) P2)) by A5, A8, A1, Th10
.= (F1 (*) G1) (*) (F2 (*) P2) by A9, A5, A4, Th10
.= F2 (*) P2 by A9, Th11, A5 ;
then consider H being Functor of D,D such that
( H is covariant & P1 (*) H = (P1 (*) Q2) (*) P2 & P2 (*) H = P2 ) and
A11: for H1 being Functor of D,D st H1 is covariant & P1 (*) H1 = (P1 (*) Q2) (*) P2 & P2 (*) H1 = P2 holds
H = H1 by A1, A2, A10, Def20;
A12: P1 (*) (id D) = P1 by A1, Th11
.= (G1 (*) F1) (*) P1 by A1, A5, Th11
.= G1 (*) (F1 (*) P1) by A1, A5, Th10
.= (P1 (*) Q2) (*) P2 by A8, A3, A1, A5, Th10 ;
A13: P2 (*) (id D) = P2 by A1, Th11;
A14: P1 (*) (Q2 (*) P2) = (P1 (*) Q2) (*) P2 by A1, A8, Th10;
P2 (*) (Q2 (*) P2) = (P2 (*) Q2) (*) P2 by A1, A8, Th10
.= P2 by A1, A8, Th11 ;
then H = Q2 (*) P2 by A11, A14, A1, A8, CAT_6:35;
hence P2 is isomorphism by A8, A13, A11, A12, A1; :: thesis: verum