Theory Transport_Compositions_Generic_Galois_Connection

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Connection›
theory Transport_Compositions_Generic_Galois_Connection
  imports
    Transport_Compositions_Generic_Galois_Property
    Transport_Compositions_Generic_Monotone
begin

context transport_comp
begin

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.t2.unit = ε⇩1" and "flip.t1.counit ≡ η⇩2"
  by (simp_all only: t1.flip_unit_eq_counit t2.flip_counit_eq_unit)

lemma galois_connection_left_rightI:
  assumes "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "rel_equivalence_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and "inflationary_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connectionI galois_prop_left_rightI
    mono_wrt_rel_leftI flip.mono_wrt_rel_leftI)
  (auto intro: inflationary_on_if_le_pred_if_inflationary_on
    in_field_if_in_dom in_field_if_in_codom)

lemma galois_connection_left_rightI':
  assumes "((≤⇘R1⇙) ⇛⇩m (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R1⇙) ⊴⇩h (≤⇘L1⇙)) r1 l1"
  and "inflationary_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and "rel_equivalence_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  and "((≤⇘L2⇙) ⊴⇩h (≤⇘R2⇙)) l2 r2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and "inflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_dom"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connectionI galois_prop_left_rightI'
    mono_wrt_rel_leftI' flip.mono_wrt_rel_leftI')
  (auto elim!: preorder_on_in_fieldE
    intro!: reflexive_on_in_field_if_transitive_if_rel_equivalence_on
    intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)

corollary galois_connection_left_right_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connection_left_rightI)
  (auto elim!: galois.galois_connectionE
    intro!: flip.t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
      t2.inflationary_on_unit_if_reflexive_on_if_galois_equivalence
    intro: in_field_if_in_codom)

corollary galois_connection_left_right_if_order_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩o (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connection_left_rightI')
  (auto elim!: rel_equivalence_onE
    intro!: t1.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
      flip.t1.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
      t2.half_galois_prop_right_left_right_if_transitive_if_inflationary_on_if_mono_wrt_rel
      flip.t2.half_galois_prop_right_left_right_if_transitive_if_inflationary_on_if_mono_wrt_rel
      preorder_on_in_field_if_transitive_if_rel_equivalence_on
      rel_comp_comp_le_assms_if_in_codom_rel_comp_comp_leI
    intro: inflationary_on_if_le_pred_if_inflationary_on
      deflationary_on_if_le_pred_if_deflationary_on
      in_field_if_in_dom in_field_if_in_codom)

end


end