Theory Transport_Compositions_Generic_Order_Equivalence

✐‹creator "Kevin Kappelmann"›
subsection ‹Order Equivalence›
theory Transport_Compositions_Generic_Order_Equivalence
  imports
    Transport_Compositions_Generic_Monotone
begin

context transport_comp
begin

context
begin

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

subsubsection ‹Unit›
paragraph ‹Inflationary›

lemma inflationary_on_in_dom_unitI:
  assumes "((≤R1)  (≤L1)) r1"
  and "((≤L1) h (≤R1)) l1 r1"
  and inflationary_unit1: "inflationary_on (in_dom (≤L1)) (≤L1) η1"
  and inflationary_counit1: "inflationary_on (in_codom (≤R1)) (≤R1) ε1"
  and refl_R1: "reflexive_on (in_dom (≤R1)) (≤R1)"
  and inflationary_unit2: "inflationary_on (in_dom (≤L2)) (≤L2) η2"
  and refl_L2: "reflexive_on (in_dom (≤L2)) (≤L2)"
  and mono_in_dom_l1: "(in_dom (≤L)  in_dom (≤L2)) l1"
  and in_codom_rel_comp_le: "in_codom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_codom ((≤R1))"
  shows "inflationary_on (in_dom (≤L)) (≤L) η"
proof (rule inflationary_onI)
  fix x assume "in_dom (≤L) x"
  show "xL η x"
  proof (rule left_relI)
    from in_dom (≤L) x ((≤L1) h (≤R1)) l1 r1 have "in_dom (≤R1) (l1 x)" by blast
    with refl_R1 have "l1 xR1 l1 x" by blast
    moreover from in_dom (≤L) x have "in_dom (≤L1) x" by blast
    moreover note inflationary_unit1
    ultimately show "x L1l1 x" by (intro t1.left_GaloisI) auto
    from in_dom (≤L) x mono_in_dom_l1 have "in_dom (≤L2) (l1 x)" by blast
    with inflationary_unit2 show "l1 xL2 r2 (l x)" by auto
    show "r2 (l x) R1η x"
    proof (rule flip.t2.left_GaloisI)
      from refl_L2 in_dom (≤L2) (l1 x) have "l1 xL2 l1 x" by blast
      with in_codom_rel_comp_le l1 xR1 l1 x l1 xL2 r2 (l x)
        have "in_codom (≤R1) (r2 (l x))" by blast
      with ((≤R1)  (≤L1)) r1 show "in_codom (≤L1) (η x)"
        by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      from in_codom (≤R1) (r2 (l x)) inflationary_counit1
        show "r2 (l x)R1 l1 (η x)" by auto
    qed
  qed
qed

lemma inflationary_on_in_codom_unitI:
  assumes "((≤R1)  (≤L1)) r1"
  and inflationary_unit1: "inflationary_on (in_codom (≤L1)) (≤L1) η1"
  and inflationary_counit1: "inflationary_on (in_codom (≤R1)) (≤R1) ε1"
  and refl_R1: "reflexive_on (in_codom (≤R1)) (≤R1)"
  and inflationary_unit2: "inflationary_on (in_codom (≤L2)) (≤L2) η2"
  and refl_L2: "reflexive_on (in_codom (≤L2)) (≤L2)"
  and mono_in_codom_l1: "(in_codom (≤L)  in_codom (≤L2)) l1"
  and in_codom_rel_comp_le: "in_codom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_codom ((≤R1))"
  shows "inflationary_on (in_codom (≤L)) (≤L) η"
proof (rule inflationary_onI)
  fix x assume "in_codom (≤L) x"
  show "xL η x"
  proof (rule left_relI)
    from in_codom (≤L) x have "in_codom (≤L1) x" "in_codom (≤R1) (l1 x)" by blast+
    with inflationary_unit1 show "x L1l1 x" by (intro t1.left_GaloisI) auto
    from mono_in_codom_l1 in_codom (≤L) x have "in_codom (≤L2) (l1 x)" by blast
    with inflationary_unit2 show "l1 xL2 r2 (l x)" by auto
    show "r2 (l x) R1η x"
    proof (rule flip.t2.left_GaloisI)
      from refl_L2 in_codom (≤L2) (l1 x) have "l1 xL2 l1 x" by blast
      moreover from refl_R1 in_codom (≤R1) (l1 x) have "l1 xR1 l1 x" by blast
      moreover note in_codom_rel_comp_le l1 xL2 r2 (l x)
      ultimately have "in_codom (≤R1) (r2 (l x))" by blast
      with ((≤R1)  (≤L1)) r1 show "in_codom (≤L1) (η x)"
        by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      from in_codom (≤R1) (r2 (l x)) inflationary_counit1
        show "r2 (l x)R1 l1 (η x)" by auto
    qed
  qed
qed

corollary inflationary_on_in_field_unitI:
  assumes "((≤R1)  (≤L1)) r1"
  and "((≤L1) h (≤R1)) l1 r1"
  and "inflationary_on (in_field (≤L1)) (≤L1) η1"
  and "inflationary_on (in_codom (≤R1)) (≤R1) ε1"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "inflationary_on (in_field (≤L2)) (≤L2) η2"
  and "reflexive_on (in_field (≤L2)) (≤L2)"
  and "(in_dom (≤L)  in_dom (≤L2)) l1"
  and "(in_codom (≤L)  in_codom (≤L2)) l1"
  and "in_codom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_codom ((≤R1))"
  shows "inflationary_on (in_field (≤L)) (≤L) η"
proof -
  from assms have "inflationary_on (in_dom (≤L)) (≤L) η"
    by (intro inflationary_on_in_dom_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  moreover from assms have "inflationary_on (in_codom (≤L)) (≤L) η"
    by (intro inflationary_on_in_codom_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed


text ‹Deflationary›

lemma deflationary_on_in_dom_unitI:
  assumes "((≤L1)  (≤R1)) l1" "((≤R1)  (≤L1)) r1"
  and refl_L1: "reflexive_on (in_dom (≤L1)) (≤L1)"
  and in_dom_R1_le_in_codom_R1: "in_dom (≤R1)  in_codom (≤R1)"
  and deflationary_L2: "deflationary_on (in_dom (≤L2)) (≤L2) η2"
  and refl_L2: "reflexive_on (in_dom (≤L2)) (≤L2)"
  and mono_in_dom_l1: "(in_dom (≤L)  in_dom (≤L2)) l1"
  and in_dom_rel_comp_le: "in_dom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_dom ((≤R1))"
  shows "deflationary_on (in_dom (≤L)) (≤L) η"
proof (rule deflationary_onI)
  fix x assume "in_dom (≤L) x"
  show "η xL x"
  proof (rule left_relI)
    from refl_L1 in_dom (≤L) x have "xL1 x" by blast
    moreover with ((≤L1)  (≤R1)) l1 have "l1 xR1 l1 x" by blast
    ultimately show "l1 x R1x" by auto
    from mono_in_dom_l1 in_dom (≤L) x have "in_dom (≤L2) (l1 x)" by blast
    with deflationary_L2 show "r2 (l x)L2 l1 x" by auto
    show "η x L1r2 (l x)"
    proof (rule t1.left_GaloisI)
      from refl_L2 in_dom (≤L2) (l1 x) have "l1 xL2 l1 x" by blast
      with in_dom_rel_comp_le r2 (l x)L2 l1 x l1 xR1 l1 x
        have "in_dom (≤R1) (r2 (l x))" by blast
      with ((≤R1)  (≤L1)) r1 have "in_dom (≤L1) (η x)"
        by (auto intro: in_dom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      with refl_L1 show "η xL1 r1 (r2 (l x))"
        by (auto intro: in_field_if_in_codom)
      from in_dom (≤R1) (r2 (l x)) in_dom_R1_le_in_codom_R1
        show "in_codom (≤R1) (r2 (l x))" by blast
    qed
  qed
qed

lemma deflationary_on_in_codom_unitI:
  assumes "((≤L1)  (≤R1)) l1" "((≤R1)  (≤L1)) r1"
  and refl_L1: "reflexive_on (in_codom (≤L1)) (≤L1)"
  and in_dom_R1_le_in_codom_R1: "in_dom (≤R1)  in_codom (≤R1)"
  and deflationary_L2: "deflationary_on (in_codom (≤L2)) (≤L2) η2"
  and refl_L2: "reflexive_on (in_codom (≤L2)) (≤L2)"
  and mono_in_codom_l1: "(in_codom (≤L)  in_codom (≤L2)) l1"
  and in_dom_rel_comp_le: "in_dom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_dom ((≤R1))"
  shows "deflationary_on (in_codom (≤L)) (≤L) η"
proof (rule deflationary_onI)
  fix x assume "in_codom (≤L) x"
  show "η xL x"
  proof (rule left_relI)
    from refl_L1 in_codom (≤L) x have "xL1 x" by blast
    moreover with ((≤L1)  (≤R1)) l1 have "l1 xR1 l1 x" by blast
    ultimately show "l1 x R1x" by auto
    from mono_in_codom_l1 in_codom (≤L) x have "in_codom (≤L2) (l1 x)" by blast
    with deflationary_L2 show "r2 (l x)L2 l1 x" by auto
    show "η x L1r2 (l x)"
    proof (rule t1.left_GaloisI)
      from refl_L2 in_codom (≤L2) (l1 x) have "l1 xL2 l1 x" by blast
      with in_dom_rel_comp_le r2 (l x)L2 l1 x l1 xR1 l1 x
        have "in_dom (≤R1) (r2 (l x))" by blast
      with in_dom_R1_le_in_codom_R1 show "in_codom (≤R1) (r2 (l x))" by blast
      with ((≤R1)  (≤L1)) r1 have "in_codom (≤L1) (η x)"
        by (auto intro: in_codom_if_rel_if_dep_mono_wrt_rel simp: mono_wrt_rel_eq_dep_mono_wrt_rel)
      with refl_L1 show "η xL1 r1 (r2 (l x))" by auto
    qed
  qed
qed

corollary deflationary_on_in_field_unitI:
  assumes "((≤L1)  (≤R1)) l1" "((≤R1)  (≤L1)) r1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "in_dom (≤R1)  in_codom (≤R1)"
  and "deflationary_on (in_field (≤L2)) (≤L2) η2"
  and "reflexive_on (in_field (≤L2)) (≤L2)"
  and "(in_dom (≤L)  in_dom (≤L2)) l1"
  and "(in_codom (≤L)  in_codom (≤L2)) l1"
  and "in_dom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_dom ((≤R1))"
  shows "deflationary_on (in_field (≤L)) (≤L) η"
proof -
  from assms have "deflationary_on (in_dom (≤L)) (≤L) η"
    by (intro deflationary_on_in_dom_unitI)
    (auto intro: deflationary_on_if_le_pred_if_deflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
  moreover from assms have "deflationary_on (in_codom (≤L)) (≤L) η"
    by (intro deflationary_on_in_codom_unitI)
    (auto intro: deflationary_on_if_le_pred_if_deflationary_on
      reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_codom)
  ultimately show ?thesis by (auto iff: in_field_iff_in_dom_or_in_codom)
qed


text ‹Relational Equivalence›

corollary rel_equivalence_on_in_field_unitI:
  assumes "((≤L1)  (≤R1)) l1" "((≤R1)  (≤L1)) r1"
  and "((≤L1) h (≤R1)) l1 r1"
  and "inflationary_on (in_field (≤L1)) (≤L1) η1"
  and "inflationary_on (in_codom (≤R1)) (≤R1) ε1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "rel_equivalence_on (in_field (≤L2)) (≤L2) η2"
  and "reflexive_on (in_field (≤L2)) (≤L2)"
  and "(in_dom (≤L)  in_dom (≤L2)) l1"
  and "(in_codom (≤L)  in_codom (≤L2)) l1"
  and "in_dom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_dom ((≤R1))"
  and "in_codom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_codom ((≤R1))"
  shows "rel_equivalence_on (in_field (≤L)) (≤L) η"
  using assms by (intro rel_equivalence_onI
    inflationary_on_in_field_unitI deflationary_on_in_field_unitI)
  (auto simp only: in_codom_eq_in_dom_if_reflexive_on_in_field)


subsubsection ‹Counit›

text ‹Corresponding lemmas for the counit can be obtained by flipping the
interpretation of the locale, i.e.

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.t2.unit ≡ ε1" and "flip.t2.counit ≡ η1"
  and "flip.t1.unit ≡ ε2" and "flip.t1.counit ≡ η2"
  and "flip.unit ≡ ε" and "flip.counit ≡ η"
  unfolding transport_comp.transport_defs
  by (auto simp: order_functors.flip_counit_eq_unit)
›

end


subsubsection ‹Order Equivalence›

interpretation flip : transport_comp R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.t2.unit  ε1" and "flip.t2.counit  η1"
  and "flip.t1.unit  ε2" and "flip.t1.counit  η2"
  and "flip.counit  η" and "flip.unit  ε"
  by (simp_all only: order_functors.flip_counit_eq_unit)

lemma order_equivalenceI:
  assumes "((≤L1)  (≤R1)) l1" "((≤R1)  (≤L1)) r1"
  and "((≤L1) h (≤R1)) l1 r1"
  and "inflationary_on (in_field (≤L1)) (≤L1) η1"
  and rel_equiv_counit1: "rel_equivalence_on (in_field (≤R1)) (≤R1) ε1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "((≤R2)  (≤L2)) r2" "((≤L2)  (≤R2)) l2"
  and "((≤R2) h (≤L2)) r2 l2"
  and rel_equiv_unit2: "rel_equivalence_on (in_field (≤L2)) (≤L2) η2"
  and "inflationary_on (in_field (≤R2)) (≤R2) ε2"
  and "reflexive_on (in_field (≤L2)) (≤L2)"
  and "reflexive_on (in_field (≤R2)) (≤R2)"
  and middle_compatible: "middle_compatible_codom"
  shows "((≤L) o (≤R)) l r"
proof (rule order_equivalenceI)
  show "((≤L)  (≤R)) l" using rel_equiv_unit2 ((≤L1) h (≤R1)) l1 r1
      ((≤L2)  (≤R2)) l2 middle_compatible
    by (intro mono_wrt_rel_leftI) auto
  show "((≤R)  (≤L)) r" using rel_equiv_counit1 ((≤R2) h (≤L2)) r2 l2
      ((≤R1)  (≤L1)) r1 middle_compatible
    by (intro flip.mono_wrt_rel_leftI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      in_field_if_in_codom)
  from middle_compatible have in_dom_rel_comp_les:
    "in_dom ((≤R1) ∘∘ (≤L2) ∘∘ (≤R1))  in_dom (≤L2)"
    "in_dom ((≤L2) ∘∘ (≤R1) ∘∘ (≤L2))  in_dom ((≤R1))"
    by (auto intro: in_dom_right1_left2_right1_le_if_right1_left2_right1_le
      flip.in_dom_right1_left2_right1_le_if_right1_left2_right1_le)
  moreover then have "(in_dom (≤L)  in_dom (≤L2)) l1"
    and "(in_codom (≤L)  in_codom (≤L2)) l1"
    using ((≤L1) h (≤R1)) l1 r1 middle_compatible
    by (auto intro: mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le
      mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le)
  ultimately show "rel_equivalence_on (in_field (≤L)) (≤L) η"
    using assms by (intro rel_equivalence_on_in_field_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      intro!: in_field_if_in_codom)
  note in_dom_rel_comp_les
  moreover then have "(in_dom (≤R)  in_dom (≤R1)) r2"
    and "(in_codom (≤R)  in_codom (≤R1)) r2"
    using ((≤R2) h (≤L2)) r2 l2 middle_compatible
    by (auto intro!: flip.mono_in_dom_left_rel_left1_if_in_dom_rel_comp_le
      flip.mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le)
  ultimately show "rel_equivalence_on (in_field (≤R)) (≤R) ε"
    using assms by (intro flip.rel_equivalence_on_in_field_unitI)
    (auto intro: inflationary_on_if_le_pred_if_inflationary_on
      intro!: in_field_if_in_codom)
qed

corollary order_equivalence_if_order_equivalenceI:
  assumes "((≤L1) o (≤R1)) l1 r1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "transitive (≤R1)"
  and "((≤L2) o (≤R2)) l2 r2"
  and "transitive (≤L2)"
  and "reflexive_on (in_field (≤R2)) (≤R2)"
  and "middle_compatible_codom"
  shows "((≤L) o (≤R)) l r"
  using assms by (intro order_equivalenceI) (auto
    elim!: t1.order_equivalenceE t2.order_equivalenceE rel_equivalence_onE
    intro!: reflexive_on_in_field_if_transitive_if_rel_equivalence_on
      t1.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
      flip.t1.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel
    intro: deflationary_on_if_le_pred_if_deflationary_on in_field_if_in_codom)

corollary order_equivalence_if_galois_equivalenceI:
  assumes "((≤L1) G (≤R1)) l1 r1"
  and "reflexive_on (in_field (≤L1)) (≤L1)"
  and "reflexive_on (in_field (≤R1)) (≤R1)"
  and "((≤L2) G (≤R2)) l2 r2"
  and "reflexive_on (in_field (≤L2)) (≤L2)"
  and "reflexive_on (in_field (≤R2)) (≤R2)"
  and "middle_compatible_codom"
  shows "((≤L) o (≤R)) l r"
  using assms by (intro order_equivalenceI)
  (auto elim!: t1.galois_equivalenceE t2.galois_equivalenceE
    intro!: t1.inflationary_on_unit_if_reflexive_on_if_galois_equivalence
      flip.t1.inflationary_on_unit_if_reflexive_on_if_galois_equivalence
      t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence
      flip.t2.rel_equivalence_on_unit_if_reflexive_on_if_galois_equivalence)

end


end