let C be non empty associative composable with_identities CategoryStr ; CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is Category
set CC = CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);
reconsider CC = CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) as non empty non void CatStr ;
A1:
for f, g being Morphism of CC holds
( [g,f] in dom the Comp of CC iff dom g = cod f )
A2:
for f, g being Morphism of CC st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
A6:
for f, g, h being Morphism of CC st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proof
let f,
g,
h be
Morphism of
CC;
( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
assume A7:
dom h = cod g
;
( not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
then A8: the
Source of
CC . h =
cod g
by GRAPH_1:def 3
.=
the
Target of
CC . g
by GRAPH_1:def 4
;
A9:
[h,g] in dom the
Comp of
CC
by A7, A1;
assume A10:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
then A11: the
Source of
CC . g =
cod f
by GRAPH_1:def 3
.=
the
Target of
CC . f
by GRAPH_1:def 4
;
A12:
[g,f] in dom the
Comp of
CC
by A10, A1;
dom h = cod (g (*) f)
by A2, A7, A10;
then A13:
[h,(g (*) f)] in dom the
Comp of
CC
by A1;
dom (h (*) g) = cod f
by A2, A7, A10;
then A14:
[(h (*) g),f] in dom the
Comp of
CC
by A1;
thus h (*) (g (*) f) =
the
Comp of
CC . (
h,
(g (*) f))
by A13, CAT_1:def 1
.=
the
Comp of
CC . (
h,
( the Comp of CC . (g,f)))
by A12, CAT_1:def 1
.=
the
Comp of
CC . (
( the Comp of CC . (h,g)),
f)
by Th39, A8, A11
.=
the
Comp of
CC . (
(h (*) g),
f)
by A9, CAT_1:def 1
.=
(h (*) g) (*) f
by A14, CAT_1:def 1
;
verum
end;
A15:
for b being Element of CC holds (IdMap C) . b in Hom (b,b)
then A17:
for b being Element of CC holds Hom (b,b) <> {}
;
for a being Element of CC ex i being Morphism of a,a st
for b being Element of CC holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proof
let a be
Element of
CC;
ex i being Morphism of a,a st
for b being Element of CC holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
set i =
(IdMap C) . a;
A18:
(IdMap C) . a in Hom (
a,
a)
by A15;
then reconsider i =
(IdMap C) . a as
Morphism of
a,
a by CAT_1:def 5;
take
i
;
for b being Element of CC holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let b be
Element of
CC;
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
thus
(
Hom (
a,
b)
<> {} implies for
g being
Morphism of
a,
b holds
g (*) i = g )
( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )proof
assume A19:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) i = g
let g be
Morphism of
a,
b;
g (*) i = g
g in Hom (
a,
b)
by A19, CAT_1:def 5;
then A20:
dom g = a
by CAT_1:1;
then
dom g = cod i
by A18, CAT_1:1;
then A21:
[g,i] in dom the
Comp of
CC
by A1;
the
Source of
CC . g = a
by A20, GRAPH_1:def 3;
then
(CompMap C) . (
g,
((IdMap C) . a))
= g
by Th40;
hence
g (*) i = g
by A21, CAT_1:def 1;
verum
end;
assume A22:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds i (*) f = f
let f be
Morphism of
b,
a;
i (*) f = f
f in Hom (
b,
a)
by A22, CAT_1:def 5;
then A23:
cod f = a
by CAT_1:1;
then
cod f = dom i
by A18, CAT_1:1;
then A24:
[i,f] in dom the
Comp of
CC
by A1;
the
Target of
CC . f = a
by A23, GRAPH_1:def 4;
then
(CompMap C) . (
((IdMap C) . a),
f)
= f
by Th40;
hence
i (*) f = f
by A24, CAT_1:def 1;
verum
end;
hence
CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is Category
by A1, A2, A6, A17, CAT_1:def 6, CAT_1:def 7, CAT_1:def 8, CAT_1:def 9, CAT_1:def 10; verum