Galois connections

Galois connections are introduced in WAYBEL_1 [6] in two steps. First, a mode for connections between two RelStrs is defined to be a pair of maps followed by a convenient $\mathrm{redefinition}^{\:\alph{redefinitions}}$.

definition let S,T be RelStr;
  mode Connection of S, T -> set means               :: WAYBEL_1:def 9
   ex g being map of S, T, d being map of T, S st it = [g, d];
end;

definition let S,T be RelStr, g be map of S,T, d be map of T,S;
 redefine func [g, d] -> Connection of S, T;
end;

Starting in this way, we can use the mode for purposes other than only one special kind of connection. Since our interest was in Galois connections, the Galois attribute for Connection was introduced.

definition let S, T be non empty RelStr, gc be Connection of S, T;
  attr gc is Galois means                           :: WAYBEL_1:def 10
   ex g being map of S, T, d being map of T, S  
    st gc = [g, d] & g is monotone & d is monotone &
       for t being Element of T, s being Element of S
        holds t <= g.s iff d.t <= s; 
end;

Right after this definition, a more convenient formulation was stated in the following theorem.

theorem                                                  :: WAYBEL_1:9 
for S,T being non empty Poset, g being map of S,T, d being map of T,S 
 holds [g, d] is Galois 
   iff g is monotone & d is monotone & 
        for t being Element of T, s being Element of S 
         holds t <= g.s iff d.t <= s;

One may wonder why we need the theorem when we already have the definition. The answer is: we do not; however, the second formulation is more convenient when:

• g and d are appropriate maps between T and S,
• [g, d] is Galois (that is, [g, d] is Connection of T, S due to the previous redefinition), and
• we would like to access the facts from the definiens of WAYBEL_1:def 10.

Because of the way the current version of MIZAR works, all we can get in one step from WAYBEL_1:def 10 is an existentially quantified formula (which can be eliminated in the same step with the consider construct) and in order to proceed, we have to use properties of equality of two ordered pairs. Using WAYBEL_1:9 instead frees us of this trouble. In the other direction, that is, from the definiens to the definiendum, both the definition and the theorem can be used in exactly the same way. The MIZAR checker is continually upgraded and one of the extensions being considered may eliminate the difference described above.

The names of adjoints are introduced using the same notation as in the CCL-book.

definition let S, T be non empty RelStr, g be map of S, T;
 attr g is upper_adjoint means                      :: WAYBEL_1:def 11
  ex d being map of T, S st [g,d] is Galois;
 synonym g has_a_lower_adjoint;
end;

definition let S, T be non empty RelStr, d be map of T, S;
 attr d is lower_adjoint means                      :: WAYBEL_1:def 12
  ex g being map of S, T st [g,d] is Galois;
 synonym d has_an_upper_adjoint;
end;

Both of these definitions could have been written in one definitional block at the expense of some confusion.

definition let S, T be non empty RelStr, g be map of S, T;
 attr g is upper_adjoint means                      
  ex d being map of T, S st [g, d] is Galois;
 synonym g has_a_lower_adjoint;
 attr g is lower_adjoint means 
  ex d being map of T, S st [d, g] is Galois;
 synonym g has_an_upper_adjoint;
end;

The MIZAR processor would not mind these expressions at all, but for human readers the combined version would be rather puzzling.

The concept of Galois connections is used to introduce Heyting algebras. Namely, a lattice is called a Heyting algebra if for each of its elements $x$, the map $s\mapsto x\sqcap s$ has an upper adjoint (cf. Definition 3.17 in [25, p. 25]). In other words, in a Heyting algebra an implication is definable.

The tasks of defining a Heyting algebra and proving that an implication can be defined in it tested the correctness of our formalization of Galois connections.

definition let S be non empty RelStr, x be Element of S;
 func x"/\" -> map of S, S means                    :: WAYBEL_1:def 18
  for s being Element of S holds it.s = x"/\"s;
end;

definition let H be non empty RelStr;
 attr H is Heyting means                            :: WAYBEL_1:def 19
  H is LATTICE & 
  for x being Element of H holds x"/\"  has_an_upper_adjoint;
 synonym H is_a_Heyting_algebra;
end;

We needed some additional functors in order to conveniently formalize the key theorem.

definition let H be non empty RelStr, a be Element of H;
 assume H is Heyting;
 func a=> -> map of H, H means                      :: WAYBEL_1:def 20
  [it, a"/\"] is Galois;
end;

definition let H be non empty RelStr, a, y be Element of H;
 func a=>y -> Element of H equals                   :: WAYBEL_1:def 21
  a=>.y;
end;

The first definition introduces => as a unary postfix operator and the second defines it as a binary operator. With the help of these functors the key theorem is now expressed as

theorem :: WAYBEL_1:70 
   for H being non empty RelStr st H is_a_Heyting_algebra
    for x, a, y being Element of H holds x >= a"/\"y iff a=>x >= y;

Galois connections are heavily used in duality theory (see Section ).