Theory Transport_Functions_Galois_Connection

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Connection›
theory Transport_Functions_Galois_Connection
  imports
    Transport_Functions_Galois_Property
    Transport_Functions_Monotone
begin

paragraph ‹Dependent Function Relator›

context transport_Dep_Fun_Rel
begin

subparagraph ‹Lemmas for Monotone Function Relator›

lemma galois_connection_left_right_if_galois_connection_mono_2_assms_leftI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_R1: "reflexive_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and R2_le1: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and mono_l2_2: "((x' : in_codom (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x') ⇒
    (in_field (≤⇘L2 x1 (r1 x')⇙)) ⇛ (≤⇘R2 (l1 x1) x'⇙)) l2"
  shows "⋀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)⇙)"
proof -
  show "((in_codom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x2' (r1 x1')⇙) (l2⇘x2' (r1 x2')⇙)"
    if "x1' ≤⇘R1⇙ x2'" for x1' x2'
  proof -
    from galois_conn1 ‹x1' ≤⇘R1⇙ x2'› have "r1 x1' ≤⇘L1⇙ r1 x2'" "r1 x2' ⇘L1⇙⪅ x2'"
      using refl_R1 by (auto intro: t1.right_left_Galois_if_reflexive_onI)
    with mono_l2_2 show ?thesis using R2_le1 ‹x1' ≤⇘R1⇙ x2'› by fastforce
  qed
  show "((in_dom (≤⇘L2 x (η⇩1 x)⇙)) ⇛ (≤⇘R2 (l1 x) (l1 x)⇙)) (l2⇘(l1 x) x⇙) (l2⇘(l1 x) (η⇩1 x)⇙)"
    if "x ≤⇘L1⇙ x" for x
  proof -
    from galois_conn1 ‹x ≤⇘L1⇙ x› have "x ≤⇘L1⇙ η⇩1 x" "η⇩1 x ⇘L1⇙⪅ l1 x"
      by (auto intro!: t1.right_left_Galois_if_right_relI
        t1.rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel
          [unfolded t1.unit_eq])
    with mono_l2_2 show ?thesis by fastforce
  qed
qed

lemma galois_connection_left_right_if_galois_connection_mono_assms_leftI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_R1: "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and R2_le1: "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 (ε⇩1 x1') x2'⇙) ≤ (≤⇘R2 x1' x2'⇙)"
  and mono_l2: "((x1' x2' ∷ (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘L2 x1 (r1 x2')⇙) ⇛ (≤⇘R2 (l1 x1) x2'⇙)) l2"
  shows "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
  and "((x' : in_codom (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x') ⇒
    (in_field (≤⇘L2 x1 (r1 x')⇙)) ⇛ (≤⇘R2 (l1 x1) x'⇙)) l2"
proof -
  show "((in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
    if "x1' ≤⇘R1⇙ x2'" for x1' x2'
  proof -
    from galois_conn1 ‹x1' ≤⇘R1⇙ x2'› have "r1 x1' ≤⇘L1⇙ r1 x1'" "r1 x1' ⇘L1⇙⪅ x1'"
      using refl_R1 by force+
    with mono_l2 show ?thesis using ‹x1' ≤⇘R1⇙ x2'› R2_le1 by (auto 11 0)
  qed
  from mono_l2 show "((x' : in_codom (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x') ⇒
    (in_field (≤⇘L2 x1 (r1 x')⇙)) ⇛ (≤⇘R2 (l1 x1) x'⇙)) l2" using refl_R1 by blast
qed

text ‹In theory, the following lemmas can be obtained by taking the flipped,
inverse interpretation of the locale; however, rewriting the assumptions is more
involved than simply copying and adapting above proofs.›

lemma galois_connection_left_right_if_galois_connection_mono_2_assms_rightI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and L2_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and mono_r2_2: "((x : in_dom (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x ⇘L1⇙⪅ x1') ⇒
    (in_field (≤⇘R2 (l1 x) x2'⇙)) ⇛ (≤⇘L2 x (r1 x2')⇙)) r2"
  shows "⋀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'⇙)"
proof -
  show "((in_dom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x1)⇙) (r2⇘x1 (l1 x2)⇙)"
    if "x1 ≤⇘L1⇙ x2" for x1 x2
  proof -
    from galois_conn1 ‹x1 ≤⇘L1⇙ x2› have "x1 ⇘L1⇙⪅ l1 x1" "l1 x1 ≤⇘R1⇙ l1 x2"
      using refl_L1 by (auto intro!: t1.left_Galois_left_if_reflexive_on_if_half_galois_prop_rightI)
    with mono_r2_2 show ?thesis using L2_le2 ‹x1 ≤⇘L1⇙ x2› by (auto 12 0)
  qed
  show "((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
    if "x' ≤⇘R1⇙ x'" for x'
  proof -
    from galois_conn1 ‹x' ≤⇘R1⇙ x'› have "r1 x' ⇘L1⇙⪅ ε⇩1 x'" "ε⇩1 x' ≤⇘R1⇙ x'"
      by (auto intro!: t1.left_Galois_left_if_left_relI
        t1.counit_rel_if_right_rel_if_half_galois_prop_left_if_mono_wrt_rel
          [unfolded t1.counit_eq])
    with mono_r2_2 show ?thesis by fastforce
  qed
qed

lemma galois_connection_left_right_if_galois_connection_mono_assms_rightI:
  assumes galois_conn1: "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and refl_L1: "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and L2_le2: "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and mono_r2: "((x1 x2 ∷ (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x2 ⇘L1⇙⪅ x1') ⇛
    in_field (≤⇘R2 (l1 x1) x2'⇙) ⇛ (≤⇘L2 x1 (r1 x2')⇙)) r2"
  shows "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹
    ((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
  and "((x : in_dom (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x ⇘L1⇙⪅ x1') ⇒
    (in_field (≤⇘R2 (l1 x) x2'⇙)) ⇛ (≤⇘L2 x (r1 x2')⇙)) r2"
proof -
  show "((in_codom (≤⇘R2 (l1 x1) (l1 x2)⇙)) ⇛ (≤⇘L2 x1 x2⇙)) (r2⇘x1 (l1 x2)⇙) (r2⇘x2 (l1 x2)⇙)"
    if "x1 ≤⇘L1⇙ x2" for x1 x2
  proof -
    from galois_conn1 ‹x1 ≤⇘L1⇙ x2› have "x2 ⇘L1⇙⪅ l1 x2" "l1 x2 ≤⇘R1⇙ l1 x2"
      using refl_L1 by (blast intro: t1.left_Galois_left_if_reflexive_on_if_half_galois_prop_rightI)+
    with mono_r2 show ?thesis using ‹x1 ≤⇘L1⇙ x2› L2_le2 by fastforce
  qed
  from mono_r2 show "((x : in_dom (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x ⇘L1⇙⪅ x1') ⇒
    (in_field (≤⇘R2 (l1 x) x2'⇙)) ⇛ (≤⇘L2 x (r1 x2')⇙)) r2" using refl_L1 by blast
qed

end


paragraph ‹Monotone Dependent Function Relator›

context transport_Mono_Dep_Fun_Rel
begin

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

lemma galois_connection_left_rightI:
  assumes "(tdfr.L ⇒ tdfr.R) l" and "(tdfr.R ⇒ tdfr.L) r"
  and "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⊴ (≤⇘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 x (η⇩1 x)⇙) ≤ (≤⇘L2 x x⇙)"
  and "⋀x'. x' ≤⇘R1⇙ x' ⟹ (≤⇘R2 (ε⇩1 x') x'⇙) ≤ (≤⇘R2 x' x'⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ (≤⇘R2 x1' x1'⇙) ≤ (≤⇘R2 x1' 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' ≤⇘R1⇙ x' ⟹
    ((in_codom (≤⇘R2 (ε⇩1 x') x'⇙)) ⇛ (≤⇘L2 (r1 x') (r1 x')⇙)) (r2⇘(r1 x') (ε⇩1 x')⇙) (r2⇘(r1 x') x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  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

lemma galois_connection_left_rightI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((≤⇘L2 (r1 x1') (r1 x2')⇙) ⇒ (≤⇘R2 (ε⇩1 x1') x2'⇙)) (l2⇘x2' (r1 x1')⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ ((≤⇘R2 (l1 x1) (l1 x2)⇙) ⇒ (≤⇘L2 x1 (η⇩1 x2)⇙)) (r2⇘x1 (l1 x2)⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⊴ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 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 "⋀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 "⋀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 "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms
  by (intro galois_connection_left_rightI tdfr.mono_wrt_rel_left_if_transitiveI
    tdfr.mono_wrt_rel_right_if_transitiveI)
  auto

lemma galois_connection_left_right_if_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "⋀x x'. x ⇘L1⇙⪅ x' ⟹ ((≤⇘L2 x (r1 x')⇙) ⊣ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 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 "⋀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 "⋀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 "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ transitive (≤⇘L2 x1 x2⇙)"
  and "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹ transitive (≤⇘R2 x1' x2'⇙)"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms
  by (intro galois_connection_left_rightI'
    tdfr.mono_wrt_rel_left2_if_mono_wrt_rel_left2_if_left_GaloisI
    tdfr.mono_wrt_rel_right2_if_mono_wrt_rel_right2_if_left_GaloisI)
  (auto 7 0)

corollary galois_connection_left_right_if_galois_connectionI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘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')⇙) ⊣ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 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 "⋀x1' x2'. x1' ≤⇘R1⇙ x2' ⟹
    ((in_dom (≤⇘L2 (r1 x1') (r1 x2')⇙)) ⇛ (≤⇘R2 x1' x2'⇙)) (l2⇘x1' (r1 x1')⇙) (l2⇘x2' (r1 x1')⇙)"
  and "((x' : in_codom (≤⇘R1⇙)) ⇒ (x1 x2 ∷ (≤⇘L1⇙) | x2 ⇘L1⇙⪅ x') ⇒
    (in_field (≤⇘L2 x1 (r1 x')⇙)) ⇛ (≤⇘R2 (l1 x1) x'⇙)) l2"
  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 "((x : in_dom (≤⇘L1⇙)) ⇒ (x1' x2' ∷ (≤⇘R1⇙) | x ⇘L1⇙⪅ x1') ⇒
    (in_field (≤⇘R2 (l1 x) x2'⇙)) ⇛ (≤⇘L2 x (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⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connection_left_right_if_galois_connectionI
    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_connection_left_right_if_mono_if_galois_connectionI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘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')⇙) ⊣ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x2 x2⇙) ≤ (≤⇘L2 x1 x2⇙)"
  and "⋀x1 x2. x1 ≤⇘L1⇙ x2 ⟹ (≤⇘L2 x1 (η⇩1 x2)⇙) ≤ (≤⇘L2 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 "((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⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connection_left_right_if_galois_connectionI'
    tdfr.galois_connection_left_right_if_galois_connection_mono_assms_leftI
    tdfr.galois_connection_left_right_if_galois_connection_mono_assms_rightI)
  auto

corollary galois_connection_left_right_if_mono_if_galois_connectionI':
  assumes "((≤⇘L1⇙) ⊣ (≤⇘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')⇙) ⊣ (≤⇘R2 (l1 x) x'⇙)) (l2⇘x' x⇙) (r2⇘x x'⇙)"
  and "((_ x2 ∷ (≤⇘L1⇙)) ⇒ (x3 x4 ∷ (≤⇘L1⇙) | (x2 ≤⇘L1⇙ x3 ∧ x4 ≤⇘L1⇙ η⇩1 x3)) ⇛ (≥)) L2"
  and "((x1' x2' ∷ (≤⇘R1⇙) | ε⇩1 x2' ≤⇘R1⇙ x1') ⇒ (x3' _ ∷ (≤⇘R1⇙) | x2' ≤⇘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⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro galois_connection_left_right_if_mono_if_galois_connectionI
    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)
  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_connection_left_rightI:
  assumes "((≤⇘L1⇙) ⊣ (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_codom (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "reflexive_on (in_dom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⊣ (≤⇘R2⇙)) l2 r2"
  and "transitive (≤⇘L2⇙)"
  and "transitive (≤⇘R2⇙)"
  shows "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  using assms by (intro tpdfr.galois_connectionI galois_prop_left_rightI
    mono_wrt_rel_leftI flip.mono_wrt_rel_leftI)
  auto

end


end