Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

**Grzegorz Bancerek**- University of Bialystok, Shinshu University, Nagano

- In the paper, we develop the notation of lattice-wise categories as concrete categories (see [10]) of lattices. Namely, the categories based on [24] with lattices as objects and at least monotone maps between them as morphisms. As examples, we introduce the categories {\it UPS}, {\it CONT}, and {\it ALG} with complete, continuous, and algebraic lattices, respectively, as objects and directed suprema preserving maps as morphisms. Some useful schemes to construct categories of lattices and functors between them are also presented.

- Lattice-wise Categories
- Equivalence of Lattice-wise Categories
- {\it UPS} Category
- Lattice-wise Subcategories

- [1]
Grzegorz Bancerek.
Cardinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
The ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Grzegorz Bancerek.
The well ordering relations.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Grzegorz Bancerek.
Zermelo theorem and axiom of choice.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Grzegorz Bancerek.
Curried and uncurried functions.
*Journal of Formalized Mathematics*, 2, 1990. - [6]
Grzegorz Bancerek.
Complete lattices.
*Journal of Formalized Mathematics*, 4, 1992. - [7]
Grzegorz Bancerek.
Bounds in posets and relational substructures.
*Journal of Formalized Mathematics*, 8, 1996. - [8]
Grzegorz Bancerek.
Directed sets, nets, ideals, filters, and maps.
*Journal of Formalized Mathematics*, 8, 1996. - [9]
Grzegorz Bancerek.
The ``way-below'' relation.
*Journal of Formalized Mathematics*, 8, 1996. - [10]
Grzegorz Bancerek.
Concrete categories.
*Journal of Formalized Mathematics*, 13, 2001. - [11]
Jozef Bialas.
Group and field definitions.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Czeslaw Bylinski.
Binary operations.
*Journal of Formalized Mathematics*, 1, 1989. - [13]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [14]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [15]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Adam Grabowski.
On the category of posets.
*Journal of Formalized Mathematics*, 8, 1996. - [17]
Adam Grabowski and Robert Milewski.
Boolean posets, posets under inclusion and products of relational structures.
*Journal of Formalized Mathematics*, 8, 1996. - [18]
Beata Madras.
On the concept of the triangulation.
*Journal of Formalized Mathematics*, 7, 1995. - [19]
Beata Madras-Kobus.
Basic properties of objects and morphisms.
*Journal of Formalized Mathematics*, 9, 1997. - [20]
Robert Milewski.
Algebraic lattices.
*Journal of Formalized Mathematics*, 8, 1996. - [21]
Michal Muzalewski.
Categories of groups.
*Journal of Formalized Mathematics*, 3, 1991. - [22]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [23]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [24]
Andrzej Trybulec.
Categories without uniqueness of \rm cod and \rm dom.
*Journal of Formalized Mathematics*, 7, 1995. - [25]
Andrzej Trybulec.
Examples of category structures.
*Journal of Formalized Mathematics*, 8, 1996. - [26]
Andrzej Trybulec.
Functors for alternative categories.
*Journal of Formalized Mathematics*, 8, 1996. - [27]
Wojciech A. Trybulec.
Partially ordered sets.
*Journal of Formalized Mathematics*, 1, 1989. - [28]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [29]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [30]
Edmund Woronowicz.
Relations defined on sets.
*Journal of Formalized Mathematics*, 1, 1989. - [31]
Edmund Woronowicz and Anna Zalewska.
Properties of binary relations.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]