Theory CZH_DG_SemiCAT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹SemiCAT› as a digraph\label{sec:dg_SemiCAT}›
theory CZH_DG_SemiCAT
  imports 
    CZH_SMC_Semifunctor
    CZH_DG_Small_Digraph
begin



subsection‹Background›


text‹
‹SemiCAT› is usually defined as a category of semicategories and semifunctors
(e.g., see \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/semicategory}
}).
However, there is little that can prevent one from exposing ‹SemiCAT›
as a digraph and provide additional structure gradually in
subsequent theories. Thus, in this section, ‹α›-‹SemiCAT› is defined as a 
digraph of semicategories and semifunctors in ‹V⇩α›.
›

named_theorems dg_SemiCAT_simps
named_theorems dg_SemiCAT_intros



subsection‹Definition and elementary properties›

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


text‹Components.›

lemma dg_SemiCAT_components:
  shows "dg_SemiCAT α⦇Obj⦈ = set {ℭ. semicategory α ℭ}"
    and "dg_SemiCAT α⦇Arr⦈ = all_smcfs α"
    and "dg_SemiCAT α⦇Dom⦈ = (λ𝔉∈⇩∘all_smcfs α. 𝔉⦇HomDom⦈)"
    and "dg_SemiCAT α⦇Cod⦈ = (λ𝔉∈⇩∘all_smcfs α. 𝔉⦇HomCod⦈)"
  unfolding dg_SemiCAT_def dg_field_simps by (simp_all add: nat_omega_simps)


subsection‹Object›

lemma dg_SemiCAT_ObjI:
  assumes "semicategory α 𝔄"
  shows "𝔄 ∈⇩∘ dg_SemiCAT α⦇Obj⦈"
  using assms unfolding dg_SemiCAT_components by auto

lemma dg_SemiCAT_ObjD:
  assumes "𝔄 ∈⇩∘ dg_SemiCAT α⦇Obj⦈"
  shows "semicategory α 𝔄"
  using assms unfolding dg_SemiCAT_components by auto

lemma dg_SemiCAT_ObjE:
  assumes "𝔄 ∈⇩∘ dg_SemiCAT α⦇Obj⦈"
  obtains "semicategory α 𝔄"
  using assms unfolding dg_SemiCAT_components by auto

lemma dg_SemiCAT_Obj_iff[dg_SemiCAT_simps]: 
  "𝔄 ∈⇩∘ dg_SemiCAT α⦇Obj⦈ ⟷ semicategory α 𝔄"
  unfolding dg_SemiCAT_components by auto



subsection‹Domain and codomain›

lemma [dg_SemiCAT_simps]:
  assumes "𝔉 ∈⇩∘ all_smcfs α"  
  shows dg_SemiCAT_Dom_app: "dg_SemiCAT α⦇Dom⦈⦇𝔉⦈ = 𝔉⦇HomDom⦈"
    and dg_SemiCAT_Cod_app: "dg_SemiCAT α⦇Cod⦈⦇𝔉⦈ = 𝔉⦇HomCod⦈"
  using assms unfolding dg_SemiCAT_components by auto



subsection‹‹SemiCAT› is a digraph›

lemma (in 𝒵) tiny_digraph_dg_SemiCAT: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_digraph β (dg_SemiCAT α)"
proof(intro tiny_digraphI)
  show "vfsequence (dg_SemiCAT α)" unfolding dg_SemiCAT_def by simp
  show "vcard (dg_SemiCAT α) = 4⇩ℕ"
    unfolding dg_SemiCAT_def by (simp add: nat_omega_simps)
  show "ℛ⇩∘ (dg_SemiCAT α⦇Dom⦈) ⊆⇩∘ dg_SemiCAT α⦇Obj⦈" 
  proof(intro vsubsetI)
    fix 𝔄 assume "𝔄 ∈⇩∘ ℛ⇩∘ (dg_SemiCAT α⦇Dom⦈)"
    then obtain 𝔉 
      where "𝔉 ∈⇩∘ all_smcfs α" and 𝔄_def: "𝔄 = 𝔉⦇HomDom⦈"
      unfolding dg_SemiCAT_components by auto
    then obtain 𝔅 𝔉 where "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
      unfolding dg_SemiCAT_components by auto
    then interpret is_semifunctor α 𝔄 𝔅 𝔉 .
    show "𝔄 ∈⇩∘ dg_SemiCAT α⦇Obj⦈"
      by (simp add: dg_SemiCAT_components HomDom.semicategory_axioms)
  qed
  show "ℛ⇩∘ (dg_SemiCAT α⦇Cod⦈) ⊆⇩∘ dg_SemiCAT α⦇Obj⦈"
  proof(intro vsubsetI)
    fix 𝔅 assume "𝔅 ∈⇩∘ ℛ⇩∘ (dg_SemiCAT α⦇Cod⦈)"
    then obtain 𝔉 where "𝔉 ∈⇩∘ 𝒟⇩∘ (dg_SemiCAT α⦇Cod⦈)" and "𝔅 = 𝔉⦇HomCod⦈"
      unfolding dg_SemiCAT_components by auto
    then obtain 𝔄 𝔉 
      where 𝔉: "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and 𝔄_def: "𝔅 = 𝔉⦇HomCod⦈"
      unfolding dg_SemiCAT_components by auto
    have "𝔅 = 𝔉⦇HomCod⦈" unfolding 𝔄_def by simp
    interpret is_semifunctor α 𝔄 𝔅 𝔉 by (rule 𝔉)
    show "𝔅 ∈⇩∘ dg_SemiCAT α⦇Obj⦈"
      by (simp add: HomCod.semicategory_axioms dg_SemiCAT_components)
  qed
  show "dg_SemiCAT α⦇Obj⦈ ∈⇩∘ Vset β"
    unfolding dg_SemiCAT_components by (rule semicategories_in_Vset[OF assms])
  show "dg_SemiCAT α⦇Arr⦈ ∈⇩∘ Vset β"
    unfolding dg_SemiCAT_components by (rule all_smcfs_in_Vset[OF assms])
qed (simp_all add: assms dg_SemiCAT_components)



subsection‹Arrow with a domain and a codomain›

lemma dg_SemiCAT_is_arrI:
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
  shows "𝔉 : 𝔄 ↦⇘dg_SemiCAT α⇙ 𝔅"
proof(intro is_arrI, unfold dg_SemiCAT_components(2))
  interpret is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms)
  from assms show "𝔉 ∈⇩∘ all_smcfs α" by auto
  with assms show "dg_SemiCAT α⦇Dom⦈⦇𝔉⦈ = 𝔄" "dg_SemiCAT α⦇Cod⦈⦇𝔉⦈ = 𝔅"
    by (simp_all add: smc_cs_simps dg_SemiCAT_components)
qed

lemma dg_SemiCAT_is_arrD:
  assumes "𝔉 : 𝔄 ↦⇘dg_SemiCAT α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
  using assms by (elim is_arrE) (auto simp: dg_SemiCAT_components)

lemma dg_SemiCAT_is_arrE:
  assumes "𝔉 : 𝔄 ↦⇘dg_SemiCAT α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  using assms by (simp add: dg_SemiCAT_is_arrD)

lemma dg_SemiCAT_is_arr_iff[dg_SemiCAT_simps]: 
  "𝔉 : 𝔄 ↦⇘dg_SemiCAT α⇙ 𝔅 ⟷ 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
  by (auto intro: dg_SemiCAT_is_arrI dest: dg_SemiCAT_is_arrD)

text‹\newpage›

end