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) m (≤L1)) r1"
  and "((≤L1)  (≤R1)) l1 r1"
  and "rel_equivalence_on (in_field (≤R1)) (≤R1) ε1"
  and "transitive (≤R1)"
  and "((≤L2) m (≤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) 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 "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