Theory CZH_ECAT_GRPH

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹GRPH››
theory CZH_ECAT_GRPH
  imports 
    CZH_ECAT_Small_Category
    CZH_Foundations.CZH_SMC_GRPH
begin



subsection‹Background›


text‹
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⦈ ∘⇩D⇩G⇩H⇩M 𝔊𝔉⦇1⇩ℕ⦈),
      (λℭ∈⇩∘set {ℭ. digraph α ℭ}. dghm_id ℭ)
    ]⇩∘"


text‹Components.›

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⦈ ∘⇩D⇩G⇩H⇩M 𝔊𝔉⦇1⇩ℕ⦈)"
    and "cat_GRPH α⦇CId⦈ = (λℭ∈⇩∘set {ℭ. digraph α ℭ}. dghm_id ℭ)"
  unfolding cat_GRPH_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

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
  show 
    "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_GRPH α)) ⟹ cat_smc (cat_GRPH α)⦇a⦈ = smc_GRPH α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        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]: 
  ―‹Digraph›
  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]: 
  ―‹Semicategory›
  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]: 
  ―‹Semicategory›
  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


subsection‹Identity›

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
qed



subsection‹‹GRPH› 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⦈⦇𝔅⦈ ∘⇩A⇘cat_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 "𝔉 ∘⇩A⇘cat_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)
qed
  (
    simp_all add: 
      assms
      cat_smc_GRPH
      cat_GRPH_components
      digraph.dg_dghm_id_is_dghm
      cat_GRPH_is_arr_iff
      tiny_semicategory_smc_GRPH
  )



subsection‹Isomorphism›

lemma cat_GRPH_is_iso_arrI: 
  assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_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 𝔉 ∘⇩A⇘cat_GRPH α⇙ 𝔉 = cat_GRPH α⦇CId⦈⦇𝔄⦈"
    unfolding cat_GRPH_CId_app[OF 𝔄] cat_GRPH_Comp_app[OF inv_𝔉 𝔉]
    by (rule iso_thms(2))
  show "𝔉 ∘⇩A⇘cat_GRPH α⇙ inv_dghm 𝔉 = cat_GRPH α⦇CId⦈⦇𝔅⦈"
    unfolding cat_GRPH_CId_app[OF 𝔅] cat_GRPH_Comp_app[OF 𝔉 inv_𝔉]
    by (rule iso_thms(3))
qed

lemma cat_GRPH_is_iso_arrD: 
  assumes "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_GRPH α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
proof-
  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 𝔊𝔉: "𝔊 ∘⇩A⇘cat_GRPH α⇙ 𝔉 = cat_GRPH α⦇CId⦈⦇𝔄'⦈"
    and 𝔉𝔊: "𝔉 ∘⇩A⇘cat_GRPH α⇙ 𝔊 = cat_GRPH α⦇CId⦈⦇𝔅'⦈"
    by auto
  from 𝔉 𝔉' have 𝔄': "𝔄' = 𝔄" and 𝔅': "𝔅' = 𝔅" by auto  
  from 𝔉 have 𝔉: "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" unfolding cat_GRPH_is_arr_iff by simp
  then have 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" by auto
  from 𝔊' have "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ 𝔄" 
    unfolding 𝔄' 𝔅' cat_GRPH_is_arr_iff by simp
  moreover from 𝔊𝔉 have "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 = dghm_id 𝔄"
    unfolding 𝔄' cat_GRPH_Comp_app[OF 𝔊' 𝔉'] cat_GRPH_CId_app[OF 𝔄] by simp
  moreover from 𝔉𝔊 have "𝔉 ∘⇩D⇩G⇩H⇩M 𝔊 = 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)
qed

lemma cat_GRPH_is_iso_arrE: 
  assumes "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_GRPH α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using assms by (auto dest: cat_GRPH_is_iso_arrD)

lemma cat_GRPH_is_iso_arr_iff[cat_GRPH_simps]: 
  "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_GRPH α⇙ 𝔅 ⟷ 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using cat_GRPH_is_iso_arrI cat_GRPH_is_iso_arrD by auto



subsection‹Isomorphic objects›

lemma cat_GRPH_obj_isoI: 
  assumes "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
  shows "𝔄 ≈⇩o⇩b⇩j⇘cat_GRPH α⇙ 𝔅"
proof-
  from iso_digraphD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
    by clarsimp
  from cat_GRPH_is_iso_arrI[OF this] show ?thesis by (rule obj_isoI)
qed

lemma cat_GRPH_obj_isoD: 
  assumes "𝔄 ≈⇩o⇩b⇩j⇘cat_GRPH α⇙ 𝔅"
  shows "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
proof-
  from obj_isoD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_GRPH α⇙ 𝔅" 
    by clarsimp
  from cat_GRPH_is_iso_arrD[OF this] show ?thesis
    by (rule iso_digraphI)
qed

lemma cat_GRPH_obj_isoE: 
  assumes "𝔄 ≈⇩o⇩b⇩j⇘cat_GRPH α⇙ 𝔅"
  obtains "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
  using assms by (auto simp: cat_GRPH_obj_isoD)

lemma cat_GRPH_obj_iso_iff: "𝔄 ≈⇩o⇩b⇩j⇘cat_GRPH α⇙ 𝔅 ⟷ 𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
  using cat_GRPH_obj_isoI cat_GRPH_obj_isoD by (intro iffI) auto

text‹\newpage›

end