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⇙) ⇒ (≤⇘R1⇙)) l1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and half_galois_prop_left2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹
    ((≤⇘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 "x ≤⇘L1⇙ 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 ⇘L1⇙⪅ l1 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⇙) ⇒ (≤⇘L1⇙)) r1"
  and half_galois_prop_right2: "⋀x x'. x ⇘L1⇙⪅ x' ⟹
    ((≤⇘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' ⇘L1⇙⪅ x'" 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⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  shows "((x1 x2 ∷ (≤⇘L1⇙) | η⇩1 x2 ≤⇘L1⇙ x1) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x2 ≤⇘L1⇙ x3) ⇛ (≤)) L2" (is ?goal1)
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩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 "x1 ≤⇘L1⇙ x2"
    moreover with galois_equiv1 preorder_L1 have "x2 ≤⇘L1⇙ η⇩1 x2"
      by (blast intro: t1.rel_unit_if_reflexive_on_if_galois_connection)
    moreover assume "η⇩1 x2 ≤⇘L1⇙ x1"
    ultimately have "x2 ≡⇘L1⇙ x1" using preorder_L1 by blast
    moreover assume "x3 ≤⇘L1⇙ x4" "x2 ≤⇘L1⇙ 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 "x3 ≤⇘L1⇙ x4" "x4 ≤⇘L1⇙ η⇩1 x3"
    moreover with galois_equiv1 preorder_L1 have "η⇩1 x3 ≤⇘L1⇙ x3"
      by (blast intro: flip.t1.counit_rel_if_reflexive_on_if_galois_connection)
    ultimately have "x3 ≡⇘L1⇙ x4" using preorder_L1 by blast
    moreover presume "x1 ≤⇘L1⇙ x2" "x2 ≤⇘L1⇙ 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⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and mono_R2: "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and mono_l2: "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "x ≤⇘L1⇙ 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 ‹x ≤⇘L1⇙ 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 x ≤⇘L1⇙ η⇩1 x" by blast
  ultimately have "in_codom (≤⇘L2 (η⇩1 x) (η⇩1 x)⇙) y" using mono_L2 by blast
  moreover from ‹x ≤⇘L1⇙ x› galois_equiv1
    have "l1 x ≤⇘R1⇙ l1 x" "η⇩1 x ≤⇘L1⇙ x" "x ⇘L1⇙⪅ l1 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 x ≤⇘R1⇙ l1 x›] ‹η⇩1 x ≤⇘L1⇙ x›]
  ultimately have "l2⇘(l1 x) (η⇩1 x)⇙ y ≤⇘R2 (ε⇩1 (l1 x)) (l1 x)⇙ l2⇘(l1 x) x⇙ y" by auto
  moreover note ‹l1 x ≤⇘R1⇙ 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) x⇙ y"
    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⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and mono_R2: "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    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' ⇘L1⇙⪅ x'"
    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 ⇘L1⇙⪅ x' ⟹
    ((≤⇘L2 x (r1 x')⇙) ≡⇩G (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 (η⇩1 x) x⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ 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. x ≤⇘L1⇙ x ⟹
    (in_dom (≤⇘L2 x (η⇩1 x)⇙) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹
    (in_codom (≤⇘L2 (η⇩1 x) x⇙) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) (η⇩1 x)⇙) (l2⇘(l1 x) x⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹
    (in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ 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. x1 ≤⇘L1⇙ 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 ⇘L1⇙⪅ x'" for x x' using ‹x ⇘L1⇙⪅ x'›
    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')⇙) ⇒ (≤⇘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. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘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. x ≤⇘L1⇙ 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 ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇩G (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x. x ≤⇘L1⇙ x ⟹ (≤⇘L2 (η⇩1 x) x⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 x1⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ 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⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "⋀x. x ≤⇘L1⇙ 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⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    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. x1 ≤⇘L1⇙ 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 ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇩G (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≤⇘L1⇙) | η⇩1 x2 ≤⇘L1⇙ x1) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x2 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x2' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | (x2' ≤⇘R1⇙ x3' ∧ x4' ≤⇘R1⇙ ε⇩1 x3')) ⇛ (≥)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "⋀x. x ≤⇘L1⇙ 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⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    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. x1 ≤⇘L1⇙ 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 ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇩G (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  and "⋀x1 x2. x1 ≤⇘L1⇙ 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 ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ≡⇘pre⇙ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((x1 x2 ∷ (≥⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | x1 ≤⇘L1⇙ x3) ⇛ (≤)) L2"
  and "((x1' x2' ∷ (≥⇘R1⇙)) ⇒ (x3' x4' ∷ (≤⇘R1⇙) | x1' ≤⇘R1⇙ x3') ⇛ (≤)) R2"
  and "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  and "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    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