Duality theory

Duality of lattices is a meta-property, that is a property of the theory of lattices. The simplest duality of lattices roughly says that any theorem formulated in terms of inf, sup, $\top$ and $\bot$ remains true if we replace them by sup, inf, $\bot$ and $\top$, respectively. This type of duality is covered in YELLOW_7 [8]. The CCL-book covers more complicated dualities, for example, the dualities of inf- and sup-preserving maps in the framework of Galois connections. In essence, these dualities can be expressed entirely within the lattice theoretic framework. While category theory helps us in formulating the gist of duality, it is of little use in obtaining dual theorems directly.

The first idea of how to formalize duality in the CCL project was to capture it without using category theory, but we knew this would result in greatly increasing the number of definitions and theorems. The definitions would be for functors expressing duality by transforming lattices and maps between them. The respective theorems would present the essence of duality without engaging category theory. This approach seemed quite appealing and reasonable since we could not spot a place in the CCL-book where category theory is used except for the succinct formulation of certain meta-properties of lattices. In practice, the lattice formulation of properties behind duality has more value. Another aspect of this approach's appeal was that MML did not contain a formalization of category theory in a form convenient for the CCL project.

However, formulating duality of lattices in the language of category theory seemed like an important test for the formal characterization of duality concepts. Besides, the CCL-book uses the language of category theory and we wanted to follow the book closely.

The work of formalizing duality theory has just started and at the moment the related articles contain formulations in both the lattice nomenclature and the language of categories. As an example, let us consider the following from the CCL-book, p. 179.

1.3. Theorem. (INF-SUP DUALITY). The categories INF and SUP are dual under the functors D and G given by the Galois connection of functions. Specifically, D and G preserve objects (the is, the ``dual'' of a complete lattice is itself under this duality). Moreover GD(g) = g and DG(d) = d for all g in INF and all d in SUP.

The two categories of interest are defined as

1.1. Definition The categories INF and SUP have the same class of objects, namely, the class of all complete lattices. The morphisms of INF preserve arbitrary infs, the morphisms of SUP preserve arbitrary sups.

Without using the terminology of category theory, the above theorem can be formalized as

theorem                         :: WAYBEL34:10 :: 1.3. THEOREM, p. 179
for S, T being complete LATTICE, g being infs-preserving map of S, T
 holds UpperAdj LowerAdj g = g;

theorem                         :: WAYBEL34:11 :: 1.3. THEOREM, p. 179
for S, T being complete LATTICE, d being sups-preserving map of S, T
  holds  LowerAdj UpperAdj d = d;

where the LowerAdj is defined as

definition
 let S, T be LATTICE, g be map of S, T;
 assume S is complete & T is complete & g is infs-preserving;
 func LowerAdj g -> map of T,S means                 :: WAYBEL34:def 1
  [g, it] is Galois;
end;

The UpperAdj is defined analogously.

When using the terminology of categories for expressing the same facts, we run into the foremost problem, mentioned in Section . Namely, in MML we cannot have a category of all continuous lattices as we must deal only with sets. Therefore, one of the categories of interest is defined as

definition :: 1.1 DEFINITION, p. 179
 let W be non empty set; given w being Element of W such that
   w is non empty;
 func W-INF_category -> lattice-wise strict category means
                                                    :: WAYBEL34:def 4
 (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 infs-preserving;
end;

and the definition of the other is analogous. The restriction to a set W serving as the source of carriers for our categories is not that important as the set can be as large as our set theory permits. Note that the assumption of W containing at least one non empty set is purely technical as it eliminates just one set, namely 1, see Endnote .

With these categories defined, we can now formulate duality in the language of categories.

theorem                          :: WAYBEL34:19 :: 1.3 THEOREM, p. 179
for W being with_non-empty_element set holds
  (W LowerAdj)*(W UpperAdj) = id (W-SUP_category) &
  (W UpperAdj)*(W LowerAdj) = id (W-INF_category);

theorem                          :: WAYBEL34:20 :: 1.3 THEOREM, p. 179
for W being with_non-empty_element set holds
  W-INF_category, W-SUP_category are_anti-isomorphic;

where the types of W LowerAdj and W UpperAdj are

  contravariant Functor of W-INF_category, W-SUP_category
  contravariant Functor of W-SUP_category, W-INF_category

respectively. Their definitions are technically complicated and we do not quote them here.

Fortunately, the basic concepts of category theory needed to formulate the above theorem were already available in FUNCTOR0 [51]

definition let A,B be transitive with_units (non empty AltCatStr);
 pred A,B are_anti-isomorphic means                 :: FUNCTOR0:def 41
  ex F being Functor of A,B st F is bijective contravariant;
 symmetry;
end;

We will not go into the details of the definiens: the terms used there correspond to the common terminology of category theory. Here we would like to stress again the importance of systematically developing a data base of formalized mathematics like MML. The basics of category theory were included in MML long before they were needed for the CCL project.