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 zL2 r2 z"
  shows "(L⪅)  ((L1⪅) ∘∘ (L2⪅))"
proof (rule le_relI)
  fix x z assume "x Lz"
  then have "xL1 r z" "in_codom (≤R) z" by auto
  with xL1 r z in_codom_mono_r2 have "x L1r2 z" by fastforce
  moreover from in_codom (≤R2) z r2_L2_self_if_in_codom have "r2 z L2z"
    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  yL2 r2 z  yR1 r2 z"
  shows "((L1⪅) ∘∘ (L2⪅))  (L⪅)"
proof (rule le_relI)
  fix x z assume "((L1⪅) ∘∘ (L2⪅)) x z"
  then obtain y where "x L1y" "y L2z" by blast
  then have "xL1 r1 y" "yL2 r2 z" "in_codom (≤R) z" by auto
  with R1_r2_if_in_codom have "yR1 r2 z" by blast
  with mono_r1 have "r1 yL1 r z" by auto
  with xL1 r1 y in_codom (≤R) z show "x Lz" 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 zL2 r2 z"
  and "y z. in_codom (≤R2) z  yL2 r2 z  yR1 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  yL2 r2 z  yR1 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  yL2 r2 z  yR1 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