Theory Transport_Compositions_Generic_Galois_Relator

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Relator›
theory Transport_Compositions_Generic_Galois_Relator
  imports
    Transport_Compositions_Generic_Base
begin

context transport_comp
begin

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.t2.unit ≡ ε⇩1"
  by (simp only: t1.flip_unit_eq_counit)

lemma left_Galois_le_comp_left_GaloisI:
  assumes mono_r1: "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and galois_prop1: "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and preorder_R1: "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and rel_comp_le: "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and mono_in_codom_r2: "(in_codom (≤⇘R⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  shows "(⇘L⇙⪅) ≤ ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
proof (rule le_relI)
  fix x z assume "x ⇘L⇙⪅ z"
  then have "in_codom (≤⇘R⇙) z" "x ≤⇘L⇙ r z" by auto
  with galois_prop1 obtain y y' where "in_dom (≤⇘L1⇙) x" "l1 x ≤⇘R1⇙ y" "y ≤⇘L2⇙ y'" "y' ≤⇘R1⇙ ε⇩1 (r2 z)"
    by (auto elim!: left_relE)
  moreover  have "ε⇩1 (r2 z) ≤⇘R1⇙ r2 z"
  proof -
    from mono_in_codom_r2 ‹in_codom (≤⇘R⇙) z› have "in_codom (≤⇘R1⇙) (r2 z)" by blast
    with mono_r1 galois_prop1 preorder_R1 show ?thesis by (blast intro!:
      t1.counit_rel_if_reflexive_on_if_half_galois_prop_left_if_mono_wrt_rel)
  qed
  ultimately have "y' ≤⇘R1⇙ r2 z" using preorder_R1 by blast
  with ‹l1 x ≤⇘R1⇙ y› ‹y ≤⇘L2⇙ y'› have "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) (l1 x) (r2 z)"
    by blast
  with rel_comp_le obtain y'' where "l1 x ≤⇘R1⇙ y''" "y'' ≤⇘L2⇙ r2 z" by blast
  with galois_prop1 ‹in_dom (≤⇘L1⇙) x›  have "x ⇘L1⇙⪅ y''"
    by (intro t1.left_Galois_if_Galois_right_if_half_galois_prop_right t1.left_GaloisI)
    auto
  moreover from ‹in_codom (≤⇘R⇙) z› ‹y'' ≤⇘L2⇙ r2 z› have "y'' ⇘L2⇙⪅ z"
    by (intro t2.left_GaloisI) auto
  ultimately show "((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅)) x z" by blast
qed

lemma comp_left_Galois_le_left_GaloisI:
  assumes mono_r1: "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and half_galois_prop_left1: "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and half_galois_prop_right1: "((≤⇘R1⇙) ⊴⇩h (≤⇘L1⇙)) r1 l1"
  and refl_R1: "reflexive_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and mono_l2: "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and refl_L2: "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and in_codom_rel_comp_le: "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅)) ≤ (⇘L⇙⪅)"
proof (intro le_relI left_GaloisI)
  fix x z assume "((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅)) x z"
  from ‹((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅)) x z› obtain y where "x ⇘L1⇙⪅ y" "y ⇘L2⇙⪅ z" by blast
  with half_galois_prop_left1 have "l1 x ≤⇘R1⇙ y" "y ≤⇘L2⇙ r2 z" by auto
  with refl_R1 refl_L2 have "y ≤⇘R1⇙ y" "y ≤⇘L2⇙ y" by auto
  show "in_codom (≤⇘R⇙) z"
  proof (intro in_codomI flip.left_relI)
    from mono_l2 ‹y ≤⇘L2⇙ y› show "l2 y ⇘R2⇙⪅ y" by blast
    show "y ≤⇘R1⇙ y" "y ⇘L2⇙⪅ z" by fact+
  qed
  show "x ≤⇘L⇙ r z"
  proof (intro left_relI)
    show "x ⇘L1⇙⪅ y" "y ≤⇘L2⇙ r2 z" by fact+
    show "r2 z ⇘R1⇙⪅ r z"
    proof (intro flip.t2.left_GaloisI)
      from ‹y ≤⇘L2⇙ y› ‹y ≤⇘R1⇙ y› ‹y ≤⇘L2⇙ r2 z› have "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) y (r2 z)"
        by blast
      with in_codom_rel_comp_le have "in_codom (≤⇘R1⇙) (r2 z)" by blast
      with refl_R1 have "r2 z ≤⇘R1⇙ r2 z" by blast
      with mono_r1 show "in_codom (≤⇘L1⇙) (r z)" by auto
      with ‹r2 z ≤⇘R1⇙ r2 z›  half_galois_prop_right1 mono_r1
        show "r2 z ≤⇘R1⇙ l1 (r z)" by (fastforce intro:
        flip.t2.rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel)
    qed
  qed
qed

corollary left_Galois_eq_comp_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R1⇙) ⊴⇩h (≤⇘L1⇙)) r1 l1"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "(in_codom (≤⇘R⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms
  by (intro antisym left_Galois_le_comp_left_GaloisI comp_left_Galois_le_left_GaloisI)
  (auto elim!: preorder_on_in_fieldE
    intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)

corollary left_Galois_eq_comp_left_GaloisI':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R1⇙) ⊴⇩h (≤⇘L1⇙)) r1 l1"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro left_Galois_eq_comp_left_GaloisI
    flip.mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le)
  auto

theorem left_Galois_eq_comp_left_Galois_if_galois_connection_if_galois_equivalenceI':
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘R2⇙) ⊣ (≤⇘L2⇙)) r2 l2"
  and "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro left_Galois_eq_comp_left_GaloisI')
  (auto elim!: t1.galois_equivalenceE)

corollary left_Galois_eq_comp_left_Galois_if_galois_connection_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘R2⇙) ⊣ (≤⇘L2⇙)) r2 l2"
  and "reflexive_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  and "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms
  by (intro left_Galois_eq_comp_left_Galois_if_galois_connection_if_galois_equivalenceI'
    flip.left2_right1_left2_le_left2_right1_if_right1_left2_right1_le_left2_right1)
  auto

corollary left_Galois_eq_comp_left_Galois_if_preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘R2⇙) ≡⇘pre⇙ (≤⇘L2⇙)) r2 l2"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  and "(≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ≤ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro
    left_Galois_eq_comp_left_Galois_if_galois_connection_if_galois_equivalenceI)
  auto

end


end