:: Categorial Background for Duality Theory
:: by Grzegorz Bancerek
::
:: Received August 1, 2001
:: Copyright (c) 2001-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 STRUCT_0, ORDERS_2, ORDERS_1, ZFMISC_1, FUNCT_1, RELAT_1, CARD_3,
XBOOLE_0, SUBSET_1, SETFAM_1, ORDERS_3, ALTCAT_1, YELLOW18, WAYBEL_0,
TARSKI, REWRITE1, PBOOLE, FUNCT_2, SEQM_3, FILTER_0, CAT_1, QC_LANG1,
FUNCTOR0, WELLORD1, ALTCAT_3, CAT_3, LATTICES, RELAT_2, ORDINAL1,
WELLORD2, CARD_1, LATTICE3, XXREAL_0, ORDINAL2, ARYTM_3, RCOMP_1,
TREES_2, WAYBEL_8, WAYBEL_3, ALTCAT_2, YELLOW21;
notations TARSKI, XBOOLE_0, ENUMSET1, SETFAM_1, ZFMISC_1, SUBSET_1, RELAT_1,
RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, CARD_3, BINOP_1, ORDINAL1,
CARD_1, WELLORD1, WELLORD2, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3,
ORDERS_3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_3, WAYBEL_8, ALTCAT_1,
ALTCAT_2, FUNCTOR0, ALTCAT_3, YELLOW18;
constructors WELLORD1, ORDERS_3, WAYBEL_8, ALTCAT_3, YELLOW18, RELSET_1,
WAYBEL20, ENUMSET1;
registrations SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
CARD_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0,
WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL10, FUNCTOR2, ALTCAT_4, WAYBEL17,
YELLOW_9, YELLOW18, WELLORD2;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_2, WELLORD1, WELLORD2, ORDERS_2, LATTICE3, ORDERS_3,
ALTCAT_1, ALTCAT_3, YELLOW_0, WAYBEL_0, WAYBEL_3, YELLOW18, XBOOLE_0;
equalities ALTCAT_1, YELLOW18, XBOOLE_0, BINOP_1, STRUCT_0;
expansions TARSKI, RELAT_2, WELLORD1, ORDERS_2, LATTICE3, ALTCAT_3, WAYBEL_3,
YELLOW18, XBOOLE_0;
theorems ZFMISC_1, RELAT_1, FUNCT_1, WELLORD1, WELLORD2, ORDERS_2, ORDERS_1,
FUNCT_2, ALTCAT_1, ALTCAT_2, ORDERS_3, ALTCAT_3, ORDINAL1, CARD_1,
CARD_5, WAYBEL_0, WAYBEL13, ORDINAL3, TARSKI, RELSET_1, RELAT_2,
YELLOW_0, YELLOW_2, WAYBEL_3, WAYBEL_8, YELLOW18, WAYBEL20, YELLOW16,
XBOOLE_0, XBOOLE_1, PARTFUN1, SETFAM_1, XTUPLE_0;
schemes TARSKI, CARD_3, PBOOLE, CLASSES1, YELLOW18, YELLOW20, XBOOLE_0;
begin :: Lattice-wise categories
reserve x, y for set;
definition
let a be object;
func a as_1-sorted -> 1-sorted equals
: Def1:
a if a is 1-sorted otherwise
the 1-sorted;
coherence;
consistency;
end;
definition
let W be set;
defpred P[object] means
$1 is strict Poset & the carrier of $1 as_1-sorted in W;
func POSETS W -> set means
: Def2:
for x being object holds
x in it iff x is strict Poset & the carrier of x as_1-sorted in W;
uniqueness
proof
let A,B be set such that
A1: for x being object holds x in A iff P[x] and
A2: for x being object holds x in B iff P[x];
thus thesis from XBOOLE_0:sch 2(A1,A2);
end;
existence
proof
defpred Q[object,object] means
ex P being strict Poset st $2 = P & the InternalRel of P = $1;
defpred P[set,set] means $2 is Order of $1;
deffunc F(set) = bool [:$1,$1:];
consider F being Function such that
A3: dom F = W and
A4: for x st x in W
for y holds y in F.x iff y in F(x) & P[x,y] from CARD_3:sch 3;
A5: now
let x,y,z be object;
assume Q[x,y];
then consider P1 be strict Poset such that
A6: y = P1 & the InternalRel of P1 = x;
A7: dom the InternalRel of P1 = the carrier of P1 by ORDERS_1:14;
assume Q[x,z];
hence y = z by A6,A7,ORDERS_1:14;
end;
consider A being set such that
A8: for x being object holds x in A iff
ex y being object st y in Union F & Q[y,x] from TARSKI:sch 1(A5);
take A;
let x be object;
hereby
assume x in A;
then consider y being object such that
A9: y in Union F and
A10: ex P being strict Poset st x = P & the InternalRel of P = y by A8;
consider P being strict Poset such that
A11: x = P and
A12: the InternalRel of P = y by A10;
thus x is strict Poset by A11;
consider z being object such that
A13: z in W and
A14: y in F.z by A3,A9,CARD_5:2;
reconsider z as set by TARSKI:1;
reconsider y as Order of z by A4,A13,A14;
dom y = z & dom y = the carrier of P by A12,ORDERS_1:14;
hence the carrier of x as_1-sorted in W by A11,A13,Def1;
end;
assume that
A15: x is strict Poset and
A16: the carrier of x as_1-sorted in W;
reconsider P = x as strict Poset by A15;
A17: x as_1-sorted = P by Def1;
then the InternalRel of P in F.the carrier of P by A4,A16;
then the InternalRel of P in Union F by A3,A16,A17,CARD_5:2;
hence thesis by A8;
end;
end;
registration
let W be non empty set;
cluster POSETS W -> non empty;
coherence
proof
set x = the Element of W,y = the Order of x;
RelStr(#x,y#) as_1-sorted = RelStr(#x,y#) by Def1;
hence thesis by Def2;
end;
end;
registration
let W be with_non-empty_elements set;
cluster POSETS W -> POSet_set-like;
coherence
proof
let a be set;
assume
A1: a in POSETS W;
then
A2: the carrier of a as_1-sorted in W by Def2;
reconsider a as Poset by A1,Def2;
a = a as_1-sorted by Def1;
hence thesis by A2;
end;
end;
definition
let C be category;
attr C is carrier-underlaid means
: Def3:
for a being Object of C ex S being
1-sorted st a = S & the_carrier_of a = the carrier of S;
end;
definition
let C be category;
attr C is lattice-wise means
: Def4:
C is semi-functional set-id-inheriting
& (for a being Object of C holds a is LATTICE) & for a,b being Object of C for
A,B being LATTICE st A = a & B = b holds <^a,b^> c= MonFuncs(A, B);
end;
definition
let C be category;
attr C is with_complete_lattices means
: Def5:
C is lattice-wise & for a being Object of C holds a is complete LATTICE;
end;
registration
cluster with_complete_lattices -> lattice-wise for category;
coherence;
cluster lattice-wise -> concrete carrier-underlaid for category;
coherence
proof
deffunc F(set) = the carrier of $1 as_1-sorted;
let C be category such that
A1: C is semi-functional set-id-inheriting and
A2: for a being Object of C holds a is LATTICE and
A3: for a,b being Object of C for A,B being LATTICE st A = a & B = b
holds <^a,b^> c= MonFuncs(A, B);
consider F being ManySortedSet of C such that
A4: for i being Element of C holds F.i = F(i) from PBOOLE:sch 5;
C is para-functional
proof
take F;
let a,b be Object of C;
reconsider A = a, B = b as LATTICE by A2;
A5: <^a,b^> c= MonFuncs(A, B) by A3;
b as_1-sorted = B by Def1;
then
A6: F.b = the carrier of B by A4;
a as_1-sorted = A by Def1;
then F.a = the carrier of A by A4;
then MonFuncs(A, B) c= Funcs(F.a, F.b) by A6,ORDERS_3:11;
hence thesis by A5;
end;
hence C is concrete by A1;
let a be Object of C;
reconsider S = a as LATTICE by A2;
idm a in <^a,a^> & <^a,a^> c= MonFuncs(S, S) by A3;
then consider f being Function of S,S such that
A7: idm a = f and
A8: f in Funcs(the carrier of S, the carrier of S) and
f is monotone by ORDERS_3:def 6;
take S;
thus a = S;
thus the_carrier_of a = dom id the_carrier_of a by RELAT_1:45
.= dom f by A1,A7
.= the carrier of S by A8,FUNCT_2:92;
end;
end;
scheme
localCLCatEx { A() -> non empty set, P[object,object,object] }:
ex C being strict
category st C is lattice-wise & the carrier of C = A() & for a,b being LATTICE,
f being monotone Function of a,b holds f in (the Arrows of C).(a,b) iff a in A(
) & b in A() & P[a,b,f]
provided
A1: for a being Element of A() holds a is LATTICE and
A2: for a,b,c being LATTICE st a in A() & b in A() & c in A() for f
being Function of a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a
,c,g*f] and
A3: for a being LATTICE st a in A() holds P[a,a,id a]
proof
defpred P[object,object] means
ex a,b being LATTICE, c being set st
c = $2 & $1 = [a,b] & for f being
object holds f in c iff f in MonFuncs(a, b) & P[a,b,f];
set A = A();
A4: now
let x be object;
assume x in [:A,A:];
then consider a,b being object such that
A5: a in A & b in A and
A6: x = [a,b] by ZFMISC_1:def 2;
reconsider a,b as LATTICE by A1,A5;
defpred Q[object] means P[a,b,$1];
consider y being set such that
A7: for f being object holds f in y iff f in MonFuncs(a, b) & Q[f] from
XBOOLE_0:sch 1;
reconsider y as object;
take y;
thus P[x,y] by A6,A7;
end;
consider F being Function such that
dom F = [:A,A:] and
A8: for x being object st x in [:A,A:] holds P[x, F.x]
from CLASSES1:sch 1(A4);
defpred PP[object,object] means
for a being LATTICE st a = $1 holds $2 = the
carrier of a;
A9: now
let x be object;
assume x in A;
then reconsider a = x as LATTICE by A1;
reconsider b = the carrier of a as object;
take b;
thus PP[x,b];
end;
consider D being Function such that
dom D = A and
A10: for x being object st x in A holds PP[x, D.x] from CLASSES1:sch 1(A9);
deffunc B(set,set) = F.[$1,$2];
A11: now
let a,b be LATTICE;
assume a in A & b in A;
then [a,b] in [:A,A:] by ZFMISC_1:87;
then P[[a,b], F.[a,b]] by A8;
then consider a9,b9 being LATTICE, c being set such that
A12: c = F.[a,b] and
A13: [a,b] = [a9,b9] and
A14: for f being object holds f in c iff f in MonFuncs(a9, b9) &
P[a9,b9,f];
let f be set;
A15: a = a9 & b = b9 by A13,XTUPLE_0:1;
hereby
assume
A16: f in F.[a,b];
hence P[a,b,f] by A14,A15,A12;
thus f in MonFuncs(a, b) by A14,A15,A16,A12;
then
ex g being Function of a, b st f = g & g in Funcs (the carrier of a
, the carrier of b) & g is monotone by ORDERS_3:def 6;
hence f in Funcs (the carrier of a, the carrier of b) & f is monotone
Function of a, b;
end;
assume f is monotone Function of a, b;
then reconsider g = f as monotone Function of a, b;
the carrier of b <> {} implies dom g = the carrier of a & rng g c=
the carrier of b by FUNCT_2:def 1;
then g in Funcs(the carrier of a, the carrier of b) by FUNCT_2:def 2;
then
A17: f in MonFuncs(a, b) by ORDERS_3:def 6;
assume P[a,b,f];
then f in c by A14,A15,A17;
hence f in F.[a,b] by A12;
end;
A18: for a,b,c being Element of A, f,g being Function st f in B(a,b) & g in
B(b,c) holds g*f in B(a,c)
proof
let a,b,c be Element of A, f,g be Function such that
A19: f in F.[a,b] and
A20: g in F.[b,c];
reconsider x = a, y = b, z = c as LATTICE by A1;
reconsider g9 = g as monotone Function of y,z by A11,A20;
reconsider f9 = f as monotone Function of x,y by A11,A19;
( P[x,y,f9])& P[y,z,g9] by A11,A19,A20;
then P[a,c,g9*f9] by A2;
then g9*f9 is monotone Function of x,z implies g9*f9 in F.[x,z] by A11;
hence thesis by YELLOW_2:12;
end;
deffunc D(set) = D.$1;
A21: for a,b being Element of A holds B(a,b) c= Funcs(D(a), D(b))
proof
let a,b be Element of A, f be object;
reconsider x = a, y = b as LATTICE by A1;
assume f in F.[a,b];
then f in Funcs(the carrier of x, the carrier of y) by A11;
then f in Funcs(D.a, the carrier of y) by A10;
hence thesis by A10;
end;
A22: now
let a be Element of A;
reconsider x = a as LATTICE by A1;
id (D.a) = id x & P[x,x,id x] by A3,A10;
hence id D(a) in B(a,a) by A11;
end;
consider C being concrete strict category such that
A23: the carrier of C = A and
for a being Object of C holds the_carrier_of a = D(a) and
A24: for a,b being Object of C holds <^a,b^> = B(a,b) from YELLOW18:sch
16(A18,A21,A22);
take C;
thus C is semi-functional set-id-inheriting;
thus for a being Object of C holds a is LATTICE by A1,A23;
thus for a,b being Object of C for A,B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs(A, B)
proof
let a, b be Object of C;
let A, B be LATTICE;
assume
A25: A = a & B = b;
let f be object;
<^a,b^> = F.[A,B] by A24,A25;
hence thesis by A11,A23,A25;
end;
thus the carrier of C = A() by A23;
let a,b be LATTICE, f be monotone Function of a,b;
hereby
assume
A26: f in (the Arrows of C).(a,b);
then [a,b] in dom the Arrows of C by FUNCT_1:def 2;
then
A27: [a,b] in [:A,A:] by A23;
hence a in A & b in A by ZFMISC_1:87;
reconsider x = a, y = b as Object of C by A23,A27,ZFMISC_1:87;
(the Arrows of C).[a,b] = <^x,y^> .= F.[x,y] by A24;
hence P[a,b,f] by A11,A23,A26;
end;
assume
A28: a in A() & b in A();
then reconsider x = a, y = b as Object of C by A23;
(the Arrows of C).[a,b] = <^x,y^> .= F.[x,y] by A24;
hence thesis by A11,A28;
end;
registration
cluster strict with_complete_lattices for category;
existence
proof
defpred P[set,set,set] means $3 = $3;
set L = the complete LATTICE;
A1: for a,b,c being LATTICE st a in {L} & b in {L} & c in {L} for f being
Function of a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f
];
A2: for a being LATTICE st a in {L} holds P[a,a,id a];
A3: for a be Element of {L} holds a is LATTICE by TARSKI:def 1;
consider C being strict category such that
A4: C is lattice-wise and
A5: the carrier of C = {L} and
for a,b being LATTICE, f being monotone Function of a,b holds f in (
the Arrows of C).(a,b) iff a in {L} & b in {L} & P[a,b,f] from localCLCatEx(A3,
A1,A2);
take C;
thus C is strict;
thus C is lattice-wise by A4;
let a be Object of C;
thus thesis by A5,TARSKI:def 1;
end;
end;
theorem
for C being carrier-underlaid category, a being Object of C holds
the_carrier_of a = the carrier of a as_1-sorted
proof
let C be carrier-underlaid category, a be Object of C;
ex S being 1-sorted st a = S & the_carrier_of a = the carrier of S by Def3;
hence thesis by Def1;
end;
theorem Th2:
for C being set-id-inheriting carrier-underlaid category for a
being Object of C holds idm a = id (a as_1-sorted)
proof
let C be set-id-inheriting carrier-underlaid category;
let a be Object of C;
ex S being 1-sorted st a = S & the_carrier_of a = the carrier of S by Def3;
then the_carrier_of a = the carrier of (a as_1-sorted) by Def1;
hence thesis by YELLOW18:def 10;
end;
notation
let C be lattice-wise category;
let a be Object of C;
synonym latt a for a as_1-sorted;
end;
definition
let C be lattice-wise category;
let a be Object of C;
redefine func latt a -> LATTICE equals :: redefines latt (YELLOW21, synonym) → as_1-sorted (YELLOW21, definition)
a;
coherence
proof
a is LATTICE by Def4;
hence thesis by Def1;
end;
compatibility
proof
a is LATTICE by Def4;
hence thesis by Def1;
end;
end;
notation
let C be with_complete_lattices category;
let a be Object of C;
synonym latt a for a as_1-sorted;
end;
definition
let C be with_complete_lattices category;
let a be Object of C;
redefine func latt a -> complete LATTICE; :: redefines latt (YELLOW21, synonym) → as_1-sorted (YELLOW21, definition)
coherence by Def5;
end;
definition
let C be lattice-wise category;
let a,b be Object of C such that
A1: <^a,b^> <> {};
let f be Morphism of a,b;
func @f -> monotone Function of latt a, latt b equals
: Def7:
f;
coherence
proof
f in <^a,b^> & <^a,b^> c= MonFuncs(latt a, latt b) by A1,Def4;
then ex g being Function of latt a, latt b st f = g & g in Funcs (the
carrier of latt a, the carrier of latt b) & g is monotone by ORDERS_3:def 6;
hence thesis;
end;
end;
theorem Th3:
for C being lattice-wise category for a,b,c being Object of C st
<^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of
b,c holds g*f = @g*@f
proof
let C be lattice-wise category;
let a,b,c be Object of C such that
A1: <^a,b^> <> {} & <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
f = @f & g = @g by A1,Def7;
hence thesis by A1,YELLOW18:36;
end;
scheme
CLCatEx1 { A() -> non empty set, P[set, set, set] }: ex C being lattice-wise
strict category st the carrier of C = A() & for a,b being Object of C, f being
monotone Function of latt a, latt b holds f in <^a,b^> iff P[latt a, latt b, f]
provided
A1: for a being Element of A() holds a is LATTICE and
A2: for a,b,c being LATTICE st a in A() & b in A() & c in A() for f
being Function of a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a
,c,g*f] and
A3: for a being LATTICE st a in A() holds P[a,a,id a]
proof
A4: for a being LATTICE st a in A() holds P[a,a,id a] by A3;
A5: for a,b,c being LATTICE st a in A() & b in A() & c in A() for f being
Function of a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f
] by A2;
consider C being strict category such that
A6: C is lattice-wise and
A7: the carrier of C = A() and
A8: for a,b being LATTICE, f being monotone Function of a,b holds f in (
the Arrows of C).(a,b) iff a in A() & b in A() & P[a,b,f] from localCLCatEx(A1,
A5,A4);
reconsider C as lattice-wise strict category by A6;
take C;
thus the carrier of C = A() by A7;
let a,b be Object of C;
thus thesis by A7,A8;
end;
scheme
CLCatEx2 { A() -> non empty set, L[object], P[set, set, set] }:
ex C being
lattice-wise strict category st (for x being LATTICE holds x is Object of C iff
x is strict & L[x] & the carrier of x in A()) & for a,b being Object of C, f
being monotone Function of latt a, latt b holds f in <^a,b^> iff P[latt a, latt
b, f]
provided
A1: ex x being strict LATTICE st L[x] & the carrier of x in A() and
A2: for a,b,c being LATTICE st L[a] & L[b] & L[c] for f being Function
of a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] and
A3: for a being LATTICE st L[a] holds P[a,a,id a]
proof
defpred p[object] means $1 is LATTICE & L[$1];
consider A being set such that
A4: for x being object holds x in A iff x in POSETS A() & p[x]
from XBOOLE_0:sch 1;
consider x being strict LATTICE such that
A5: L[x] and
A6: the carrier of x in A() by A1;
x as_1-sorted = x by Def1;
then x in POSETS A() by A6,Def2;
then reconsider A as non empty set by A4,A5;
A7: now
let a,b,c be LATTICE;
assume that
A8: a in A & b in A and
A9: c in A;
A10: L[c] by A4,A9;
( L[a])& L[b] by A4,A8;
hence
for f being Function of a,b, g being Function of b,c st P[a,b,f] & P[
b,c,g] holds P[a,c,g*f] by A2,A10;
end;
A11: for a being LATTICE st a in A holds P[a,a,id a] by A3,A4;
A12: for a being Element of A holds a is LATTICE by A4;
consider C being lattice-wise strict category such that
A13: the carrier of C = A and
A14: for a,b being Object of C, f being monotone Function of latt a,
latt b holds f in <^a,b^> iff P[latt a, latt b, f] from CLCatEx1(A12,A7,A11);
take C;
hereby
let x be LATTICE;
x as_1-sorted = x by Def1;
then x in POSETS A() iff x is strict Poset & the carrier of x in A() by
Def2;
hence x is Object of C iff x is strict & L[x] & the carrier of x in A() by
A4,A13;
end;
thus thesis by A14;
end;
scheme
CLCatUniq1 { A() -> non empty set, P[set, set, set] }: for C1, C2 being
lattice-wise category st the carrier of C1 = A() & (for a,b being Object of C1,
f being monotone Function of latt a, latt b holds f in <^a,b^> iff P[a,b,f]) &
the carrier of C2 = A() & (for a,b being Object of C2, f being monotone
Function of latt a, latt b holds f in <^a,b^> iff P[a,b,f]) holds the AltCatStr
of C1 = the AltCatStr of C2 proof
let A1, A2 be lattice-wise category;
deffunc B(set,set) = (the Arrows of A1).($1,$2);
assume that
A1: the carrier of A1 = A() and
A2: for a,b being Object of A1, f being monotone Function of latt a,
latt b holds f in <^a,b^> iff P[a,b,f] and
A3: the carrier of A2 = A() and
A4: for a,b being Object of A2, f being monotone Function of latt a,
latt b holds f in <^a,b^> iff P[a,b,f];
A5: now
let a,b be Object of A2;
reconsider a9 = a, b9 = b as Object of A1 by A1,A3;
A6: <^a9,b9^> = (the Arrows of A1).(a9,b9);
thus <^a,b^> = (the Arrows of A1).(a,b)
proof
hereby
let x be object;
assume
A7: x in <^a,b^>;
then reconsider f = x as Morphism of a,b;
A8: @f = f by A7,Def7;
then P[latt a9,latt b9,@f] by A4,A7;
hence x in (the Arrows of A1).(a,b) by A2,A6,A8;
end;
let x be object;
assume
A9: x in (the Arrows of A1).(a,b);
then reconsider f = x as Morphism of a9,b9;
A10: @f = f by A9,Def7;
then P[latt a,latt b,@f] by A2,A9;
hence thesis by A4,A10;
end;
end;
A11: for a,b being Object of A1 holds <^a,b^> = (the Arrows of A1).(a,b);
for C1, C2 being para-functional semi-functional category st the carrier
of C1 = A() & (for a,b being Object of C1 holds <^a,b^> = B(a,b)) & the carrier
of C2 = A() & (for a,b being Object of C2 holds <^a,b^> = B(a,b)) holds the
AltCatStr of C1 = the AltCatStr of C2 from YELLOW18:sch 19;
hence thesis by A1,A3,A11,A5;
end;
scheme
CLCatUniq2 { A() -> non empty set, L[object], P[set, set, set] }:
for C1, C2
being lattice-wise category st (for x being LATTICE holds x is Object of C1 iff
x is strict & L[x] & the carrier of x in A()) & (for a,b being Object of C1, f
being monotone Function of latt a, latt b holds f in <^a,b^> iff P[a,b,f]) & (
for x being LATTICE holds x is Object of C2 iff x is strict & L[x] & the
carrier of x in A()) & (for a,b being Object of C2, f being monotone Function
of latt a, latt b holds f in <^a,b^> iff P[a,b,f]) holds the AltCatStr of C1 =
the AltCatStr of C2 proof
let A1, A2 be lattice-wise category;
assume that
A1: for x being LATTICE holds x is Object of A1 iff x is strict & L[x] &
the carrier of x in A() and
A2: for a,b being Object of A1, f being monotone Function of latt a,
latt b holds f in <^a,b^> iff P[a,b,f] and
A3: for x being LATTICE holds x is Object of A2 iff x is strict & L[x] &
the carrier of x in A();
A4: the carrier of A2 = the carrier of A1
proof
hereby
let x be object;
assume
A5: x in the carrier of A2;
then
A6: x is LATTICE by Def4;
then
A7: x is strict LATTICE & L[x] by A3,A5;
A8: x as_1-sorted = x by A6,Def1;
then the carrier of x as_1-sorted in A() by A3,A5,A6;
then x is Object of A1 by A1,A8,A7;
hence x in the carrier of A1;
end;
let x be object;
assume
A9: x in the carrier of A1;
then
A10: x is LATTICE by Def4;
then
A11: x is strict LATTICE & L[x] by A1,A9;
A12: x as_1-sorted = x by A10,Def1;
then the carrier of x as_1-sorted in A() by A1,A9,A10;
then x is Object of A2 by A3,A12,A11;
hence thesis;
end;
for C1, C2 being lattice-wise category st the carrier of C1 = the
carrier of A1 & (for a,b being Object of C1, f being monotone Function of latt
a, latt b holds f in <^a,b^> iff P[a,b,f]) & the carrier of C2 = the carrier of
A1 & (for a,b being Object of C2, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff P[a,b,f]) holds the AltCatStr of C1 = the AltCatStr of
C2 from CLCatUniq1;
hence thesis by A2,A4;
end;
scheme
CLCovariantFunctorEx { P, Q[set, set, set], A,B() -> lattice-wise category,
O(set) -> LATTICE, F(set,set,set) -> Function }: ex F being covariant strict
Functor of A(),B() st (for a being Object of A() holds F.a = O(latt a)) & for a
,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F.f =
F(latt a, latt b, @f)
provided
A1: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of A()).(a,b) iff a in the carrier of A() & b in the carrier of A() & P[
a,b,f] and
A2: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of B()).(a,b) iff a in the carrier of B() & b in the carrier of B() & Q[
a,b,f] and
A3: for a being LATTICE st a in the carrier of A() holds O(a) in the
carrier of B() and
A4: for a,b being LATTICE, f being Function of a,b st P[a,b,f] holds F(a
,b,f) is Function of O(a),O(b) & Q[O(a),O(b),F(a,b,f)] and
A5: for a being LATTICE st a in the carrier of A() holds F(a,a,id a) =
id O(a) and
A6: for a,b,c being LATTICE, f being Function of a,b, g being Function
of b,c st P[a,b,f] & P[b,c,g] holds F(a,c,g*f) = F(b,c,g)*F(a,b,f)
proof
A7: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
holds F(a,b,f) in (the Arrows of B()).(O(a), O(b))
proof
let a,b be Object of A() such that
A8: <^a,b^> <> {};
let f be Morphism of a,b;
A9: f = @f by A8,Def7;
then P[a,b,f] by A1,A8;
then
A10: F(a,b,f) is Function of O(a),O(b) & Q[O(a),O(b),F(a,b,f)] by A4,A9;
O(a) in the carrier of B() & O(b) in the carrier of B() by A3,A9;
hence thesis by A2,A10;
end;
A11: now
let a,b,c be Object of A() such that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
let a9,b9,c9 be Object of B() such that
A14: a9 = O(a) and
A15: b9 = O(b) and
A16: c9 = O(c);
let f9 be Morphism of a9,b9, g9 be Morphism of b9,c9 such that
A17: f9 = F(a,b,f) & g9 = F(b,c,g);
A18: F(a,b,f) in (the Arrows of B()).(O(a), O(b)) by A7,A12;
then
A19: @f9 = f9 by A14,A15,Def7;
A20: @g = g by A13,Def7;
then
A21: P[b,c,g] by A1,A13;
A22: F(b,c,g) in (the Arrows of B()).(O(b), O(c)) by A7,A13;
then
A23: @g9 = g9 by A15,A16,Def7;
A24: @f = f by A12,Def7;
then P[a,b,f] by A1,A12;
then F(a,c,@g*@f) = F(b,c,g)*F(a,b,f) by A6,A24,A20,A21
.= g9*f9 by A14,A15,A16,A17,A18,A22,A19,A23,Th3;
hence F(a,c,g*f) = g9*f9 by A12,A13,Th3;
end;
A25: now
let a be Object of A(), a9 be Object of B();
assume
A26: a9 = O(a);
idm a = id latt a by Th2;
hence F(a,a,idm a) = id latt a9 by A5,A26
.= idm a9 by Th2;
end;
A27: for a being Object of A() holds O(a) is Object of B()
proof
let a be Object of A();
a is LATTICE by Def4;
hence thesis by A3;
end;
consider F being covariant strict Functor of A(),B() such that
A28: for a being Object of A() holds F.a = O(a) and
A29: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism
of a,b holds F.f = F(a, b, f) from YELLOW18:sch 8(A27,A7,A11,A25);
take F;
thus for a be Object of A() holds F.a = O(latt a) by A28;
let a,b be Object of A() such that
A30: <^a, b^> <> {};
let f be Morphism of a,b;
f = @f by A30,Def7;
hence thesis by A29,A30;
end;
scheme
CLContravariantFunctorEx { P, Q[set, set, set], A,B() -> lattice-wise
category, O(set) -> LATTICE, F(set,set,set) -> Function }: ex F being
contravariant strict Functor of A(),B() st (for a being Object of A() holds F.a
= O(latt a)) & for a,b being Object of A() st <^a,b^> <> {} for f being
Morphism of a,b holds F.f = F(latt a, latt b, @f)
provided
A1: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of A()).(a,b) iff a in the carrier of A() & b in the carrier of A() & P[
a,b,f] and
A2: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of B()).(a,b) iff a in the carrier of B() & b in the carrier of B() & Q[
a,b,f] and
A3: for a being LATTICE st a in the carrier of A() holds O(a) in the
carrier of B() and
A4: for a,b being LATTICE, f being Function of a,b st P[a,b,f] holds F(a
,b,f) is Function of O(b),O(a) & Q[O(b),O(a),F(a,b,f)] and
A5: for a being LATTICE st a in the carrier of A() holds F(a,a,id a) =
id O(a) and
A6: for a,b,c being LATTICE, f being Function of a,b, g being Function
of b,c st P[a,b,f] & P[b,c,g] holds F(a,c,g*f) = F(a,b,f)*F(b,c,g)
proof
A7: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
holds F(a,b,f) in (the Arrows of B()).(O(b), O(a))
proof
let a,b be Object of A() such that
A8: <^a,b^> <> {};
let f be Morphism of a,b;
A9: f = @f by A8,Def7;
then P[a,b,f] by A1,A8;
then
A10: F(a,b,f) is Function of O(b),O(a) & Q[O(b),O(a),F(a,b,f)] by A4,A9;
O(a) in the carrier of B() & O(b) in the carrier of B() by A3,A9;
hence thesis by A2,A10;
end;
A11: now
let a,b,c be Object of A() such that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
let a9,b9,c9 be Object of B() such that
A14: a9 = O(a) and
A15: b9 = O(b) and
A16: c9 = O(c);
let f9 be Morphism of b9,a9, g9 be Morphism of c9,b9 such that
A17: f9 = F(a,b,f) & g9 = F(b,c,g);
A18: F(a,b,f) in (the Arrows of B()).(O(b), O(a)) by A7,A12;
then
A19: @f9 = f9 by A14,A15,Def7;
A20: @g = g by A13,Def7;
then
A21: P[b,c,g] by A1,A13;
A22: F(b,c,g) in (the Arrows of B()).(O(c), O(b)) by A7,A13;
then
A23: @g9 = g9 by A15,A16,Def7;
A24: @f = f by A12,Def7;
then P[a,b,f] by A1,A12;
then F(a,c,@g*@f) = F(a,b,f)*F(b,c,g) by A6,A24,A20,A21
.= f9*g9 by A14,A15,A16,A17,A18,A22,A19,A23,Th3;
hence F(a,c,g*f) = f9*g9 by A12,A13,Th3;
end;
A25: now
let a be Object of A(), a9 be Object of B();
assume
A26: a9 = O(a);
idm a = id latt a by Th2;
hence F(a,a,idm a) = id latt a9 by A5,A26
.= idm a9 by Th2;
end;
A27: for a being Object of A() holds O(a) is Object of B()
proof
let a be Object of A();
a is LATTICE by Def4;
hence thesis by A3;
end;
consider F being contravariant strict Functor of A(),B() such that
A28: for a being Object of A() holds F.a = O(a) and
A29: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism
of a,b holds F.f = F(a, b, f) from YELLOW18:sch 9(A27,A7,A11,A25);
take F;
thus for a be Object of A() holds F.a = O(latt a) by A28;
let a,b be Object of A() such that
A30: <^a, b^> <> {};
let f be Morphism of a,b;
f = @f by A30,Def7;
hence thesis by A29,A30;
end;
scheme
CLCatIsomorphism { P, Q[set, set, set], A,B() -> lattice-wise category, O(
set) -> LATTICE, F(set,set,set) -> Function }: A(), B() are_isomorphic
provided
A1: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of A()).(a,b) iff a in the carrier of A() & b in the carrier of A() & P[
a,b,f] and
A2: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of B()).(a,b) iff a in the carrier of B() & b in the carrier of B() & Q[
a,b,f] and
A3: ex F being covariant Functor of A(),B() st (for a being Object of A(
) holds F.a = O(a)) & for a,b being Object of A() st <^a,b^> <> {} for f being
Morphism of a,b holds F.f = F(a,b,f) and
A4: for a,b being LATTICE st a in the carrier of A() & b in the carrier
of A() holds O(a) = O(b) implies a = b and
A5: for a,b being LATTICE for f,g being Function of a,b st P[a,b,f] & P[
a,b,g] holds F(a,b,f) = F(a,b,g) implies f = g and
A6: for a,b being LATTICE, f being Function of a,b st Q[a,b,f] ex c,d
being LATTICE, g being Function of c,d st c in the carrier of A() & d in the
carrier of A() & P[c,d,g] & a = O(c) & b = O(d) & f = F(c,d,g)
proof
A7: for a,b being Object of A() st O(a) = O(b) holds a = b
proof
let a,b be Object of A();
a = latt a & b = latt b;
hence thesis by A4;
end;
A8: now
let a,b be Object of B() such that
A9: <^a,b^> <> {};
let f be Morphism of a,b;
A10: @f = f by A9,Def7;
then Q[latt a, latt b, @f] by A2,A9;
then consider c,d being LATTICE, g being Function of c,d such that
A11: c in the carrier of A() & d in the carrier of A() and
A12: P[c,d,g] and
A13: latt a = O(c) & latt b = O(d) & @f = F(c,d,g) by A6;
reconsider c9 = c, d9 = d as Object of A() by A11;
g in <^c9,d9^> by A1,A12;
hence
ex c,d being Object of A(), g being Morphism of c,d st a = O(c) & b =
O(d) & <^c,d^> <> {} & f = F(c,d,g) by A10,A13;
end;
A14: for a,b being Object of A() st <^a,b^> <> {} for f,g being Morphism of
a,b st F(a,b,f) = F(a,b,g) holds f = g
proof
let a, b be Object of A() such that
A15: <^a,b^> <> {};
let f,g be Morphism of a,b;
A16: @g = g by A15,Def7;
then
A17: P[latt a, latt b, @g] by A1,A15;
A18: @f = f by A15,Def7;
then P[latt a, latt b, @f] by A1,A15;
hence thesis by A5,A18,A16,A17;
end;
A19: ex F being covariant Functor of A(),B() st (for a being Object of A()
holds F.a = O(a)) & for a,b being Object of A() st <^a,b^> <> {} for f being
Morphism of a,b holds F.f = F(a,b,f) by A3;
thus thesis from YELLOW18:sch 11(A19,A7,A14,A8);
end;
scheme
CLCatAntiIsomorphism { P, Q[set, set, set], A,B() -> lattice-wise category,
O(set) -> LATTICE, F(set,set,set) -> Function }: A(), B() are_anti-isomorphic
provided
A1: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of A()).(a,b) iff a in the carrier of A() & b in the carrier of A() & P[
a,b,f] and
A2: for a,b being LATTICE, f being Function of a,b holds f in (the
Arrows of B()).(a,b) iff a in the carrier of B() & b in the carrier of B() & Q[
a,b,f] and
A3: ex F being contravariant Functor of A(),B() st (for a being Object
of A() holds F.a = O(a)) & for a,b being Object of A() st <^a,b^> <> {} for f
being Morphism of a,b holds F.f = F(a,b,f) and
A4: for a,b being LATTICE st a in the carrier of A() & b in the carrier
of A() holds O(a) = O(b) implies a = b and
A5: for a,b being LATTICE, f,g being Function of a,b st F(a,b,f) = F(a,b
,g) holds f = g and
A6: for a,b being LATTICE, f being Function of a,b st Q[a,b,f] ex c,d
being LATTICE, g being Function of c,d st c in the carrier of A() & d in the
carrier of A() & P[c,d,g] & b = O(c) & a = O(d) & f = F(c,d,g)
proof
A7: for a,b being Object of A() st O(a) = O(b) holds a = b
proof
let a,b be Object of A();
a = latt a & b = latt b;
hence thesis by A4;
end;
A8: now
let a,b be Object of B() such that
A9: <^a,b^> <> {};
let f be Morphism of a,b;
A10: @f = f by A9,Def7;
then Q[latt a, latt b, @f] by A2,A9;
then consider c,d being LATTICE, g being Function of c,d such that
A11: c in the carrier of A() & d in the carrier of A() and
A12: P[c,d,g] and
A13: latt b = O(c) & latt a = O(d) & @f = F(c,d,g) by A6;
reconsider c9 = c, d9 = d as Object of A() by A11;
g in <^c9,d9^> by A1,A12;
hence
ex c,d being Object of A(), g being Morphism of c,d st b = O(c) & a =
O(d) & <^c,d^> <> {} & f = F(c,d,g) by A10,A13;
end;
A14: for a,b being Object of A() st <^a,b^> <> {} for f,g being Morphism of
a,b st F(a,b,f) = F(a,b,g) holds f = g
proof
let a, b be Object of A() such that
A15: <^a,b^> <> {};
let f,g be Morphism of a,b;
@f = f & @g = g by A15,Def7;
hence thesis by A5;
end;
A16: ex F being contravariant Functor of A(),B() st (for a being Object of A(
) holds F.a = O(a)) & for a,b being Object of A() st <^a,b^> <> {} for f being
Morphism of a,b holds F.f = F(a,b,f) by A3;
thus thesis from YELLOW18:sch 13(A16,A7,A14,A8);
end;
begin :: Equivalence of lattice-wise categories
definition
let C be lattice-wise category;
attr C is with_all_isomorphisms means
: Def8:
for a,b being Object of C, f
being Function of latt a, latt b st f is isomorphic holds f in <^a,b^>;
end;
registration
cluster with_all_isomorphisms for strict lattice-wise category;
existence
proof
defpred P[set,set,set] means $3 = $3;
set L = the LATTICE;
A1: for a,b,c being LATTICE st a in {L} & b in {L} & c in {L} for f being
Function of a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f
];
A2: for a being LATTICE st a in {L} holds P[a,a,id a];
A3: for a be Element of {L} holds a is LATTICE by TARSKI:def 1;
consider C being strict category such that
A4: C is lattice-wise and
A5: the carrier of C = {L} & for a,b being LATTICE, f being monotone
Function of a,b holds f in (the Arrows of C).(a,b) iff a in {L} & b in {L} & P[
a,b,f] from localCLCatEx(A3,A1,A2);
reconsider C as strict lattice-wise category by A4;
take C;
let a,b be Object of C, f be Function of latt a, latt b;
thus thesis by A5;
end;
end;
theorem
for C being with_all_isomorphisms lattice-wise category for a,b
being Object of C for f being Morphism of a,b st @f is isomorphic holds f is
iso
proof
let C be with_all_isomorphisms lattice-wise category;
let a,b be Object of C;
let f be Morphism of a,b;
assume
A1: @f is isomorphic;
then consider g being monotone Function of latt b, latt a such that
A2: @f*g = id latt b and
A3: g*@f = id latt a by YELLOW16:15;
A4: @f in <^a,b^> by A1,Def8;
A5: g is isomorphic by A2,A3,YELLOW16:15;
then
A6: g in <^b,a^> by Def8;
reconsider g as Morphism of b,a by A5,Def8;
A7: @g = g by A6,Def7;
idm b = id latt b by Th2;
then
f*g = idm b by A2,A4,A6,A7,Th3;
then
A8: g is_right_inverse_of f;
idm a = id latt a by Th2;
then
g*f = idm a by A3,A4,A6,A7,Th3;
then
A9: g is_left_inverse_of f;
then f is retraction coretraction by A8;
hence f*f" = idm b & f"*f = idm a by A4,A6,A9,A8,ALTCAT_3:def 4;
end;
theorem
for C being lattice-wise category for a,b being Object of C st <^a,b^>
<> {} & <^b,a^> <> {} for f being Morphism of a,b st f is iso holds @f is
isomorphic
proof
let C be lattice-wise category;
let a,b be Object of C;
assume
A1: <^a,b^> <> {} & <^b,a^> <> {};
let f be Morphism of a,b such that
A2: f*f" = idm b & f"*f = idm a;
A3: idm a = id latt a & idm b = id latt b by Th2;
@f*@(f") = f*f" & @(f")*@f = f"*f by A1,Th3;
hence thesis by A2,A3,YELLOW16:15;
end;
scheme
CLCatEquivalence { P, Q[set, set, set], A,B() -> lattice-wise category, O1,
O2(set) -> LATTICE, F1, F2(set,set,set) -> Function, A, B(set) -> Function }: A
(), B() are_equivalent
provided
A1: for a,b being Object of A(), f being monotone Function of latt a,
latt b holds f in <^a,b^> iff P[latt a, latt b, f] and
A2: for a,b being Object of B(), f being monotone Function of latt a,
latt b holds f in <^a,b^> iff Q[latt a, latt b, f] and
A3: ex F being covariant Functor of A(),B() st (for a being Object of A(
) holds F.a = O1(a)) & for a,b being Object of A() st <^a,b^> <> {} for f being
Morphism of a,b holds F.f = F1(a,b,f) and
A4: ex G being covariant Functor of B(),A() st (for a being Object of B(
) holds G.a = O2(a)) & for a,b being Object of B() st <^a,b^> <> {} for f being
Morphism of a,b holds G.f = F2(a,b,f) and
A5: for a being LATTICE st a in the carrier of A() ex f being monotone
Function of O2(O1(a)), a st f = A(a) & f is isomorphic & P[O2(O1(a)), a, f] & P
[a, O2(O1(a)), f"] and
A6: for a being LATTICE st a in the carrier of B() ex f being monotone
Function of a, O1(O2(a)) st f = B(a) & f is isomorphic & Q[a, O1(O2(a)), f] & Q
[O1(O2(a)), a, f"] and
A7: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of
a,b holds A(b)*F2(O1(a),O1(b),F1(a,b,f)) = @f*A(a) and
A8: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of
a,b holds F1(O2(a),O2(b),F2(a,b,f))*B(a) = B(b)*@f
proof
A9: ex G being covariant Functor of B(),A() st (for a being Object of B()
holds G.a = O2(a)) & for a,b being Object of B() st <^a,b^> <> {} for f being
Morphism of a,b holds G.f = F2(a,b,f) by A4;
A10: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,
b holds F1(O2(a),O2(b),F2(a,b,f))*B(a) = B(b)*f
proof
let a,b be Object of B() such that
A11: <^a,b^> <> {};
let f be Morphism of a,b;
@f = f by A11,Def7;
hence thesis by A8,A11;
end;
A12: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,
b holds A(b)*F2(O1(a),O1(b),F1(a,b,f)) = f*A(a)
proof
let a,b be Object of A() such that
A13: <^a,b^> <> {};
let f be Morphism of a,b;
@f = f by A13,Def7;
hence thesis by A7,A13;
end;
A14: for a, b being Object of B() st b = O1(O2(a)) holds B(a) in <^a, b^> &
B(a)" in <^b,a^> & B(a) is one-to-one
proof
let a, b be Object of B() such that
A15: b = O1(O2(a));
consider f being monotone Function of latt a, O1(O2(a)) such that
A16: f = B(a) and
A17: f is isomorphic and
A18: Q[latt a, O1(O2(a)), f] and
A19: Q[O1(O2(a)), latt a, f"] by A6;
A20: latt b = b;
hence B(a) in <^a, b^> by A2,A15,A16,A18;
ex g being Function of O1(O2(a)), latt a st g = f" & g is monotone by A17,
WAYBEL_0:def 38;
hence B(a)" in <^b,a^> by A2,A15,A20,A16,A19;
thus thesis by A16,A17;
end;
A21: for a, b being Object of A() st a = O2(O1(b)) holds A(b) in <^a, b^> &
A(b)" in <^b,a^> & A(b) is one-to-one
proof
let a, b be Object of A() such that
A22: a = O2(O1(b));
consider f being monotone Function of O2(O1(b)), latt b such that
A23: f = A(b) and
A24: f is isomorphic and
A25: P[O2(O1(b)), latt b, f] and
A26: P[latt b, O2(O1(b)), f"] by A5;
A27: latt a = a;
hence A(b) in <^a, b^> by A1,A22,A23,A25;
ex g being Function of latt b, O2(O1(b)) st g = f" & g is monotone by A24,
WAYBEL_0:def 38;
hence A(b)" in <^b,a^> by A1,A22,A27,A23,A26;
thus thesis by A23,A24;
end;
A28: ex F being covariant Functor of A(),B() st (for a being Object of A()
holds F.a = O1(a)) & for a,b being Object of A() st <^a,b^> <> {} for f being
Morphism of a,b holds F.f = F1(a,b,f) by A3;
thus thesis from YELLOW18:sch 22(A28,A9, A21,A14,A12,A10);
end;
begin :: UPS category
definition
let R be Relation;
attr R is upper-bounded means
ex x st for y st y in field R holds [y ,x] in R;
end;
Lm1: for X being set holds x in X iff X = X \{x} \/ {x}
by ZFMISC_1:31,XBOOLE_1:7,XBOOLE_1:45;
registration
cluster well-ordering -> reflexive transitive antisymmetric connected
well_founded for Relation;
coherence;
end;
registration
cluster well-ordering for Relation;
existence
proof
consider r being Relation such that
A1: r well_orders {0,1,2,3,4} by WELLORD2:17;
take r|_2 {0,1,2,3,4};
thus thesis by A1,WELLORD2:16;
end;
end;
theorem Th6:
for x,y being object holds
for f being one-to-one Function, R being Relation holds [x,y] in
f*R*(f") iff x in dom f & y in dom f & [f.x, f.y] in R
proof let x,y be object;
let f be one-to-one Function, R be Relation;
A1: rng f = dom (f") by FUNCT_1:33;
A2: dom f = rng (f") by FUNCT_1:33;
hereby
assume [x,y] in f*R*(f");
then consider a being object such that
A3: [x,a] in f*R and
A4: [a,y] in f" by RELAT_1:def 8;
A5: y = f".a & a in rng f by A1,A4,FUNCT_1:1;
consider b being object such that
A6: [x,b] in f and
A7: [b,a] in R by A3,RELAT_1:def 8;
thus x in dom f & y in dom f by A2,A4,A6,XTUPLE_0:def 12,def 13;
b = f.x by A6,FUNCT_1:1;
hence [f.x, f.y] in R by A7,A5,FUNCT_1:35;
end;
assume that
A8: x in dom f and
A9: y in dom f and
A10: [f.x, f.y] in R;
f".(f.y) = y & f.y in rng f by A9,FUNCT_1:34,def 3;
then
A11: [f.y,y] in f" by A1,FUNCT_1:1;
[x,f.x] in f by A8,FUNCT_1:1;
then [x,f.y] in f*R by A10,RELAT_1:def 8;
hence thesis by A11,RELAT_1:def 8;
end;
registration
let f be one-to-one Function;
let R be reflexive Relation;
cluster f*R*(f") -> reflexive;
coherence
proof
let x be object;
A1: R is_reflexive_in field R by RELAT_2:def 9;
assume x in field (f*R*(f"));
then
A2: x in dom (f*R*(f")) \/ rng (f*R*(f")) by RELAT_1:def 6;
per cases by A2,XBOOLE_0:def 3;
suppose
x in dom (f*R*(f"));
then consider y being object such that
A3: [x,y] in (f*R*(f")) by XTUPLE_0:def 12;
[f.x, f.y] in R by A3,Th6;
then f.x in field R by RELAT_1:15;
then
A4: [f.x, f.x] in R by A1;
x in dom f by A3,Th6;
hence thesis by A4,Th6;
end;
suppose
x in rng (f*R*(f"));
then consider y being object such that
A5: [y,x] in (f*R*(f")) by XTUPLE_0:def 13;
[f.y, f.x] in R by A5,Th6;
then f.x in field R by RELAT_1:15;
then
A6: [f.x, f.x] in R by A1;
x in dom f by A5,Th6;
hence thesis by A6,Th6;
end;
end;
end;
registration
let f be one-to-one Function;
let R be antisymmetric Relation;
cluster f*R*(f") -> antisymmetric;
coherence
proof
let x,y be object;
assume that
x in field (f*R*(f")) and
y in field (f*R*(f"));
assume that
A1: [x,y] in f*R*(f") and
A2: [y,x] in f*R*(f");
A3: x in dom f & y in dom f by A1,Th6;
A4: R is_antisymmetric_in field R by RELAT_2:def 12;
A5: [f.y, f.x] in R by A2,Th6;
A6: [f.x, f.y] in R by A1,Th6;
then f.x in field R & f.y in field R by RELAT_1:15;
then f.x = f.y by A6,A5,A4;
hence thesis by A3,FUNCT_1:def 4;
end;
end;
registration
let f be one-to-one Function;
let R be transitive Relation;
cluster f*R*(f") -> transitive;
coherence
proof
let x,y,z be object;
assume that
x in field (f*R*(f")) and
y in field (f*R*(f")) and
z in field (f*R*(f") );
assume that
A1: [x,y] in f*R*(f") and
A2: [y,z] in f*R*(f");
A3: x in dom f & z in dom f by A1,A2,Th6;
A4: [f.y, f.z] in R by A2,Th6;
then
A5: f.z in field R by RELAT_1:15;
A6: R is_transitive_in field R by RELAT_2:def 16;
A7: [f.x, f.y] in R by A1,Th6;
then f.x in field R & f.y in field R by RELAT_1:15;
then [f.x, f.z] in R by A7,A4,A5,A6;
hence thesis by A3,Th6;
end;
end;
theorem Th7:
for X being set, A being Ordinal st X,A are_equipotent ex R being
Order of X st R well_orders X & order_type_of R = A
proof
let X be set, A be Ordinal;
given f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = A;
reconsider f as Function of X,A by A2,A3,FUNCT_2:2;
reconsider g = f" as Function of A,X by A1,A3,FUNCT_2:25;
A4: dom g = A by A1,A3,FUNCT_1:33;
reconsider f9 = f as one-to-one Function by A1;
A5: dom RelIncl A = A by ORDERS_1:14;
rng RelIncl A = A by ORDERS_1:14;
then
A6: rng (f*(RelIncl A)) = A by A3,A5,RELAT_1:28;
set R = f*(RelIncl A)*g;
dom (f*(RelIncl A)) = X by A2,A3,A5,RELAT_1:27;
then
A7: dom R = X by A4,A6,RELAT_1:27;
rng g = X by A1,A2,FUNCT_1:33;
then rng R = X by A4,A6,RELAT_1:28;
then
A8: field R = X \/ X by A7,RELAT_1:def 6
.= X;
reconsider R as Relation of X;
f9*(RelIncl A)*(f9") is_reflexive_in X by A8,RELAT_2:def 9;
then reconsider R as Order of X by A7,PARTFUN1:def 2;
A9: f is_isomorphism_of R, RelIncl A
proof
thus dom f = field R & rng f = field RelIncl A & f is one-to-one by A1,A2
,A3,A8,WELLORD2:def 1;
let a,b be object;
hereby
assume
A10: [a,b] in R;
hence a in field R & b in field R by RELAT_1:15;
consider x being object such that
A11: [a,x] in f*RelIncl A and
A12: [x,b] in g by A10,RELAT_1:def 8;
A13: b = g.x & x in dom g by A12,FUNCT_1:1;
consider y being object such that
A14: [a,y] in f and
A15: [y,x] in RelIncl A by A11,RELAT_1:def 8;
y = f.a by A14,FUNCT_1:1;
hence [f.a,f.b] in RelIncl A by A1,A3,A15,A13,FUNCT_1:35;
end;
assume that
A16: a in field R and
A17: b in field R and
A18: [f.a,f.b] in RelIncl A;
[a,f.a] in f by A2,A8,A16,FUNCT_1:1;
then
A19: [a,f.b] in f*RelIncl A by A18,RELAT_1:def 8;
f".(f.b) = b & f.b in A by A1,A2,A3,A8,A17,FUNCT_1:34,def 3;
then [f.b,b] in g by A4,FUNCT_1:1;
hence thesis by A19,RELAT_1:def 8;
end;
then f" is_isomorphism_of RelIncl A, R by WELLORD1:39;
then R is connected well_founded by WELLORD1:43;
then
A20: R is_connected_in X & R is_well_founded_in X by A8;
take R;
A21: R is_antisymmetric_in X by A8,RELAT_2:def 12;
R is_reflexive_in X & R is_transitive_in X by A8,RELAT_2:def 9,def 16;
hence R well_orders X by A21,A20;
then
A22: R is well-ordering by A8,WELLORD1:4;
R, RelIncl A are_isomorphic by A9;
hence thesis by A22,WELLORD2:def 2;
end;
registration
let X be non empty set;
cluster upper-bounded well-ordering for Order of X;
existence
proof
set x = the Element of X;
A1: X\{x},card (X\{x}) are_equipotent & {x},{card (X\{x})} are_equipotent
by CARD_1:28,def 2;
A2: succ card (X\{x}) = card (X\{x}) \/ {card (X\{x})} by ORDINAL1:def 1;
not card (X\{x}) in card (X\{x});
then
A3: {card (X\{x})} misses card (X\{x}) by ZFMISC_1:50;
{x} misses (X\{x}) & X = (X\{x}) \/ {x} by Lm1,XBOOLE_1:79;
then consider r being Order of X such that
A4: r well_orders X and
A5: order_type_of r = succ card (X\{x}) by A1,A3,A2,Th7,CARD_1:31;
take r;
A6: field r = X by ORDERS_1:15;
then r is well-ordering by A4,WELLORD1:4;
then r, RelIncl order_type_of r are_isomorphic by WELLORD2:def 2;
then RelIncl order_type_of r, r are_isomorphic by WELLORD1:40;
then consider f being Function such that
A7: f is_isomorphism_of RelIncl order_type_of r, r;
A8: f is one-to-one by A7;
A9: rng f = X by A6,A7;
field RelIncl order_type_of r = order_type_of r by WELLORD2:def 1;
then
A10: dom f = order_type_of r by A7;
thus r is upper-bounded
proof
take a = f.card (X\{x});
let y;
A11: card (X\{x}) in order_type_of r by A2,A5,ZFMISC_1:136;
assume
A12: y in field r;
then
A13: f".y in order_type_of r by A6,A8,A10,A9,FUNCT_1:32;
then reconsider b = f".y as Ordinal;
f".y in card (X\{x}) or f".y = card (X\{x}) by A2,A5,A13,ZFMISC_1:136;
then b c= card (X\{x}) by ORDINAL1:def 2;
then [b, card (X\{x})] in RelIncl order_type_of r by A13,A11,
WELLORD2:def 1;
then [f.b, a] in r by A7;
hence thesis by A6,A8,A9,A12,FUNCT_1:35;
end;
thus thesis by A4,A6,WELLORD1:4;
end;
end;
theorem Th8:
for P being reflexive non empty RelStr holds P is upper-bounded
iff the InternalRel of P is upper-bounded
proof
let P be reflexive non empty RelStr;
(the carrier of P) \/ the carrier of P = the carrier of P;
then
A1: field the InternalRel of P c= the carrier of P by RELSET_1:8;
thus P is upper-bounded implies the InternalRel of P is upper-bounded
proof
given x being Element of P such that
A2: x is_>=_than the carrier of P;
take x;
let y;
assume y in field the InternalRel of P;
then reconsider y as Element of P by A1;
x >= y by A2;
hence thesis;
end;
set y = the Element of P;
given x such that
A3: for y st y in field the InternalRel of P holds [y,x] in the
InternalRel of P;
y <= y;
then [y,y] in the InternalRel of P;
then y in field the InternalRel of P by RELAT_1:15;
then [y,x] in the InternalRel of P by A3;
then x in field the InternalRel of P by RELAT_1:15;
then reconsider x as Element of P by A1;
take x;
let y be Element of P;
y <= y;
then [y,y] in the InternalRel of P;
then y in field the InternalRel of P by RELAT_1:15;
then [y,x] in the InternalRel of P by A3;
hence thesis;
end;
theorem Th9:
for P being upper-bounded non empty Poset st the InternalRel of
P is well-ordering holds P is connected complete continuous
proof
let P be upper-bounded non empty Poset such that
A1: the InternalRel of P is well-ordering;
A2: field the InternalRel of P = the carrier of P by ORDERS_1:15;
thus
A3: P is connected
proof
let x,y being Element of P;
A4: x = y or x <> y;
the InternalRel of P is_connected_in the carrier of P & the
InternalRel of P is_reflexive_in the carrier of P by A1,A2,RELAT_2:def 9,def 14
;
then [x,y] in the InternalRel of P or [y,x] in the InternalRel of P by A4;
hence x <= y or y <= x;
end;
thus P is complete
proof
set y = the Element of P;
let X be set;
defpred P[object] means
for y being Element of P st y in X holds [y,$1] in
the InternalRel of P;
consider Y being set such that
A5: for x being object holds x in Y iff x in the carrier of P & P[x]
from XBOOLE_0:sch 1;
A6: Y c= the carrier of P
by A5;
the InternalRel of P is upper-bounded by Th8;
then consider x such that
A7: for y st y in field the InternalRel of P holds [y,x] in the
InternalRel of P;
[y,x] in the InternalRel of P by A2,A7;
then reconsider x as Element of P by A2,RELAT_1:15;
for y being Element of P st y in X holds [y,x] in the InternalRel of
P by A2,A7;
then x in Y by A5;
then consider a being object such that
A8: a in Y and
A9: for b being object st b in Y holds [a,b] in the InternalRel of P
by A1,A2,A6,WELLORD1:6;
reconsider a as Element of P by A6,A8;
take a;
thus for y be Element of P st y in X holds y <= a by A5,A8;
let b be Element of P;
assume
A10: for c being Element of P st c in X holds c <= b;
for c being Element of P st c in X
holds [c,b] in the InternalRel of P by ORDERS_2:def 5,A10;
then b in Y by A5;
then [a,b] in the InternalRel of P by A9;
hence a <= b;
end;
hence thesis by A3;
end;
theorem Th10:
for P being upper-bounded non empty Poset st the InternalRel
of P is well-ordering for x,y being Element of P st y < x ex z being Element of
P st z is compact & y <= z & z <= x
proof
let P be upper-bounded non empty Poset;
set R = the InternalRel of P, A = order_type_of R;
A1: field RelIncl A = A by WELLORD2:def 1;
assume
A2: R is well-ordering;
then reconsider L = P as complete Chain by Th9;
let x,y be Element of P;
R, RelIncl A are_isomorphic by A2,WELLORD2:def 2;
then consider f being Function such that
A3: f is_isomorphism_of R, RelIncl A;
assume
A4: y < x;
then y <= x;
then
A5: [y,x] in R;
then
A6: [f.y, f.x] in RelIncl A by A3;
then
A7: f.x in A by A1,RELAT_1:15;
A8: f.x <> f.y by A3,A4,A5,WELLORD1:36;
A9: f.y in A by A6,A1,RELAT_1:15;
then reconsider a = f.x, b = f.y as Ordinal by A7;
b c= a by A6,A7,A9,WELLORD2:def 1;
then b c< a by A8;
then b in a by ORDINAL1:11;
then
A10: succ b c= a by ORDINAL1:21;
then
A11: succ b in A by A7,ORDINAL1:12;
then
A12: [succ b, f.x] in RelIncl A by A7,A10,WELLORD2:def 1;
A13: b c= succ b by ORDINAL3:1;
rng f = A by A3,A1;
then consider z being object such that
A14: z in dom f and
A15: succ b = f.z by A11,FUNCT_1:def 3;
A16: field R = the carrier of P by ORDERS_1:15;
then reconsider z as Element of P by A3,A14;
take z;
A17: dom f = field R by A3;
thus z is compact
proof
let D be non empty directed Subset of P such that
A18: z <= sup D and
A19: for d being Element of P st d in D holds not z <= d;
A20: L is complete;
D is_<=_than y
proof
let c be Element of P;
A21: f is one-to-one by A3;
assume
A22: c in D;
then not z <= c by A19;
then z >= c by A20,WAYBEL_0:def 29;
then [c,z] in R;
then
A23: [f.c, succ b] in RelIncl A by A3,A15;
then
A24: f.c in A by A1,RELAT_1:15;
then reconsider fc = f.c as Ordinal;
A25: fc c= succ b by A11,A23,A24,WELLORD2:def 1;
c <> z by A19,A22;
then fc <> succ b by A15,A16,A17,A21,FUNCT_1:def 4;
then fc c< succ b by A25;
then fc in succ b by ORDINAL1:11;
then fc c= b by ORDINAL1:22;
then [fc,b] in RelIncl A by A9,A24,WELLORD2:def 1;
hence [c,y] in R by A3,A16;
end;
then sup D <= y by A20,YELLOW_0:32;
then z <= y by A18,YELLOW_0:def 2;
then [z,y] in R;
then [succ b, b] in RelIncl A by A3,A15;
then succ b c= b by A9,A11,WELLORD2:def 1;
then b = succ b by A13;
hence contradiction by ORDINAL1:9;
end;
[f.y, succ b] in RelIncl A by A9,A13,A11,WELLORD2:def 1;
hence [y,z] in R & [z,x] in R by A3,A15,A16,A12;
end;
theorem Th11:
for P being upper-bounded non empty Poset st the InternalRel
of P is well-ordering holds P is algebraic
proof
let P be upper-bounded non empty Poset;
assume
A1: the InternalRel of P is well-ordering;
then reconsider L = P as connected complete continuous non empty Poset by Th9
;
now
let x,y be Element of L;
assume x << y;
then x is compact & x <= x & x <= y or x < y by WAYBEL_3:1;
then consider z being Element of L such that
A2: z is compact and
A3: x <= z & z <= y by A1,Th10;
take z;
thus z in the carrier of CompactSublatt L by A2,WAYBEL_8:def 1;
thus x <= z & z <= y by A3;
end;
hence thesis by WAYBEL_8:7;
end;
registration
let X be non empty set;
let R be upper-bounded well-ordering Order of X;
cluster RelStr(#X,R#) -> complete connected continuous algebraic;
coherence
proof
RelStr(#X,R#) is upper-bounded by Th8;
hence thesis by Th9,Th11;
end;
end;
definition
defpred P[LATTICE,LATTICE, Function of $1,$2] means $3 is
directed-sups-preserving;
defpred L[LATTICE] means $1 is complete;
let W be non empty set;
given w being Element of W such that
A1: w is non empty;
func W-UPS_category -> lattice-wise strict category means
: Def10:
(for x
being LATTICE holds x is Object of it iff x is strict complete & the carrier of
x in W) & for a,b being Object of it, f being monotone Function of latt a, latt
b holds f in <^a,b^> iff f is directed-sups-preserving;
existence
proof
reconsider w as non empty set by A1;
set r = the upper-bounded well-ordering Order of w;
A2: for a being LATTICE st L[a] holds P[a,a,id a];
RelStr(#w,r#) is complete;
then
A3: ex x being strict LATTICE st L[x] & the carrier of x in W;
A4: for a,b,c being LATTICE st L[a] & L[b] & L[c] for f being Function of
a,b, g being Function of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by
WAYBEL20:28;
thus ex It being lattice-wise strict category st (for x being LATTICE
holds x is Object of It iff x is strict & L[x] & the carrier of x in W) & for a
,b being Object of It, f being monotone Function of latt a, latt b holds f in
<^a,b^> iff P[latt a, latt b, f] from CLCatEx2(A3,A4,A2);
end;
correctness
proof
reconsider w as non empty set by A1;
let C1, C2 be lattice-wise strict category such that
A5: for x being LATTICE holds x is Object of C1 iff x is strict & L[x]
& the carrier of x in W and
A6: for a,b being Object of C1, f being monotone Function of latt a,
latt b holds f in <^a,b^> iff f is directed-sups-preserving and
A7: for x being LATTICE holds x is Object of C2 iff x is strict & L[x]
& the carrier of x in W and
A8: for a,b being Object of C2, f being monotone Function of latt a,
latt b holds f in <^a,b^> iff f is directed-sups-preserving;
defpred Q[set, set, set] means ex L1,L2 being LATTICE, f being Function of
L1,L2 st $1 = L1 & $2 = L2 & $3 = f & f is directed-sups-preserving;
A9: now
let a,b be Object of C1;
let f be monotone Function of latt a, latt b;
f in <^a,b^> iff f is directed-sups-preserving by A6;
hence f in <^a,b^> iff Q[a,b,f];
end;
A10: now
let a,b be Object of C2;
let f be monotone Function of latt a, latt b;
f in <^a,b^> iff f is directed-sups-preserving by A8;
hence f in <^a,b^> iff Q[a,b,f];
end;
for C1, C2 being lattice-wise category st (for x being LATTICE holds
x is Object of C1 iff x is strict & L[x] & the carrier of x in W) & (for a,b
being Object of C1, f being monotone Function of latt a, latt b holds f in <^a,
b^> iff Q[a,b,f]) & (for x being LATTICE holds x is Object of C2 iff x is
strict & L[x] & the carrier of x in W) & (for a,b being Object of C2, f being
monotone Function of latt a, latt b holds f in <^a,b^> iff Q[a,b,f]) holds the
AltCatStr of C1 = the AltCatStr of C2 from CLCatUniq2;
hence thesis by A5,A7,A9,A10;
end;
end;
registration
let W be with_non-empty_element set;
cluster W-UPS_category -> with_complete_lattices with_all_isomorphisms;
coherence
proof
set C = W-UPS_category;
thus C is lattice-wise;
A1: ex w being non empty set st w in W by SETFAM_1:def 10;
hereby
let a be Object of C;
a = latt a;
hence a is complete LATTICE by A1,Def10;
end;
let a,b be Object of C, f be Function of latt a, latt b;
reconsider S = latt a, T = latt b as complete LATTICE by A1,Def10;
assume f is isomorphic;
then f is sups-preserving Function of S, T by WAYBEL13:20;
hence thesis by A1,Def10;
end;
end;
theorem Th12:
for W being with_non-empty_element set holds the carrier of W
-UPS_category c= POSETS W
proof
let W be with_non-empty_element set;
let x be object;
assume x in the carrier of W-UPS_category;
then reconsider x as Object of W-UPS_category;
A1: ex w being non empty set st w in W by SETFAM_1:def 10;
then
A2: the carrier of latt x in W by Def10;
latt x = x;
then x is strict Poset by A1,Def10;
hence thesis by A2,Def2;
end;
theorem Th13:
for W being with_non-empty_element set for x holds x is Object
of W-UPS_category iff x is complete LATTICE & x in POSETS W
proof
let W be with_non-empty_element set;
let x;
hereby
assume x is Object of W-UPS_category;
then reconsider a = x as Object of W-UPS_category;
latt a = x;
hence x is complete LATTICE;
a in the carrier of W-UPS_category & the carrier of W-UPS_category c=
POSETS W by Th12;
hence x in POSETS W;
end;
assume x is complete LATTICE;
then reconsider L = x as complete LATTICE;
assume x in POSETS W;
then
A1: the carrier of L as_1-sorted in W & L is strict by Def2;
L as_1-sorted = L by Def1;
hence thesis by A1,Def10;
end;
theorem Th14:
for W being with_non-empty_element set for L being LATTICE st
the carrier of L in W holds L is Object of W-UPS_category iff L is strict
complete
proof
let W be with_non-empty_element set;
let L be LATTICE;
assume
A1: the carrier of L in W;
L as_1-sorted = L by Def1;
then L in POSETS W iff L is strict by A1,Def2;
hence thesis by Th13;
end;
theorem Th15:
for W being with_non-empty_element set for a,b being Object of W
-UPS_category for f being set holds f in <^a,b^> iff f is
directed-sups-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-UPS_category;
let f be set;
A1: ex w being non empty set st w in W by SETFAM_1:def 10;
hereby
assume
A2: f in <^a,b^>;
then reconsider g = f as Morphism of a,b;
f = @g by A2,Def7;
hence f is directed-sups-preserving Function of latt a, latt b by A1,A2
,Def10;
end;
thus thesis by A1,Def10;
end;
registration
let W be with_non-empty_element set;
let a,b be Object of W-UPS_category;
cluster <^a,b^> -> non empty;
coherence
proof
set f = the directed-sups-preserving Function of latt a, latt b;
f in <^a,b^> by Th15;
hence thesis;
end;
end;
begin
registration
let A be set-id-inheriting category;
cluster -> set-id-inheriting for non empty subcategory of A;
coherence
proof
let B be non empty subcategory of A;
let b be Object of B;
b in the carrier of B & the carrier of B c= the carrier of A by
ALTCAT_2:def 11;
then reconsider a = b as Object of A;
thus idm b = idm a by ALTCAT_2:34
.= id the_carrier_of a by YELLOW18:def 10
.= id the_carrier_of b by ALTCAT_2:34;
end;
end;
registration
let A be para-functional category;
cluster -> para-functional for non empty subcategory of A;
coherence
proof
let B be non empty subcategory of A;
consider F being ManySortedSet of A such that
A1: for a1,a2 being Object of A holds <^a1,a2^> c= Funcs(F.a1,F.a2) by
YELLOW18:def 7;
set G = F|the carrier of B;
A2: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
dom F = the carrier of A by PARTFUN1:def 2;
then dom G = the carrier of B by A2,RELAT_1:62;
then reconsider G as ManySortedSet of B by PARTFUN1:def 2,RELAT_1:def 18;
take G;
let a1,a2 be Object of B;
reconsider b1 = a1, b2 = a2 as Object of A by A2;
F.a1 = G.a1 & F.a2 = G.a2 by FUNCT_1:49;
then <^a1,a2^> c= <^b1,b2^> & <^b1,b2^> c= Funcs(G.a1,G.a2) by A1,
ALTCAT_2:31;
hence thesis;
end;
end;
registration
let A be semi-functional category;
cluster -> semi-functional for non empty transitive SubCatStr of A;
coherence
proof
let B be non empty transitive SubCatStr of A;
let b1,b2,b3 be Object of B such that
A1: <^b1,b2^> <> {} and
A2: <^b2,b3^> <> {} and
A3: <^b1,b3^> <> {};
reconsider a1 = b1, a2 = b2, a3 = b3 as Object of A by ALTCAT_2:29;
A4: <^a1,a2^> <> {} & <^a2,a3^> <> {} by A1,A2,ALTCAT_2:31,XBOOLE_1:3;
let f1 be Morphism of b1,b2, f2 be Morphism of b2,b3;
reconsider g2 = f2 as Morphism of a2,a3 by A2,ALTCAT_2:33;
reconsider g1 = f1 as Morphism of a1,a2 by A1,ALTCAT_2:33;
A5: <^a1,a3^> <> {} by A3,ALTCAT_2:31,XBOOLE_1:3;
let f9, g9 be Function;
assume f1 = f9 & f2 = g9;
then g2*g1 = g9*f9 by A4,A5,ALTCAT_1:def 12;
hence thesis by A1,A2,ALTCAT_2:32;
end;
end;
registration
let A be carrier-underlaid category;
cluster -> carrier-underlaid for non empty subcategory of A;
coherence
proof
let B be non empty subcategory of A;
let b being Object of B;
reconsider a = b as Object of A by ALTCAT_2:29;
consider S being 1-sorted such that
A1: a = S and
A2: the_carrier_of a = the carrier of S by Def3;
take S;
thus b = S by A1;
thus thesis by A2,ALTCAT_2:34;
end;
end;
registration
let A be lattice-wise category;
cluster -> lattice-wise for non empty subcategory of A;
coherence
proof
let B be non empty subcategory of A;
thus B is semi-functional set-id-inheriting;
hereby
let b be Object of B;
reconsider a = b as Object of A by ALTCAT_2:29;
a is LATTICE by Def4;
hence b is LATTICE;
end;
let a,b be Object of B;
reconsider a9 = a, b9 = b as Object of A by ALTCAT_2:29;
let A,B be LATTICE;
assume A = a & B = b;
then <^a,b^> c= <^a9,b9^> & <^a9,b9^> c= MonFuncs(A, B) by Def4,ALTCAT_2:31
;
hence thesis;
end;
end;
registration
let A be with_all_isomorphisms lattice-wise category;
cluster full -> with_all_isomorphisms for non empty subcategory of A;
coherence
proof
let B be non empty subcategory of A such that
A1: B is full;
let a,b be Object of B, f be Function of latt a, latt b;
reconsider a9 = a, b9 = b as Object of A by ALTCAT_2:29;
assume f is isomorphic;
then f in <^a9, b9^> by Def8;
hence thesis by A1,ALTCAT_2:28;
end;
end;
registration
let A be with_complete_lattices category;
cluster -> with_complete_lattices for non empty subcategory of A;
coherence
proof
let B be non empty subcategory of A;
thus B is lattice-wise;
let b be Object of B;
reconsider a = b as Object of A by ALTCAT_2:29;
a is complete LATTICE by Def5;
hence thesis;
end;
end;
definition
let W be with_non-empty_element set;
defpred P[Object of W-UPS_category] means latt $1 is continuous;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
set r = the upper-bounded well-ordering Order of a;
set b = RelStr(#a,r#);
func W-CONT_category -> strict full non empty subcategory of W-UPS_category
means
: Def11:
for a being Object of W-UPS_category holds a is Object of it iff
latt a is continuous;
existence
proof
reconsider b as Object of W-UPS_category by A1,Def10;
b = latt b;
then
A2: ex b being Object of W-UPS_category st P[b];
thus ex C being strict full non empty subcategory of W-UPS_category st for
a being Object of W-UPS_category holds a is Object of C iff P[a] from YELLOW20:
sch 2(A2);
end;
correctness
proof
let B1,B2 be strict full non empty subcategory of W-UPS_category such that
A3: for a being Object of W-UPS_category holds a is Object of B1 iff P [a] and
A4: for a being Object of W-UPS_category holds a is Object of B2 iff P [a];
the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3(A3, A4);
hence thesis;
end;
end;
definition
let W be with_non-empty_element set;
defpred P[Object of W-CONT_category] means latt $1 is algebraic;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
set r = the upper-bounded well-ordering Order of a;
set b = RelStr(#a,r#);
func W-ALG_category -> strict full non empty subcategory of W-CONT_category
means
: Def12:
for a being Object of W-CONT_category holds a is Object of it
iff latt a is algebraic;
existence
proof
reconsider b as Object of W-UPS_category by A1,Def10;
b = latt b;
then reconsider b as Object of W-CONT_category by Def11;
b = latt b;
then
A2: ex b being Object of W-CONT_category st P[b];
thus ex C being strict full non empty subcategory of W-CONT_category st
for a being Object of W-CONT_category holds a is Object of C iff P[a] from
YELLOW20:sch 2(A2);
end;
correctness
proof
let B1,B2 be strict full non empty subcategory of W-CONT_category such
that
A3: for a being Object of W-CONT_category holds a is Object of B1 iff P[a] and
A4: for a being Object of W-CONT_category holds a is Object of B2 iff P[a];
the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3(A3, A4);
hence thesis;
end;
end;
theorem Th16:
for W being with_non-empty_element set for L being LATTICE st
the carrier of L in W holds L is Object of W-CONT_category iff L is strict
complete continuous
proof
let W be with_non-empty_element set, L be LATTICE such that
A1: the carrier of L in W;
hereby
assume L is Object of W-CONT_category;
then reconsider a = L as Object of W-CONT_category;
L = latt a & a is Object of W-UPS_category by ALTCAT_2:29;
hence L is strict complete continuous by A1,Def11,Th14;
end;
assume
A2: L is strict complete continuous;
then reconsider a = L as Object of W-UPS_category by A1,Th14;
latt a = L;
hence thesis by A2,Def11;
end;
theorem
for W being with_non-empty_element set for L being LATTICE st the
carrier of L in W holds L is Object of W-ALG_category iff L is strict complete
algebraic
proof
let W be with_non-empty_element set, L be LATTICE such that
A1: the carrier of L in W;
hereby
assume L is Object of W-ALG_category;
then reconsider a = L as Object of W-ALG_category;
L = latt a & a is Object of W-CONT_category by ALTCAT_2:29;
hence L is strict complete algebraic by A1,Def12,Th16;
end;
assume
A2: L is strict complete algebraic;
then reconsider a = L as Object of W-CONT_category by A1,Th16;
latt a = L;
hence thesis by A2,Def12;
end;
theorem Th18:
for W being with_non-empty_element set for a,b being Object of W
-CONT_category for f being set holds f in <^a,b^> iff f is
directed-sups-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-CONT_category, f be set;
reconsider a1 = a, b1 = b as Object of W-UPS_category by ALTCAT_2:29;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence thesis by Th15;
end;
theorem Th19:
for W being with_non-empty_element set for a,b being Object of W
-ALG_category for f being set holds f in <^a,b^> iff f is
directed-sups-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-ALG_category, f be set;
reconsider a1 = a, b1 = b as Object of W-CONT_category by ALTCAT_2:29;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence thesis by Th18;
end;
registration
let W be with_non-empty_element set;
let a,b be Object of W-CONT_category;
cluster <^a,b^> -> non empty;
coherence
proof
set f = the directed-sups-preserving Function of latt a, latt b;
f in <^a,b^> by Th18;
hence thesis;
end;
end;
registration
let W be with_non-empty_element set;
let a,b be Object of W-ALG_category;
cluster <^a,b^> -> non empty;
coherence
proof
set f = the directed-sups-preserving Function of latt a, latt b;
f in <^a,b^> by Th19;
hence thesis;
end;
end;