Theory Transport_Natural_Functors_Galois_Relator

✐‹creator "Kevin Kappelmann"›
subsection ‹Galois Relator›
theory Transport_Natural_Functors_Galois_Relator
  imports
    Transport_Natural_Functors_Base
begin

context transport_natural_functor
begin

lemma left_Galois_Frel_left_Galois: "(⇘L⇙⪅) ≤ Frel (⇘L1⇙⪅) (⇘L2⇙⪅) (⇘L3⇙⪅)"
  apply (rule le_relI)
  apply (erule left_GaloisE)
  apply (unfold left_rel_eq_Frel right_rel_eq_Frel right_eq_Fmap)
  apply (subst (asm) in_codom_Frel_eq_Fpred_in_codom)
  apply (erule FpredE)
  apply (subst (asm) Frel_Fmap_eq2)
  apply (rule Frel_mono_strong,
    assumption;
    rule t1.left_GaloisI t2.left_GaloisI t3.left_GaloisI;
    assumption)
  done

lemma Frel_left_Galois_le_left_Galois:
  "Frel (⇘L1⇙⪅) (⇘L2⇙⪅) (⇘L3⇙⪅) ≤ (⇘L⇙⪅)"
  apply (rule le_relI)
  apply (unfold t1.left_Galois_iff_in_codom_and_left_rel_right
    t2.left_Galois_iff_in_codom_and_left_rel_right
    t3.left_Galois_iff_in_codom_and_left_rel_right)
  apply (fold
    rel_restrict_right_eq[of "λx y. x ≤⇘L1⇙ r1 y" "in_codom (≤⇘R1⇙)",
      unfolded rel_restrict_left_pred_def rel_inv_iff_rel]
    rel_restrict_right_eq[of "λx y. x ≤⇘L2⇙ r2 y" "in_codom (≤⇘R2⇙)",
      unfolded rel_restrict_left_pred_def rel_inv_iff_rel]
    rel_restrict_right_eq[of "λx y. x ≤⇘L3⇙ r3 y" "in_codom (≤⇘R3⇙)",
      unfolded rel_restrict_left_pred_def rel_inv_iff_rel])
  apply (subst (asm) Frel_restrict_right_Fpred_eq_Frel_restrict_right[symmetric])
  apply (erule rel_restrict_rightE)
  apply (subst (asm) in_codom_Frel_eq_Fpred_in_codom[symmetric])
  apply (erule in_codomE)
  apply (rule left_GaloisI)
    apply (rule in_codomI)
    apply (subst right_rel_eq_Frel)
    apply assumption
    apply (unfold left_rel_eq_Frel right_eq_Fmap Frel_Fmap_eq2)
    apply assumption
  done

corollary left_Galois_eq_Frel_left_Galois: "(⇘L⇙⪅) = Frel (⇘L1⇙⪅) (⇘L2⇙⪅) (⇘L3⇙⪅)"
  by (intro antisym left_Galois_Frel_left_Galois Frel_left_Galois_le_left_Galois)

end


end