ORDERS_3: On the Category of Posets

attr f is monotone means :: ORDERS_3:def 5
for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b;

end;

:: deftheorem defines monotone ORDERS_3:def 5 :

Lm1: 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 )

proof end;

definition

let A, B be RelStr ;

func MonFuncs (A,B) -> set means :Def6: :: ORDERS_3:def 6
for a being set holds
( a in it iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines MonFuncs ORDERS_3:def 6 :

theorem Th6: :: ORDERS_3:6

for A, B, C being non empty RelStr
for f, g being Function st f in MonFuncs (A,B) & g in MonFuncs (B,C) holds
g * f in MonFuncs (A,C)

proof end;

theorem Th7: :: ORDERS_3:7

for T being non empty RelStr holds id the carrier of T in MonFuncs (T,T)

proof end;

registration

let T be non empty RelStr ;

cluster MonFuncs (T,T) -> non empty ;

coherence by Th7;

end;

definition

let X be set ;

func Carr X -> set means :Def7: :: ORDERS_3:def 7
for a being set holds
( a in it iff ex s being 1-sorted st
( s in X & a = the carrier of s ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Carr ORDERS_3:def 7 :

Lm2: for P being non empty POSet_set
for A being Element of P holds the carrier of A in Carr P
by Def7;

registration

let P be non empty POSet_set;

cluster Carr P -> non empty ;

coherence by Lm2;

end;

theorem :: ORDERS_3:8

for f being 1-sorted holds Carr {f} = { the carrier of f}

proof end;

theorem :: ORDERS_3:9

for f, g being 1-sorted holds Carr {f,g} = { the carrier of f, the carrier of g}

proof end;

theorem Th10: :: ORDERS_3:10

for P being non empty POSet_set
for A, B being Element of P holds MonFuncs (A,B) c= Funcs (Carr P)

proof end;

theorem Th11: :: ORDERS_3:11

for A, B being RelStr holds MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B)

proof end;

registration

let A, B be non empty Poset;

cluster MonFuncs (A,B) -> functional ;

coherence

proof end;

end;

definition

let P be non empty POSet_set;

func POSCat P -> strict with_triple-like_morphisms Category means :: ORDERS_3:def 8
( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines POSCat ORDERS_3:def 8 :

scheme :: ORDERS_3:sch 1
AltCatEx{ F₁() -> non empty set , F₂( object , object ) -> functional set } :

ex C being strict AltCatStr st
( the carrier of C = F₁() & ( for i, j being Element of F₁() holds
( the Arrows of C . (i,j) = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C . (i,j,k) = FuncComp (F₂(i,j),F₂(j,k)) ) ) ) )

provided

A1: for i, j, k being Element of F₁()
for f, g being Function st f in F₂(i,j) & g in F₂(j,k) holds
g * f in F₂(i,k)

proof end;

scheme :: ORDERS_3:sch 2
AltCatUniq{ F₁() -> non empty set , F₂( object , object ) -> functional set } :

for C1, C2 being strict AltCatStr st the carrier of C1 = F₁() & ( for i, j being Element of F₁() holds
( the Arrows of C1 . (i,j) = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C1 . (i,j,k) = FuncComp (F₂(i,j),F₂(j,k)) ) ) ) & the carrier of C2 = F₁() & ( for i, j being Element of F₁() holds
( the Arrows of C2 . (i,j) = F₂(i,j) & ( for i, j, k being Element of F₁() holds the Comp of C2 . (i,j,k) = FuncComp (F₂(i,j),F₂(j,k)) ) ) ) holds
C1 = C2

proof end;

definition

let P be non empty POSet_set;

func POSAltCat P -> strict AltCatStr means :Def9: :: ORDERS_3:def 9
( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines POSAltCat ORDERS_3:def 9 :

registration

let P be non empty POSet_set;

cluster POSAltCat P -> non empty transitive strict ;

coherence

proof end;

end;

registration

let P be non empty POSet_set;

cluster POSAltCat P -> strict associative with_units ;

coherence

proof end;

end;

theorem :: ORDERS_3:12

for P being non empty POSet_set
for o1, o2 being Object of (POSAltCat P)
for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)

proof end;