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


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 :
for IT being RelStr holds
( IT is discrete iff the InternalRel of IT = id the carrier of IT );

registration
cluster non empty strict V68() reflexive transitive antisymmetric discrete for RelStr ;
existence
ex b1 being Poset st
( b1 is strict & b1 is discrete & not b1 is empty )
proof end;
end;

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

registration
cluster empty -> discrete for RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
b1 is discrete ;
end;

definition
let P be RelStr ;
let IT be Subset of P;
attr IT is disconnected means :: 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 defines disconnected ORDERS_3:def 2 :
for P being RelStr
for IT being Subset of P holds
( IT is disconnected iff 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) ) );

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 :: ORDERS_3:def 3
 [#] IT is disconnected ;
end;

:: deftheorem defines disconnected ORDERS_3:def 3 :
for IT being RelStr holds
( IT is disconnected iff [#] IT is disconnected );

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
T is connected
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 V68() reflexive transitive antisymmetric connected for RelStr ;
existence
ex b1 being non empty Poset st
( b1 is strict & b1 is connected )
proof end;
cluster non empty strict V68() reflexive transitive antisymmetric discrete disconnected for RelStr ;
existence
ex b1 being non empty Poset st
( b1 is strict & b1 is disconnected & b1 is discrete )
proof end;
end;

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 :
for IT being set holds
( IT is POSet_set-like iff for a being set st a in IT holds
a is non empty Poset );

registration
cluster non empty POSet_set-like for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is POSet_set-like )
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
for b1 being Element of P holds b1 is non empty Poset by Def4;
end;

definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
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 :
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is monotone iff 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 );

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
ex b1 being set st
for a being set holds
( a in b1 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 ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 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 ) ) ) & ( for a being set holds
( a in b2 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 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines MonFuncs ORDERS_3:def 6 :
for A, B being RelStr
for b3 being set holds
( b3 = MonFuncs (A,B) iff for a being set holds
( a in b3 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 ) ) );

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
not MonFuncs (T,T) is empty 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
ex b1 being set st
for a being set holds
( a in b1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) & ( for a being set holds
( a in b2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Carr ORDERS_3:def 7 :
for X, b2 being set holds
( b2 = Carr X iff for a being set holds
( a in b2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) );

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
not Carr P is empty 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
MonFuncs (A,B) is functional
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
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)] ) )
proof end;
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
proof end;
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)] ) ) );

scheme :: ORDERS_3:sch 1
AltCatEx{ F1() -> non empty set , F2( object , object ) -> 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)
proof end;

scheme :: ORDERS_3:sch 2
AltCatUniq{ F1() -> non empty set , F2( object , object ) -> 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
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
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))) ) ) ) )
proof end;
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
proof end;
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))) ) ) ) ) );

registration
let P be non empty POSet_set;
cluster POSAltCat P -> non empty transitive strict ;
coherence
( POSAltCat P is transitive & not POSAltCat P is empty )
proof end;
end;

registration
let P be non empty POSet_set;
cluster POSAltCat P -> strict associative with_units ;
coherence
( POSAltCat P is associative & POSAltCat P is with_units )
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;