Theory Transport_Compositions_Agree_Galois_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Equivalence›
theory Transport_Compositions_Agree_Galois_Equivalence
  imports
    Transport_Compositions_Agree_Galois_Connection
begin

context transport_comp_agree
begin

interpretation flip : transport_comp_agree R2 L2 r2 l2 R1 L1 r1 l1 .

lemma galois_equivalenceI:
  assumes galois: "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1" "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and mono_L1_L2_l1: "⋀x y. x ≤⇘L1⇙ y ⟹ l1 x ≤⇘R1⇙ l1 y ⟹ l1 x ≤⇘L2⇙ l1 y"
  and mono_R2_R1_r2: "⋀x y. x ≤⇘R2⇙ y ⟹ r2 x ≤⇘L2⇙ r2 y ⟹ r2 x ≤⇘R1⇙ r2 y"
  and "(in_dom (≤⇘L1⇙) ⇛ in_codom (≤⇘R2⇙) ⇛ (⟷))
    (rel_bimap l1 r2 (≤⇘R1⇙)) (rel_bimap l1 r2 (≤⇘L2⇙))"
  and mono_iff2: "(in_dom (≤⇘R2⇙) ⇛ in_codom (≤⇘L1⇙) ⇛ (⟷))
    (rel_bimap r2 l1 (≤⇘R1⇙)) (rel_bimap r2 l1 (≤⇘L2⇙))"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
proof -
  from galois mono_L1_L2_l1 have "(in_codom (≤⇘L1⇙) ⇒ in_codom (≤⇘L2⇙)) l1"
    by (intro mono_wrt_predI) blast
  moreover from galois mono_R2_R1_r2 have "(in_dom (≤⇘R2⇙) ⇒ in_dom (≤⇘R1⇙)) r2"
    by (intro mono_wrt_predI) blast
  moreover from mono_iff2 have "(in_dom (≤⇘R2⇙) ⇛ in_codom (≤⇘L1⇙) ⇛ (⟷))
    (rel_bimap r2 l1 (≤⇘L2⇙)) (rel_bimap r2 l1 (≤⇘R1⇙))" by blast
  ultimately show ?thesis using assms
    by (intro galois_equivalenceI galois_connectionI flip.galois_propI) auto
qed

lemma galois_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1" "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and "((≤⇘L1⇙) ⇒ (≤⇘L2⇙)) l1" "((≤⇘R2⇙) ⇒ (≤⇘R1⇙)) r2"
  and "(in_dom (≤⇘L1⇙) ⇛ in_codom (≤⇘R2⇙) ⇛ (⟷))
    (rel_bimap l1 r2 (≤⇘R1⇙)) (rel_bimap l1 r2 (≤⇘L2⇙))"
  and "(in_dom (≤⇘R2⇙) ⇛ in_codom (≤⇘L1⇙) ⇛ (⟷))
    (rel_bimap r2 l1 (≤⇘R1⇙)) (rel_bimap r2 l1 (≤⇘L2⇙))"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms by (intro galois_equivalenceI) auto

end

context transport_comp_same
begin

lemma galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1" "((≤⇘R1⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms by (rule galois_equivalenceI) auto

end


end