Theory Transport_Functions_Galois_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Equivalence›
theory Transport_Functions_Galois_Equivalence
  imports
    Transport_Functions_Galois_Connection
    Transport_Functions_Order_Base
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

subparagraph ‹Lemmas for Monotone Function Relator›

lemma flip_half_galois_prop_left2_if_half_galois_prop_left2_if_left_GaloisI:
  assumes "((≤L1) m (≤R1)) l1"
  and "((≤L1) h (≤R1)) l1 r1"
  and half_galois_prop_left2: "x x'. x L1x' 
    ((≤⇘R2 (l1 x) x') h (≤⇘L2 x (r1 x'))) (r2⇘x x') (l2⇘x' x) "
  and "(≤⇘L2 (η1 x) x) = (≤⇘L2 x x)"
  and "(≤⇘L2 x (η1 x)) = (≤⇘L2 x x)"
  and "xL1 x"
  shows "((≤⇘R2 (l1 x) (l1 x)) h (≤⇘L2 (η1 x) x)) (r2⇘x (l1 x)) (l2⇘(l1 x) x)"
proof -
  from assms have "x L1l1 x" by (intro t1.left_Galois_left_if_left_relI) auto
  with half_galois_prop_left2
    have "((≤⇘R2 (l1 x) (l1 x)) h (≤⇘L2 x (η1 x))) (r2⇘x (l1 x)) (l2⇘(l1 x) x)" by auto
  with assms show ?thesis by simp
qed

lemma flip_half_galois_prop_right2_if_half_galois_prop_right2_if_GaloisI:
  assumes "((≤R1) m (≤L1)) r1"
  and half_galois_prop_right2: "x x'. x L1x' 
    ((≤⇘R2 (l1 x) x') h (≤⇘L2 x (r1 x'))) (r2⇘x x') (l2⇘x' x)"
  and "(≤⇘R2 (ε1 x') x') = (≤⇘R2 x' x')"
  and "(≤⇘R2 x' (ε1 x')) = (≤⇘R2 x' x')"
  and "x'R1 x'"
  shows "((≤⇘R2 x' (ε1 x')) h (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') x') (l2⇘x' (r1 x'))"
proof -
  from assms have "r1 x' L1x'" by (intro t1.right_left_Galois_if_right_relI) auto
  with half_galois_prop_right2
    have "((≤⇘R2 (ε1 x') x') h (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') x') (l2⇘x' (r1 x'))" by auto
  with assms show ?thesis by simp
qed

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

lemma galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI:
  assumes galois_equiv1: "((≤L1) G (≤R1)) l1 r1"
  and preorder_L1: "preorder_on (in_field (≤L1)) (≤L1)"
  and mono_L2: "((x1 x2  (≥L1)) m (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  shows "((x1 x2  (≤L1) | η1 x2L1 x1) m (x3 x4  (≤L1) | x2L1 x3)  (≤)) L2" (is ?goal1)
  and "((x1 x2  (≤L1)) m (x3 x4  (≤L1) | (x2L1 x3  x4L1 η1 x3))  (≥)) L2" (is ?goal2)
proof -
  show ?goal1
  proof (intro dep_mono_wrt_relI rel_if_if_impI Dep_Fun_Rel_relI)
    fix x1 x2 x3 x4 assume "x1L1 x2"
    moreover with galois_equiv1 preorder_L1 have "x2L1 η1 x2"
      by (blast intro: t1.rel_unit_if_reflexive_on_if_galois_connection)
    moreover assume "η1 x2L1 x1"
    ultimately have "x2 ≡⇘L1x1" using preorder_L1 by blast
    moreover assume "x3L1 x4" "x2L1 x3"
    ultimately show "(≤⇘L2 x1 x3)  (≤⇘L2 x2 x4)" using preorder_L1 mono_L2
      by (intro le_relI) (blast dest!: rel_ifD elim!: dep_mono_wrt_relE)
  qed
  show ?goal2
  proof (intro dep_mono_wrt_relI rel_if_if_impI Dep_Fun_Rel_relI)
    fix x1 x2 x3 x4 presume "x3L1 x4" "x4L1 η1 x3"
    moreover with galois_equiv1 preorder_L1 have "η1 x3L1 x3"
      by (blast intro: flip.t1.counit_rel_if_reflexive_on_if_galois_connection)
    ultimately have "x3 ≡⇘L1x4" using preorder_L1 by blast
    moreover presume "x1L1 x2" "x2L1 x3"
    ultimately show "(≤⇘L2 x2 x4)  (≤⇘L2 x1 x3)" using preorder_L1 mono_L2 by fast
  qed auto
qed

lemma galois_equivalence_if_mono_if_galois_equivalence_Dep_Fun_Rel_pred_assm_leftI:
  assumes galois_equiv1: "((≤L1) G (≤R1)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤L1)) (≤L1)"
  and refl_R1: "reflexive_on (in_field (≤R1)) (≤R1)"
  and mono_L2: "((x1 x2  (≥L1)) m (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and mono_R2: "((x1' x2'  (≥R1)) m (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and mono_l2: "((x1' x2'  (≤R1)) m (x1 x2  (≤L1) | x2 L1x1') 
    in_field (≤⇘L2 x1 (r1 x2'))  (≤⇘R2 (l1 x1) x2')) l2"
  and "xL1 x"
  shows "(in_codom (≤⇘L2 (η1 x) x)  (≤⇘R2 (l1 x) (l1 x))) (l2⇘(l1 x) (η1 x)) (l2⇘(l1 x) x)"
proof (intro Fun_Rel_predI)
  fix y assume "in_codom (≤⇘L2 (η1 x) x) y"
  moreover from xL1 x galois_equiv1 refl_L1 have "x ≡⇘L1η1 x"
    by (blast intro: bi_related_if_rel_equivalence_on
      t1.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)
  moreover with refl_L1 have "η1 xL1 η1 x" by blast
  ultimately have "in_codom (≤⇘L2 (η1 x) (η1 x)) y" using mono_L2 by blast
  moreover from xL1 x galois_equiv1
    have "l1 xR1 l1 x" "η1 xL1 x" "x L1l1 x"
    by (blast intro: t1.left_Galois_left_if_left_relI
      flip.t1.counit_rel_if_right_rel_if_galois_connection)+
  moreover note
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_l2 l1 xR1 l1 x] η1 xL1 x]
  ultimately have "l2⇘(l1 x) (η1 x)y ≤⇘R2 (ε1 (l1 x)) (l1 x)⇙ l2⇘(l1 x) xy" by auto
  moreover note l1 xR1 l1 x
  moreover with galois_equiv1 refl_R1 have "l1 x ≡⇘R1ε1 (l1 x)"
    by (blast intro: bi_related_if_rel_equivalence_on
      flip.t1.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)
  ultimately show "l2⇘(l1 x) (η1 x)y ≤⇘R2 (l1 x) (l1 x)⇙ l2⇘(l1 x) xy"
    using mono_R2 by blast
qed

lemma galois_equivalence_if_mono_if_galois_equivalence_Dep_Fun_Rel_pred_assm_right:
  assumes galois_equiv1: "((≤L1) G (≤R1)) l1 r1"
  and refl_R1: "reflexive_on (in_field (≤R1)) (≤R1)"
  and mono_L2: "((x1 x2  (≥L1)) m (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and mono_R2: "((x1' x2'  (≥R1)) m (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and mono_r2: "((x1 x2  (≤L1)) m (x1' x2'  (≤R1) | x2 L1x1') 
    in_field (≤⇘R2 (l1 x1) x2')  (≤⇘L2 x1 (r1 x2'))) r2"
  and "x'R1 x'"
  shows "(in_dom (≤⇘R2 x' (ε1 x'))  (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') x') (r2⇘(r1 x') (ε1 x'))"
proof (intro Fun_Rel_predI)
  fix y assume "in_dom (≤⇘R2 x' (ε1 x')) y"
  moreover from x'R1 x' galois_equiv1 refl_R1 have "x' ≡⇘R1ε1 x'"
    by (blast intro: bi_related_if_rel_equivalence_on
      flip.t1.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)
  moreover with refl_R1 have "ε1 x'R1 ε1 x'" by blast
  ultimately have "in_dom (≤⇘R2 (ε1 x') (ε1 x')) y" using mono_R2 by blast
  moreover from x'R1 x' galois_equiv1
    have "r1 x'L1 r1 x'" "x'R1 ε1 x'" "r1 x' L1x'"
    by (blast intro: t1.right_left_Galois_if_right_relI
      flip.t1.rel_unit_if_left_rel_if_galois_connection)+
  moreover note
    Dep_Fun_Rel_relD[OF dep_mono_wrt_relD[OF mono_r2 r1 x'L1 r1 x'] x'R1 ε1 x']
  ultimately have "r2⇘(r1 x') x'y ≤⇘L2 (r1 x') (η1 (r1 x'))⇙ r2⇘(r1 x') (ε1 x')y" by auto
  moreover note r1 x'L1 r1 x'
  moreover with galois_equiv1 refl_R1 have "r1 x' ≡⇘L1η1 (r1 x')"
    by (blast intro: bi_related_if_rel_equivalence_on
      t1.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)
  ultimately show "r2⇘(r1 x') x'y ≤⇘L2 (r1 x') (r1 x')⇙ r2⇘(r1 x') (ε1 x')y"
    using mono_L2 by blast
qed

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

context
begin

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

lemma galois_equivalence_if_galois_equivalenceI:
  assumes galois_equiv1: "((≤L1) G (≤R1)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and galois_equiv2: "x x'. x L1x' 
    ((≤⇘L2 x (r1 x')) G (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1 x2. x1L1 x2  (≤⇘L2 x2 x2)  (≤⇘L2 x1 x2)"
  and "x. xL1 x  (≤⇘L2 (η1 x) x)  (≤⇘L2 x x)"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 x1)  (≤⇘L2 x1 x2)"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 (η1 x2))  (≤⇘L2 x1 x2)"
  and "x1' x2'. x1'R1 x2'  (≤⇘R2 x2' x2')  (≤⇘R2 x1' x2')"
  and "x1' x2'. x1'R1 x2'  (≤⇘R2 (ε1 x1') x2')  (≤⇘R2 x1' x2')"
  and "x1' x2'. x1'R1 x2'  (≤⇘R2 x1' x1')  (≤⇘R2 x1' x2')"
  and "x'. x'R1 x'  (≤⇘R2 x' (ε1 x'))  (≤⇘R2 x' x')"
  and "x1' x2'. x1'R1 x2' 
    (in_dom (≤⇘L2 (r1 x1') (r1 x2'))  (≤⇘R2 x1' x2')) (l2⇘x1' (r1 x1')) (l2⇘x2' (r1 x1'))"
  and "x1' x2'. x1'R1 x2' 
    (in_codom (≤⇘L2 (r1 x1') (r1 x2'))  (≤⇘R2 x1' x2')) (l2⇘x2' (r1 x1')) (l2⇘x2' (r1 x2'))"
  and "x. xL1 x 
    (in_dom (≤⇘L2 x (η1 x))  (≤⇘R2 (l1 x) (l1 x))) (l2⇘(l1 x) x) (l2⇘(l1 x) (η1 x))"
  and "x. xL1 x 
    (in_codom (≤⇘L2 (η1 x) x)  (≤⇘R2 (l1 x) (l1 x))) (l2⇘(l1 x) (η1 x)) (l2⇘(l1 x) x)"
  and "x1 x2. x1L1 x2 
    (in_codom (≤⇘R2 (l1 x1) (l1 x2))  (≤⇘L2 x1 x2)) (r2⇘x1 (l1 x2)) (r2⇘x2 (l1 x2))"
  and "x1 x2. x1L1 x2 
    (in_dom (≤⇘R2 (l1 x1) (l1 x2))  (≤⇘L2 x1 x2)) (r2⇘x1 (l1 x1)) (r2⇘x1 (l1 x2))"
  and "x'. x'R1 x' 
    (in_codom (≤⇘R2 (ε1 x') x')  (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') (ε1 x')) (r2⇘(r1 x') x')"
  and "x'. x'R1 x' 
    (in_dom (≤⇘R2 x' (ε1 x'))  (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') x') (r2⇘(r1 x') (ε1 x'))"
  and "x1 x2. x1L1 x2  transitive (≤⇘L2 x1 x2)"
  and "x1' x2'. x1'R1 x2'  transitive (≤⇘R2 x1' x2')"
  shows "((≤L) G (≤R)) l r"
proof -
  from galois_equiv2 have
    "((≤⇘L2 x (r1 x'))  (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
    "((≤⇘R2 (l1 x) x') h (≤⇘L2 x (r1 x'))) (r2⇘x x') (l2⇘x' x)"
    "((≤⇘R2 (l1 x) x') h (≤⇘L2 x (r1 x'))) (r2⇘x x') (l2⇘x' x)"
    if "x L1x'" for x x' using x L1x'
    by (blast elim: galois.galois_connectionE galois_prop.galois_propE)+
  moreover from galois_equiv1 galois_equiv2 have
    "x1' x2'. x1'R1 x2' 
      ((≤⇘L2 (r1 x1') (r1 x2')) m (≤⇘R2 (ε1 x1') x2')) (l2⇘x2' (r1 x1'))"
    by (intro tdfr.mono_wrt_rel_left2_if_mono_wrt_rel_left2_if_left_GaloisI) auto
  moreover from galois_equiv1 galois_equiv2 have
    "x1 x2. x1L1 x2  ((≤⇘R2 (l1 x1) (l1 x2)) m (≤⇘L2 x1 (η1 x2))) (r2⇘x1 (l1 x2))"
    by (intro tdfr.mono_wrt_rel_right2_if_mono_wrt_rel_right2_if_left_GaloisI)
    (auto elim!: t1.galois_equivalenceE)
  moreover from galois_equiv1 refl_L1 have
    "x. xL1 x  x ≡⇘L1η1 x"
    "x'. x'R1 x'  x' ≡⇘R1ε1 x'"
    by (blast intro!: bi_related_if_rel_equivalence_on
      t1.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
      flip.t1.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)+
  ultimately show ?thesis using assms
    by (intro galois_equivalenceI
      galois_connection_left_right_if_galois_connectionI flip.galois_prop_left_rightI
      tdfr.flip_half_galois_prop_left2_if_half_galois_prop_left2_if_left_GaloisI
      tdfr.flip_half_galois_prop_right2_if_half_galois_prop_right2_if_GaloisI
      tdfr.mono_wrt_rel_left_if_transitiveI tdfr.mono_wrt_rel_right_if_transitiveI
      flip.tdfr.left_rel_right_if_left_right_rel_le_right2_assmI
      flip.tdfr.left_right_rel_if_left_rel_right_ge_left2_assmI
      tdfr.left_rel2_unit_eqs_left_rel2I
      flip.tdfr.left_rel2_unit_eqs_left_rel2I)
    (auto elim!: t1.galois_equivalenceE
      intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom
      in_field_if_in_codom)
qed

corollary galois_equivalence_if_galois_equivalenceI':
  assumes "((≤L1) G (≤R1)) l1 r1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x')) G (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "x1 x2. x1L1 x2  (≤⇘L2 x2 x2)  (≤⇘L2 x1 x2)"
  and "x. xL1 x  (≤⇘L2 (η1 x) x)  (≤⇘L2 x x)"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 x1)  (≤⇘L2 x1 x2)"
  and "x1 x2. x1L1 x2  (≤⇘L2 x1 (η1 x2))  (≤⇘L2 x1 x2)"
  and "x1' x2'. x1'R1 x2'  (≤⇘R2 x2' x2')  (≤⇘R2 x1' x2')"
  and "x1' x2'. x1'R1 x2'  (≤⇘R2 (ε1 x1') x2')  (≤⇘R2 x1' x2')"
  and "x1' x2'. x1'R1 x2'  (≤⇘R2 x1' x1')  (≤⇘R2 x1' x2')"
  and "x'. x'R1 x'  (≤⇘R2 x' (ε1 x'))  (≤⇘R2 x' x')"
  and "((x1' x2'  (≤R1)) m (x1 x2  (≤L1) | x2 L1x1') 
    in_field (≤⇘L2 x1 (r1 x2'))  (≤⇘R2 (l1 x1) x2')) l2"
  and "x. xL1 x 
    (in_codom (≤⇘L2 (η1 x) x)  (≤⇘R2 (l1 x) (l1 x))) (l2⇘(l1 x) (η1 x)) (l2⇘(l1 x) x)"
  and "((x1 x2  (≤L1)) m (x1' x2'  (≤R1) | x2 L1x1') 
    in_field (≤⇘R2 (l1 x1) x2')  (≤⇘L2 x1 (r1 x2'))) r2"
  and "x'. x'R1 x' 
    (in_dom (≤⇘R2 x' (ε1 x'))  (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') x') (r2⇘(r1 x') (ε1 x'))"
  and "x1 x2. x1L1 x2  transitive (≤⇘L2 x1 x2)"
  and "x1' x2'. x1'R1 x2'  transitive (≤⇘R2 x1' x2')"
  shows "((≤L) G (≤R)) l r"
  using assms by (intro galois_equivalence_if_galois_equivalenceI
    tdfr.galois_connection_left_right_if_galois_connection_mono_assms_leftI
    tdfr.galois_connection_left_right_if_galois_connection_mono_assms_rightI
    tdfr.galois_connection_left_right_if_galois_connection_mono_2_assms_leftI
    tdfr.galois_connection_left_right_if_galois_connection_mono_2_assms_rightI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom
    in_field_if_in_codom)

corollary galois_equivalence_if_mono_if_galois_equivalenceI:
  assumes "((≤L1) G (≤R1)) l1 r1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x')) G (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "((x1 x2  (≤L1) | η1 x2L1 x1) m (x3 x4  (≤L1) | x2L1 x3)  (≤)) L2"
  and "((x1 x2  (≤L1)) m (x3 x4  (≤L1) | (x2L1 x3  x4L1 η1 x3))  (≥)) L2"
  and "((x1' x2'  (≤R1) | ε1 x2'R1 x1') m (x3' x4'  (≤R1) | x2'R1 x3')  (≤)) R2"
  and "((x1' x2'  (≤R1)) m (x3' x4'  (≤R1) | (x2'R1 x3'  x4'R1 ε1 x3'))  (≥)) R2"
  and "((x1' x2'  (≤R1)) m (x1 x2  (≤L1) | x2 L1x1') 
    in_field (≤⇘L2 x1 (r1 x2'))  (≤⇘R2 (l1 x1) x2')) l2"
  and "x. xL1 x 
    (in_codom (≤⇘L2 (η1 x) x)  (≤⇘R2 (l1 x) (l1 x))) (l2⇘(l1 x) (η1 x)) (l2⇘(l1 x) x)"
  and "((x1 x2  (≤L1)) m (x1' x2'  (≤R1) | x2 L1x1') 
    in_field (≤⇘R2 (l1 x1) x2')  (≤⇘L2 x1 (r1 x2'))) r2"
  and "x'. x'R1 x' 
    (in_dom (≤⇘R2 x' (ε1 x'))  (≤⇘L2 (r1 x') (r1 x'))) (r2⇘(r1 x') x') (r2⇘(r1 x') (ε1 x'))"
  and "x1 x2. x1L1 x2  transitive (≤⇘L2 x1 x2)"
  and "x1' x2'. x1'R1 x2'  transitive (≤⇘R2 x1' x2')"
  shows "((≤L) G (≤R)) l r"
  using assms by (intro galois_equivalence_if_galois_equivalenceI'
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    flip.tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_leftI
    tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI
    flip.tdfr.left_rel_right_iff_left_right_rel_if_galois_prop_le_assms_rightI)
  auto

end

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

lemma galois_equivalence_if_mono_if_preorder_equivalenceI:
  assumes "((≤L1) ≡pre (≤R1)) l1 r1"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x')) G (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "((x1 x2  (≥L1)) m (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and "((x1' x2'  (≥R1)) m (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and "((x1' x2'  (≤R1)) m (x1 x2  (≤L1) | x2 L1x1') 
    in_field (≤⇘L2 x1 (r1 x2'))  (≤⇘R2 (l1 x1) x2')) l2"
  and "((x1 x2  (≤L1)) m (x1' x2'  (≤R1) | x2 L1x1') 
    in_field (≤⇘R2 (l1 x1) x2')  (≤⇘L2 x1 (r1 x2'))) r2"
  and "x1 x2. x1L1 x2  transitive (≤⇘L2 x1 x2)"
  and "x1' x2'. x1'R1 x2'  transitive (≤⇘R2 x1' x2')"
  shows "((≤L) G (≤R)) l r"
  using assms by (intro galois_equivalence_if_mono_if_galois_equivalenceI
    tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    flip.tdfr.galois_equivalence_if_mono_if_galois_equivalence_mono_assms_leftI
    tdfr.galois_equivalence_if_mono_if_galois_equivalence_Dep_Fun_Rel_pred_assm_leftI
    tdfr.galois_equivalence_if_mono_if_galois_equivalence_Dep_Fun_Rel_pred_assm_right)
  auto

theorem galois_equivalence_if_mono_if_preorder_equivalenceI':
  assumes "((≤L1) ≡pre (≤R1)) l1 r1"
  and "x x'. x L1x'  ((≤⇘L2 x (r1 x'))pre (≤⇘R2 (l1 x) x')) (l2⇘x' x) (r2⇘x x')"
  and "((x1 x2  (≥L1)) m (x3 x4  (≤L1) | x1L1 x3)  (≤)) L2"
  and "((x1' x2'  (≥R1)) m (x3' x4'  (≤R1) | x1'R1 x3')  (≤)) R2"
  and "((x1' x2'  (≤R1)) m (x1 x2  (≤L1) | x2 L1x1') 
    in_field (≤⇘L2 x1 (r1 x2'))  (≤⇘R2 (l1 x1) x2')) l2"
  and "((x1 x2  (≤L1)) m (x1' x2'  (≤R1) | x2 L1x1') 
    in_field (≤⇘R2 (l1 x1) x2')  (≤⇘L2 x1 (r1 x2'))) r2"
  shows "((≤L) G (≤R)) l r"
  using assms by (intro galois_equivalence_if_mono_if_preorder_equivalenceI
    tdfr.transitive_left2_if_preorder_equivalenceI
    tdfr.transitive_right2_if_preorder_equivalenceI)
  auto

end


paragraph ‹Monotone Function Relator›

context transport_Mono_Fun_Rel
begin

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

lemma galois_equivalenceI:
  assumes "((≤L1) G (≤R1)) l1 r1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "((≤L2) G (≤R2)) l2 r2"
  and "transitive (≤L2)"
  and "transitive (≤R2)"
  shows "((≤L) G (≤R)) l r"
  using assms by (intro tpdfr.galois_equivalenceI
    galois_connection_left_rightI flip.galois_prop_left_rightI)
  (auto intro: reflexive_on_if_le_pred_if_reflexive_on
    in_field_if_in_dom in_field_if_in_codom)

end


end