let A, B be Category; :: thesis: for F being Functor of A,B
for a, b being Object of A
for f being Morphism of a,b st f is invertible holds
F /. f is invertible
let F be Functor of A,B; :: thesis: for a, b being Object of A
for f being Morphism of a,b st f is invertible holds
F /. f is invertible
let a, b be Object of A; :: thesis: for f being Morphism of a,b st f is invertible holds
F /. f is invertible
let f be Morphism of a,b; :: thesis: ( f is invertible implies F /. f is invertible )
assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def 16 :: thesis: ( for b₁ being Morphism of b,a holds
( not f * b₁ = id b or not b₁ * f = id a ) or F /. f is invertible )
given g being Morphism of b,a such that A2: f * g = id b and
A3: g * f = id a ; :: thesis: F /. f is invertible
A4: dom g = b by A1, CAT_1:5
.= cod f by A1, CAT_1:5 ;
A5: cod g = a by A1, CAT_1:5
.= dom f by A1, CAT_1:5 ;
A6: cod f = b by A1, CAT_1:5;
A7: dom f = a by A1, CAT_1:5;
A8: f (*) g = id (cod f) by A2, A1, A6, CAT_1:def 13;
A9: g (*) f = id (dom f) by A3, A1, A7, CAT_1:def 13;
thus A10: ( Hom ((F . a),(F . b)) <> {} & Hom ((F . b),(F . a)) <> {} ) by A1, CAT_1:84; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of F . b,F . a st
( (F /. f) * b₁ = id (F . b) & b₁ * (F /. f) = id (F . a) )
take F /. g ; :: thesis: ( (F /. f) * (F /. g) = id (F . b) & (F /. g) * (F /. f) = id (F . a) )
A11: F /. f = F . f by A1, CAT_3:def 10;
A12: F /. g = F . g by A1, CAT_3:def 10;
thus (F /. f) * (F /. g) = (F . f) (*) (F . g) by A10, A11, A12, CAT_1:def 13
.= F . (f (*) g) by A5, CAT_1:64
.= id (cod (F /. f)) by A8, A11, CAT_1:63
.= id (F . b) by A10, CAT_1:5 ; :: thesis: (F /. g) * (F /. f) = id (F . a)
thus (F /. g) * (F /. f) = (F . g) (*) (F . f) by A10, A11, A12, CAT_1:def 13
.= F . (g (*) f) by A4, CAT_1:64
.= id (dom (F /. f)) by A9, A11, CAT_1:63
.= id (F . a) by A10, CAT_1:5 ; :: thesis: verum