Theory Transport_Compositions_Generic_Galois_Property

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Property›
theory Transport_Compositions_Generic_Galois_Property
  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" and "flip.t1.counit ≡ η⇩2"
  by (simp_all only: t1.flip_unit_eq_counit t2.flip_counit_eq_unit)

lemma half_galois_prop_left_left_rightI:
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and deflationary_counit1: "deflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and trans_R1: "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "reflexive_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_codom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_codom (≤⇘L2⇙)"
  and mono_in_codom_r2: "(in_codom (≤⇘R⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
proof (rule half_galois_prop_leftI)
  fix x z assume "x ⇘L⇙⪅ z"
  then show "l x ≤⇘R⇙ z"
  proof (intro right_rel_if_left_relI)
    from ‹x ⇘L⇙⪅ z› show "in_codom (≤⇘R2⇙) z" by blast
    fix y assume "y ≤⇘R1⇙ l1 (r z)"
    moreover have "l1 (r z) ≤⇘R1⇙ r2 z"
    proof -
      from mono_in_codom_r2 ‹x ⇘L⇙⪅ z› have "in_codom (≤⇘R1⇙) (r2 z)" by blast
      with deflationary_counit1 show "l1 (r z) ≤⇘R1⇙ r2 z" by auto
    qed
    ultimately show "y ≤⇘R1⇙ r2 z" using trans_R1 by blast
  next
    fix y assume "l1 x ≤⇘L2⇙ y"
    with ‹((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2› show "l x ≤⇘R2⇙ l2 y" by auto
  qed (insert assms, auto)
qed

lemma half_galois_prop_left_left_rightI':
  assumes "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and deflationary_counit1: "deflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and trans_R1: "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and refl_L2: "reflexive_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_dom ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙) ∘∘ (≤⇘R1⇙)) ≤ in_dom (≤⇘L2⇙)"
  and mono_in_codom_r2: "(in_codom (≤⇘R⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
proof (rule half_galois_prop_leftI)
  fix x z assume "x ⇘L⇙⪅ z"
  then show "l x ≤⇘R⇙ z"
  proof (intro right_rel_if_left_relI')
    from ‹x ⇘L⇙⪅ z› show "in_codom (≤⇘R2⇙) z" by blast
    fix y assume "y ≤⇘R1⇙ l1 (r z)"
    moreover have "l1 (r z) ≤⇘R1⇙ r2 z"
    proof -
      from mono_in_codom_r2 ‹x ⇘L⇙⪅ z› have "in_codom (≤⇘R1⇙) (r2 z)" by blast
      with deflationary_counit1 show "l1 (r z) ≤⇘R1⇙ r2 z" by auto
    qed
    ultimately show "y ≤⇘R1⇙ r2 z" using trans_R1 by blast
  next
    assume "in_dom (≤⇘L2⇙) (l1 x)"
    with refl_L2 have "l1 x ≤⇘L2⇙ l1 x" by blast
    with ‹((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2› show "in_codom (≤⇘L2⇙) (l1 x)" "l x ≤⇘R2⇙ l2 (l1 x)"
      by auto
  qed (insert assms, auto)
qed

lemma half_galois_prop_right_left_rightI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1"
  and inflationary_counit1: "inflationary_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and inflationary_unit2: "inflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and trans_L2: "transitive (≤⇘L2⇙)"
  and mono_in_dom_l1: "(in_dom (≤⇘L⇙) ⇒ in_dom (≤⇘L2⇙)) l1"
  and "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘R1⇙) ∘∘ (≤⇘L2⇙))"
  and "in_codom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_codom (≤⇘R1⇙)"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
proof (rule half_galois_prop_rightI)
  fix x z assume "x ⪅⇘R⇙ z"
  then show "x ≤⇘L⇙ r z"
  proof (intro flip.right_rel_if_left_relI)
    fix y assume "r2 (l x) ≤⇘L2⇙ y"
    moreover have "l1 x ≤⇘L2⇙ r2 (l x)"
    proof -
      from mono_in_dom_l1 ‹x ⪅⇘R⇙ z› have "in_dom (≤⇘L2⇙) (l1 x)" by blast
      with inflationary_unit2 show "l1 x ≤⇘L2⇙ r2 (l x)" by auto
    qed
    ultimately show "l1 x ≤⇘L2⇙ y" using trans_L2 by blast
    fix y assume "l1 x ≤⇘R1⇙ y"
    with ‹((≤⇘L1⇙) ⊴⇩h (≤⇘R1⇙)) l1 r1› ‹x ⪅⇘R⇙ z› show "x ≤⇘L1⇙ r1 y" by blast
  next
    assume "in_codom (≤⇘R1⇙) (r2 z)"
    with inflationary_counit1 show "r2 z ≤⇘R1⇙ l1 (r z)" by auto
    from ‹((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1› ‹in_codom (≤⇘R1⇙) (r2 z)› show "in_codom (≤⇘L1⇙) (r z)"
      by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel
        simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
  qed (insert assms, auto elim: galois_rel.left_GaloisE)
qed

lemma half_galois_prop_right_left_rightI':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and inflationary_unit1: "inflationary_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and inflationary_counit1: "⋀y z. y ≤⇘R1⇙ r2 z ⟹ y ≤⇘R1⇙ l1 (r z)"
  and "in_dom (≤⇘R1⇙) ≤ in_codom (≤⇘R1⇙)"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and inflationary_unit2: "inflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and trans_L2: "transitive (≤⇘L2⇙)"
  and mono_in_dom_l1: "(in_dom (≤⇘L⇙) ⇒ in_dom (≤⇘L2⇙)) l1"
  and "((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙))"
  and "in_dom ((≤⇘L2⇙) ∘∘ (≤⇘R1⇙) ∘∘ (≤⇘L2⇙)) ≤ in_dom (≤⇘R1⇙)"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
proof (rule half_galois_prop_rightI)
  fix x z assume "x ⪅⇘R⇙ z"
  then show "x ≤⇘L⇙ r z"
  proof (intro flip.right_rel_if_left_relI')
    from ‹x ⪅⇘R⇙ z› inflationary_unit1 show "x ≤⇘L1⇙ r1 (l1 x)"
      by (fastforce elim: galois_rel.left_GaloisE)
    fix y assume "y ≤⇘R1⇙ r2 z"
    with inflationary_counit1 show "y ≤⇘R1⇙ l1 (r z)" by auto
  next
    fix y
    from mono_in_dom_l1 ‹x ⪅⇘R⇙ z› have "in_dom (≤⇘L2⇙) (l1 x)" by blast
    with inflationary_unit2 have "l1 x ≤⇘L2⇙ r2 (l x)" by auto
    moreover assume "r2 (l x) ≤⇘L2⇙ y"
    ultimately show "l1 x ≤⇘L2⇙ y" using trans_L2 by blast
  qed (insert assms, auto elim: galois_rel.left_GaloisE)
qed

lemma galois_prop_left_rightI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⊴ (≤⇘R1⇙)) l1 r1"
  and "rel_equivalence_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and "inflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
  using assms by (intro galois_propI
    half_galois_prop_left_left_rightI half_galois_prop_right_left_rightI
    flip.mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le
    mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le
    in_dom_right1_left2_right1_le_if_right1_left2_right1_le)
  (auto elim!: preorder_on_in_fieldE
    intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)

lemma galois_prop_left_rightI':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "((≤⇘L1⇙) ⇩h⊴ (≤⇘R1⇙)) l1 r1"
  and "inflationary_on (in_dom (≤⇘L1⇙)) (≤⇘L1⇙) η⇩1"
  and rel_equiv_counit1: "rel_equivalence_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙) ε⇩1"
  and trans_R1: "transitive (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ⇒ (≤⇘R2⇙)) l2"
  and "((≤⇘R2⇙) ⇩h⊴ (≤⇘L2⇙)) r2 l2"
  and "inflationary_on (in_dom (≤⇘L2⇙)) (≤⇘L2⇙) η⇩2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "middle_compatible_dom"
  shows "((≤⇘L⇙) ⊴ (≤⇘R⇙)) l r"
proof (rule galois_propI)
  show "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r" using assms
    by (intro half_galois_prop_left_left_rightI'
      flip.mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le
      flip.in_codom_right1_left2_right1_le_if_right1_left2_right1_le)
    (auto elim!: rel_equivalence_onE preorder_on_in_fieldE
      intro: deflationary_on_if_le_pred_if_deflationary_on
        reflexive_on_if_le_pred_if_reflexive_on
        in_field_if_in_dom in_field_if_in_codom)
  have "y ≤⇘R1⇙ l1 (r1 (r2 z))" if "y ≤⇘R1⇙ r2 z" for y z
  proof -
    note ‹y ≤⇘R1⇙ r2 z›
    moreover with rel_equiv_counit1 have "r2 z ≤⇘R1⇙ ε⇩1 (r2 z)" by blast
    ultimately show ?thesis using trans_R1 by auto
  qed
  moreover have "in_dom (≤⇘R1⇙) ≤ in_codom (≤⇘R1⇙)"
  proof -
    from rel_equiv_counit1 trans_R1 have "reflexive_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
      by (intro reflexive_on_in_field_if_transitive_if_rel_equivalence_on) auto
    then show ?thesis by (simp only: in_codom_eq_in_dom_if_reflexive_on_in_field)
  qed
  ultimately show "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r" using assms
    by (intro half_galois_prop_right_left_rightI'
      mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le)
    auto
qed

end


end