Theory Transport_Compositions_Generic_Galois_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Equivalence›
theory Transport_Compositions_Generic_Galois_Equivalence
  imports
    Transport_Compositions_Generic_Galois_Connection
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" and "flip.t1.unit ≡ ε⇩2"
  by (simp_all only: order_functors.flip_unit_eq_counit)

lemma galois_equivalenceI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "rel_equivalence_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⊴ (≤⇘L2⇙)) r2 l2"
  and "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "transitive (≤⇘L2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms by (intro galois_equivalenceI galois_connection_left_rightI
    flip.galois_prop_left_rightI)
  (auto intro!: preorder_on_in_field_if_transitive_if_rel_equivalence_on
    intro: rel_equivalence_on_if_le_pred_if_rel_equivalence_on
      inflationary_on_if_le_pred_if_inflationary_on
      in_field_if_in_dom in_field_if_in_codom)

lemma galois_equivalenceI':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘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⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘L2⇙) ⊴⇩h (≤⇘R2⇙)) l2 r2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and "rel_equivalence_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "inflationary_on (in_dom (≤⇘R2⇙)) (≤⇘R2⇙) ε⇩2"
  and "transitive (≤⇘L2⇙)"
  and "middle_compatible_dom"
  shows "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms by (intro galois.galois_equivalenceI galois_connection_left_rightI'
    flip.galois_prop_left_rightI')
  (auto elim!: rel_equivalence_onE
    intro!: preorder_on_in_field_if_transitive_if_rel_equivalence_on
    intro: inflationary_on_if_le_pred_if_inflationary_on
      in_field_if_in_dom)

corollary galois_equivalence_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⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms by (intro galois_equivalenceI)
  (auto intro!: t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
      flip.t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
    intro: reflexive_on_if_le_pred_if_reflexive_on
      in_field_if_in_dom in_field_if_in_codom)

corollary galois_equivalence_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⇙) ≡⇩G (≤⇘R⇙)) l r"
  using assms by (intro galois_equivalenceI')
  (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
      rel_comp_comp_le_assms_if_in_codom_rel_comp_comp_leI
      preorder_on_in_field_if_transitive_if_rel_equivalence_on
    intro: deflationary_on_if_le_pred_if_deflationary_on
      inflationary_on_if_le_pred_if_inflationary_on
      in_field_if_in_dom in_field_if_in_codom)

end


end