Theory CZH_DG_GRPH

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹GRPH› as a digraph›
theory CZH_DG_GRPH
  imports 
    CZH_DG_DGHM
    CZH_DG_Small_Digraph
begin



subsection‹Background›


text‹
Conventionally, ‹GRPH› defined as a category of digraphs and digraph 
homomorphisms (e.g., see Chapter II-7 in \<^cite>‹"mac_lane_categories_2010"›).
However, there is little that can prevent one from exposing ‹GRPH›
as a digraph and provide additional structure gradually later. 
Thus, in this section, ‹α›-‹GRPH› is 
defined as a digraph of digraphs and digraph homomorphisms in ‹V⇩α›.
›

named_theorems GRPH_cs_simps
named_theorems GRPH_cs_intros



subsection‹Definition and elementary properties›

definition dg_GRPH :: "V ⇒ V"
  where "dg_GRPH α =
    [
      set {ℭ. digraph α ℭ},
      all_dghms α,
      (λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomDom⦈),
      (λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomCod⦈)
    ]⇩∘"


text‹Components.›

lemma dg_GRPH_components:
  shows "dg_GRPH α⦇Obj⦈ = set {ℭ. digraph α ℭ}"
    and "dg_GRPH α⦇Arr⦈ = all_dghms α"
    and "dg_GRPH α⦇Dom⦈ = (λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomDom⦈)"
    and "dg_GRPH α⦇Cod⦈ = (λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomCod⦈)"
  unfolding dg_GRPH_def dg_field_simps by (simp_all add: nat_omega_simps)



subsection‹Object›

lemma dg_GRPH_ObjI:
  assumes "digraph α 𝔄"
  shows "𝔄 ∈⇩∘ dg_GRPH α⦇Obj⦈"
  using assms unfolding dg_GRPH_components by auto

lemma dg_GRPH_ObjD:
  assumes "𝔄 ∈⇩∘ dg_GRPH α⦇Obj⦈"
  shows "digraph α 𝔄"
  using assms unfolding dg_GRPH_components by auto

lemma dg_GRPH_ObjE:
  assumes "𝔄 ∈⇩∘ dg_GRPH α⦇Obj⦈"
  obtains "digraph α 𝔄"
  using assms unfolding dg_GRPH_components by auto

lemma dg_GRPH_Obj_iff[GRPH_cs_simps]: 
  "𝔄 ∈⇩∘ dg_GRPH α⦇Obj⦈ ⟷ digraph α 𝔄"
  unfolding dg_GRPH_components by auto



subsection‹Domain›

mk_VLambda dg_GRPH_components(3)
  |vsv dg_GRPH_Dom_vsv[GRPH_cs_intros]|
  |vdomain dg_GRPH_Dom_vdomain[GRPH_cs_simps]|
  |app dg_GRPH_Dom_app[GRPH_cs_simps]|

lemma dg_GRPH_Dom_vrange: "ℛ⇩∘ (dg_GRPH α⦇Dom⦈) ⊆⇩∘ dg_GRPH α⦇Obj⦈"
  unfolding dg_GRPH_components by (rule vrange_VLambda_vsubset) auto



subsection‹Codomain›

mk_VLambda dg_GRPH_components(4)
  |vsv dg_GRPH_Cod_vsv[GRPH_cs_intros]|
  |vdomain dg_GRPH_Cod_vdomain[GRPH_cs_simps]|
  |app dg_GRPH_Cod_app[GRPH_cs_simps]|

lemma dg_GRPH_Cod_vrange: "ℛ⇩∘ (dg_GRPH α⦇Cod⦈) ⊆⇩∘ dg_GRPH α⦇Obj⦈"
  unfolding dg_GRPH_components by (rule vrange_VLambda_vsubset) auto



subsection‹‹GRPH› is a digraph›

lemma (in 𝒵) tiny_digraph_dg_GRPH: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_digraph β (dg_GRPH α)"
proof(intro tiny_digraphI)
  show "vfsequence (dg_GRPH α)" unfolding dg_GRPH_def by simp
  show "vcard (dg_GRPH α) = 4⇩ℕ"
    unfolding dg_GRPH_def by (simp add: nat_omega_simps)
  show "ℛ⇩∘ (dg_GRPH α⦇Dom⦈) ⊆⇩∘ dg_GRPH α⦇Obj⦈" by (simp add: dg_GRPH_Dom_vrange)
  show "ℛ⇩∘ (dg_GRPH α⦇Cod⦈) ⊆⇩∘ dg_GRPH α⦇Obj⦈" by (simp add: dg_GRPH_Cod_vrange)
  show "dg_GRPH α⦇Obj⦈ ∈⇩∘ Vset β"
    unfolding dg_GRPH_components by (rule digraphs_in_Vset[OF assms])
  show "dg_GRPH α⦇Arr⦈ ∈⇩∘ Vset β"
    unfolding dg_GRPH_components by (rule all_dghms_in_Vset[OF assms])
qed (auto simp: assms dg_GRPH_components)



subsection‹Arrow with a domain and a codomain›

lemma dg_GRPH_is_arrI:
  assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" 
  shows "𝔉 : 𝔄 ↦⇘dg_GRPH α⇙ 𝔅"
proof(intro is_arrI; unfold dg_GRPH_components)
  from assms show "𝔉 ∈⇩∘ all_dghms α" by auto
  with assms show 
    "(λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomDom⦈)⦇𝔉⦈ = 𝔄" 
    "(λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomCod⦈)⦇𝔉⦈ = 𝔅"
    by (auto simp: GRPH_cs_simps)
qed

lemma dg_GRPH_is_arrD:
  assumes "𝔉 : 𝔄 ↦⇘dg_GRPH α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" 
  using assms by (elim is_arrE) (auto simp: dg_GRPH_components)

lemma dg_GRPH_is_arrE:
  assumes "𝔉 : 𝔄 ↦⇘dg_GRPH α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  using assms by (simp add: dg_GRPH_is_arrD)

lemma dg_GRPH_is_arr_iff[GRPH_cs_simps]: 
  "𝔉 : 𝔄 ↦⇘dg_GRPH α⇙ 𝔅 ⟷ 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" 
  by (auto intro: dg_GRPH_is_arrI dest: dg_GRPH_is_arrD)

text‹\newpage›

end