ORDERS_3: On the Category of Posets

:: On the Category of Posets
:: by Adam Grabowski
::
:: Received January 22, 1996
:: Copyright (c) 1996 Association of Mizar Users

begin

definition

let IT be RelStr ;
attr IT is discrete means :Def1: :: ORDERS_3:def 1
the InternalRel of IT = id the carrier of IT;

end;

:: deftheorem Def1 defines discrete ORDERS_3:def 1 :

registration

cluster non empty strict V58() reflexive transitive antisymmetric discrete RelStr ;
existence

proof end;

end;

registration

cluster RelStr(# {},(id {}) #) -> empty ;
coherence ;
let P be empty RelStr ;
cluster the InternalRel of P -> empty ;
coherence ;

end;

Lm1: for P being RelStr st P is empty holds
P is discrete

proof end;

registration

cluster empty -> discrete RelStr ;
coherence by Lm1;

end;

definition

let P be RelStr ;
let IT be Subset of P;
attr IT is disconnected means :Def2: :: ORDERS_3:def 2
ex A, B being Subset of P st
( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = ( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) );

end;

:: deftheorem Def2 defines disconnected ORDERS_3:def 2 :

notation

let P be RelStr ;
let IT be Subset of P;
antonym connected IT for disconnected ;

end;

definition

let IT be RelStr ;
attr IT is disconnected means :Def3: :: ORDERS_3:def 3
[#] IT is disconnected ;

end;

:: deftheorem Def3 defines disconnected ORDERS_3:def 3 :

notation

let IT be RelStr ;
antonym connected IT for disconnected ;

end;

theorem :: ORDERS_3:1

for DP being non empty discrete RelStr
for x, y being Element of DP holds
( x <= y iff x = y )

proof end;

theorem :: ORDERS_3:2

for R being Relation
for a being set st R is Order of {a} holds
R = id {a}

proof end;

theorem :: ORDERS_3:3

for T being non empty RelStr
for a being Element of T st T is reflexive & [#] T = {a} holds
T is discrete

proof end;

theorem Th4: :: ORDERS_3:4

for T being non empty RelStr
for a being set st [#] T = {a} holds
not T is disconnected

proof end;

theorem Th5: :: ORDERS_3:5

for DP being non empty discrete Poset st ex a, b being Element of DP st a <> b holds
DP is disconnected

proof end;

registration

cluster non empty strict V58() reflexive transitive antisymmetric connected RelStr ;
existence

proof end;

cluster non empty strict V58() reflexive transitive antisymmetric discrete disconnected RelStr ;
existence

proof end;

end;

begin

definition

let IT be set ;
attr IT is POSet_set-like means :Def4: :: ORDERS_3:def 4
for a being set st a in IT holds
a is non empty Poset;

end;

:: deftheorem Def4 defines POSet_set-like ORDERS_3:def 4 :

registration

cluster non empty POSet_set-like set ;
existence

proof end;

end;

definition

mode POSet_set is POSet_set-like set ;

end;

definition

let P be non empty POSet_set;
:: original: Element
redefine mode Element of P -> non empty Poset;
coherence by Def4;

end;

definition

let L1, L2 be RelStr ;
let f be Function of L1,L2;
attr f is monotone means :Def5: :: 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 Def5 defines monotone ORDERS_3:def 5 :

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 )

proof end;

Lm3: for T being non empty RelStr holds id T 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 :

Lm4: 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 Lm4;

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 :

begin

scheme :: ORDERS_3:sch 1
AltCatEx{ F₁() -> non empty set , F₂( set , set ) -> 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₂( set , set ) -> 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;