Theory Galois_Base
section ‹Galois›
subsection ‹Basic Abbreviations›
theory Galois_Base
imports
Order_Functors_Base
begin
locale galois = order_functors
begin
text ‹The locale @{locale galois} serves to define concepts that ultimately lead
to the definition of Galois connections and Galois equivalences.
Galois connections and equivalences are special cases of adjoints and
adjoint equivalences, respectively, known from category theory.
As such, in what follows, we sometimes borrow vocabulary from category theory
to highlight this connection.
A ∗‹Galois connection› between two relations @{term "(≤⇘L⇙)"} and
@{term "(≤⇘R⇙)"} consists of two monotone functions (i.e. order functors)
@{term "l"} and @{term "r"} such that @{term "x ≤⇘L⇙ r y ⟷ l x ≤⇘R⇙ y"}.
We call this the ∗‹Galois property›.
@{term "l"} is called the ∗‹left adjoint› and @{term "r"} the ∗‹right adjoint›.
We call @{term "(≤⇘L⇙)"} the ∗‹left relation› and @{term "(≤⇘R⇙)"} the ∗‹right relation›.
By composing the adjoints, we obtain the unit @{term "η"} and counit @{term "ε"}
of the Galois connection.›
end
end