begin
Lm1:
for P being RelStr st P is empty holds
P is discrete
begin
Lm2:
for A, B, C being non empty RelStr
for f being Function of A,B
for g being Function of B,C st f is monotone & g is monotone holds
ex gf being Function of A,C st
( gf = g * f & gf is monotone )
Lm3:
for T being non empty RelStr holds id T is monotone
Lm4:
for P being non empty POSet_set
for A being Element of P holds the carrier of A in Carr P
by Def7;
definition
let P be non
empty POSet_set;
func POSCat P -> strict with_triple-like_morphisms Category means
( the
carrier of
it = P & ( for
a,
b being
Element of
P for
f being
Element of
Funcs (Carr P) st
f in MonFuncs (
a,
b) holds
[[a,b],f] is
Morphism of
it ) & ( for
m being
Morphism of
it ex
a,
b being
Element of
P ex
f being
Element of
Funcs (Carr P) st
(
m = [[a,b],f] &
f in MonFuncs (
a,
b) ) ) & ( for
m1,
m2 being
Morphism of
it for
a1,
a2,
a3 being
Element of
P for
f1,
f2 being
Element of
Funcs (Carr P) st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) );
existence
ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) )
uniqueness
for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) & the carrier of b2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) holds
b1 = b2
end;
::
deftheorem defines
POSCat ORDERS_3:def 8 :
for P being non empty POSet_set
for b2 being strict with_triple-like_morphisms Category holds
( b2 = POSCat P iff ( the carrier of b2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) );
begin
scheme
AltCatEx{
F1()
-> non
empty set ,
F2(
set ,
set )
-> functional set } :
ex
C being
strict AltCatStr st
( the
carrier of
C = F1() & ( for
i,
j being
Element of
F1() holds
( the
Arrows of
C . (
i,
j)
= F2(
i,
j) & ( for
i,
j,
k being
Element of
F1() holds the
Comp of
C . (
i,
j,
k)
= FuncComp (
F2(
i,
j),
F2(
j,
k)) ) ) ) )
provided
A1:
for
i,
j,
k being
Element of
F1()
for
f,
g being
Function st
f in F2(
i,
j) &
g in F2(
j,
k) holds
g * f in F2(
i,
k)
scheme
AltCatUniq{
F1()
-> non
empty set ,
F2(
set ,
set )
-> functional set } :
for
C1,
C2 being
strict AltCatStr st the
carrier of
C1 = F1() & ( for
i,
j being
Element of
F1() holds
( the
Arrows of
C1 . (
i,
j)
= F2(
i,
j) & ( for
i,
j,
k being
Element of
F1() holds the
Comp of
C1 . (
i,
j,
k)
= FuncComp (
F2(
i,
j),
F2(
j,
k)) ) ) ) & the
carrier of
C2 = F1() & ( for
i,
j being
Element of
F1() holds
( the
Arrows of
C2 . (
i,
j)
= F2(
i,
j) & ( for
i,
j,
k being
Element of
F1() holds the
Comp of
C2 . (
i,
j,
k)
= FuncComp (
F2(
i,
j),
F2(
j,
k)) ) ) ) holds
C1 = C2
definition
let P be non
empty POSet_set;
func POSAltCat P -> strict AltCatStr means :
Def9:
( the
carrier of
it = P & ( for
i,
j being
Element of
P holds
( the
Arrows of
it . (
i,
j)
= MonFuncs (
i,
j) & ( for
i,
j,
k being
Element of
P holds the
Comp of
it . (
i,
j,
k)
= FuncComp (
(MonFuncs (i,j)),
(MonFuncs (j,k))) ) ) ) );
existence
ex b1 being strict AltCatStr st
( the carrier of b1 = P & ( for i, j being Element of P holds
( the Arrows of b1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) )
uniqueness
for b1, b2 being strict AltCatStr st the carrier of b1 = P & ( for i, j being Element of P holds
( the Arrows of b1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) & the carrier of b2 = P & ( for i, j being Element of P holds
( the Arrows of b2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) holds
b1 = b2
end;
::
deftheorem Def9 defines
POSAltCat ORDERS_3:def 9 :
for P being non empty POSet_set
for b2 being strict AltCatStr holds
( b2 = POSAltCat P iff ( the carrier of b2 = P & ( for i, j being Element of P holds
( the Arrows of b2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) );