Theory Galois_Relator

✐‹creator "Kevin Kappelmann"›
subsection ‹Relator For Galois Connections›
theory Galois_Relator
  imports
    Galois_Relator_Base
    Galois_Property
begin

context galois_prop
begin

interpretation flip_inv : galois_rel "(≥⇘R⇙)" "(≥⇘L⇙)" l .

lemma left_Galois_if_Galois_right_if_half_galois_prop_right:
  assumes "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "x ⪅⇘R⇙ y"
  shows "x ⇘L⇙⪅ y"
  using assms by (intro left_GaloisI) auto

lemma Galois_right_if_left_Galois_if_half_galois_prop_left:
  assumes "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "x ⇘L⇙⪅ y"
  shows "x ⪅⇘R⇙ y"
  using assms by fast

corollary Galois_right_iff_left_Galois_if_galois_prop [iff]:
  assumes "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  shows "x ⪅⇘R⇙ y ⟷ x ⇘L⇙⪅ y"
  using assms
    left_Galois_if_Galois_right_if_half_galois_prop_right
    Galois_right_if_left_Galois_if_half_galois_prop_left
  by blast

lemma rel_inv_Galois_eq_flip_Galois_rel_inv_if_galois_prop [simp]:
  assumes "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  shows "(⪆⇘L⇙) = (⇘R⇙⪆)"
  using assms by blast

corollary flip_Galois_rel_inv_iff_Galois_if_galois_prop [iff]:
  assumes "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  shows "y ⇘R⇙⪆ x ⟷ x ⇘L⇙⪅ y"
  using assms by blast

corollary inv_flip_Galois_rel_inv_eq_Galois_if_galois_prop [simp]:
  assumes "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  shows "(⪅⇘R⇙) = (⇘L⇙⪅)" ―‹Note that @{term "(⪅⇘R⇙) = (galois_rel.Galois (≥⇘R⇙) (≥⇘L⇙) l)¯"}›
  using assms by (subst rel_inv_eq_iff_eq[symmetric]) simp

end

context galois
begin

interpretation flip_inv : galois "(≥⇘R⇙)" "(≥⇘L⇙)" r l .

context
begin

interpretation flip : galois R L r l .

lemma left_Galois_left_if_left_relI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "x ≤⇘L⇙ x'"
  shows "x ⇘L⇙⪅ l x'"
  using assms
  by (intro left_Galois_if_Galois_right_if_half_galois_prop_right) (auto 5 0)

corollary left_Galois_left_if_reflexive_on_if_half_galois_prop_rightI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  and "P x"
  shows "x ⇘L⇙⪅ l x"
  using assms by (intro left_Galois_left_if_left_relI) auto

lemma left_Galois_left_if_in_codom_if_inflationary_onI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "inflationary_on P (≤⇘L⇙) η"
  and "in_codom (≤⇘L⇙) x"
  and "P x"
  shows "x ⇘L⇙⪅ l x"
  using assms by (intro left_GaloisI) (auto elim!: in_codomE)

lemma left_Galois_left_if_in_codom_if_inflationary_on_in_codomI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "inflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
  and "in_codom (≤⇘L⇙) x"
  shows "x ⇘L⇙⪅ l x"
  using assms by (auto intro!: left_Galois_left_if_in_codom_if_inflationary_onI)

lemma left_Galois_left_if_left_rel_if_inflationary_on_in_fieldI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "inflationary_on (in_field (≤⇘L⇙)) (≤⇘L⇙) η"
  and "x ≤⇘L⇙ x"
  shows "x ⇘L⇙⪅ l x"
  using assms by (auto intro!: left_Galois_left_if_in_codom_if_inflationary_onI)

lemma right_left_Galois_if_right_relI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "y ≤⇘R⇙ y'"
  shows "r y ⇘L⇙⪅ y'"
  using assms by (intro left_GaloisI) auto

corollary right_left_Galois_if_reflexive_onI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "reflexive_on P (≤⇘R⇙)"
  and "P y"
  shows "r y ⇘L⇙⪅ y"
  using assms by (intro right_left_Galois_if_right_relI) auto

lemma left_Galois_if_right_rel_if_left_GaloisI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "transitive (≤⇘L⇙)"
  and "x ⇘L⇙⪅ y"
  and "y ≤⇘R⇙ z"
  shows "x ⇘L⇙⪅ z"
  using assms by (intro left_GaloisI) (auto 5 0)

lemma left_Galois_if_left_Galois_if_left_relI:
  assumes "transitive (≤⇘L⇙)"
  and "x ≤⇘L⇙ y"
  and "y ⇘L⇙⪅ z"
  shows "x ⇘L⇙⪅ z"
  using assms by (intro left_GaloisI) auto

lemma left_rel_if_right_Galois_if_left_GaloisI:
  assumes "((≤⇘R⇙) ⇩h⊴ (≤⇘L⇙)) r l"
  and "transitive (≤⇘L⇙)"
  and "x ⇘L⇙⪅ y"
  and "y ⇘R⇙⪅ z"
  shows "x ≤⇘L⇙ z"
  using assms by auto

lemma Dep_Fun_Rel_left_Galois_right_Galois_if_mono_wrt_rel [intro]:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  shows "((⇘L⇙⪅) ⇛ (⇘R⇙⪅)) l r"
  using assms by blast

lemma left_ge_Galois_eq_left_Galois_if_in_codom_eq_in_dom_if_symmetric:
  assumes "symmetric (≤⇘L⇙)"
  and "in_codom (≤⇘R⇙) = in_dom (≤⇘R⇙)"
  shows "(⇘L⇙⪆) = (⇘L⇙⪅)" ―‹Note that @{term "(⇘L⇙⪆) = galois_rel.Galois (≥⇘L⇙) (≥⇘R⇙) r"}›
  using assms by (intro ext iffI)
  (auto elim!: galois_rel.left_GaloisE intro!: galois_rel.left_GaloisI)

end

interpretation flip : galois R L r l .

lemma ge_Galois_right_eq_left_Galois_if_symmetric_if_in_codom_eq_in_dom_if_galois_prop:
  assumes "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  and "in_codom (≤⇘L⇙) = in_dom (≤⇘L⇙)"
  and "symmetric (≤⇘R⇙)"
  shows "(⪆⇘R⇙) = (⇘L⇙⪅)" ―‹Note that @{term "(⪆⇘R⇙) = (galois_rel.Galois (≤⇘R⇙) (≤⇘L⇙) l)¯"}›
  using assms
  by (simp only: inv_flip_Galois_rel_inv_eq_Galois_if_galois_prop
    flip: flip.left_ge_Galois_eq_left_Galois_if_in_codom_eq_in_dom_if_symmetric)

interpretation gp : galois_prop "(⇘L⇙⪅)" "(⇘R⇙⪅)" l l .

lemma half_galois_prop_left_left_Galois_right_Galois_if_half_galois_prop_leftI [intro]:
  assumes "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "((⇘L⇙⪅) ⇩h⊴ (⇘R⇙⪅)) l l"
  using assms by fast

lemma half_galois_prop_right_left_Galois_right_Galois_if_half_galois_prop_rightI [intro]:
  assumes "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "((⇘L⇙⪅) ⊴⇩h (⇘R⇙⪅)) l l"
  using assms by fast

corollary galois_prop_left_Galois_right_Galois_if_galois_prop [intro]:
  assumes "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  shows "((⇘L⇙⪅) ⊴ (⇘R⇙⪅)) l l"
  using assms by blast

end


end