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) ⇛m (≤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) ⇛m 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) ⇛m (≤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) ⇛m (≤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) ⇛m (≤L1)) r1"
  and "((≤L1) ⊴ (≤R1)) l1 r1"
  and "((≤R1) ⊴h (≤L1)) r1 l1"
  and "preorder_on (in_field (≤R1)) (≤R1)"
  and "((≤L2) ⇛m (≤R2)) l2"
  and "reflexive_on (in_dom (≤L2)) (≤L2)"
  and "((≤R1) ∘∘ (≤L2) ∘∘ (≤R1)) ≤ ((≤R1) ∘∘ (≤L2))"
  and "(in_codom (≤R) ⇛m 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) ⇛m (≤L1)) r1"
  and "((≤L1) ⊴ (≤R1)) l1 r1"
  and "((≤R1) ⊴h (≤L1)) r1 l1"
  and "preorder_on (in_field (≤R1)) (≤R1)"
  and "((≤L2) ⇛m (≤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