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 Lz"
  then have "in_codom (≤R) z" "xL r z" by auto
  with galois_prop1 obtain y y' where "in_dom (≤L1) x" "l1 xR1 y" "yL2 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 xR1 y yL2 y' have "((≤R1) ∘∘ (≤L2) ∘∘ (≤R1)) (l1 x) (r2 z)"
    by blast
  with rel_comp_le obtain y'' where "l1 xR1 y''" "y''L2 r2 z" by blast
  with galois_prop1 in_dom (≤L1) x  have "x L1y''"
    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'' L2z"
    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 L1y" "y L2z" by blast
  with half_galois_prop_left1 have "l1 xR1 y" "yL2 r2 z" by auto
  with refl_R1 refl_L2 have "yR1 y" "yL2 y" by auto
  show "in_codom (≤R) z"
  proof (intro in_codomI flip.left_relI)
    from mono_l2 yL2 y show "l2 y R2y" by blast
    show "yR1 y" "y L2z" by fact+
  qed
  show "xL r z"
  proof (intro left_relI)
    show "x L1y" "yL2 r2 z" by fact+
    show "r2 z R1r z"
    proof (intro flip.t2.left_GaloisI)
      from yL2 y yR1 y yL2 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 zR1 r2 z" by blast
      with mono_r1 show "in_codom (≤L1) (r z)" by auto
      with r2 zR1 r2 z  half_galois_prop_right1 mono_r1
        show "r2 zR1 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