Theory Transport_Compositions_Generic

✐‹creator "Kevin Kappelmann"›
theory Transport_Compositions_Generic
  imports
    Transport_Compositions_Generic_Galois_Equivalence
    Transport_Compositions_Generic_Galois_Relator
    Transport_Compositions_Generic_Order_Base
    Transport_Compositions_Generic_Order_Equivalence
begin

paragraph ‹Summary of Main Results›

subparagraph ‹Closure of Order and Galois Concepts›

context transport_comp
begin

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

lemma preorder_galois_connection_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "reflexive_on (in_field (≤⇘R2⇙)) (≤⇘R2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_galois_connectionI)
  (auto elim!: t1.galois_equivalenceE t2.galois_equivalenceE
    intro!: galois_connection_left_right_if_galois_equivalenceI
      preorder_on_in_field_leftI flip.preorder_on_in_field_leftI
      mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le
      flip.mono_in_codom_left_rel_left1_if_in_codom_rel_comp_le
      in_codom_eq_in_dom_if_reflexive_on_in_field)

theorem preorder_galois_connection_if_preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘pre⇙ (≤⇘R2⇙)) l2 r2"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_galois_connection_if_galois_equivalenceI)
  auto

lemma preorder_equivalence_if_galois_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇩G (≤⇘R1⇙)) l1 r1"
  and "reflexive_on (in_field (≤⇘L1⇙)) (≤⇘L1⇙)"
  and "preorder_on (in_field (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘L2⇙) ≡⇩G (≤⇘R2⇙)) l2 r2"
  and "preorder_on (in_field (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "reflexive_on (in_field (≤⇘R2⇙)) (≤⇘R2⇙)"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
proof -
  from assms have "((≤⇘L⇙) ⊣⇘pre⇙ (≤⇘R⇙)) l r"
    by (intro preorder_galois_connection_if_galois_equivalenceI) auto
  with assms show ?thesis by (intro preorder_equivalence_if_galois_equivalenceI)
    (auto intro!: galois_equivalence_if_galois_equivalenceI
      preorder_galois_connection_if_galois_equivalenceI)
qed

theorem preorder_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘pre⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘pre⇙ (≤⇘R2⇙)) l2 r2"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇘pre⇙ (≤⇘R⇙)) l r"
  using assms by (intro preorder_equivalence_if_galois_equivalenceI) auto

theorem partial_equivalence_rel_equivalenceI:
  assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
  and "((≤⇘L2⇙) ≡⇘PER⇙ (≤⇘R2⇙)) l2 r2"
  and "middle_compatible_codom"
  shows "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  using assms by (intro partial_equivalence_rel_equivalence_if_galois_equivalenceI
    galois_equivalence_if_galois_equivalenceI
    partial_equivalence_rel_leftI flip.partial_equivalence_rel_leftI
    in_codom_eq_in_dom_if_partial_equivalence_rel)
  auto


subparagraph ‹Simplification of Galois relator›

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

text ‹For theorems with weaker assumptions, see
@{thm "left_Galois_eq_comp_left_GaloisI'"
"left_Galois_eq_comp_left_Galois_if_galois_connection_if_galois_equivalenceI"}.›


subparagraph ‹Simplification of Compatibility Assumption›

text ‹See @{theory "Transport.Transport_Compositions_Generic_Base"}.›

end


end