:: Categorial Background for Duality Theory
:: by Grzegorz Bancerek
::
:: Received August 1, 2001
:: Copyright (c) 2001-2018 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, WELLORD1, WELLORD2;
requirements SUBSET, BOOLE;
begin :: Lattice-wise categories
reserve x, y for set;
definition
let a be object;
func a as_1-sorted -> 1-sorted equals
:: YELLOW21:def 1
a if a is 1-sorted otherwise
the 1-sorted;
end;
definition
let W be set;
func POSETS W -> set means
:: YELLOW21:def 2
for x being object holds
x in it iff x is strict Poset & the carrier of x as_1-sorted in W;
end;
registration
let W be non empty set;
cluster POSETS W -> non empty;
end;
registration
let W be with_non-empty_elements set;
cluster POSETS W -> POSet_set-like;
end;
definition
let C be category;
attr C is carrier-underlaid means
:: YELLOW21:def 3
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
:: YELLOW21:def 4
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
:: YELLOW21:def 5
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;
cluster lattice-wise -> concrete carrier-underlaid for category;
end;
scheme :: YELLOW21:sch 1
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
for a being Element of A() holds a is LATTICE and
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
for a being LATTICE st a in A() holds P[a,a,id a];
registration
cluster strict with_complete_lattices for category;
end;
theorem :: YELLOW21:1
for C being carrier-underlaid category, a being Object of C holds
the_carrier_of a = the carrier of a as_1-sorted;
theorem :: YELLOW21:2
for C being set-id-inheriting carrier-underlaid category for a
being Object of C holds idm a = id (a as_1-sorted);
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
:: YELLOW21:def 6
a;
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;
end;
definition
let C be lattice-wise category;
let a,b be Object of C such that
<^a,b^> <> {};
let f be Morphism of a,b;
func @f -> monotone Function of latt a, latt b equals
:: YELLOW21:def 7
f;
end;
theorem :: YELLOW21:3
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;
scheme :: YELLOW21:sch 2
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
for a being Element of A() holds a is LATTICE and
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
for a being LATTICE st a in A() holds P[a,a,id a];
scheme :: YELLOW21:sch 3
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
ex x being strict LATTICE st L[x] & the carrier of x in A() and
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
for a being LATTICE st L[a] holds P[a,a,id a];
scheme :: YELLOW21:sch 4
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;
scheme :: YELLOW21:sch 5
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;
scheme :: YELLOW21:sch 6
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
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
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
for a being LATTICE st a in the carrier of A() holds O(a) in the
carrier of B() and
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
for a being LATTICE st a in the carrier of A() holds F(a,a,id a) =
id O(a) and
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);
scheme :: YELLOW21:sch 7
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
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
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
for a being LATTICE st a in the carrier of A() holds O(a) in the
carrier of B() and
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
for a being LATTICE st a in the carrier of A() holds F(a,a,id a) =
id O(a) and
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);
scheme :: YELLOW21:sch 8
CLCatIsomorphism { P, Q[set, set, set], A,B() -> lattice-wise category, O(
set) -> LATTICE, F(set,set,set) -> Function }: A(), B() are_isomorphic
provided
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
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
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
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
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
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);
scheme :: YELLOW21:sch 9
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
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
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
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
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
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
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);
begin :: Equivalence of lattice-wise categories
definition
let C be lattice-wise category;
attr C is with_all_isomorphisms means
:: YELLOW21:def 8
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;
end;
theorem :: YELLOW21:4
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;
theorem :: YELLOW21:5
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;
scheme :: YELLOW21:sch 10
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
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
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
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
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
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
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
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
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;
begin :: UPS category
definition
let R be Relation;
attr R is upper-bounded means
:: YELLOW21:def 9
ex x st for y st y in field R holds [y ,x] in R;
end;
registration
cluster well-ordering -> reflexive transitive antisymmetric connected
well_founded for Relation;
end;
registration
cluster well-ordering for Relation;
end;
theorem :: YELLOW21:6
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;
registration
let f be one-to-one Function;
let R be reflexive Relation;
cluster f*R*(f") -> reflexive;
end;
registration
let f be one-to-one Function;
let R be antisymmetric Relation;
cluster f*R*(f") -> antisymmetric;
end;
registration
let f be one-to-one Function;
let R be transitive Relation;
cluster f*R*(f") -> transitive;
end;
theorem :: YELLOW21:7
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;
registration
let X be non empty set;
cluster upper-bounded well-ordering for Order of X;
end;
theorem :: YELLOW21:8
for P being reflexive non empty RelStr holds P is upper-bounded
iff the InternalRel of P is upper-bounded;
theorem :: YELLOW21:9
for P being upper-bounded non empty Poset st the InternalRel of
P is well-ordering holds P is connected complete continuous;
theorem :: YELLOW21:10
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;
theorem :: YELLOW21:11
for P being upper-bounded non empty Poset st the InternalRel
of P is well-ordering holds P is algebraic;
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;
end;
definition
let W be non empty set;
given w being Element of W such that
w is non empty;
func W-UPS_category -> lattice-wise strict category means
:: YELLOW21:def 10
(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;
end;
registration
let W be with_non-empty_element set;
cluster W-UPS_category -> with_complete_lattices with_all_isomorphisms;
end;
theorem :: YELLOW21:12
for W being with_non-empty_element set holds the carrier of W
-UPS_category c= POSETS W;
theorem :: YELLOW21:13
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;
theorem :: YELLOW21:14
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;
theorem :: YELLOW21:15
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;
registration
let W be with_non-empty_element set;
let a,b be Object of W-UPS_category;
cluster <^a,b^> -> non empty;
end;
begin
registration
let A be set-id-inheriting category;
cluster -> set-id-inheriting for non empty subcategory of A;
end;
registration
let A be para-functional category;
cluster -> para-functional for non empty subcategory of A;
end;
registration
let A be semi-functional category;
cluster -> semi-functional for non empty transitive SubCatStr of A;
end;
registration
let A be carrier-underlaid category;
cluster -> carrier-underlaid for non empty subcategory of A;
end;
registration
let A be lattice-wise category;
cluster -> lattice-wise for non empty subcategory of A;
end;
registration
let A be with_all_isomorphisms lattice-wise category;
cluster full -> with_all_isomorphisms for non empty subcategory of A;
end;
registration
let A be with_complete_lattices category;
cluster -> with_complete_lattices for non empty subcategory of A;
end;
definition
let W be with_non-empty_element set;
func W-CONT_category -> strict full non empty subcategory of W-UPS_category
means
:: YELLOW21:def 11
for a being Object of W-UPS_category holds a is Object of it iff
latt a is continuous;
end;
definition
let W be with_non-empty_element set;
func W-ALG_category -> strict full non empty subcategory of W-CONT_category
means
:: YELLOW21:def 12
for a being Object of W-CONT_category holds a is Object of it
iff latt a is algebraic;
end;
theorem :: YELLOW21:16
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;
theorem :: YELLOW21:17
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;
theorem :: YELLOW21:18
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;
theorem :: YELLOW21:19
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;
registration
let W be with_non-empty_element set;
let a,b be Object of W-CONT_category;
cluster <^a,b^> -> non empty;
end;
registration
let W be with_non-empty_element set;
let a,b be Object of W-ALG_category;
cluster <^a,b^> -> non empty;
end;