(* Copyright 2021 (C) Mihails Milehins *)



The methodology for the exposition of GRPH› as a category is analogous to
the one used in cite"milehins_category_2021"
for the exposition of GRPH› as a semicategory.

named_theorems cat_GRPH_simps
named_theorems cat_GRPH_intros

subsection‹Definition and elementary properties›

definition cat_GRPH :: "V  V"
  where "cat_GRPH α =
      set {. digraph α }, 
      all_dghms α, 
      (λ𝔉all_dghms α. 𝔉HomDom), 
      (λ𝔉all_dghms α. 𝔉HomCod),
      (λ𝔊𝔉composable_arrs (dg_GRPH α). 𝔊𝔉0 DGHM 𝔊𝔉1),
      (λset {. digraph α }. dghm_id )


lemma cat_GRPH_components:
  shows "cat_GRPH αObj = set {. digraph α }"
    and "cat_GRPH αArr = all_dghms α"
    and "cat_GRPH αDom = (λ𝔉all_dghms α. 𝔉HomDom)"
    and "cat_GRPH αCod = (λ𝔉all_dghms α. 𝔉HomCod)"
    and "cat_GRPH αComp =
      (λ𝔊𝔉composable_arrs (dg_GRPH α). 𝔊𝔉0 DGHM 𝔊𝔉1)"
    and "cat_GRPH αCId = (λset {. digraph α }. dghm_id )"
  unfolding cat_GRPH_def dg_field_simps by (simp_all add: nat_omega_simps)


lemma cat_smc_GRPH: "cat_smc (cat_GRPH α) = smc_GRPH α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟 (cat_smc (cat_GRPH α)) = 5" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟 (smc_GRPH α) = 5"
    unfolding smc_GRPH_def by (simp add: nat_omega_simps)
  show "𝒟 (cat_smc (cat_GRPH α)) = 𝒟 (smc_GRPH α)"
    unfolding dom_lhs dom_rhs by simp
    "a  𝒟 (cat_smc (cat_GRPH α))  cat_smc (cat_GRPH α)a = smc_GRPH αa"
    for a
        unfold dom_lhs, 
        unfold cat_smc_def dg_field_simps cat_GRPH_def smc_GRPH_def
      (auto simp: nat_omega_simps)
qed (auto simp: cat_smc_def smc_GRPH_def)

lemmas_with [folded cat_smc_GRPH, unfolded slicing_simps]: 
  cat_GRPH_ObjI = smc_GRPH_ObjI
  and cat_GRPH_ObjD = smc_GRPH_ObjD
  and cat_GRPH_ObjE = smc_GRPH_ObjE
  and cat_GRPH_Obj_iff[cat_GRPH_simps] = smc_GRPH_Obj_iff  
  and cat_GRPH_Dom_app[cat_GRPH_simps] = smc_GRPH_Dom_app
  and cat_GRPH_Cod_app[cat_GRPH_simps] = smc_GRPH_Cod_app
  and cat_GRPH_is_arrI = smc_GRPH_is_arrI
  and cat_GRPH_is_arrD = smc_GRPH_is_arrD
  and cat_GRPH_is_arrE = smc_GRPH_is_arrE
  and cat_GRPH_is_arr_iff[cat_GRPH_simps] = smc_GRPH_is_arr_iff

lemmas_with [folded cat_smc_GRPH, unfolded slicing_simps, unfolded cat_smc_GRPH]: 
  cat_GRPH_Comp_vdomain = smc_GRPH_Comp_vdomain
  and cat_GRPH_composable_arrs_dg_GRPH = smc_GRPH_composable_arrs_dg_GRPH
  and cat_GRPH_Comp = smc_GRPH_Comp
  and cat_GRPH_Comp_app[cat_GRPH_simps] = smc_GRPH_Comp_app

lemmas_with (in 𝒵) [folded cat_smc_GRPH, unfolded slicing_simps]: 
  cat_GRPH_obj_initialI = smc_GRPH_obj_initialI
  and cat_GRPH_obj_initialD = smc_GRPH_obj_initialD
  and cat_GRPH_obj_initialE = smc_GRPH_obj_initialE
  and cat_GRPH_obj_initial_iff[cat_GRPH_simps] = smc_GRPH_obj_initial_iff
  and cat_GRPH_obj_terminalI = smc_GRPH_obj_terminalI
  and cat_GRPH_obj_terminalE = smc_GRPH_obj_terminalE


lemma cat_GRPH_CId_app[cat_GRPH_simps]: 
  assumes "digraph α "
  shows "cat_GRPH αCId = dghm_id "
  using assms unfolding cat_GRPH_components by simp

lemma cat_GRPH_CId_vdomain: "𝒟 (cat_GRPH αCId) = set {. digraph α }"
  unfolding cat_GRPH_components by auto

lemma cat_GRPH_CId_vrange: " (cat_GRPH αCId)  all_dghms α"
proof(rule vsubsetI)
  fix  assume "   (cat_GRPH αCId)"
  then obtain 𝔄 
    where ℌ_def: " = cat_GRPH αCId𝔄" and 𝔄: "𝔄  𝒟 (cat_GRPH αCId)"
    unfolding cat_GRPH_components by auto
  from 𝔄 have ℌ_def': " = dghm_id 𝔄" 
    unfolding ℌ_def cat_GRPH_CId_vdomain by (auto simp: cat_GRPH_CId_app)
  from 𝔄 digraph.dg_dghm_id_is_dghm show "  all_dghms α" 
    unfolding ℌ_def' cat_GRPH_CId_vdomain by force

subsectionGRPH› is a category›

lemma (in 𝒵) tiny_category_cat_GRPH: 
  assumes "𝒵 β" and "α  β"
  shows "tiny_category β (cat_GRPH α)"
proof(intro tiny_categoryI)
  interpret β: 𝒵 β by (rule assms(1))
  show "vfsequence (cat_GRPH α)" unfolding cat_GRPH_def by simp
  show "vcard (cat_GRPH α) = 6"
    unfolding cat_GRPH_def by (simp add: nat_omega_simps)
  show "cat_GRPH αCId𝔅 Acat_GRPH α𝔉 = 𝔉"
    if "𝔉 : 𝔄 cat_GRPH α𝔅" for 𝔉 𝔄 𝔅
    using that
    unfolding cat_GRPH_is_arr_iff
    by (cs_concl cs_simp: dg_cs_simps cat_GRPH_simps cs_intro: dg_cs_intros)
  show "𝔉 Acat_GRPH αcat_GRPH αCId𝔅 = 𝔉"
    if "𝔉 : 𝔅 cat_GRPH α" for 𝔉 𝔅 
    using that
    unfolding cat_GRPH_is_arr_iff
    by (cs_concl cs_simp: dg_cs_simps cat_GRPH_simps cs_intro: dg_cs_intros)
    simp_all add: 


lemma cat_GRPH_is_iso_arrI: 
  assumes "𝔉 : 𝔄 ↦↦DG.isoα𝔅"
  shows "𝔉 : 𝔄 isocat_GRPH α𝔅"
proof(intro is_iso_arrI is_inverseI)
  from assms show 𝔉: "𝔉 : 𝔄 cat_GRPH α𝔅"
    unfolding cat_GRPH_is_arr_iff by auto
  note iso_thms = is_iso_dghm_is_iso_arr[OF assms]
  from iso_thms(1) show inv_𝔉: "inv_dghm 𝔉 : 𝔅 cat_GRPH α𝔄"
    unfolding cat_GRPH_is_arr_iff by auto
  from assms show "𝔉 : 𝔄 cat_GRPH α𝔅"
    unfolding cat_GRPH_is_arr_iff by auto
  from assms have 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" by auto
  show "inv_dghm 𝔉 Acat_GRPH α𝔉 = cat_GRPH αCId𝔄"
    unfolding cat_GRPH_CId_app[OF 𝔄] cat_GRPH_Comp_app[OF inv_𝔉 𝔉]
    by (rule iso_thms(2))
  show "𝔉 Acat_GRPH αinv_dghm 𝔉 = cat_GRPH αCId𝔅"
    unfolding cat_GRPH_CId_app[OF 𝔅] cat_GRPH_Comp_app[OF 𝔉 inv_𝔉]
    by (rule iso_thms(3))

lemma cat_GRPH_is_iso_arrD: 
  assumes "𝔉 : 𝔄 isocat_GRPH α𝔅"
  shows "𝔉 : 𝔄 ↦↦DG.isoα𝔅"
  from is_iso_arrD[OF assms] have 𝔉: "𝔉 : 𝔄 cat_GRPH α𝔅" 
    and "(𝔊. is_inverse (cat_GRPH α) 𝔊 𝔉)"
    by simp_all
  then obtain 𝔊 where 𝔊𝔉: "is_inverse (cat_GRPH α) 𝔊 𝔉" by clarsimp
  then obtain 𝔄' 𝔅' where 𝔊': "𝔊 : 𝔅' cat_GRPH α𝔄'"
    and 𝔉': "𝔉 : 𝔄' cat_GRPH α𝔅'"
    and 𝔊𝔉: "𝔊 Acat_GRPH α𝔉 = cat_GRPH αCId𝔄'"
    and 𝔉𝔊: "𝔉 Acat_GRPH α𝔊 = cat_GRPH αCId𝔅'"
    by auto
  from 𝔉 𝔉' have 𝔄': "𝔄' = 𝔄" and 𝔅': "𝔅' = 𝔅" by auto  
  from 𝔉 have 𝔉: "𝔉 : 𝔄 ↦↦DGα𝔅" unfolding cat_GRPH_is_arr_iff by simp
  then have 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" by auto
  from 𝔊' have "𝔊 : 𝔅 ↦↦DGα𝔄" 
    unfolding 𝔄' 𝔅' cat_GRPH_is_arr_iff by simp
  moreover from 𝔊𝔉 have "𝔊 DGHM 𝔉 = dghm_id 𝔄"
    unfolding 𝔄' cat_GRPH_Comp_app[OF 𝔊' 𝔉'] cat_GRPH_CId_app[OF 𝔄] by simp
  moreover from 𝔉𝔊 have "𝔉 DGHM 𝔊 = dghm_id 𝔅"
    unfolding 𝔅' cat_GRPH_Comp_app[OF 𝔉' 𝔊'] cat_GRPH_CId_app[OF 𝔅] by simp
  ultimately show ?thesis using 𝔉 by (elim is_iso_arr_is_iso_dghm)

lemma cat_GRPH_is_iso_arrE: 
  assumes "𝔉 : 𝔄 isocat_GRPH α𝔅"
  obtains "𝔉 : 𝔄 ↦↦DG.isoα𝔅"
  using assms by (auto dest: cat_GRPH_is_iso_arrD)

lemma cat_GRPH_is_iso_arr_iff[cat_GRPH_simps]: 
  "𝔉 : 𝔄 isocat_GRPH α𝔅  𝔉 : 𝔄 ↦↦DG.isoα𝔅"
  using cat_GRPH_is_iso_arrI cat_GRPH_is_iso_arrD by auto

subsection‹Isomorphic objects›

lemma cat_GRPH_obj_isoI: 
  assumes "𝔄 DGα𝔅"
  shows "𝔄 objcat_GRPH α𝔅"
  from iso_digraphD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 ↦↦DG.isoα𝔅"
    by clarsimp
  from cat_GRPH_is_iso_arrI[OF this] show ?thesis by (rule obj_isoI)

lemma cat_GRPH_obj_isoD: 
  assumes "𝔄 objcat_GRPH α𝔅"
  shows "𝔄 DGα𝔅"
  from obj_isoD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 isocat_GRPH α𝔅" 
    by clarsimp
  from cat_GRPH_is_iso_arrD[OF this] show ?thesis
    by (rule iso_digraphI)

lemma cat_GRPH_obj_isoE: 
  assumes "𝔄 objcat_GRPH α𝔅"
  obtains "𝔄 DGα𝔅"
  using assms by (auto simp: cat_GRPH_obj_isoD)

lemma cat_GRPH_obj_iso_iff: "𝔄 objcat_GRPH α𝔅  𝔄 DGα𝔅"
  using cat_GRPH_obj_isoI cat_GRPH_obj_isoD by (intro iffI) auto