Theory Galois_Property

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Property›
theory Galois_Property
  imports
    Half_Galois_Property
begin

context galois_prop
begin

definition "galois_prop ≡ ((≤L) h⊴ (≤R)) ⊓ ((≤L) ⊴h (≤R))"

notation galois_prop.galois_prop (infix ‹⊴› 50)

lemma galois_propI [intro]:
  assumes "((≤L) h⊴ (≤R)) l r"
  and "((≤L) ⊴h (≤R)) l r"
  shows "((≤L) ⊴ (≤R)) l r"
  unfolding galois_prop_def using assms by auto

lemma galois_propI':
  assumes "⋀x y. in_dom (≤L) x ⟹ in_codom (≤R) y ⟹ x ≤L r y ⟷ l x ≤R y"
  shows "((≤L) ⊴ (≤R)) l r"
  using assms by (blast elim: galois_rel.left_GaloisE)

lemma galois_propE [elim]:
  assumes "((≤L) ⊴ (≤R)) l r"
  obtains "((≤L) h⊴ (≤R)) l r" "((≤L) ⊴h (≤R)) l r"
  using assms unfolding galois_prop_def by auto

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

lemma galois_prop_eq_half_galois_prop_left_rel_inf_half_galois_prop_right:
  "((≤L) ⊴ (≤R)) = ((≤L) h⊴ (≤R)) ⊓ ((≤L) ⊴h (≤R))"
  by (intro ext) auto

lemma galois_prop_left_rel_right_iff_left_right_rel:
  assumes "((≤L) ⊴ (≤R)) l r"
  and "in_dom (≤L) x" "in_codom (≤R) y"
  shows "x ≤L r y ⟷ l x ≤R y"
  using assms by blast

lemma rel_inv_galois_prop_eq_galois_prop_rel_inv [simp]:
  "((≤R) ⊴ (≤L))¯ = ((≥L) ⊴ (≥R))"
  by (intro ext) blast

corollary galois_prop_rel_inv_iff_galois_prop [iff]:
  "((≥L) ⊴ (≥R)) f g ⟷ ((≤R) ⊴ (≤L)) g f"
  by auto

end

context galois
begin

lemma galois_prop_left_right_if_transitive_if_deflationary_on_if_inflationary_on_if_mono_wrt_rel:
  assumes "((≤L) ⇒ (≤R)) l" and "((≤R) ⇒ (≤L)) r"
  and "inflationary_on (in_dom (≤L)) (≤L) η"
  and "deflationary_on (in_codom (≤R)) (≤R) ε"
  and "transitive (≤L)" "transitive (≤R)"
  shows "((≤L) ⊴ (≤R)) l r"
  using assms
  by (intro galois_propI
    half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
    half_galois_prop_right_left_right_if_transitive_if_inflationary_on_if_mono_wrt_rel)

end


end