Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek
- Received August 1, 2001
- MML identifier: YELLOW21
- [
Mizar article,
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;
begin :: Lattice-wise categories
reserve x, y for set;
definition
let a be set;
func a as_1-sorted -> 1-sorted equals
:: YELLOW21:def 1
a if a is 1-sorted otherwise 1-sorted(#a#);
end;
definition
let W be set;
func POSETS W means
:: YELLOW21:def 2
x in it iff x is strict Poset & the carrier of x as_1-sorted in W;
end;
definition
let W be non empty set;
cluster POSETS W -> non empty;
end;
definition
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;
definition
cluster with_complete_lattices -> lattice-wise category;
cluster lattice-wise -> concrete carrier-underlaid category;
end;
definition
cluster strict with_complete_lattices 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);
definition
let C be lattice-wise category;
let a be object of C;
redefine func a as_1-sorted -> LATTICE equals
:: YELLOW21:def 6
a;
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;
synonym latt a;
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 map 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 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
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 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
for a being LATTICE st a in A() holds P[a,a,id a];
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
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 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
for a being LATTICE st L[a] holds P[a,a,id a];
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;
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;
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
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
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
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 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
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 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);
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
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
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
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 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
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 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);
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
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
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
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 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
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);
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
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
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
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 map of a,b st F(a,b,f) = F(a,b,g)
holds f = g
and
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);
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 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);
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 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 map 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 map 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 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
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
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;
definition
cluster well-ordering ->
reflexive transitive antisymmetric connected well_founded Relation;
end;
definition
cluster well-ordering Relation;
end;
theorem :: YELLOW21:6
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;
definition
let f be one-to-one Function;
let R be reflexive Relation;
cluster f*R*(f") -> reflexive;
end;
definition
let f be one-to-one Function;
let R be antisymmetric Relation;
cluster f*R*(f") -> antisymmetric;
end;
definition
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;
definition
let X be non empty set;
cluster upper-bounded well-ordering 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;
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;
end;
definition
cluster non trivial -> with_non-empty_element set;
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 map of latt a, latt b
holds f in <^a,b^> iff f is directed-sups-preserving;
end;
definition
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 map of latt a, latt b;
definition
let W be with_non-empty_element set;
let a,b be object of W-UPS_category;
cluster <^a,b^> -> non empty;
end;
begin :: Lattice-wise subcategories
theorem :: YELLOW21:16
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;
definition
let A be set-id-inheriting category;
cluster -> set-id-inheriting (non empty subcategory of A);
end;
definition
let A be para-functional category;
cluster -> para-functional (non empty subcategory of A);
end;
definition
let A be semi-functional category;
cluster -> semi-functional (non empty transitive SubCatStr of A);
end;
definition
let A be carrier-underlaid category;
cluster -> carrier-underlaid (non empty subcategory of A);
end;
definition
let A be lattice-wise category;
cluster -> lattice-wise (non empty subcategory of A);
end;
definition
let A be with_all_isomorphisms (lattice-wise category);
cluster full -> with_all_isomorphisms (non empty subcategory of A);
end;
definition
let A be with_complete_lattices category;
cluster -> with_complete_lattices (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: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-CONT_category iff L is strict complete continuous;
theorem :: YELLOW21:18
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:19
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;
theorem :: YELLOW21:20
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;
definition
let W be with_non-empty_element set;
let a,b be object of W-CONT_category;
cluster <^a,b^> -> non empty;
end;
definition
let W be with_non-empty_element set;
let a,b be object of W-ALG_category;
cluster <^a,b^> -> non empty;
end;
Back to top