Theory Galois_Equivalences

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Equivalences›
theory Galois_Equivalences
  imports
    Galois_Connections
    Order_Equivalences
    Partial_Equivalence_Relations
begin

context galois
begin

text‹In the literature, an adjoint equivalence is an adjunction for which
the unit and counit are natural isomorphisms.
Translated to the category of orders,
this means that a ∗‹Galois equivalence› between two relations
@{term "(≤⇘L⇙)"} and @{term "(≤⇘R⇙)"} is a Galois connection for which the unit
@{term "η"} is @{term "deflationary"} and the counit @{term "ε"} is
@{term "inflationary"}.

For reasons of symmetry, we give a different definition which next to
@{term "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"} requires @{term "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"}.
In other words, a Galois equivalence is a Galois connection for which the left
and right adjoints are also right and left adjoints, respectively.
As shown below, in the case of preorders, the definitions coincide.›

definition "galois_equivalence ≡ ((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r ∧ ((≤⇘R⇙) ⊴ (≤⇘L⇙)) r l"

notation galois.galois_equivalence (infix ‹≡⇩G› 50)

lemma galois_equivalenceI [intro]:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "((≤⇘R⇙) ⊴ (≤⇘L⇙)) r l"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  unfolding galois_equivalence_def using assms by blast

lemma galois_equivalenceE [elim]:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r" "((≤⇘R⇙) ⊣ (≤⇘L⇙)) r l"
  using assms unfolding galois_equivalence_def
  by (blast intro: galois.galois_connectionI)

context
begin

interpretation g : galois S T f g for S T f g.

lemma galois_equivalence_eq_galois_connection_rel_inf_galois_prop:
  "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) = ((≤⇘L⇙) ⊣ (≤⇘R⇙)) ⊓ ((≥⇘L⇙) ⊴ (≥⇘R⇙))"
  by (intro ext) auto

lemma rel_inv_galois_equivalence_eq_galois_equivalence [simp]:
  "((≤⇘R⇙) ≡⇩G (≤⇘L⇙))¯ = ((≤⇘L⇙) ≡⇩G (≤⇘R⇙))"
  by (intro ext) auto

corollary galois_equivalence_right_left_iff_galois_equivalence_left_right:
  "((≤⇘R⇙) ≡⇩G (≤⇘L⇙)) r l ⟷ ((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  by auto

lemma galois_equivalence_rel_inv_eq_galois_equivalence [simp]:
  "((≥⇘L⇙) ≡⇩G (≥⇘R⇙)) = ((≤⇘L⇙) ≡⇩G (≤⇘R⇙))"
  by (intro ext) auto

lemma inflationary_on_unit_if_reflexive_on_if_galois_equivalence:
  fixes P :: "'a ⇒ bool"
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  shows "inflationary_on P (≤⇘L⇙) η"
  using assms by (intro inflationary_on_unit_if_reflexive_on_if_galois_connection)
  (elim galois_equivalenceE)

end

lemma deflationary_on_unit_if_reflexive_on_if_galois_equivalence:
  fixes P :: "'a ⇒ bool"
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  shows "deflationary_on P (≤⇘L⇙) η"
proof -
  interpret flip : galois R L r l .
  show ?thesis using assms
  by (auto intro: flip.deflationary_on_counit_if_reflexive_on_if_galois_connection
    simp only: flip.flip_unit_eq_counit)
qed

text ‹Every @{term "galois_equivalence"} on reflexive orders is a Galois
equivalence in the sense of the common literature.›
lemma rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence:
  fixes P :: "'a ⇒ bool"
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  shows "rel_equivalence_on P (≤⇘L⇙) η"
  using assms by (intro rel_equivalence_onI
    inflationary_on_unit_if_reflexive_on_if_galois_equivalence
    deflationary_on_unit_if_reflexive_on_if_galois_equivalence)

lemma galois_equivalence_partial_equivalence_rel_not_reflexive_not_transitive:
  assumes "∃(y :: 'b) y'. y ≠ y'"
  shows "∃(L :: 'a ⇒ 'a ⇒ bool) (R :: 'b ⇒ 'b ⇒ bool) l r.
    (L ≡⇩G R) l r ∧ partial_equivalence_rel L ∧
    ¬(reflexive_on (in_field R) R) ∧ ¬(transitive_on (in_field R) R)"
proof -
  from assms obtain cy cy' where "(cy :: 'b) ≠ cy'" by blast
  let ?cx = "undefined :: 'a"
  let ?L = "λx x'. ?cx = x ∧ x = x'"
  and ?R = "λy y'. (y = cy ∨ y = cy') ∧ (y' = cy ∨ y' = cy') ∧ (y ≠ cy' ∨ y' ≠ cy')"
  and ?l = "λ(a :: 'a). cy"
  and ?r = "λ(b :: 'b). ?cx"
  interpret g : galois ?L ?R ?l ?r .
  interpret flip_g : galois ?R ?L ?r ?l .
  have "(?L ≡⇩G ?R) ?l ?r" using ‹cy ≠ cy'› by blast
  moreover have "partial_equivalence_rel ?L" by blast
  moreover have
    "¬(transitive_on (in_field ?R) ?R)" and "¬(reflexive_on (in_field ?R) ?R)"
    using ‹cy ≠ cy'› by auto
  ultimately show "?thesis" by blast
qed


subsection ‹Equivalence of Order Equivalences and Galois Equivalences›

text ‹In general categories, every adjoint equivalence is an equivalence but not vice versa.
In the category of preorders, however, they are morally the same: the
adjoint zigzag equations are satisfied up to unique isomorphism rather than equality.
In the category of partial orders, the concepts coincide.›

lemma half_galois_prop_left_left_right_if_transitive_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)" "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  using assms
  by (intro half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel)
  (auto elim!: order_equivalenceE
    intro: deflationary_on_if_le_pred_if_deflationary_on in_field_if_in_codom
    intro!: le_predI)

lemma half_galois_prop_right_left_right_if_transitive_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)" "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  using assms
  by (intro half_galois_prop_right_left_right_if_transitive_if_inflationary_on_if_mono_wrt_rel)
  (auto elim!: order_equivalenceE
    intro: inflationary_on_if_le_pred_if_inflationary_on in_field_if_in_dom
    intro!: le_predI
    simp only: flip_counit_eq_unit)

lemma galois_prop_left_right_if_transitive_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)" "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms
    half_galois_prop_left_left_right_if_transitive_if_order_equivalence
    half_galois_prop_right_left_right_if_transitive_if_order_equivalence
  by blast

corollary galois_connection_left_right_if_transitive_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)" "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms galois_prop_left_right_if_transitive_if_order_equivalence
  by (intro galois_connectionI) auto

interpretation flip : galois R L r l
  rewrites "flip.unit ≡ ε"
  by (simp only: flip_unit_eq_counit)

corollary galois_equivalence_left_right_if_transitive_if_order_equivalence:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)" "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms galois_connection_left_right_if_transitive_if_order_equivalence
    flip.galois_prop_left_right_if_transitive_if_order_equivalence
  by (intro galois_equivalenceI)
  (auto simp only: order_equivalence_right_left_iff_order_equivalence_left_right)

lemma order_equivalence_if_reflexive_on_in_field_if_galois_equivalence:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  and "reflexive_on (in_field (≤⇘L⇙)) (≤⇘L⇙)" "reflexive_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  using assms rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
    flip.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
  by (intro order_equivalenceI)
  (auto simp only: galois_equivalence_right_left_iff_galois_equivalence_left_right)

corollary galois_equivalence_eq_order_equivalence_if_preorder_on_in_field:
  assumes "preorder_on (in_field (≤⇘L⇙)) (≤⇘L⇙)" "preorder_on (in_field (≤⇘R⇙)) (≤⇘R⇙)"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) = ((≤⇘L⇙) ≡⇩o (≤⇘R⇙))"
  using assms
    galois.order_equivalence_if_reflexive_on_in_field_if_galois_equivalence
    galois.galois_equivalence_left_right_if_transitive_if_order_equivalence
  by (elim preorder_on_in_fieldE, intro ext) blast

end


end