Theory Galois_Connections

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Connections›
theory Galois_Connections
  imports
    Galois_Property
begin

context galois
begin

definition "galois_connection ≡
  ((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l ∧ ((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r ∧ ((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"

notation galois.galois_connection (infix "⊣" 50)

lemma galois_connectionI [intro]:
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l" and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  unfolding galois_connection_def using assms by blast

lemma galois_connectionE [elim]:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  obtains "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l" "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r" "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms unfolding galois_connection_def by blast

context
begin

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

lemma rel_inv_galois_connection_eq_galois_connection_rel_inv [simp]:
  "((≤⇘R⇙) ⊣ (≤⇘L⇙))¯ = ((≥⇘L⇙) ⊣ (≥⇘R⇙))"
  by (intro ext) blast

corollary galois_connection_rel_inv_iff_galois_connection [iff]:
  "((≥⇘L⇙) ⊣ (≥⇘R⇙)) l r ⟷ ((≤⇘R⇙) ⊣ (≤⇘L⇙)) r l"
  by (simp flip: rel_inv_galois_connection_eq_galois_connection_rel_inv)

lemma rel_unit_if_left_rel_if_galois_connection:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "x ≤⇘L⇙ x'"
  shows "x ≤⇘L⇙ η x'"
  using assms
  by (blast intro: rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel)

end

lemma counit_rel_if_right_rel_if_galois_connection:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "y ≤⇘R⇙ y'"
  shows "ε y ≤⇘R⇙ y'"
  using assms
  by (blast intro: counit_rel_if_right_rel_if_half_galois_prop_left_if_mono_wrt_rel)

lemma rel_unit_if_reflexive_on_if_galois_connection:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  and "P x"
  shows "x ≤⇘L⇙ η x"
  using assms
  by (blast intro: rel_unit_if_reflexive_on_if_half_galois_prop_right_if_mono_wrt_rel)

lemma counit_rel_if_reflexive_on_if_galois_connection:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘R⇙)"
  and "P y"
  shows "ε y ≤⇘R⇙ y"
  using assms
  by (blast intro: counit_rel_if_reflexive_on_if_half_galois_prop_left_if_mono_wrt_rel)

lemma inflationary_on_unit_if_reflexive_on_if_galois_connection:
  fixes P :: "'a ⇒ bool"
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  shows "inflationary_on P (≤⇘L⇙) η"
  using assms
  by (blast intro: inflationary_on_unit_if_reflexive_on_if_half_galois_prop_rightI)

lemma deflationary_on_counit_if_reflexive_on_if_galois_connection:
  fixes P :: "'b ⇒ bool"
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘R⇙)"
  shows "deflationary_on P (≤⇘R⇙) ε"
  using assms
  by (blast intro: deflationary_on_counit_if_reflexive_on_if_half_galois_prop_leftI)

end


end