:: On the Category of Posets
:: by Adam Grabowski
::
:: Received January 22, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDERS_2, NATTRA_1, RELAT_1, STRUCT_0, XBOOLE_0, ORDERS_1,
SUBSET_1, WELLORD1, RELAT_2, XXREAL_0, TARSKI, ZFMISC_1, FUNCT_1, SEQM_3,
FUNCT_2, CAT_5, CAT_1, ALTCAT_1, PBOOLE, FUNCOP_1, BINOP_1, ORDERS_3,
MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDERS_1,
CAT_5, XTUPLE_0, MCART_1, WELLORD1, MULTOP_1, PBOOLE, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1, STRUCT_0, ORDERS_2, CAT_1, ENS_1,
ALTCAT_1;
constructors RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_2, ENS_1, CAT_5,
ALTCAT_1, MULTOP_1, PBOOLE, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
STRUCT_0, ORDERS_2, ENS_1, CAT_5, ALTCAT_1;
requirements BOOLE, SUBSET;
definitions TARSKI, ALTCAT_1, FUNCOP_1, XBOOLE_0;
equalities ALTCAT_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;
theorems RELAT_1, RELSET_1, ORDERS_2, TARSKI, ZFMISC_1, WELLORD1, SYSREL,
FUNCT_1, FUNCT_2, MCART_1, ENS_1, PBOOLE, MULTOP_1, ALTCAT_1, XBOOLE_0,
XBOOLE_1, PARTFUN1;
schemes TARSKI, CAT_5, ALTCAT_1, XBOOLE_0;
begin :: Preliminaries
definition
let IT be RelStr;
attr IT is discrete means
:Def1:
the InternalRel of IT = id (the carrier of IT);
end;
registration
cluster strict discrete non empty for Poset;
existence
proof
set A = the non empty set;
reconsider R = id A as Relation of A;
reconsider R as Order of A;
take RelStr(#A,R#);
thus thesis;
end;
end;
registration
cluster RelStr (#{},id {}#) -> empty;
coherence;
let P be empty RelStr;
cluster the InternalRel of P -> empty;
coherence;
end;
registration
cluster empty -> discrete for RelStr;
coherence;
end;
definition
let P be RelStr;
let IT be Subset of P;
attr IT is disconnected means
ex A,B be 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;
notation
let P be RelStr;
let IT be Subset of P;
antonym IT is connected for IT is disconnected;
end;
definition
let IT be RelStr;
attr IT is disconnected means
[#] IT is disconnected;
end;
notation
let IT be RelStr;
antonym IT is connected for IT is disconnected;
end;
reserve T for non empty RelStr,
a for Element of T;
theorem
for DP be discrete non empty RelStr, x,y be Element of DP holds x <= y
iff x = y
proof
let DP be discrete non empty RelStr, x,y be Element of DP;
hereby
assume x <= y;
then [x,y] in the InternalRel of DP by ORDERS_2:def 5;
then [x,y] in id (the carrier of DP) by Def1;
hence x = y by RELAT_1:def 10;
end;
assume x = y;
then [x,y] in id (the carrier of DP) by RELAT_1:def 10;
then [x,y] in the InternalRel of DP by Def1;
hence thesis by ORDERS_2:def 5;
end;
theorem
for R be Relation, a be set st R is Order of {a} holds R = id {a}
proof
let R be Relation, a be set;
assume
A1: R is Order of {a};
then A2: R <> {};
R c= [:{a},{a}:] by A1;
then R c= {[a,a]} by ZFMISC_1:29;
then R = { [a,a] } by A2,ZFMISC_1:33;
hence thesis by SYSREL:13;
end;
theorem
T is reflexive & [#] T = {a} implies T is discrete
proof
assume
A1: T is reflexive;
set R = the InternalRel of T;
assume
A2: [#] T = {a};
R = id {a}
proof
A3: id {a} = {[a,a]} by SYSREL:13;
R c= [:{a},{a}:] by A2;
hence R c= id {a} by A3,ZFMISC_1:29;
let x be object;
assume x in id {a};
then
A4: x = [a,a] by A3,TARSKI:def 1;
a >= a by A1,ORDERS_2:1;
hence thesis by A4,ORDERS_2:def 5;
end;
hence thesis by A2;
end;
reserve a for set;
theorem Th4:
[#] T = {a} implies T is connected
proof
reconsider OT = [#] T as non empty set;
assume
A1: [#] T = {a};
A2: for Z,Z9 be non empty Subset of OT holds not Z misses Z9
proof
let Z,Z9 be non empty Subset of OT;
Z = {a} by A1,ZFMISC_1:33;
hence thesis by A1,ZFMISC_1:33;
end;
[#] T is connected
by A2;
hence thesis;
end;
theorem Th5:
for DP be discrete non empty Poset st (ex a,b be Element of DP st
a <> b) holds DP is disconnected
proof
let DP be discrete non empty Poset;
given a,b be Element of DP such that
A1: a <> b;
not b in {a} by A1,TARSKI:def 1;
then reconsider
A = ( (the carrier of DP) \ {a} ) as non empty Subset of DP by XBOOLE_0:def 5;
reconsider B = {a} as non empty Subset of DP;
A2: the carrier of DP = ( (the carrier of DP) \ {a} ) \/ {a} & ( (the
carrier of DP) \ {a} ) misses {a} by XBOOLE_1:45,79;
the InternalRel of DP c= ([:A,A:] \/ [:B,B:])
proof
let x be object;
assume
A3: x in the InternalRel of DP;
then consider x1,x2 be object such that
A4: x = [x1,x2] by RELAT_1:def 1;
A5: x in id (the carrier of DP) by A3,Def1;
then
A6: x1 = x2 by A4,RELAT_1:def 10;
per cases;
suppose
A7: x1 in A;
A8: [:A,A:] c= ([:A,A:] \/ [:B,B:]) by XBOOLE_1:7;
[x1,x1] in [:A,A:] by A7,ZFMISC_1:87;
hence thesis by A4,A6,A8;
end;
suppose
A9: not x1 in A;
x1 in the carrier of DP by A5,A4,RELAT_1:def 10;
then x1 in (the carrier of DP) \ A by A9,XBOOLE_0:def 5;
then x1 in (the carrier of DP) /\ B by XBOOLE_1:48;
then x1 in B by XBOOLE_1:28;
then
A10: [x1,x1] in [:B,B:] by ZFMISC_1:87;
[:B,B:] c= ([:A,A:] \/ [:B,B:]) by XBOOLE_1:7;
hence thesis by A4,A6,A10;
end;
end;
then
A11: the InternalRel of DP = ((the InternalRel of DP) /\ ([:A,A:] \/ [:B,B:]
)) by XBOOLE_1:28;
(the InternalRel of DP) |_2 A = ((the InternalRel of DP) /\ [:A,A:]) & (
the InternalRel of DP) |_2 B = ((the InternalRel of DP) /\ [:B,B:]) by
WELLORD1:def 6;
then the InternalRel of DP = (the InternalRel of DP) |_2 A \/ (the
InternalRel of DP) |_2 B by A11,XBOOLE_1:23;
then [#] DP is disconnected by A2;
hence thesis;
end;
registration
cluster strict connected for non empty Poset;
existence
proof
set x = the set;
reconsider A = RelStr (#{x},id {x}#) as non empty Poset;
A is connected by Th4;
hence thesis;
end;
cluster strict disconnected discrete for non empty Poset;
existence
proof
ex Y be non empty Poset st Y is strict & Y is disconnected & Y is discrete
proof
reconsider A = RelStr (#{1,2},id {1,2}#) as non empty Poset;
reconsider A as discrete non empty Poset by Def1;
take A;
ex a,b be Element of A st a <> b
proof
set a = 1 , b = 2;
reconsider a, b as Element of A by TARSKI:def 2;
take a, b;
thus thesis;
end;
hence thesis by Th5;
end;
hence thesis;
end;
end;
begin :: Category of Posets
definition
let IT be set;
attr IT is POSet_set-like means
:Def4:
for a be set st a in IT holds a is non empty Poset;
end;
registration
cluster non empty POSet_set-like for set;
existence
proof
set P = the non empty Poset;
set A = {P};
take A;
for a be set st a in A holds a is non empty Poset by TARSKI:def 1;
hence thesis;
end;
end;
definition
mode POSet_set is POSet_set-like set;
end;
definition
let P be non empty POSet_set;
redefine mode Element of P -> non empty Poset; :: redefines Element (SUBSET_1, definition)
coherence by Def4;
end;
definition
let L1,L2 be RelStr;
let f be Function of L1, L2;
attr f is monotone means
for x,y being Element of L1 st x <= y for a,
b being Element of L2 st a = f.x & b = f.y holds a <= b;
end;
Lm1: for A,B,C be non empty RelStr for f be Function of A, B, g be Function of
B, C st f is monotone & g is monotone ex gf be Function of A, C st gf = g * f &
gf is monotone
proof
let A,B,C be non empty RelStr;
let f be Function of A, B, g be Function of B, C;
assume that
A1: f is monotone and
A2: g is monotone;
reconsider gf = g * f as Function of A, C;
take gf;
now
let p1,p2 be Element of A;
reconsider p19 = f.p1, p29 = f.p2 as Element of B;
dom f = the carrier of A by FUNCT_2:def 1;
then
A3: g.(f.p1) = (g*f).p1 & g.(f.p2) = (g*f).p2 by FUNCT_1:13;
assume p1 <= p2;
then
A4: p19 <= p29 by A1;
let r1, r2 be Element of C;
assume r1 = gf.p1 & r2 = gf.p2;
hence r1 <= r2 by A2,A3,A4;
end;
hence thesis;
end;
reserve P for non empty POSet_set,
A,B for Element of P;
definition
let A,B be RelStr;
func MonFuncs (A,B) -> set means
:Def6:
a in it iff ex f be Function of A, B st a =
f & f in Funcs (the carrier of A, the carrier of B) & f is monotone;
existence
proof
defpred P[object] means
ex f be Function of A, B st f = $1 & f is monotone;
consider AB be set such that
A1: for a be object holds a in AB iff a in Funcs (the carrier of A, the
carrier of B) & P[a] from XBOOLE_0:sch 1;
take AB;
thus a in AB iff ex f be Function of A, B st a = f & f in Funcs (the
carrier of A, the carrier of B) & f is monotone
proof
hereby
assume
A2: a in AB;
then consider f be Function of A, B such that
A3: f = a & f is monotone by A1;
take f;
thus a = f & f in Funcs (the carrier of A, the carrier of B) & f is
monotone by A1,A2,A3;
end;
given f be Function of A, B such that
A4: a = f & f in Funcs (the carrier of A, the carrier of B) & f is monotone;
thus thesis by A1,A4;
end;
end;
uniqueness
proof
let A1, A2 be set such that
A5: a in A1 iff ex f be Function of A, B st a = f & f in Funcs (the
carrier of A, the carrier of B) & f is monotone and
A6: a in A2 iff ex f be Function of A, B st a = f & f in Funcs (the
carrier of A, the carrier of B) & f is monotone;
for a being object holds a in A2 implies a in A1
proof let a be object;
assume a in A2;
then ex f be Function of A, B st a = f & f in Funcs (the carrier of A,
the carrier of B) &f is monotone by A6;
hence thesis by A5;
end;
then
A7: A2 c= A1;
for a being object holds a in A1 implies a in A2
proof let a be object;
assume a in A1;
then ex f be Function of A, B st a = f & f in Funcs (the carrier of A,
the carrier of B) & f is monotone by A5;
hence thesis by A6;
end;
then A1 c= A2;
hence A1 = A2 by A7;
end;
end;
theorem Th6:
for A,B,C be non empty RelStr for f,g be Function st f in
MonFuncs (A,B) & g in MonFuncs (B,C) holds (g*f) in MonFuncs (A,C)
proof
let A,B,C be non empty RelStr;
let f,g be Function;
assume that
A1: f in MonFuncs (A,B) and
A2: g in MonFuncs (B,C);
consider f9 be Function of A, B such that
A3: f = f9 and
f9 in Funcs (the carrier of A, the carrier of B) and
A4: f9 is monotone by A1,Def6;
consider g9 be Function of B, C such that
A5: g = g9 and
g9 in Funcs (the carrier of B, the carrier of C) and
A6: g9 is monotone by A2,Def6;
consider gf be Function of A,C such that
A7: gf = g9 * f9 & gf is monotone by A4,A6,Lm1;
gf in Funcs (the carrier of A, the carrier of C) by FUNCT_2:8;
hence thesis by A3,A5,A7,Def6;
end;
theorem Th7:
id the carrier of T in MonFuncs (T,T)
proof
reconsider IT = id T as Function of the carrier of T, the carrier of T;
reconsider IT9 = IT as Function of T,T;
id T is monotone & IT9 in Funcs (the carrier of T, the carrier of T) by
FUNCT_2:9;
hence thesis by Def6;
end;
registration
let T;
cluster MonFuncs (T,T) -> non empty;
coherence by Th7;
end;
definition
let X be set;
func Carr X -> set means
:Def7:
a in it iff ex s be 1-sorted st s in X & a = the carrier of s;
existence
proof
defpred P[object,object] means
ex s be 1-sorted st s = $1 & $2 = the carrier of s;
A1: for x,y,z be object st P[x,y] & P[x,z] holds y = z;
consider CX be set such that
A2: for x be object holds x in CX iff ex y be object st y in X & P[y,x]
from TARSKI:sch 1(A1);
take CX;
let x be set;
x in CX iff ex s be 1-sorted st s in X & x = the carrier of s
proof
thus x in CX implies ex s be 1-sorted st s in X & x = the carrier of s
proof
assume x in CX;
then consider y be object such that
A3: y in X and
A4: ex s be 1-sorted st s = y & x = the carrier of s by A2;
consider s be 1-sorted such that
A5: s = y and
x = the carrier of s by A4;
take s;
thus thesis by A3,A4,A5;
end;
given s be 1-sorted such that
A6: s in X & x = the carrier of s;
thus thesis by A2,A6;
end;
hence thesis;
end;
uniqueness
proof
let C1,C2 be set;
assume that
A7: a in C1 iff ex s be 1-sorted st s in X & a = the carrier of s and
A8: a in C2 iff ex s be 1-sorted st s in X & a = the carrier of s;
for a being object holds a in C1 iff a in C2
proof let a be object;
thus a in C1 implies a in C2
proof
assume a in C1;
then ex s be 1-sorted st s in X & a = the carrier of s by A7;
hence thesis by A8;
end;
thus a in C2 implies a in C1
proof
assume a in C2;
then ex s be 1-sorted st s in X & a = the carrier of s by A8;
hence thesis by A7;
end;
end;
hence thesis by TARSKI:2;
end;
end;
Lm2: the carrier of A in Carr P by Def7;
registration
let P;
cluster Carr P -> non empty;
coherence by Lm2;
end;
theorem
for f be 1-sorted holds Carr {f} = {the carrier of f}
proof
let f be 1-sorted;
thus Carr {f} c= {the carrier of f}
proof
let a be object;
assume a in Carr {f};
then consider s be 1-sorted such that
A1: s in {f} and
A2: a = the carrier of s by Def7;
s = f by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
A3: f in {f} by TARSKI:def 1;
thus {the carrier of f} c= Carr {f}
proof
let a be object;
assume a in {the carrier of f};
then a = the carrier of f by TARSKI:def 1;
hence thesis by A3,Def7;
end;
end;
theorem
for f,g be 1-sorted holds Carr {f,g} = {the carrier of f, the carrier of g }
proof
let f,g be 1-sorted;
thus Carr {f,g} c= {the carrier of f, the carrier of g}
proof
let a be object;
assume a in Carr {f,g};
then consider s be 1-sorted such that
A1: s in {f,g} and
A2: a = the carrier of s by Def7;
per cases by A1,TARSKI:def 2;
suppose
s = f;
hence thesis by A2,TARSKI:def 2;
end;
suppose
s = g;
hence thesis by A2,TARSKI:def 2;
end;
end;
thus {the carrier of f, the carrier of g} c= Carr {f,g}
proof
let a be object;
A3: f in {f,g} by TARSKI:def 2;
A4: g in {f,g} by TARSKI:def 2;
assume
A5: a in {the carrier of f, the carrier of g};
per cases by A5,TARSKI:def 2;
suppose
a = the carrier of f;
hence thesis by A3,Def7;
end;
suppose
a = the carrier of g;
hence thesis by A4,Def7;
end;
end;
end;
theorem Th10:
MonFuncs (A,B) c= Funcs Carr P
proof
reconsider CA = the carrier of A, CB = the carrier of B as Element of Carr P
by Def7;
let x be object;
assume x in MonFuncs(A,B);
then
A1: ex g be Function of A, B st x = g & g in Funcs (the carrier of A, the
carrier of B) & g is monotone by Def6;
Funcs (CA,CB) c= Funcs Carr P by ENS_1:2;
hence thesis by A1;
end;
theorem Th11:
for A,B be RelStr holds MonFuncs (A,B) c= Funcs (the carrier of
A,the carrier of B)
proof
let A,B be RelStr;
let a be object;
assume a in MonFuncs (A,B);
then ex f be Function of A, B st a = f & f in Funcs (the carrier of A, the
carrier of B) & f is monotone by Def6;
hence thesis;
end;
registration
let A,B be non empty Poset;
cluster MonFuncs (A,B) -> functional;
coherence
proof
reconsider X = MonFuncs (A,B) as Subset of Funcs (the carrier of A,the
carrier of B) by Th11;
X is functional;
hence thesis;
end;
end;
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 be Element of P, f be Element of Funcs Carr P st f
in MonFuncs (a,b) holds [[a,b],f] is Morphism of it) & (for m be Morphism of it
ex a,b be Element of P, f be Element of Funcs (Carr P) st m = [[a,b],f] & f in
MonFuncs (a,b)) & for m1,m2 be (Morphism of it), a1,a2,a3 be Element of P, f1,
f2 be Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2(*)m1 = [[a1,a3], f2*f1];
existence
proof
deffunc F(Function, Function) = $1*$2;
defpred P[Element of P, Element of P, set] means $3 in MonFuncs($1,$2);
A1: for a,b,c be Element of P, f,g be Element of Funcs (Carr P) st P[a,b,f
] & P[b,c,g] holds F(g,f) in Funcs (Carr P) & P[a,c,F(g,f)]
proof
let a,b,c be Element of P;
let f,g be Element of Funcs (Carr P);
assume f in MonFuncs(a,b) & g in MonFuncs (b,c);
then
A2: (g*f) in MonFuncs (a,c) by Th6;
MonFuncs (a,c) c= Funcs (Carr P) by Th10;
hence thesis by A2;
end;
A3: for a be Element of P ex f be Element of Funcs (Carr P) st P[a,a,f] &
for b be Element of P, g be Element of Funcs (Carr P) holds (P[a,b,g] implies F
(g,f) = g) & (P[b,a,g] implies F(f,g) = g)
proof
let a be Element of P;
set f = id the carrier of a;
MonFuncs (a,a) c= Funcs (Carr P) & f in MonFuncs (a,a) by Th7,Th10;
then reconsider f as Element of Funcs (Carr P);
take f;
now
let b be Element of P, g be Element of Funcs (Carr P);
A4: g in MonFuncs (b,a) implies (f*g) = g
proof
assume g in MonFuncs (b,a);
then ex g9 be Function of b, a st g9 = g & g9 in Funcs (the carrier
of b, the carrier of a) & g9 is monotone by Def6;
then reconsider g as Function of the carrier of b, the carrier of a;
rng g c= the carrier of a;
hence thesis by RELAT_1:53;
end;
g in MonFuncs (a,b) implies (g*f) = g
proof
assume g in MonFuncs (a,b);
then ex g9 be Function of a, b st g9 = g & g9 in Funcs (the carrier
of a, the carrier of b) & g9 is monotone by Def6;
then reconsider g as Function of the carrier of a, the carrier of b;
dom g = the carrier of a by FUNCT_2:def 1;
hence thesis by RELAT_1:51;
end;
hence (g in MonFuncs (a,b) implies (g*f) = g) & (g in MonFuncs (b,a)
implies (f*g) = g) by A4;
end;
hence thesis by Th7;
end;
A5: for a,b,c,d be Element of P, f,g,h be Element of Funcs Carr P st P[a,
b,f] & P[b,c,g] & P[c,d,h] holds F(h,F(g,f)) = F(F(h,g),f) by RELAT_1:36;
ex C be with_triple-like_morphisms strict Category st the carrier of
C = P & (for a,b be Element of P, f be Element of Funcs (Carr P) st P[a,b,f]
holds [[a,b],f] is Morphism of C) & (for m be Morphism of C ex a,b be Element
of P, f be Element of Funcs (Carr P) st m = [[a,b],f] & P[a,b,f]) & for m1,m2
be (Morphism of C), a1,a2,a3 be Element of P, f1,f2 be Element of Funcs (Carr P
) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2(*)m1 = [[a1,a3], F(f2,f1)]
from CAT_5:sch 1(A1,A3,A5);
hence thesis;
end;
uniqueness
proof
deffunc F(Element of Funcs Carr P, Element of Funcs Carr P) = $1*$2;
defpred P[Element of P, Element of P, Element of Funcs Carr P] means $3 in
MonFuncs($1,$2);
A6: now
let a be Element of P;
thus ex f be Element of Funcs Carr P st P[a,a,f] & for b be Element of P
, g be Element of Funcs Carr P holds (P[a,b,g] implies F(g,f) = g) & (P[b,a,g]
implies F(f,g) = g)
proof
set f = id the carrier of a;
A7: f in MonFuncs (a,a) by Th7;
MonFuncs (a,a) c= Funcs (Carr P) by Th10;
then reconsider f as Element of Funcs (Carr P) by A7;
now
let b be Element of P, g be Element of Funcs (Carr P);
A8: g in MonFuncs (b,a) implies (f*g) = g
proof
assume g in MonFuncs (b,a);
then
ex g9 be Function of b, a st g9 = g & g9 in Funcs (the carrier
of b,the carrier of a) & g9 is monotone by Def6;
then reconsider
g as Function of the carrier of b, the carrier of a;
rng g c= the carrier of a;
hence thesis by RELAT_1:53;
end;
g in MonFuncs (a,b) implies (g*f) = g
proof
assume g in MonFuncs (a,b);
then
ex g9 be Function of a, b st g9 = g & g9 in Funcs (the carrier
of a,the carrier of b) & g9 is monotone by Def6;
then reconsider
g as Function of the carrier of a, the carrier of b;
dom g = the carrier of a by FUNCT_2:def 1;
hence thesis by RELAT_1:51;
end;
hence (g in MonFuncs (a,b) implies (g*f) = g) & (g in MonFuncs (b,a)
implies (f*g) = g) by A8;
end;
hence thesis by A7;
end;
end;
thus for C1, C2 be strict with_triple-like_morphisms Category st the
carrier of C1 = P & (for a,b be Element of P, f be Element of Funcs Carr P st P
[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m be Morphism of C1 ex a,b be
Element of P, f be Element of Funcs Carr P st m = [[a,b],f] & P[a,b,f]) & (for
m1,m2 be (Morphism of C1), a1,a2,a3 be Element of P, f1,f2 be Element of Funcs
Carr P st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1
)]) & the carrier of C2 = P & (for a,b be Element of P, f be Element of Funcs
Carr P st P[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m be Morphism of
C2 ex a,b be Element of P, f be Element of Funcs Carr P st m = [[a,b],f] & P[a,
b,f] ) & for m1,m2 be (Morphism of C2), a1,a2,a3 be Element of P, f1,f2 be
Element of Funcs Carr P st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 =
[[a1,a3], F(f2,f1)] holds C1 = C2 from CAT_5:sch 2(A6);
end;
end;
begin :: Alternative Category of Posets
scheme
AltCatEx {A() -> non empty set, F(object,object) -> functional set }:
ex C be
strict AltCatStr st the carrier of C = A() & for i,j be Element of A() holds (
the Arrows of C).(i,j) = F (i,j) & for i,j,k be Element of A() holds (the Comp
of C).(i,j,k) = FuncComp ( F(i,j) , F(j,k) )
provided
A1: for i,j,k be Element of A() for f,g be Function st f in F(i,j) & g
in F(j,k) holds g * f in F (i,k)
proof
deffunc H(set,set,set) = FuncComp(F($1,$2),F($2,$3));
consider M be ManySortedSet of [:A(),A():] such that
A2: for i,j be Element of A() holds M.(i,j) = F(i,j) from ALTCAT_1:sch 2;
consider c be ManySortedSet of [:A(),A(),A():] such that
A3: for i,j,k be Element of A() holds c.(i,j,k) = H(i,j,k) from ALTCAT_1
:sch 4;
c is Function-yielding
proof
let i be object;
assume i in dom c;
then i in [:A(),A(),A():];
then consider x1,x2,x3 be object such that
A4: x1 in A() & x2 in A() & x3 in A() and
A5: i = [x1,x2,x3] by MCART_1:68;
c.i = c.(x1,x2,x3) by A5,MULTOP_1:def 1
.= FuncComp(F(x1,x2),F(x2,x3)) by A3,A4;
hence thesis;
end;
then reconsider c as ManySortedFunction of [:A(),A(),A():];
now
let i be object;
assume i in [:A(),A(),A():];
then consider x1,x2,x3 be object such that
A6: x1 in A() and
A7: x2 in A() and
A8: x3 in A() and
A9: i = [x1,x2,x3] by MCART_1:68;
M.(x1,x2) = F(x1,x2) by A2,A6,A7;
then
A10: [:F(x2,x3),F(x1,x2):] = [:M.(x2,x3),M.(x1,x2):] by A2,A7,A8
.= {|M,M|}.(x1,x2,x3) by A6,A7,A8,ALTCAT_1:def 4
.= {|M,M|}.i by A9,MULTOP_1:def 1;
A11: {|M|}.i = {|M|}.(x1,x2,x3) by A9,MULTOP_1:def 1
.= M.(x1,x3) by A6,A7,A8,ALTCAT_1:def 3;
A12: now
assume {|M,M|}.i <> {};
then consider j be object such that
A13: j in [:F(x2,x3),F(x1,x2):] by A10,XBOOLE_0:def 1;
consider j1,j2 be object such that
A14: j1 in F(x2,x3) and
A15: j2 in F(x1,x2) and
j = [j1,j2] by A13,ZFMISC_1:84;
reconsider j2 as Function by A15;
reconsider j1 as Function by A14;
j1*j2 in F (x1,x3) by A1,A6,A7,A8,A14,A15;
hence {|M|}.i <> {} by A2,A6,A8,A11;
end;
A16: c.i = c.(x1,x2,x3) by A9,MULTOP_1:def 1
.= FuncComp(F(x1,x2),F(x2,x3)) by A3,A6,A7,A8;
then reconsider ci = c.i as Function;
A17: dom ci = [:F(x2,x3),F(x1,x2):] by A16,PARTFUN1:def 2;
rng FuncComp(F(x1,x2),F(x2,x3)) c= F (x1,x3)
proof
set F = FuncComp(F(x1,x2),F(x2,x3));
let i be object;
assume i in rng F;
then consider j be object such that
A18: j in dom F and
A19: i = F.j by FUNCT_1:def 3;
consider f,g be Function such that
A20: j = [g,f] and
A21: F.j = g*f by A18,ALTCAT_1:def 9;
g in F(x2,x3) & f in F(x1,x2) by A18,A20,ZFMISC_1:87;
hence thesis by A1,A6,A7,A8,A19,A21;
end;
then rng ci c= {|M|}.i by A2,A6,A8,A16,A11;
hence c.i is Function of {|M,M|}.i, {|M|}.i by A17,A10,A12,FUNCT_2:def 1
,RELSET_1:4;
end;
then reconsider c as BinComp of M by PBOOLE:def 15;
set C = AltCatStr(#A(),M,c#);
take C;
thus the carrier of C = A();
let i,j be Element of A();
thus (the Arrows of C).(i,j) = F (i,j) by A2;
let i,j,k be Element of A();
thus thesis by A3;
end;
scheme
AltCatUniq {A() -> non empty set, F(object,object) -> functional set } :
for C1,C2
be strict AltCatStr st ( the carrier of C1 = A() & for i,j be Element of A()
holds (the Arrows of C1).(i,j) = F (i,j) & for i,j,k be Element of A() holds (
the Comp of C1).(i,j,k) = FuncComp ( F(i,j) , F(j,k) ) ) & ( the carrier of C2
= A() & for i,j be Element of A() holds (the Arrows of C2).(i,j) = F (i,j) &
for i,j,k be Element of A() holds (the Comp of C2).(i,j,k) = FuncComp ( F(i,j)
, F(j,k) ) ) holds C1 = C2 proof
let C1,C2 be strict AltCatStr;
assume that
A1: the carrier of C1 = A() and
A2: for i,j be Element of A() holds (the Arrows of C1).(i,j) = F (i,j) &
for i,j,k be Element of A() holds (the Comp of C1).(i,j,k) = FuncComp ( F(i,j)
, F(j,k) ) and
A3: the carrier of C2 = A() and
A4: for i,j be Element of A() holds (the Arrows of C2).(i,j) = F (i,j) &
for i,j,k be Element of A() holds (the Comp of C2).(i,j,k) = FuncComp ( F(i,j)
, F(j,k) );
A5: now
let i,j,k be object;
assume
A6: i in A() & j in A() & k in A();
hence (the Comp of C1).(i,j,k) = FuncComp ( F(i,j) , F(j,k) ) by A2
.= (the Comp of C2).(i,j,k) by A4,A6;
end;
now
let i,j be Element of A();
thus (the Arrows of C1).(i,j) = F (i,j) by A2
.= (the Arrows of C2).(i,j) by A4;
end;
then the Arrows of C1 = the Arrows of C2 by A1,A3,ALTCAT_1:7;
hence thesis by A1,A3,A5,ALTCAT_1:8;
end;
definition
let P be non empty POSet_set;
func POSAltCat P -> strict AltCatStr means
:Def9:
the carrier of it = P &
for i,j be Element of P holds (the Arrows of it).(i,j) = MonFuncs (i,j) & for i
,j,k be Element of P holds (the Comp of it).(i,j,k) = FuncComp ( MonFuncs (i,j)
, MonFuncs (j,k) );
existence
proof
A1: for i,j,k be Element of P for f,g be Function st f in MonFuncs(i,j) &
g in MonFuncs(j,k) holds g * f in MonFuncs(i,k) by Th6;
thus ex C be strict AltCatStr st the carrier of C = P & for i,j be Element
of P holds (the Arrows of C).(i,j) = MonFuncs(i,j) & for i,j,k be Element of P
holds (the Comp of C).(i,j,k) = FuncComp ( MonFuncs(i,j) , MonFuncs(j,k) ) from
AltCatEx(A1);
end;
uniqueness
proof
thus for C1,C2 be strict AltCatStr st ( the carrier of C1 = P & for i,j be
Element of P holds (the Arrows of C1).(i,j) = MonFuncs(i,j) & for i,j,k be
Element of P holds (the Comp of C1).(i,j,k) = FuncComp ( MonFuncs(i,j) ,
MonFuncs(j,k) ) ) & ( the carrier of C2 = P & for i,j be Element of P holds (
the Arrows of C2).(i,j) = MonFuncs(i,j) & for i,j,k be Element of P holds (the
Comp of C2).(i,j,k) = FuncComp ( MonFuncs(i,j) , MonFuncs(j,k) ) ) holds C1 =
C2 from AltCatUniq;
end;
end;
registration
let P be non empty POSet_set;
cluster POSAltCat P -> transitive non empty;
coherence
proof
set A = POSAltCat P;
thus A is transitive
proof
let o1,o2,o3 be Object of A;
reconsider o19 = o1,o29 = o2,o39 = o3 as Element of P by Def9;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
MonFuncs (o19,o29) <> {} by A1,Def9;
then consider f be object such that
A3: f in MonFuncs (o19,o29) by XBOOLE_0:def 1;
MonFuncs (o29,o39) <> {} by A2,Def9;
then consider g be object such that
A4: g in MonFuncs (o29,o39) by XBOOLE_0:def 1;
reconsider f,g as Function by A3,A4;
g * f in MonFuncs (o19,o39) by A3,A4,Th6;
hence thesis by Def9;
end;
thus thesis by Def9;
end;
end;
registration
let P be non empty POSet_set;
cluster POSAltCat P -> associative with_units;
coherence
proof
set A = POSAltCat P;
set G = the Arrows of A, C = the Comp of A;
thus C is associative
proof
let i,j,k,l be Element of A;
let f,g,h be set;
reconsider i9=i,j9=j,k9=k,l9=l as Element of P by Def9;
assume that
A1: f in G.(i,j) and
A2: g in G.(j,k) and
A3: h in G.(k,l);
A4: g in MonFuncs (j9,k9) by A2,Def9;
A5: h in MonFuncs (k9,l9) by A3,Def9;
A6: f in MonFuncs (i9,j9) by A1,Def9;
then reconsider f9 = f, g9=g,h9=h as Function by A4,A5;
A7: C.(i,j,l) = FuncComp ( MonFuncs (i9,j9) , MonFuncs (j9,l9) ) by Def9;
C.(j,k,l) = FuncComp ( MonFuncs (j9,k9) , MonFuncs (k9,l9) ) by Def9;
then
A8: C.(j,k,l).(h,g) = h9 * g9 by A4,A5,ALTCAT_1:11;
C.(i,j,k) = FuncComp ( MonFuncs (i9,j9) , MonFuncs (j9,k9) ) by Def9;
then
A9: C.(i,j,k).(g,f) = g9 * f9 by A6,A4,ALTCAT_1:11;
h9 * g9 in MonFuncs (j9,l9) by A4,A5,Th6;
then
A10: C.(i,j,l).((h9 *g9),f9) = (h9 * g9) * f9 by A6,A7,ALTCAT_1:11;
A11: C.(i,k,l) = FuncComp ( MonFuncs (i9,k9) , MonFuncs (k9,l9) ) by Def9;
g9 * f9 in MonFuncs (i9,k9) by A6,A4,Th6;
then C.(i,k,l).(h,g9*f9) = h9 * ( g9 *f9) by A5,A11,ALTCAT_1:11;
hence thesis by A9,A8,A10,RELAT_1:36;
end;
thus C is with_left_units
proof
let j be Element of A;
reconsider j9 = j as Element of P by Def9;
take e = id the carrier of j9;
G.(j,j) = MonFuncs (j9,j9) by Def9;
hence e in G.(j,j) by Th7;
let i be Element of A, f be set;
reconsider i9 = i as Element of P by Def9;
A12: C.(i,j,j) = FuncComp ( MonFuncs (i9,j9) , MonFuncs (j9,j9) ) by Def9;
assume f in G.(i,j);
then
A13: f in MonFuncs(i9,j9) by Def9;
then consider f9 be Function of i9, j9 such that
A14: f = f9 and
f9 in Funcs (the carrier of i9,the carrier of j9) and
f9 is monotone by Def6;
A15: e in MonFuncs (j9,j9) by Th7;
then consider e9 be Function of j9, j9 such that
A16: e = e9 and
e9 in Funcs (the carrier of j9,the carrier of j9) and
e9 is monotone by Def6;
rng f9 c= the carrier of j9;
then e9 * f9 = f by A16,A14,RELAT_1:53;
hence thesis by A15,A16,A13,A14,A12,ALTCAT_1:11;
end;
thus C is with_right_units
proof
let i be Element of A;
reconsider i9 = i as Element of P by Def9;
take e = id the carrier of i9;
G.(i,i) = MonFuncs (i9,i9) by Def9;
hence e in G.(i,i) by Th7;
let j be Element of A, f be set;
reconsider j9 = j as Element of P by Def9;
A17: C.(i,i,j) = FuncComp ( MonFuncs (i9,i9) , MonFuncs (i9,j9) ) by Def9;
assume f in G.(i,j);
then
A18: f in MonFuncs(i9,j9) by Def9;
then consider f9 be Function of i9, j9 such that
A19: f = f9 and
f9 in Funcs (the carrier of i9,the carrier of j9) and
f9 is monotone by Def6;
A20: e in MonFuncs (i9,i9) by Th7;
then consider e9 be Function of i9, i9 such that
A21: e = e9 and
e9 in Funcs (the carrier of i9,the carrier of i9) and
e9 is monotone by Def6;
dom f9 = the carrier of i9 by FUNCT_2:def 1;
then f9 * e9 = f by A21,A19,RELAT_1:52;
hence thesis by A20,A21,A18,A19,A17,ALTCAT_1:11;
end;
end;
end;
theorem
for o1,o2 be Object of POSAltCat P, A,B be Element of P st o1 = A & o2
= B holds <^ o1, o2 ^> c= Funcs (the carrier of A, the carrier of B)
proof
let o1,o2 be Object of POSAltCat P, A,B be Element of P;
assume
A1: o1 = A & o2 = B;
let x be object;
assume x in <^ o1, o2 ^>;
then x in MonFuncs (A,B) by A1,Def9;
then ex f be Function of A, B st f = x & f in Funcs (the carrier of A,the
carrier of B) & f is monotone by Def6;
hence thesis;
end;