Theory CZH_DG_CAT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹CAT› as a digraph\label{sec:dg_CAT}›
theory CZH_DG_CAT
  imports 
    CZH_ECAT_Functor
    CZH_ECAT_Small_Category
begin



subsection‹Background›


text‹
‹CAT› is usually defined as a category of categories and functors
(e.g., see Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›).
However, there is little that can prevent one from exposing ‹CAT›
as a digraph and provide additional structure gradually in
subsequent theories. 
Thus, in this section, ‹α›-‹CAT› is defined as a digraph of categories 
and functors in the set ‹V⇩α›, and ‹α›-‹Cat› is defined
as a digraph of tiny categories and tiny functors in ‹V⇩α›.
›

named_theorems dg_CAT_simps
named_theorems dg_CAT_intros



subsection‹Definition and elementary properties›

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


text‹Components.›

lemma dg_CAT_components:
  shows "dg_CAT α⦇Obj⦈ = set {ℭ. category α ℭ}"
    and "dg_CAT α⦇Arr⦈ = all_cfs α"
    and "dg_CAT α⦇Dom⦈ = (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomDom⦈)"
    and "dg_CAT α⦇Cod⦈ = (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomCod⦈)"
  unfolding dg_CAT_def dg_field_simps by (simp_all add: nat_omega_simps)



subsection‹Object›

lemma dg_CAT_ObjI:
  assumes "category α 𝔄"
  shows "𝔄 ∈⇩∘ dg_CAT α⦇Obj⦈"
  using assms unfolding dg_CAT_components by auto

lemma dg_CAT_ObjD:
  assumes "𝔄 ∈⇩∘ dg_CAT α⦇Obj⦈"
  shows "category α 𝔄"
  using assms unfolding dg_CAT_components by auto

lemma dg_CAT_ObjE:
  assumes "𝔄 ∈⇩∘ dg_CAT α⦇Obj⦈"
  obtains "category α 𝔄"
  using assms unfolding dg_CAT_components by auto

lemma dg_CAT_Obj_iff[dg_CAT_simps]: "𝔄 ∈⇩∘ dg_CAT α⦇Obj⦈ ⟷ category α 𝔄"
  unfolding dg_CAT_components by auto



subsection‹Domain and codomain›

lemma [dg_CAT_simps]:
  assumes "𝔉 ∈⇩∘ all_cfs α"  
  shows dg_CAT_Dom_app: "dg_CAT α⦇Dom⦈⦇𝔉⦈ = 𝔉⦇HomDom⦈"
    and dg_CAT_Cod_app: "dg_CAT α⦇Cod⦈⦇𝔉⦈ = 𝔉⦇HomCod⦈"
  using assms unfolding dg_CAT_components by auto



subsection‹‹CAT› is a digraph›

lemma (in 𝒵) tiny_category_dg_CAT: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_digraph β (dg_CAT α)"
proof(intro tiny_digraphI)
  interpret β: 𝒵 β by (rule assms(1))
  show "vfsequence (dg_CAT α)" unfolding dg_CAT_def by simp
  show "vcard (dg_CAT α) = 4⇩ℕ"
    unfolding dg_CAT_def by (simp add: nat_omega_simps)
  show "ℛ⇩∘ (dg_CAT α⦇Dom⦈) ⊆⇩∘ dg_CAT α⦇Obj⦈" 
  proof(intro vsubsetI)
    fix 𝔄 assume "𝔄 ∈⇩∘ ℛ⇩∘ (dg_CAT α⦇Dom⦈)"
    then obtain 𝔉 where "𝔉 ∈⇩∘ all_cfs α" and "𝔄 = 𝔉⦇HomDom⦈"
      unfolding dg_CAT_components by auto
    then obtain 𝔅 𝔉 where "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
      unfolding dg_CAT_components by auto
    then interpret is_functor α 𝔄 𝔅 𝔉 by simp
    show "𝔄 ∈⇩∘ dg_CAT α⦇Obj⦈"
      by (simp add: dg_CAT_components HomDom.category_axioms)
  qed
  show "ℛ⇩∘ (dg_CAT α⦇Cod⦈) ⊆⇩∘ dg_CAT α⦇Obj⦈"
  proof(intro vsubsetI)
    fix 𝔅 assume "𝔅 ∈⇩∘ ℛ⇩∘ (dg_CAT α⦇Cod⦈)"
    then obtain 𝔉 where "𝔉 ∈⇩∘ 𝒟⇩∘ (dg_CAT α⦇Cod⦈)" and "𝔅 = 𝔉⦇HomCod⦈"
      unfolding dg_CAT_components by auto
    then obtain 𝔄 𝔉 
      where 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and 𝔅_def: "𝔅 = 𝔉⦇HomCod⦈"
      unfolding dg_CAT_components by auto
    have "𝔅 = 𝔉⦇HomCod⦈" unfolding 𝔅_def by simp
    interpret is_functor α 𝔄 𝔅 𝔉 by (rule 𝔉)
    show "𝔅 ∈⇩∘ dg_CAT α⦇Obj⦈"
      by (simp add: HomCod.category_axioms dg_CAT_components)
  qed
  show "dg_CAT α⦇Obj⦈ ∈⇩∘ Vset β"
    unfolding dg_CAT_components by (rule categories_in_Vset[OF assms])
  show "dg_CAT α⦇Arr⦈ ∈⇩∘ Vset β"
    unfolding dg_CAT_components by (rule all_cfs_in_Vset[OF assms])
qed (simp_all add: assms dg_CAT_components)



subsection‹Arrow with a domain and a codomain›

lemma dg_CAT_is_arrI:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
  shows "𝔉 : 𝔄 ↦⇘dg_CAT α⇙ 𝔅"
proof(intro is_arrI, unfold dg_CAT_components(2))
  interpret is_functor α 𝔄 𝔅 𝔉 by (rule assms)
  from assms show "𝔉 ∈⇩∘ all_cfs α" by auto
  with assms show "dg_CAT α⦇Dom⦈⦇𝔉⦈ = 𝔄" "dg_CAT α⦇Cod⦈⦇𝔉⦈ = 𝔅"
    by (simp_all add: dg_CAT_components cat_cs_simps)
qed 

lemma dg_CAT_is_arrD:
  assumes "𝔉 : 𝔄 ↦⇘dg_CAT α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
  using assms by (elim is_arrE) (auto simp: dg_CAT_components)

lemma dg_CAT_is_arrE:
  assumes "𝔉 : 𝔄 ↦⇘dg_CAT α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms by (simp add: dg_CAT_is_arrD)

lemma dg_CAT_is_arr_iff[dg_CAT_simps]: 
  "𝔉 : 𝔄 ↦⇘dg_CAT α⇙ 𝔅 ⟷ 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
  by (auto intro: dg_CAT_is_arrI dest: dg_CAT_is_arrD)

text‹\newpage›

end