Theory Transport_Compositions_Agree_Galois_Connection

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Connection›
theory Transport_Compositions_Agree_Galois_Connection
  imports
    Transport_Compositions_Agree_Monotone
    Transport_Compositions_Agree_Galois_Property
begin

context transport_comp_agree
begin

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

lemma galois_connectionI:
  assumes galois: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1" "((≤⇘L2⇙) ⊣ (≤⇘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⇙))"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
proof -
  from galois mono_L1_L2_l1 have "(in_dom (≤⇘L1⇙) ⇒ in_dom (≤⇘L2⇙)) l1"
    by (intro mono_wrt_predI) (blast elim!: in_domE g1.galois_connectionE)
  moreover from galois mono_R2_R1_r2
    have "(in_codom (≤⇘R2⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
    by (intro mono_wrt_predI) (blast elim!: in_codomE g2.galois_connectionE)
  ultimately show ?thesis using assms
    by (intro galois_connectionI galois_propI mono_wrt_rel_leftI
      flip.mono_wrt_rel_leftI)
    auto
qed

lemma galois_connectionI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1" "((≤⇘L2⇙) ⊣ (≤⇘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⇙))"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connectionI) auto

end

context transport_comp_same
begin

corollary galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1" "((≤⇘R1⇙) ⊣ (≤⇘R2⇙)) l2 r2"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (rule galois_connectionI) auto

end


end