Theory Transport_Compositions_Agree_Galois_Relator

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Relator›
theory Transport_Compositions_Agree_Galois_Relator
  imports
    Transport_Compositions_Agree_Base
begin

context transport_comp_agree
begin

lemma left_Galois_le_comp_left_GaloisI:
  assumes in_codom_mono_r2: "(in_codom (≤⇘R2⇙) ⇒ in_codom (≤⇘R1⇙)) r2"
  and r2_L2_self_if_in_codom: "⋀z. in_codom (≤⇘R2⇙) z ⟹ r2 z ≤⇘L2⇙ r2 z"
  shows "(⇘L⇙⪅) ≤ ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
proof (rule le_relI)
  fix x z assume "x ⇘L⇙⪅ z"
  then have "x ≤⇘L1⇙ r z" "in_codom (≤⇘R⇙) z" by auto
  with ‹x ≤⇘L1⇙ r z› in_codom_mono_r2 have "x ⇘L1⇙⪅ r2 z" by fastforce
  moreover from ‹in_codom (≤⇘R2⇙) z› r2_L2_self_if_in_codom have "r2 z ⇘L2⇙⪅ z"
    by (intro g2.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 trans_L1: "transitive (≤⇘L1⇙)"
  and R1_r2_if_in_codom: "⋀y z. in_codom (≤⇘R2⇙) z ⟹ y ≤⇘L2⇙ r2 z ⟹ y ≤⇘R1⇙ r2 z"
  shows "((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅)) ≤ (⇘L⇙⪅)"
proof (rule le_relI)
  fix x z assume "((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅)) x z"
  then obtain y where "x ⇘L1⇙⪅ y" "y ⇘L2⇙⪅ z" by blast
  then have "x ≤⇘L1⇙ r1 y" "y ≤⇘L2⇙ r2 z" "in_codom (≤⇘R⇙) z" by auto
  with R1_r2_if_in_codom have "y ≤⇘R1⇙ r2 z" by blast
  with mono_r1 have "r1 y ≤⇘L1⇙ r z" by auto
  with ‹x ≤⇘L1⇙ r1 y› ‹in_codom (≤⇘R⇙) z› show "x ⇘L⇙⪅ z" using trans_L1 by blast
qed

corollary left_Galois_eq_comp_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "transitive (≤⇘L1⇙)"
  and "⋀z. in_codom (≤⇘R2⇙) z ⟹ r2 z ≤⇘L2⇙ r2 z"
  and "⋀y z. in_codom (≤⇘R2⇙) z ⟹ y ≤⇘L2⇙ r2 z ⟹ y ≤⇘R1⇙ r2 z"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms
  by (intro antisym left_Galois_le_comp_left_GaloisI comp_left_Galois_le_left_GaloisI
    dep_mono_wrt_predI)
  fastforce

corollary left_Galois_eq_comp_left_GaloisI':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "reflexive_on (in_codom (≤⇘R2⇙)) (≤⇘R2⇙)"
  and "⋀y z. in_codom (≤⇘R2⇙) z ⟹ y ≤⇘L2⇙ r2 z ⟹ y ≤⇘R1⇙ r2 z"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro left_Galois_eq_comp_left_GaloisI) (auto 5 0)

corollary left_Galois_eq_comp_left_GaloisI'':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇒ (≤⇘L2⇙)) r2"
  and "reflexive_on (in_codom (≤⇘L2⇙)) (≤⇘L2⇙)"
  and "⋀y z. in_codom (≤⇘R2⇙) z ⟹ y ≤⇘L2⇙ r2 z ⟹ y ≤⇘R1⇙ r2 z"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro left_Galois_eq_comp_left_GaloisI) (auto 0 6)

end

context transport_comp_same
begin

lemma left_Galois_eq_comp_left_GaloisI:
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "transitive (≤⇘L1⇙)"
  and "((≤⇘R2⇙) ⇒ (≤⇘R1⇙)) r2"
  and "reflexive_on (in_codom (≤⇘R2⇙)) (≤⇘R2⇙)"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro left_Galois_eq_comp_left_GaloisI') auto

lemma left_Galois_eq_comp_left_GaloisI':
  assumes "((≤⇘R1⇙) ⇒ (≤⇘L1⇙)) r1"
  and "transitive (≤⇘L1⇙)"
  and "reflexive_on (in_codom (≤⇘R1⇙)) (≤⇘R1⇙)"
  and "((≤⇘R2⇙) ⇒ (≤⇘R1⇙)) r2"
  shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ∘∘ (⇘L2⇙⪅))"
  using assms by (intro left_Galois_eq_comp_left_GaloisI'') auto

end


end