### The Mizar article:

### Categorial Background for Duality Theory

**by****Grzegorz Bancerek**

- Received August 1, 2001
Copyright (c) 2001 Association of Mizar Users

- MML identifier: YELLOW21
- [ MML identifier index ]

environ vocabulary ORDERS_1, FUNCT_1, RELAT_1, PROB_1, AMI_1, ORDERS_3, BOOLE, ALTCAT_1, YELLOW18, WAYBEL_0, BHSP_3, PBOOLE, FUNCT_2, PRE_TOPC, SEQM_3, FILTER_0, CAT_1, QC_LANG1, FUNCTOR0, WELLORD1, ALTCAT_3, CAT_3, ISOCAT_1, SUBSET_1, LATTICES, RELAT_2, ORDINAL1, TARSKI, WELLORD2, CARD_1, LATTICE3, ORDINAL2, COMPTS_1, QUANTAL1, WAYBEL_8, WAYBEL_3, REALSET1, TRIANG_1, ALTCAT_2, FUNCT_5, YELLOW21; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, REALSET1, FUNCT_2, PROB_1, BINOP_1, ORDINAL1, CARD_1, AMI_1, TRIANG_1, STRUCT_0, ORDERS_1, LATTICE3, GRCAT_1, ORDERS_3, FUNCT_5, WELLORD1, WELLORD2, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_8, PRE_TOPC, ALTCAT_1, ALTCAT_2, FUNCTOR0, ALTCAT_3, YELLOW18; constructors GRCAT_1, TOPS_2, TRIANG_1, AMI_1, ORDERS_3, WAYBEL_1, WAYBEL_8, YELLOW_9, QUANTAL1, WAYBEL18, ALTCAT_3, YELLOW18, PROB_1; clusters SUBSET_1, RELSET_1, FUNCT_1, ORDINAL1, CARD_1, REALSET1, AMI_1, STRUCT_0, ORDERS_1, LATTICE3, WAYBEL_0, WAYBEL_3, TRIANG_1, WAYBEL_8, YELLOW_9, WAYBEL10, WAYBEL17, ALTCAT_2, FUNCTOR0, FUNCTOR2, ALTCAT_4, YELLOW18; requirements SUBSET, BOOLE; definitions TARSKI, RELAT_2, WELLORD1, WELLORD2, ORDERS_1, LATTICE3, ORDERS_3, ALTCAT_1, ALTCAT_3, YELLOW_0, WAYBEL_0, WAYBEL_3, YELLOW18, XBOOLE_0; theorems ZFMISC_1, RELAT_1, FUNCT_1, PBOOLE, SETWISEO, STRUCT_0, PRE_TOPC, WELLORD1, WELLORD2, ORDERS_1, ORDERS_2, FUNCT_2, GRCAT_1, BINOP_1, TRIANG_1, ALTCAT_1, ALTCAT_2, ORDERS_3, ALTCAT_3, ORDINAL1, CARD_1, CARD_5, WAYBEL_0, WAYBEL13, AMI_1, ORDINAL3, TARSKI, RELSET_1, RELAT_2, TOPS_2, REALSET1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_3, WAYBEL_8, YELLOW18, WAYBEL20, YELLOW16, XBOOLE_0, XBOOLE_1, PARTFUN1; schemes TARSKI, CARD_3, PRALG_2, ZFREFLE1, YELLOW18, YELLOW20, XBOOLE_0; begin :: Lattice-wise categories reserve x, y for set; definition let a be set; func a as_1-sorted -> 1-sorted equals: Def1: a if a is 1-sorted otherwise 1-sorted(#a#); coherence; consistency; end; definition let W be set; defpred P[set] means $1 is strict Poset & the carrier of $1 as_1-sorted in W; func POSETS W means: Def2: 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: x in A iff P[x] and A2: x in B iff P[x]; thus thesis from Extensionality(A1,A2); end; existence proof deffunc F(set) = bool [:$1,$1:]; defpred P[set,set] means $2 is Order of $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 FuncSeparation; defpred Q[set,set] means ex P being strict Poset st $2 = P & the InternalRel of P = $1; A5: now let x,y,z be set; assume Q[x,y]; then consider P1 be strict Poset such that A6: y = P1 & the InternalRel of P1 = x; assume Q[x,z]; then consider P2 being strict Poset such that A7: z = P2 & the InternalRel of P2 = x; dom the InternalRel of P1 = the carrier of P1 by ORDERS_2:1; hence y = z by A6,A7,ORDERS_2:1; end; consider A being set such that A8: x in A iff ex y st y in Union F & Q[y,x] from Fraenkel(A5); take A; let x; hereby assume x in A; then consider y 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 & the InternalRel of P = y by A10; consider z being set such that A12: z in W & y in F.z by A3,A9,CARD_5:10; reconsider y as Order of z by A4,A12; thus x is strict Poset by A11; dom y = z & dom y = the carrier of P & x as_1-sorted = P by A11,Def1,ORDERS_2:1; hence the carrier of x as_1-sorted in W by A12; end; assume A13: x is strict Poset & the carrier of x as_1-sorted in W; then reconsider P = x as strict Poset; A14: x as_1-sorted = P by Def1; the InternalRel of P in bool [:the carrier of P, the carrier of P:]; then the InternalRel of P in F.the carrier of P by A4,A13,A14; then the InternalRel of P in Union F by A3,A13,A14,CARD_5:10; hence thesis by A8; end; end; definition let W be non empty set; cluster POSETS W -> non empty; coherence proof consider x being Element of W, y being Order of x; RelStr(#x,y#) as_1-sorted = RelStr(#x,y#) by Def1; hence thesis by Def2; end; end; definition 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: a is strict Poset & the carrier of a as_1-sorted in W by Def2; reconsider a as Poset by A1,Def2; a = a as_1-sorted & the carrier of a as_1-sorted <> {} by A2,Def1,AMI_1:def 1; hence thesis by STRUCT_0:def 1; 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; definition cluster with_complete_lattices -> lattice-wise category; coherence by Def5; cluster lattice-wise -> concrete carrier-underlaid category; coherence proof 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); deffunc F(set) = the carrier of $1 as_1-sorted; consider F being ManySortedSet of C such that A4: for i being Element of C holds F.i = F(i) from LambdaDMS; C is para-functional proof take F; let a,b be object of C; reconsider A = a, B = b as LATTICE by A2; a as_1-sorted = A & b as_1-sorted = B by Def1; then F.a = the carrier of A & F.b = the carrier of B by A4; then <^a,b^> c= MonFuncs(A, B) & MonFuncs(A, B) c= Funcs(F.a, F.b) by A3,ORDERS_3:11; hence thesis by XBOOLE_1:1; end; hence C is concrete by A1,YELLOW18:def 11; let a be object of C; reconsider S = a as LATTICE by A2; take S; thus a = S; idm a in <^a,a^> & <^a,a^> c= MonFuncs(S, S) by A3; then consider f being map of S,S such that A5: idm a = f and A6: f in Funcs(the carrier of S, the carrier of S) and f is monotone by ORDERS_3:def 6; thus the_carrier_of a = dom id the_carrier_of a by RELAT_1:71 .= dom f by A1,A5,YELLOW18:def 10 .= the carrier of S by A6,ALTCAT_1:6; end; end; local_CLCatEx { A() -> non empty set, P[set, set, set] }: ex C being strict category st C is lattice-wise & the carrier of C = A() & for a,b being LATTICE, f being monotone map 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 map of a,b, g being map 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 set A = A(); defpred P[set,set] means ex a,b being LATTICE st $1 = [a,b] & for f being set holds f in $2 iff f in MonFuncs(a, b) & P[a,b,f]; A4: now let x; assume x in [:A,A:]; then consider a,b being set such that A5: a in A & b in A & x = [a,b] by ZFMISC_1:def 2; reconsider a,b as LATTICE by A1,A5; defpred Q[set] means P[a,b,$1]; consider y being set such that A6: for f being set holds f in y iff f in MonFuncs(a, b) & Q[f] from Separation; take y; thus P[x,y] by A5,A6; end; consider F being Function such that dom F = [:A,A:] and A7: for x st x in [:A,A:] holds P[x, F.x] from NonUniqFuncEx(A4); A8: now let a,b be LATTICE; assume a in A & b in A; then [a,b] in [:A,A:] by ZFMISC_1:106; then consider a',b' being LATTICE such that A9: [a,b] = [a',b'] and A10: for f being set holds f in F.[a,b] iff f in MonFuncs(a', b') & P[a',b',f] by A7; A11: a = a' & b = b' by A9,ZFMISC_1:33; let f be set; hereby assume A12: f in F.[a,b]; hence P[a,b,f] by A10,A11; thus f in MonFuncs(a, b) by A10,A11,A12; then ex g being map 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 map of a, b; end; assume f is monotone map of a, b; then reconsider g = f as monotone map 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 f in MonFuncs(a, b) by ORDERS_3:def 6; hence P[a,b,f] implies f in F.[a,b] by A10,A11; end; defpred P[set,set] means for a being LATTICE st a = $1 holds $2 = the carrier of a; A13: now let x; assume x in A; then reconsider a = x as LATTICE by A1; reconsider b = the carrier of a as set; take b; thus P[x,b]; end; consider D being Function such that dom D = A and A14: for x st x in A holds P[x, D.x] from NonUniqFuncEx(A13); deffunc D(set) = D.$1; deffunc B(set,set) = F.[$1,$2]; A15: 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 A16: f in F.[a,b] & g in F.[b,c]; reconsider x = a, y = b, z = c as LATTICE by A1; reconsider f' = f as monotone map of x,y by A8,A16; reconsider g' = g as monotone map of y,z by A8,A16; P[x,y,f'] & P[y,z,g'] by A8,A16; then P[a,c,g'*f'] by A2; then g'*f' is monotone map of x,z implies g'*f' in F.[x,z] by A8; hence thesis by YELLOW_2:14; end; A17: 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 set; 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 A8; then f in Funcs(D.a, the carrier of y) by A14; hence thesis by A14; end; A18: now let a be Element of A; reconsider x = a as LATTICE by A1; D.a = the carrier of x by A14; then id (D.a) = id x & P[x,x,id x] by A3,GRCAT_1:def 11; hence id D(a) in B(a,a) by A8; end; consider C being concrete strict category such that A19: the carrier of C = A and for a being object of C holds the_carrier_of a = D(a) and A20: for a,b being object of C holds <^a,b^> = B(a,b) from ConcreteCategoryLambda(A15,A17,A18); take C; thus C is semi-functional set-id-inheriting; thus for a being object of C holds a is LATTICE by A1,A19; 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 A21: A = a & B = b; let f be set; <^a,b^> = F.[A,B] by A20,A21; hence thesis by A8,A19,A21; end; thus the carrier of C = A() by A19; let a,b be LATTICE, f be monotone map of a,b; A22: (the Arrows of C).[a,b] = (the Arrows of C).(a,b) by BINOP_1:def 1; hereby assume A23: f in (the Arrows of C).(a,b); then [a,b] in dom the Arrows of C by A22,FUNCT_1:def 4; then [a,b] in [:A,A:] by A19,PBOOLE:def 3; hence a in A & b in A by ZFMISC_1:106; then reconsider x = a, y = b as object of C by A19; (the Arrows of C).[a,b] = <^x,y^> by A22,ALTCAT_1:def 2 .= F.[x,y] by A20; hence P[a,b,f] by A8,A19,A22,A23; end; assume A24: a in A() & b in A(); then reconsider x = a, y = b as object of C by A19; (the Arrows of C).[a,b] = <^x,y^> by A22,ALTCAT_1:def 2 .= F.[x,y] by A20; hence thesis by A8,A22,A24; end; definition cluster strict with_complete_lattices category; existence proof consider L being complete LATTICE; defpred P[set,set,set] means $3 = $3; A1: for a be Element of {L} holds a is LATTICE by TARSKI:def 1; A2: for a,b,c being LATTICE st a in {L} & b in {L} & c in {L} for f being map of a,b, g being map of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f]; A3: for a being LATTICE st a in {L} holds P[a,a,id a]; 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 map of a,b holds f in (the Arrows of C).(a,b) iff a in {L} & b in {L} & P[a,b,f] from local_CLCatEx(A1,A2,A3); 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 idm a = id the carrier of (a as_1-sorted) by YELLOW18:def 10 .= id (a as_1-sorted) by GRCAT_1:def 11; end; definition let C be lattice-wise category; let a be object of C; redefine func a as_1-sorted -> LATTICE equals: Def6: 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; synonym latt a; end; definition let C be with_complete_lattices category; let a be object of C; redefine func a as_1-sorted -> complete LATTICE; coherence proof a is complete LATTICE by Def5; hence thesis by Def1; end; synonym latt a; 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 map of latt a, latt b equals: Def7: f; coherence proof latt a = a & latt b = b by Def6; then f in <^a,b^> & <^a,b^> c= MonFuncs(latt a, latt b) by A1,Def4; then ex g being map 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 g*f = @g*@f by A1,YELLOW18:38; 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 map 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 map of a,b, g being map 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[set, set, set] means P[$1,$2,$3]; A4: for a,b,c being LATTICE st a in A() & b in A() & c in A() for f being map of a,b, g being map of b,c st p[a,b,f] & p[b,c,g] holds p[a,c,g*f] by A2; A5: for a being LATTICE st a in A() holds p[a,a,id a] by A3; 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 map of a,b holds f in (the Arrows of C).(a,b) iff a in A() & b in A() & p[a,b,f] from local_CLCatEx(A1,A4,A5); 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; latt a = a & latt b = b & <^a,b^> = (the Arrows of C).(a,b) by Def6,ALTCAT_1:def 2; hence thesis by A7,A8; end; scheme CLCatEx2 { A() -> non empty set, L[set], 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 map 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 map of a,b, g being map 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[set] means $1 is LATTICE & L[$1]; consider A being set such that A4: x in A iff x in POSETS A() & p[x] from Separation; consider x being strict LATTICE such that A5: L[x] & the carrier of x in A() by A1; x as_1-sorted = x by Def1; then x in POSETS A() by A5,Def2; then reconsider A as non empty set by A4,A5; defpred p[set, set, set] means P[$1,$2,$3]; A6: for a being Element of A holds a is LATTICE by A4; A7: now let a,b,c be LATTICE; assume a in A & b in A & c in A; then L[a] & L[b] & L[c] by A4; hence for f being map of a,b, g being map of b,c st p[a,b,f] & p[b,c,g] holds p[a,c,g*f] by A2; end; A8: now let a be LATTICE; assume a in A; then L[a] by A4; hence p[a,a,id a] by A3; end; consider C being lattice-wise strict category such that A9: the carrier of C = A and A10: for a,b being object of C, f being monotone map of latt a, latt b holds f in <^a,b^> iff p[latt a, latt b, f] from CLCatEx1(A6,A7,A8); 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; then x in A iff x is strict & L[x] & the carrier of x in A() by A4; hence x is object of C iff x is strict & L[x] & the carrier of x in A() by A9; end; thus thesis by A10; 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 map 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 map 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); A1: 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 ConcreteCategoryUniq1; assume that A2: the carrier of A1 = A() and A3: for a,b being object of A1, f being monotone map of latt a, latt b holds f in <^a,b^> iff P[a,b,f] and A4: the carrier of A2 = A() and A5: for a,b being object of A2, f being monotone map of latt a, latt b holds f in <^a,b^> iff P[a,b,f]; A6: for a,b being object of A1 holds <^a,b^> = (the Arrows of A1).(a,b) by ALTCAT_1:def 2; now let a,b be object of A2; reconsider a' = a, b' = b as object of A1 by A2,A4; A7: latt a = a & latt b = b & latt a' = a & latt b' = b by Def6; A8: <^a',b'^> = (the Arrows of A1).(a',b') by ALTCAT_1:def 2; thus <^a,b^> = (the Arrows of A1).(a,b) proof hereby let x; assume A9: x in <^a,b^>; then reconsider f = x as Morphism of a,b ; A10: @f = f by A9,Def7; then P[latt a',latt b',@f] & @f is map of latt a',latt b' by A5,A7,A9; hence x in (the Arrows of A1).(a,b) by A3,A7,A8,A10; end; let x; assume A11: x in (the Arrows of A1).(a,b); then reconsider f = x as Morphism of a',b' by A8; @f = f by A8,A11,Def7; then P[latt a,latt b,@f] & f = @f by A3,A7,A8,A11; hence x in <^a,b^> by A5,A7; end; end; hence thesis by A1,A2,A4,A6; end; scheme CLCatUniq2 { A() -> non empty set, L[set], 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 map 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 map 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; defpred p[set, set, set] means P[$1,$2,$3]; A1: 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 map 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 map 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; assume that A2: for x being LATTICE holds x is object of A1 iff x is strict & L[x] & the carrier of x in A() and A3: for a,b being object of A1, f being monotone map of latt a, latt b holds f in <^a,b^> iff P[a,b,f] and A4: for x being LATTICE holds x is object of A2 iff x is strict & L[x] & the carrier of x in A(); the carrier of A2 = the carrier of A1 proof hereby let x; assume x in the carrier of A2; then A5: x is object of A2; then A6: x is LATTICE by Def4; then A7: x as_1-sorted = x by Def1; then x is strict LATTICE & L[x] & the carrier of x as_1-sorted in A() by A4,A5,A6; then x is object of A1 by A2,A7; hence x in the carrier of A1; end; let x; assume x in the carrier of A1; then A8: x is object of A1; then A9: x is LATTICE by Def4; then A10: x as_1-sorted = x by Def1; then x is strict LATTICE & L[x] & the carrier of x as_1-sorted in A() by A2,A8,A9; then x is object of A2 by A4,A10; hence x in the carrier of A2; end; hence thesis by A1,A3; 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 map 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 map 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 map of a,b st P[a,b,f] holds F(a,b,f) is map 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 map of a,b, g being map 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 deffunc o(set) = O($1); deffunc f(set,set,set) = F($1,$2,$3); A7: for a being object of A() holds o(a) is object of B() proof let a be object of A(); a is LATTICE & a in the carrier of A() by Def4; then O(a) in the carrier of B() by A3; hence thesis; end; A8: 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 A9: <^a,b^> <> {}; let f be Morphism of a,b; A10: f = @f & a = latt a & b = latt b by A9,Def6,Def7; <^a,b^> = (the Arrows of A()).(a,b) by ALTCAT_1:def 2; then a in the carrier of A() & b in the carrier of A() & P[a,b,f] by A1,A9,A10; then O(a) in the carrier of B() & O(b) in the carrier of B() & F(a,b,f) is map of O(a),O(b) & Q[O(a),O(b),F(a,b,f)] by A3,A4,A10; hence thesis by A2; end; A11: now let a,b,c be object of A() such that A12: <^a,b^> <> {} & <^b,c^> <> {}; let f be Morphism of a,b, g be Morphism of b,c; let a',b',c' be object of B() such that A13: a' = o(a) & b' = o(b) & c' = o(c); let f' be Morphism of a',b', g' be Morphism of b',c' such that A14: f' = f(a,b,f) & g' = f(b,c,g); A15: latt a = a & latt b = b & latt c = c by Def6; A16: @f = f & @g = g by A12,Def7; latt a' = a' & latt b' = b' & latt c' = c' & F(a,b,f) in (the Arrows of B()).(O(a), O(b)) & F(b,c,g) in (the Arrows of B()).(O(b), O(c)) by A8,A12,Def6; then A17: F(a,b,f) in <^a',b'^> & F(b,c,g) in <^b',c'^> by A13,ALTCAT_1:def 2 ; then A18: @f' = f' & @g' = g' by Def7; <^a,b^> = (the Arrows of A()).(a,b) & <^b,c^> = (the Arrows of A()).(b,c) by ALTCAT_1:def 2; then P[a,b,f] & P[b,c,g] by A1,A12,A15,A16; then F(a,c,@g*@f) = F(b,c,g)*F(a,b,f) by A6,A15,A16 .= g'*f' by A14,A17, A18,Th3; hence f(a,c,g*f) = g'*f' by A12,Th3; end; A19: now let a be object of A(), a' be object of B(); assume a' = o(a); then a in the carrier of A() & latt a' = O(a) & latt a = a & idm a = id latt a by Def6,Th2; hence f(a,a,idm a) = id latt a' by A5 .= idm a' by Th2; end; consider F being covariant strict Functor of A(),B() such that A20: for a being object of A() holds F.a = o(a) and A21: 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 CovariantFunctorLambda(A7,A8,A11,A19); take F; hereby let a be object of A(); a = latt a by Def6; hence F.a = O(latt a) by A20; end; let a,b be object of A() such that A22: <^a, b^> <> {}; let f be Morphism of a,b; a = latt a & b = latt b & f = @f by A22,Def6,Def7; hence thesis by A21,A22; 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 map 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 map 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 map of a,b st P[a,b,f] holds F(a,b,f) is map 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 map of a,b, g being map 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 deffunc o(set) = O($1); deffunc f(set,set,set) = F($1,$2,$3); A7: for a being object of A() holds o(a) is object of B() proof let a be object of A(); a is LATTICE & a in the carrier of A() by Def4; then O(a) in the carrier of B() by A3; hence thesis; end; A8: 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 A9: <^a,b^> <> {}; let f be Morphism of a,b; A10: f = @f & a = latt a & b = latt b by A9,Def6,Def7; <^a,b^> = (the Arrows of A()).(a,b) by ALTCAT_1:def 2; then a in the carrier of A() & b in the carrier of A() & P[a,b,f] by A1,A9,A10; then O(a) in the carrier of B() & O(b) in the carrier of B() & F(a,b,f) is map of O(b),O(a) & Q[O(b),O(a),F(a,b,f)] by A3,A4,A10; hence thesis by A2; end; A11: now let a,b,c be object of A() such that A12: <^a,b^> <> {} & <^b,c^> <> {}; let f be Morphism of a,b, g be Morphism of b,c; let a',b',c' be object of B() such that A13: a' = o(a) & b' = o(b) & c' = o(c); let f' be Morphism of b',a', g' be Morphism of c',b' such that A14: f' = f(a,b,f) & g' = f(b,c,g); A15: latt a = a & latt b = b & latt c = c by Def6; A16: @f = f & @g = g by A12,Def7; latt a' = a' & latt b' = b' & latt c' = c' & F(a,b,f) in (the Arrows of B()).(O(b), O(a)) & F(b,c,g) in (the Arrows of B()).(O(c), O(b)) by A8,A12,Def6; then A17: F(a,b,f) in <^b',a'^> & F(b,c,g) in <^c',b'^> by A13,ALTCAT_1:def 2 ; then A18: @f' = f' & @g' = g' by Def7; <^a,b^> = (the Arrows of A()).(a,b) & <^b,c^> = (the Arrows of A()).(b,c) by ALTCAT_1:def 2; then P[a,b,f] & P[b,c,g] by A1,A12,A15,A16; then F(a,c,@g*@f) = F(a,b,f)*F(b,c,g) by A6,A15,A16 .= f'*g' by A14,A17, A18,Th3; hence f(a,c,g*f) = f'*g' by A12,Th3; end; A19: now let a be object of A(), a' be object of B(); assume a' = o(a); then a in the carrier of A() & latt a' = O(a) & latt a = a & idm a = id latt a by Def6,Th2; hence f(a,a,idm a) = id latt a' by A5 .= idm a' by Th2; end; consider F being contravariant strict Functor of A(),B() such that A20: for a being object of A() holds F.a = o(a) and A21: 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 ContravariantFunctorLambda(A7,A8,A11,A19); take F; hereby let a be object of A(); a = latt a by Def6; hence F.a = O(latt a) by A20; end; let a,b be object of A() such that A22: <^a, b^> <> {}; let f be Morphism of a,b; a = latt a & b = latt b & f = @f by A22,Def6,Def7; hence thesis by A21,A22; 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 map 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 map 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 map 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 map of a,b st Q[a,b,f] ex c,d being LATTICE, g being map 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 deffunc o(set) = O($1); deffunc f(set,set,set) = F($1,$2,$3); A7: 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; A8: for a,b being object of A() st o(a) = o(b) holds a = b proof let a,b be object of A(); a in the carrier of A() & a = latt a & b = latt b by Def6; hence thesis by A4; end; A9: 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 A10: <^a,b^> <> {}; let f,g be Morphism of a,b; A11: latt a = a & latt b = b & @f = f & @g = g by A10,Def6,Def7; <^a,b^> = (the Arrows of A()).(a,b) by ALTCAT_1:def 2; then P[latt a, latt b, @f] & P[latt a, latt b, @g] by A1,A10,A11; hence thesis by A5,A11; end; A12: now let a,b be object of B() such that A13: <^a,b^> <> {}; let f be Morphism of a,b; A14: latt a = a & latt b = b & @f = f by A13,Def6,Def7; <^a,b^> = (the Arrows of B()).(a,b) by ALTCAT_1:def 2; then Q[latt a, latt b, @f] by A2,A13,A14; then consider c,d being LATTICE, g being map of c,d such that A15: c in the carrier of A() & d in the carrier of A() & P[c,d,g] & latt a = O(c) & latt b = O(d) & @f = F(c,d,g) by A6; reconsider c' = c, d' = d as object of A() by A15; <^c',d'^> = (the Arrows of A()).(c,d) by ALTCAT_1:def 2; then g in <^c',d'^> by A1,A15; 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 A14,A15; end; thus thesis from CatIsomorphism(A7,A8,A9,A12); 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 map 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 map 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 map of a,b st F(a,b,f) = F(a,b,g) holds f = g and A6: for a,b being LATTICE, f being map of a,b st Q[a,b,f] ex c,d being LATTICE, g being map 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 deffunc o(set) = O($1); deffunc f(set,set,set) = F($1,$2,$3); A7: 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; A8: for a,b being object of A() st o(a) = o(b) holds a = b proof let a,b be object of A(); a in the carrier of A() & a = latt a & b = latt b by Def6; hence thesis by A4; end; A9: 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 A10: <^a,b^> <> {}; let f,g be Morphism of a,b; latt a = a & latt b = b & @f = f & @g = g by A10,Def6,Def7; hence thesis by A5; end; A11: now let a,b be object of B() such that A12: <^a,b^> <> {}; let f be Morphism of a,b; A13: latt a = a & latt b = b & @f = f by A12,Def6,Def7; <^a,b^> = (the Arrows of B()).(a,b) by ALTCAT_1:def 2; then Q[latt a, latt b, @f] by A2,A12,A13; then consider c,d being LATTICE, g being map of c,d such that A14: c in the carrier of A() & d in the carrier of A() & P[c,d,g] & latt b = O(c) & latt a = O(d) & @f = F(c,d,g) by A6; reconsider c' = c, d' = d as object of A() by A14; <^c',d'^> = (the Arrows of A()).(c,d) by ALTCAT_1:def 2; then g in <^c',d'^> by A1,A14; 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 A13,A14; end; thus thesis from CatAntiIsomorphism(A7,A8,A9,A11); 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 map of latt a, latt b st f is isomorphic holds f in <^a,b^>; end; definition cluster with_all_isomorphisms (strict lattice-wise category); existence proof consider L being LATTICE; defpred P[set,set,set] means $3 = $3; A1: for a be Element of {L} holds a is LATTICE by TARSKI:def 1; A2: for a,b,c being LATTICE st a in {L} & b in {L} & c in {L} for f being map of a,b, g being map of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f]; A3: for a being LATTICE st a in {L} holds P[a,a,id a]; consider C being strict category such that A4: C is lattice-wise and A5: the carrier of C = {L} and A6: for a,b being LATTICE, f being monotone map of a,b holds f in (the Arrows of C).(a,b) iff a in {L} & b in {L} & P[a,b,f] from local_CLCatEx(A1,A2,A3); reconsider C as strict lattice-wise category by A4; take C; let a,b be object of C, f be map of latt a, latt b; A7: latt a = a & latt b = b by Def6; then (f is isomorphic implies f is monotone) & (the Arrows of C).(latt a, latt b) = <^a,b^> by ALTCAT_1:def 2,YELLOW16:17; hence thesis by A5,A6,A7; 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 map of latt b, latt a such that A2: @f*g = id latt b & g*@f = id latt a by YELLOW16:17; A3: idm a = id latt a & idm b = id latt b by Th2; g is isomorphic by A2,YELLOW16:17; then A4: @f in <^a,b^> & g in <^b,a^> by A1,Def8; then reconsider g as Morphism of b,a ; @g = g by A4,Def7; then A5: f*g = idm b & g*f = idm a by A2,A3,A4,Th3; then A6: g is_left_inverse_of f & g is_right_inverse_of f by ALTCAT_3:def 1; then f is retraction coretraction by ALTCAT_3:def 2,def 3; hence f*f" = idm b & f"*f = idm a by A4,A5,A6,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: @f*@(f") = f*f" & @(f")*@f = f"*f by A1,Th3; idm a = id latt a & idm b = id latt b by Th2; hence thesis by A2,A3,YELLOW16:17; 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 map 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 map 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 map 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 map 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 deffunc o1(set) = O1($1); deffunc f1(set,set,set) = F1($1,$2,$3); deffunc o2(set) = O2($1); deffunc f2(set,set,set) = F2($1,$2,$3); deffunc a(set) = A($1); deffunc b(set) = B($1); A9: 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; A10: 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; A11: 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 A12: a = O2(O1(b)); A13: latt a = a & latt b = b by Def6; then consider f being monotone map of O2(O1(b)), latt b such that A14: f = A(b) & f is isomorphic & P[O2(O1(b)), latt b, f] & P[latt b, O2(O1(b)), f"] by A5; thus A(b) in <^a, b^> by A1,A12,A13,A14; ex g being map of latt b, O2(O1(b)) st g = f" & g is monotone by A14,WAYBEL_0:def 38; hence A(b)" in <^b,a^> by A1,A12,A13,A14; thus thesis by A14,WAYBEL_0:66; end; A16: 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 A17: b = O1(O2(a)); A18: latt a = a & latt b = b by Def6; then consider f being monotone map of latt a, O1(O2(a)) such that A19: f = B(a) & f is isomorphic & Q[latt a, O1(O2(a)), f] & Q[O1(O2(a)), latt a, f"] by A6; thus B(a) in <^a, b^> by A2,A17,A18,A19; ex g being map of O1(O2(a)), latt a st g = f" & g is monotone by A19,WAYBEL_0:def 38; hence B(a)" in <^b,a^> by A2,A17,A18,A19; thus thesis by A19,WAYBEL_0:66; end; A21: 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 A22: <^a,b^> <> {}; let f be Morphism of a,b; @f = f by A22,Def7; hence thesis by A7,A22; end; A23: 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 A24: <^a,b^> <> {}; let f be Morphism of a,b; @f = f by A24,Def7; hence thesis by A8,A24; end; thus thesis from ConcreteCatEquivalence(A9,A10, A11,A16,A21,A23); end; begin :: UPS category definition let R be Relation; attr R is upper-bounded means: Def9: 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} proof let X be set; x in X iff {x} c= X by ZFMISC_1:37; hence thesis by XBOOLE_1:7,45; end; definition cluster well-ordering -> reflexive transitive antisymmetric connected well_founded Relation; coherence by WELLORD1:def 4; end; definition cluster well-ordering Relation; existence proof consider r being Relation such that A1: r well_orders 5 by WELLORD2:26; take r|_2 5; thus thesis by A1,WELLORD2:25; end; end; theorem Th6: 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 f be one-to-one Function, R be Relation; A1: dom f = rng (f") & rng f = dom (f") by FUNCT_1:55; hereby assume [x,y] in f*R*(f"); then consider a being set such that A2: [x,a] in f*R & [a,y] in f" by RELAT_1:def 8; consider b being set such that A3: [x,b] in f & [b,a] in R by A2,RELAT_1:def 8; thus x in dom f & y in dom f by A1,A2,A3,RELAT_1:def 4,def 5; b = f.x & y = f".a & a in rng f by A1,A2,A3,FUNCT_1:8; hence [f.x, f.y] in R by A3,FUNCT_1:57; end; assume A4: x in dom f & y in dom f & [f.x, f.y] in R; then [x,f.x] in f & f".(f.y) = y & f.y in rng f by FUNCT_1:8,56,def 5; then [x,f.y] in f*R & [f.y,y] in f" by A1,A4,FUNCT_1:8,RELAT_1:def 8; hence [x,y] in f*R*(f") by RELAT_1:def 8; end; definition let f be one-to-one Function; let R be reflexive Relation; cluster f*R*(f") -> reflexive; coherence proof let x; assume x in field (f*R*(f")); then A1: x in dom (f*R*(f")) \/ rng (f*R*(f")) by RELAT_1:def 6; A2: R is_reflexive_in field R by RELAT_2:def 9; per cases by A1,XBOOLE_0:def 2; suppose x in dom (f*R*(f")); then consider y being set such that A3: [x,y] in (f*R*(f")) by RELAT_1:def 4; A4: x in dom f & [f.x, f.y] in R by A3,Th6; then f.x in field R by RELAT_1:30; then [f.x, f.x] in R by A2,RELAT_2:def 1; hence thesis by A4,Th6; suppose x in rng (f*R*(f")); then consider y being set such that A5: [y,x] in (f*R*(f")) by RELAT_1:def 5; A6: x in dom f & [f.y, f.x] in R by A5,Th6; then f.x in field R by RELAT_1:30; then [f.x, f.x] in R by A2,RELAT_2:def 1; hence thesis by A6,Th6; end; end; definition let f be one-to-one Function; let R be antisymmetric Relation; cluster f*R*(f") -> antisymmetric; coherence proof let x,y be set; assume x in field (f*R*(f")) & y in field (f*R*(f")); assume [x,y] in f*R*(f") & [y,x] in f*R*(f"); then A1: x in dom f & y in dom f & [f.x, f.y] in R & [f.y, f.x] in R by Th6; then f.x in field R & f.y in field R & R is_antisymmetric_in field R by RELAT_1:30,RELAT_2:def 12; then f.x = f.y by A1,RELAT_2:def 4; hence thesis by A1,FUNCT_1:def 8; end; end; definition let f be one-to-one Function; let R be transitive Relation; cluster f*R*(f") -> transitive; coherence proof let x,y,z be set; assume x in field (f*R*(f")) & y in field (f*R*(f")) & z in field (f*R*(f")); assume [x,y] in f*R*(f") & [y,z] in f*R*(f"); then A1: x in dom f & z in dom f & [f.x, f.y] in R & [f.y, f.z] in R by Th6; then f.x in field R & f.y in field R & f.z in field R & R is_transitive_in field R by RELAT_1:30,RELAT_2:def 16; then [f.x, f.z] in R by A1,RELAT_2:def 8; hence thesis by A1,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 & dom f = X & rng f = A; reconsider f as Function of X,A by A1,FUNCT_2:4; reconsider f' = f as one-to-one Function by A1; reconsider g = f" as Function of A,X by A1,FUNCT_2:31; A2: dom g = A & rng g = X by A1,FUNCT_1:55; set R = f*(RelIncl A)*g; dom RelIncl A = A & rng RelIncl A = A by ORDERS_2:1; then rng (f*(RelIncl A)) = A & dom (f*(RelIncl A)) = X by A1,RELAT_1:46,47; then A3: dom R = X & rng R = X by A2,RELAT_1:46,47; then A4: field R = X \/ X by RELAT_1:def 6 .= X; then A5: f'*(RelIncl A)*(f'") is_reflexive_in X & f'*(RelIncl A)*(f'") is_antisymmetric_in X & f'*(RelIncl A)*(f'") is_transitive_in X by RELAT_2:def 9,def 12,def 16; reconsider R as Relation of X; reconsider R as Order of X by A3,A5,PARTFUN1:def 4; A6: 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,A4,WELLORD2:def 1; let a,b be set; hereby assume A7: [a,b] in R; hence a in field R & b in field R by RELAT_1:30; consider x being set such that A8: [a,x] in f*RelIncl A & [x,b] in g by A7,RELAT_1:def 8; consider y being set such that A9: [a,y] in f & [y,x] in RelIncl A by A8,RELAT_1:def 8; y = f.a & b = g.x & a in dom f & x in dom g by A8,A9,FUNCT_1:8; hence [f.a,f.b] in RelIncl A by A1,A9,FUNCT_1:57; end; assume A10: a in field R & b in field R & [f.a,f.b] in RelIncl A; then f".(f.b) = b & f.b in A by A1,A4,FUNCT_1:56,def 5; then A11: [a,f.a] in f & [f.b,b] in g by A1,A2,A4,A10,FUNCT_1:8; then [a,f.b] in f*RelIncl A by A10,RELAT_1:def 8; hence thesis by A11,RELAT_1:def 8; end; then A12: f" is_isomorphism_of RelIncl A, R by WELLORD1:49; A13: R, RelIncl A are_isomorphic by A6,WELLORD1:def 8; take R; thus R well_orders X proof thus R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X by A5; RelIncl A is connected well_founded by WELLORD2:4,6; then R is connected well_founded by A12,WELLORD1:53; hence R is_connected_in X & R is_well_founded_in X by A4,RELAT_2:def 14,WELLORD1:5; end; then R is well-ordering by A4,WELLORD1:8; hence thesis by A13,WELLORD2:def 2; end; definition let X be non empty set; cluster upper-bounded well-ordering Order of X; existence proof consider x being Element of X; A1: X\{x},Card (X\{x}) are_equipotent by CARD_1:def 5; A2: {x},{Card (X\{x})} are_equipotent by CARD_1:48; A3: {x} misses (X\{x}) by XBOOLE_1:79; not Card (X\{x}) in Card (X\{x}); then A4: {Card (X\{x})} misses Card (X\{x}) by ZFMISC_1:56; A5: succ Card (X\{x}) = Card (X\{x}) \/ {Card (X\{x})} & X = (X\{x}) \/ {x} by Lm1,ORDINAL1:def 1; then X,succ Card (X\{x}) are_equipotent by A1,A2,A3,A4,CARD_1:58; then consider r being Order of X such that A6: r well_orders X and A7: order_type_of r = succ Card (X\{x}) by Th7; A8: field r = X by ORDERS_2:2; then r is well-ordering by A6,WELLORD1:8; then r, RelIncl order_type_of r are_isomorphic by WELLORD2:def 2; then RelIncl order_type_of r, r are_isomorphic by WELLORD1:50; then consider f being Function such that A9:f is_isomorphism_of RelIncl order_type_of r, r by WELLORD1:def 8; field RelIncl order_type_of r = order_type_of r by WELLORD2:def 1; then A10:f is one-to-one & dom f = order_type_of r & rng f = X by A8,A9,WELLORD1:def 7; take r; thus r is upper-bounded proof take a = f.Card (X\{x}); let y; assume A11: y in field r; then A12: f".y in order_type_of r by A8,A10,FUNCT_1:54; then A13: f".y in Card (X\{x}) or f".y = Card (X\{x}) by A5,A7,SETWISEO:6; reconsider b = f".y as Ordinal by A12,ORDINAL1:23; b c= Card (X\{x}) & Card (X\{x}) in order_type_of r by A5,A7,A13,ORDINAL1:def 2,SETWISEO:6; then [b, Card (X\{x})] in RelIncl order_type_of r by A12,WELLORD2:def 1; then [f.b, a] in r by A9,WELLORD1:def 7; hence thesis by A8,A10,A11,FUNCT_1:57; end; thus thesis by A6,A8,WELLORD1:8; 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:19; 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,LATTICE3:def 9; hence thesis by ORDERS_1:def 9; end; given x such that A3: for y st y in field the InternalRel of P holds [y,x] in the InternalRel of P; consider y being Element of P; y <= y; then [y,y] in the InternalRel of P by ORDERS_1:def 9; then y in field the InternalRel of P by RELAT_1:30; then [y,x] in the InternalRel of P by A3; then x in field the InternalRel of P by RELAT_1:30; 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 by ORDERS_1:def 9; then y in field the InternalRel of P by RELAT_1:30; then [y,x] in the InternalRel of P by A3; hence thesis by ORDERS_1:def 9; 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_2:2; thus A3: P is connected proof let x,y being Element of P; the InternalRel of P is connected reflexive by A1,WELLORD1:def 4; then the InternalRel of P is_connected_in the carrier of P & the InternalRel of P is_reflexive_in the carrier of P & (x = y or x <> y) by A2,RELAT_2:def 9,def 14; then [x,y] in the InternalRel of P or [y,x] in the InternalRel of P by RELAT_2:def 1,def 6; hence x <= y or y <= x by ORDERS_1:def 9; end; thus P is complete proof let X be set; defpred P[set] 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 A4: x in Y iff x in the carrier of P & P[x] from Separation; the InternalRel of P is upper-bounded by Th8; then consider x such that A5: for y st y in field the InternalRel of P holds [y,x] in the InternalRel of P by Def9; consider y being Element of P; [y,x] in the InternalRel of P by A2,A5; then x in field the InternalRel of P by RELAT_1:30; then reconsider x as Element of P by A2; A6: Y c= the carrier of P proof let x; thus thesis by A4; end; for y being Element of P st y in X holds [y,x] in the InternalRel of P by A2,A5; then x in Y by A4; then consider a being set such that A7: a in Y & for b being set st b in Y holds [a,b] in the InternalRel of P by A1,A2,A6,WELLORD1:10; reconsider a as Element of P by A6,A7; take a; hereby let y be Element of P; assume y in X; then [y,a] in the InternalRel of P by A4,A7; hence y <= a by ORDERS_1:def 9; end; let b be Element of P; assume A8: for c being Element of P st c in X holds c <= b; now let c being Element of P; assume c in X; then c <= b by A8; hence [c,b] in the InternalRel of P by ORDERS_1:def 9; end; then b in Y by A4; then [a,b] in the InternalRel of P by A7; hence a <= b by ORDERS_1:def 9; end; then P is complete Chain by A3; hence thesis; 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; assume A1: R is well-ordering; then R, RelIncl A are_isomorphic by WELLORD2:def 2; then consider f being Function such that A2: f is_isomorphism_of R, RelIncl A by WELLORD1:def 8; reconsider L = P as complete Chain by A1,Th9; let x,y be Element of P; assume A3: y < x; then y <= x & y <> x by ORDERS_1:def 10; then [y,x] in R by ORDERS_1:def 9; then A4: [f.y, f.x] in RelIncl A & f.x <> f.y by A2,A3,WELLORD1:45; A5: field RelIncl A = A by WELLORD2:def 1; then A6: f.x in A & f.y in A by A4,RELAT_1:30; then reconsider a = f.x, b = f.y as Ordinal by ORDINAL1:23; b c= a by A4,A6,WELLORD2:def 1; then b c< a by A4,XBOOLE_0:def 8; then b in a by ORDINAL1:21; then A7: succ b c= a & b c= succ b by ORDINAL1:33,ORDINAL3:1; then A8: succ b in A by A6,ORDINAL1:22; rng f = A by A2,A5,WELLORD1:def 7; then consider z being set such that A9: z in dom f & succ b = f.z by A8,FUNCT_1:def 5; A10: field R = the carrier of P by ORDERS_2:2; A11: dom f = field R by A2,WELLORD1:def 7; then reconsider z as Element of P by A9,A10; take z; thus z is compact proof let D be non empty directed Subset of P such that A12: z <= sup D and A13: for d being Element of P st d in D holds not z <= d; A14: L is complete; D is_<=_than y proof let c be Element of P; assume A15: c in D; then not z <= c & z <= z by A13; then z >= c by A14,WAYBEL_0:def 29; then [c,z] in R by ORDERS_1:def 9; then A16: [f.c, succ b] in RelIncl A by A2,A9,WELLORD1:def 7; then A17: f.c in A by A5,RELAT_1:30; then reconsider fc = f.c as Ordinal by ORDINAL1:23; c <> z & f is one-to-one by A2,A13,A15,WELLORD1:def 7; then fc c= succ b & fc <> succ b by A8,A9,A10,A11,A16,A17,FUNCT_1:def 8,WELLORD2:def 1; then fc c< succ b by XBOOLE_0:def 8; then fc in succ b by ORDINAL1:21; then fc c= b by ORDINAL1:34; then [fc,b] in RelIncl A by A6,A17,WELLORD2:def 1; hence [c,y] in R by A2,A10,WELLORD1:def 7; end; then sup D <= y by A14,YELLOW_0:32; then z <= y by A12,YELLOW_0:def 2; then [z,y] in R by ORDERS_1:def 9; then [succ b, b] in RelIncl A by A2,A9,WELLORD1:def 7; then succ b c= b by A6,A8,WELLORD2:def 1; then b = succ b by A7,XBOOLE_0:def 10; hence contradiction by ORDINAL1:14; end; [f.y, succ b] in RelIncl A & [succ b, f.x] in RelIncl A by A6,A7,A8,WELLORD2:def 1; hence [y,z] in R & [z,x] in R by A2,A9,A10,WELLORD1:def 7; 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,14; then consider z being Element of L such that A2: z is compact & 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 A2; end; hence thesis by WAYBEL_8:7; end; definition 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 cluster non trivial -> with_non-empty_element set; coherence proof let W be set; assume W is non trivial; then reconsider W as non trivial set; consider w1 being Element of W; consider w2 being Element of W \ {w1}; W \ {w1} is non empty by REALSET1:32; then w2 in W & w2 <> w1 & (w1 = {} or w1 <> {}) by ZFMISC_1:64; hence thesis by TRIANG_1:def 1; end; end; definition let W be non empty set; given w being Element of W such that A1: w is non empty; reconsider w as non empty set by A1; defpred L[LATTICE] means $1 is complete; defpred P[LATTICE,LATTICE, map of $1,$2] means $3 is directed-sups-preserving; consider r being upper-bounded well-ordering Order of w; RelStr(#w,r#) is complete; then A2: ex x being strict LATTICE st L[x] & the carrier of x in W; A3: for a,b,c being LATTICE st L[a] & L[b] & L[c] for f being map of a,b, g being map of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by WAYBEL20:29; A4: for a being LATTICE st L[a] holds P[a,a,id a]; 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 map of latt a, latt b holds f in <^a,b^> iff f is directed-sups-preserving; existence proof 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 map of latt a, latt b holds f in <^a,b^> iff P[latt a, latt b, f] from CLCatEx2(A2,A3,A4); end; correctness proof 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 map 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 map 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 map 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 map of latt a, latt b; latt a = a & latt b = b & (f in <^a,b^> iff f is directed-sups-preserving) by A6,Def6; hence f in <^a,b^> iff Q[a,b,f]; end; A10: now let a,b be object of C2; let f be monotone map of latt a, latt b; latt a = a & latt b = b & (f in <^a,b^> iff f is directed-sups-preserving) by A8,Def6; 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 map 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 map 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; definition 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; A1: ex w being non empty set st w in W by TRIANG_1:def 1; thus C is lattice-wise; hereby let a be object of C; a = latt a by Def6; hence a is complete LATTICE by A1,Def10; end; let a,b be object of C, f be map of latt a, latt b; assume A2: f is isomorphic; a = latt a & b = latt b by Def6; then reconsider S = latt a, T = latt b as complete LATTICE by A1,Def10; f is sups-preserving map of S, T by A2,WAYBEL13:20; hence f in <^a,b^> 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; A1: ex w being non empty set st w in W by TRIANG_1:def 1; let x; assume x in the carrier of W-UPS_category; then reconsider x as object of W-UPS_category; latt x = x by Def6; then the carrier of latt x in W & x is strict Poset by A1,Def10; hence thesis by 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; A1: ex w being non empty set st w in W by TRIANG_1:def 1; let x; hereby assume x is object of W-UPS_category; then reconsider a = x as object of W-UPS_category; latt a = x by Def6; 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 L as_1-sorted = L & the carrier of L as_1-sorted in W & L is strict by Def1,Def2; 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; A1: L as_1-sorted = L by Def1; assume the carrier of L in W; 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 map of latt a, latt b proof let W be with_non-empty_element set; A1: ex w being non empty set st w in W by TRIANG_1:def 1; let a,b be object of W-UPS_category; let f be set; 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 map of latt a, latt b by A1,A2,Def10; end; thus thesis by A1,Def10; end; definition let W be with_non-empty_element set; let a,b be object of W-UPS_category; cluster <^a,b^> -> non empty; coherence proof consider f being directed-sups-preserving map of latt a, latt b; f in <^a,b^> by Th15; hence thesis; end; end; begin :: Lattice-wise subcategories theorem Th16: for A being category, B being non empty subcategory of A for a being object of A, b being object of B st b = a holds the_carrier_of b = the_carrier_of a proof let A be category, B be non empty subcategory of A; let a be object of A, b be object of B such that A1: b = a; thus the_carrier_of b = proj1 idm b by YELLOW18:def 9 .= proj1 idm a by A1,ALTCAT_2:35 .= the_carrier_of a by YELLOW18:def 9; end; definition let A be set-id-inheriting category; cluster -> set-id-inheriting (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:35 .= id the_carrier_of a by YELLOW18:def 10 .= id the_carrier_of b by Th16; end; end; definition let A be para-functional category; cluster -> para-functional (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: dom F = the carrier of A & the carrier of B c= the carrier of A by ALTCAT_2:def 11,PBOOLE:def 3; then dom G = the carrier of B by RELAT_1:91; then reconsider G as ManySortedSet of B by PBOOLE:def 3; take G; let a1,a2 be object of B; a1 in the carrier of B & a2 in the carrier of B; then reconsider b1 = a1, b2 = a2 as object of A by A2; F.a1 = G.a1 & F.a2 = G.a2 by FUNCT_1:72; then <^a1,a2^> c= <^b1,b2^> & <^b1,b2^> c= Funcs(G.a1,G.a2) by A1,ALTCAT_2: 32; hence thesis by XBOOLE_1:1; end; end; definition let A be semi-functional category; cluster -> semi-functional (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^> <> {} & <^b2,b3^> <> {} & <^b1,b3^> <> {}; let f1 be Morphism of b1,b2, f2 be Morphism of b2,b3; let f', g' be Function such that A2: f1 = f' & f2 = g'; reconsider a1 = b1, a2 = b2, a3 = b3 as object of A by ALTCAT_2:30; reconsider g1 = f1 as Morphism of a1,a2 by A1,ALTCAT_2:34; reconsider g2 = f2 as Morphism of a2,a3 by A1,ALTCAT_2:34; <^b1,b2^> c= <^a1,a2^> & <^b2,b3^> c= <^a2,a3^> & <^b1,b3^>c= <^a1,a3^> by ALTCAT_2:32; then <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} by A1,XBOOLE_1:3; then g2*g1 = g'*f' by A2,ALTCAT_1:def 14; hence thesis by A1,ALTCAT_2:33; end; end; definition let A be carrier-underlaid category; cluster -> carrier-underlaid (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:30; consider S being 1-sorted such that A1: a = S & the_carrier_of a = the carrier of S by Def3; take S; thus b = S by A1; thus the_carrier_of b = proj1 idm b by YELLOW18:def 9 .= proj1 idm a by ALTCAT_2:35 .= the carrier of S by A1,YELLOW18:def 9; end; end; definition let A be lattice-wise category; cluster -> lattice-wise (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:30; a is LATTICE by Def4; hence b is LATTICE; end; let a,b be object of B; reconsider a' = a, b' = b as object of A by ALTCAT_2:30; let A,B be LATTICE; assume A = a & B = b; then <^a,b^> c= <^a',b'^> & <^a',b'^> c= MonFuncs(A, B) by Def4,ALTCAT_2:32 ; hence thesis by XBOOLE_1:1; end; end; definition let A be with_all_isomorphisms (lattice-wise category); cluster full -> with_all_isomorphisms (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 map of latt a, latt b; reconsider a' = a, b' = b as object of A by ALTCAT_2:30; assume f is isomorphic; then f in <^a', b'^> & <^a,b^> = <^a',b'^> by A1,Def8,ALTCAT_2:29; hence f in <^a,b^>; end; end; definition let A be with_complete_lattices category; cluster -> with_complete_lattices (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:30; a is complete LATTICE by Def5; hence thesis; end; end; definition let W be with_non-empty_element set; consider a being non empty set such that A1: a in W by TRIANG_1:def 1; consider r being upper-bounded well-ordering Order of a; set b = RelStr(#a,r#); reconsider b as object of W-UPS_category by A1,Def10; defpred P[object of W-UPS_category] means latt $1 is continuous; b = latt b by Def6; then A2: ex b being object of W-UPS_category st P[b]; 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 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 FullSubcategoryEx(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 FullSubcategoryUniq(A3,A4) ; hence thesis; end; end; definition let W be with_non-empty_element set; consider a being non empty set such that A1: a in W by TRIANG_1:def 1; consider r being upper-bounded well-ordering Order of a; set b = RelStr(#a,r#); reconsider b as object of W-UPS_category by A1,Def10; b = latt b by Def6; then reconsider b as object of W-CONT_category by Def11; defpred P[object of W-CONT_category] means latt $1 is algebraic; b = latt b by Def6; then A2: ex b being object of W-CONT_category st P[b]; 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 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 FullSubcategoryEx(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 FullSubcategoryUniq(A3,A4) ; hence thesis; end; end; theorem Th17: 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 Def6,ALTCAT_2:30; 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 by Def6; 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 Def6,ALTCAT_2:30; hence L is strict complete algebraic by A1,Def12,Th17; end; assume A2: L is strict complete algebraic; then L is strict complete algebraic LATTICE; then reconsider a = L as object of W-CONT_category by A1,Th17; latt a = L by Def6; hence thesis by A2,Def12; end; theorem Th19: 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 map 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:30; <^a,b^> = <^a1,b1^> by ALTCAT_2:29; hence thesis by Th15; end; theorem Th20: 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 map 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:30; <^a,b^> = <^a1,b1^> by ALTCAT_2:29; hence thesis by Th19; end; definition let W be with_non-empty_element set; let a,b be object of W-CONT_category; cluster <^a,b^> -> non empty; coherence proof consider f being directed-sups-preserving map of latt a, latt b; f in <^a,b^> by Th19; hence thesis; end; end; definition let W be with_non-empty_element set; let a,b be object of W-ALG_category; cluster <^a,b^> -> non empty; coherence proof consider f being directed-sups-preserving map of latt a, latt b; f in <^a,b^> by Th20; hence thesis; end; end;

Back to top