Theory Galois_Connections

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

context galois
begin

definition "galois_connection ≡ ((≤⇘L⇙) ⇒ (≤⇘R⇙)) l ∧ ((≤⇘R⇙) ⇒ (≤⇘L⇙)) r ∧ ((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"

notation galois.galois_connection (infix ‹⊣› 50)

lemma galois_connectionI [intro]:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l" and "((≤⇘R⇙) ⇒ (≤⇘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⇙) ⇒ (≤⇘R⇙)) l" "((≤⇘R⇙) ⇒ (≤⇘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 galois_connection_rel_inv_eq_rel_inv_galois_connection [simp]:
  "((≥⇘L⇙) ⊣ (≥⇘R⇙)) = ((≤⇘R⇙) ⊣ (≤⇘L⇙))¯"
  by (intro ext iffI) (auto 0 5)

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