Theory Transport_Compositions_Agree_Galois_Property

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Property›
theory Transport_Compositions_Agree_Galois_Property
  imports
    Transport_Compositions_Agree_Base
begin

context transport_comp_agree
begin

lemma galois_propI:
  assumes galois1: "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and galois2: "((≤⇘L2⇙) ⊴ (≤⇘R2⇙)) l2 r2"
  and mono_l1: "(in_dom (≤⇘L1⇙) ⇒ in_dom (≤⇘L2⇙)) l1"
  and mono_r2: "(in_codom (≤⇘R2⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  and agree: "(in_dom (≤⇘L1⇙) ⇛ in_codom (≤⇘R2⇙) ⇛ (⟷))
    (rel_bimap l1 r2 (≤⇘R1⇙)) (rel_bimap l1 r2 (≤⇘L2⇙))"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
proof (rule galois_prop.galois_propI')
  fix x y assume "in_dom (≤⇘L⇙) x" "in_codom (≤⇘R⇙) y"
  with mono_r2 mono_l1 have "in_dom (≤⇘L2⇙) (l1 x)" "in_codom (≤⇘R1⇙) (r2 y)" by auto
  have "x ≤⇘L⇙ r y ⟷ x ≤⇘L1⇙ r1 (r2 y)" by simp
  also from galois1 ‹in_dom (≤⇘L1⇙) x› ‹in_codom (≤⇘R1⇙) (r2 y)›
    have "... ⟷ l1 x ≤⇘R1⇙ r2 y"
    by (rule g1.galois_prop_left_rel_right_iff_left_right_rel)
  also from agree ‹in_dom (≤⇘L1⇙) x› ‹in_codom (≤⇘R2⇙) y›
    have "... ⟷ l1 x ≤⇘L2⇙ r2 y" by fastforce
  also from galois2 ‹in_dom (≤⇘L2⇙) (l1 x)› ‹in_codom (≤⇘R2⇙) y›
    have "... ⟷ l x ≤⇘R2⇙ y"
    unfolding l_def
    by (simp add: g2.galois_prop_left_rel_right_iff_left_right_rel)
  finally show "x ≤⇘L⇙ r y ⟷ l x ≤⇘R⇙ y" .
qed

end

context transport_comp_same
begin

corollary galois_propI:
  assumes "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R1⇙) ⊴ (≤⇘R2⇙)) l2 r2"
  and "(in_dom (≤⇘L1⇙) ⇒ in_dom (≤⇘R1⇙)) l1"
  and "(in_codom (≤⇘R2⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms by (rule galois_propI) auto

end


end