Concrete categories

A category $\mathcal C$ is concrete if there exists a function assigning to each object $A$ of $\mathcal C$ its carrying set, the ${\mathcal C}$-carrier of $A$, such that

• a morphism in $\mathcal C$ from $A$ to $B$ is a function from $\mathcal C$-carrier of $A$ to $\mathcal C$-carrier of $B$,
• the composition of morphisms is a function composition, and
• identity morphisms are identity maps.

The formalization of concrete categories in MML was motivated by the duality theory for continuous lattices (see [25, p. 189]). In duality theory, we have to consider various types of maps between lattices and it is natural to use the framework of category theory. Namely, we cope with concrete categories whose objects are lattices and morphisms are maps preserving some lattice properties. For example, the base category of this theory, the category UPS, has complete lattices as its objects and maps preserving directed suprema as morphisms. Other categories INF and SUP, also with complete lattices as objects, have morphisms preserving infima and suprema, respectively.

The problem with formalizing such notions lies again in the task of expressing concepts from a set theory with classes in the terminology of a set theory without classes, like the Tarski-Grothendieck set theory selected for MML. For example, we cannot define a category with all complete lattices as objects. In MIZAR formalization, all objects of a fixed category must form a set and, because there is no set of all complete lattices, there is also no category of all complete lattices (see Section ).

The MIZAR formalization may be seen as more general and forces investigations of different categories, that is, categories over different sets of lattices. As a result, categories with fixed universa as in the CCL-book become one of the covered instances. Fortunately, the theory does not refer to the richness of these categories and the fact that they are closed under some algebraic constructions does not affect our work now.

There are two approaches in MML to the formalization of categories. The first method proposed in CAT_1 [19] introduces a structure with uniqueness of domain and codomain. Namely, the structure includes fields Cod and Dom which are functions from morphisms to objects. So, the concept of a morphism from one object to another is defined by values of Dom and Cod. In other words, the hom-sets are disjoint. The concrete category Ens V of all sets from the family V and functions among them was formalized in this approach with morphisms as triples [[a, b], f], where f is Function of a, b. In particular, morphisms of Ens V are not functions and their composition is expressed in a slightly complicated way in ENS_1 [20].

definition let V be set, m1, m2 be Element of Maps V;
  assume  cod m1 = dom m2;
  func m2*m1 -> Element of Maps V equals                :: ENS_1:def 7
   [[dom m1, cod m2], m2`2*m1`2];
end;

This definition is permissive, that is, its definiens is available only when the assumed condition is met. This means that we can use the expression m2*m1 freely and it always denotes an element of Maps V. However, what this term is equal to we can determine only when cod m1 = dom m2. Maps V is the set of morphisms of Ens V.

The second approach, introduced in ALTCAT_1 [50], starts from the concept of a morphism. Namely, AltCatStr has a field Arrows which assigns to each pair of objects a set of morphisms. The EnsCat V category is formalized as AltCatStr with Arrows assigning to any pair of sets the set of all functions from the first set into the second. The composition of morphisms in EnsCat V is a composition of functions. This approach complicates the concept of functors and their composition, but on the other hand it enables us to generalize functors.

The second approach was chosen to introduce a general framework for concrete categories and, eventually, lattice-wise categories. A lattice-wise category is a concrete category $\mathcal C$ with lattices as objects and monotone maps as morphisms. The carrying set of an object of $\mathcal C$ is the value of the carrier selector of the object, that is

for C being lattice-wise category, a being object of C
 ex S being 1-sorted st S = a & C-carrier a = the carrier of S

In the current implementation, because it is impossible to redefine object of to be RelStr or even 1-sorted, the following so called casting functor was introduced for convenience.

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;

A suitable redefinition was made for objects of lattice-wise categories

definition
 let C be lattice-wise category,  a be object of C;
 redefine func a as_1-sorted -> LATTICE equals       :: YELLOW21:def 6
  a;
 synonym latt a;
end;

and another casting functor was defined for decoding the category morphisms to the lattice language.

definition
 let C be lattice-wise category, 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;

The two theorems below state the correspondence of isomorphisms expressed in terms of categories and lattices.

theorem                                                  :: YELLOW21:4
for C being with_all_isomorphisms (lattice-wise category)
    a, b being object of C, f being Morphism of a,b
 st @f is isomorphic holds f is iso;

theorem                                                  :: YELLOW21:5
 for C being lattice-wise category, 
     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;

The isomorphic attribute is a notion about relational structures while iso is from the world of categories.

The machinery of categories presented in this section was heavily used in the formalization of duality (see Section ).