Theory CZH_ECAT_CAT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹CAT››
theory CZH_ECAT_CAT
  imports CZH_SMC_CAT
begin



subsection‹Background›


text‹
The subsection presents the theory of the categories of ‹α›-categories.
It continues the development that was initiated in sections 
\ref{sec:dg_CAT}-\ref{sec:smc_CAT}.
›

named_theorems cat_CAT_simps
named_theorems cat_CAT_intros



subsection‹Definition and elementary properties›

definition cat_CAT :: "V ⇒ V"
  where "cat_CAT α =
    [
      set {ℭ. category α ℭ},
      all_cfs α, 
      (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomDom⦈),
      (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomCod⦈),
      (λ𝔊𝔉∈⇩∘composable_arrs (dg_CAT α). 𝔊𝔉⦇0⦈ ∘⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈),
      (λℭ∈⇩∘set {ℭ. category α ℭ}. cf_id ℭ)
    ]⇩∘"


text‹Components.›

lemma cat_CAT_components:
  shows "cat_CAT α⦇Obj⦈ = set {ℭ. category α ℭ}"
    and "cat_CAT α⦇Arr⦈ = all_cfs α"
    and "cat_CAT α⦇Dom⦈ = (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomDom⦈)"
    and "cat_CAT α⦇Cod⦈ = (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomCod⦈)"
    and "cat_CAT α⦇Comp⦈ = 
      (λ𝔊𝔉∈⇩∘composable_arrs (dg_CAT α). 𝔊𝔉⦇0⦈ ∘⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈)"
    and "cat_CAT α⦇CId⦈ = (λℭ∈⇩∘set {ℭ. category α ℭ}. cf_id ℭ)"
  unfolding cat_CAT_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_CAT: "cat_smc (cat_CAT α) = smc_CAT α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ (cat_smc (cat_CAT α)) = 5⇩ℕ" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smc_CAT α) = 5⇩ℕ"
    unfolding smc_CAT_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cat_smc (cat_CAT α)) = 𝒟⇩∘ (smc_CAT α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_CAT α)) ⟹ cat_smc (cat_CAT α)⦇a⦈ = smc_CAT α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold cat_smc_def dg_field_simps cat_CAT_def smc_CAT_def
      )
      (auto simp: nat_omega_simps)
qed (auto simp: cat_smc_def smc_CAT_def)

lemmas_with [folded cat_smc_CAT, unfolded slicing_simps]: 
  ―‹Digraph›
  cat_CAT_ObjI = smc_CAT_ObjI
  and cat_CAT_ObjD = smc_CAT_ObjD
  and cat_CAT_ObjE = smc_CAT_ObjE
  and cat_CAT_Obj_iff[cat_CAT_simps] = smc_CAT_Obj_iff  
  and cat_CAT_Dom_app[cat_CAT_simps] = smc_CAT_Dom_app
  and cat_CAT_Cod_app[cat_CAT_simps] = smc_CAT_Cod_app
  and cat_CAT_is_arrI = smc_CAT_is_arrI
  and cat_CAT_is_arrD = smc_CAT_is_arrD
  and cat_CAT_is_arrE = smc_CAT_is_arrE
  and cat_CAT_is_arr_iff[cat_CAT_simps] = smc_CAT_is_arr_iff

lemmas_with [folded cat_smc_CAT, unfolded slicing_simps, unfolded cat_smc_CAT]: 
  ―‹Semicategory›
  cat_CAT_Comp_vdomain = smc_CAT_Comp_vdomain
  and cat_CAT_composable_arrs_dg_CAT = smc_CAT_composable_arrs_dg_CAT
  and cat_CAT_Comp = smc_CAT_Comp
  and cat_CAT_Comp_app[cat_CAT_simps] = smc_CAT_Comp_app
  and cat_CAT_Comp_vrange = smc_CAT_Comp_vrange

lemmas_with (in 𝒵) [folded cat_smc_CAT, unfolded slicing_simps]: 
  ―‹Semicategory›
  cat_CAT_obj_initialI = smc_CAT_obj_initialI
  and cat_CAT_obj_initialD = smc_CAT_obj_initialD
  and cat_CAT_obj_initialE = smc_CAT_obj_initialE
  and cat_CAT_obj_initial_iff[cat_CAT_simps] = smc_CAT_obj_initial_iff
  and cat_CAT_obj_terminalI = smc_CAT_obj_terminalI
  and cat_CAT_obj_terminalE = smc_CAT_obj_terminalE



subsection‹Identity›

lemma cat_CAT_CId_app[cat_CAT_simps]: 
  assumes "category α ℭ"
  shows "cat_CAT α⦇CId⦈⦇ℭ⦈ = cf_id ℭ"
  using assms unfolding cat_CAT_components by simp

lemma cat_CAT_CId_vdomain: "𝒟⇩∘ (cat_CAT α⦇CId⦈) = set {ℭ. category α ℭ}"
  unfolding cat_CAT_components by auto

lemma cat_CAT_CId_vrange: "ℛ⇩∘ (cat_CAT α⦇CId⦈) ⊆⇩∘ all_cfs α"
proof(rule vsubsetI)
  fix ℌ assume "ℌ ∈⇩∘ ℛ⇩∘ (cat_CAT α⦇CId⦈)"
  then obtain 𝔄 
    where ℌ_def: "ℌ = cat_CAT α⦇CId⦈⦇𝔄⦈" 
      and 𝔄: "𝔄 ∈⇩∘ 𝒟⇩∘ (cat_CAT α⦇CId⦈)"
    unfolding cat_CAT_components by auto
  from 𝔄 have ℌ_def': "ℌ = cf_id 𝔄" 
    unfolding ℌ_def cat_CAT_CId_vdomain by (auto simp: cat_CAT_CId_app)
  from 𝔄 category.cat_cf_id_is_functor show "ℌ ∈⇩∘ all_cfs α"
    unfolding ℌ_def' cat_CAT_CId_vdomain by force
qed



subsection‹‹CAT› is a category›

lemma (in 𝒵) tiny_category_cat_CAT: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_category β (cat_CAT α)"
proof(intro tiny_categoryI)
  interpret β: 𝒵 β by (rule assms(1))
  show "vfsequence (cat_CAT α)" unfolding cat_CAT_def by simp
  show "vcard (cat_CAT α) = 6⇩ℕ"
    unfolding cat_CAT_def by (simp add: nat_omega_simps)
  show "𝔉 : 𝔄 ↦⇘cat_CAT α⇙ 𝔅 ⟹ cat_CAT α⦇CId⦈⦇𝔅⦈ ∘⇩A⇘cat_CAT α⇙ 𝔉 = 𝔉" 
    for 𝔉 𝔄 𝔅
  proof-
    assume prems: "𝔉 : 𝔄 ↦⇘cat_CAT α⇙ 𝔅"
    then have b: "category α 𝔅" unfolding cat_CAT_is_arr_iff by auto
    with digraph.dg_dghm_id_is_dghm have 
      "cat_CAT α⦇CId⦈⦇𝔅⦈ : 𝔅 ↦⇘cat_CAT α⇙ 𝔅"
      by 
        (
          simp add: 
            cat_CAT_CId_app cat_CAT_is_arrI category.cat_cf_id_is_functor
        )
    with prems b show "cat_CAT α⦇CId⦈⦇𝔅⦈ ∘⇩A⇘cat_CAT α⇙ 𝔉 = 𝔉" 
      by
        (
          simp add: 
            cat_CAT_CId_app 
            cat_CAT_Comp_app 
            cat_CAT_is_arr_iff
            is_functor.cf_cf_comp_cf_id_left
        )
  qed
  show "𝔉 : 𝔅 ↦⇘cat_CAT α⇙ ℭ ⟹ 𝔉 ∘⇩A⇘cat_CAT α⇙ cat_CAT α⦇CId⦈⦇𝔅⦈ = 𝔉" 
    for 𝔉 𝔅 ℭ
  proof-
    assume prems: "𝔉 : 𝔅 ↦⇘cat_CAT α⇙ ℭ"
    then have b: "category α 𝔅" unfolding cat_CAT_is_arr_iff by auto
    then have "cat_CAT α⦇CId⦈⦇𝔅⦈ : 𝔅 ↦⇘cat_CAT α⇙ 𝔅"
      by 
        (
          simp add: 
            cat_CAT_CId_app cat_CAT_is_arrI category.cat_cf_id_is_functor
        )
    with prems b show "𝔉 ∘⇩A⇘cat_CAT α⇙ cat_CAT α⦇CId⦈⦇𝔅⦈ = 𝔉"
      by 
        (
          auto 
            simp: cat_CAT_CId_app cat_CAT_Comp_app cat_CAT_is_arr_iff
            intro: is_functor.cf_cf_comp_cf_id_right 
        )
  qed
qed 
  (
    simp_all add:
      assms
      cat_smc_CAT
      cat_CAT_components 
      𝒵.intro 
      𝒵_Limit_αω 
      𝒵_ω_αω
      cat_CAT_is_arr_iff
      tiny_semicategory_smc_CAT
      category.cat_cf_id_is_functor
  )

lemmas [cat_cs_intros] = 𝒵.tiny_category_cat_CAT



subsection‹Isomorphism›

lemma cat_CAT_is_iso_arrI: 
  assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_CAT α⇙ 𝔅"
proof(intro is_iso_arrI is_inverseI)
  from assms show 𝔉: "𝔉 : 𝔄 ↦⇘cat_CAT α⇙ 𝔅"
    unfolding cat_CAT_is_arr_iff by auto
  note iso_thms = is_iso_functor_is_iso_arr[OF assms]
  from iso_thms(1) show inv_𝔉: "inv_cf 𝔉 : 𝔅 ↦⇘cat_CAT α⇙ 𝔄"
    unfolding cat_CAT_is_arr_iff by auto
  from assms show "𝔉 : 𝔄 ↦⇘cat_CAT α⇙ 𝔅"
    unfolding cat_CAT_is_arr_iff by auto
  from assms have 𝔄: "category α 𝔄" and 𝔅: "category α 𝔅" by auto
  show "inv_cf 𝔉 ∘⇩A⇘cat_CAT α⇙ 𝔉 = cat_CAT α⦇CId⦈⦇𝔄⦈"
    unfolding cat_CAT_CId_app[OF 𝔄] cat_CAT_Comp_app[OF inv_𝔉 𝔉]
    by (rule iso_thms(2))
  show "𝔉 ∘⇩A⇘cat_CAT α⇙ inv_cf 𝔉 = cat_CAT α⦇CId⦈⦇𝔅⦈"
    unfolding cat_CAT_CId_app[OF 𝔅] cat_CAT_Comp_app[OF 𝔉 inv_𝔉]
    by (rule iso_thms(3))
qed

lemma cat_CAT_is_iso_arrD: 
  assumes "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_CAT α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
proof-
  from is_iso_arrD[OF assms] have 𝔉: "𝔉 : 𝔄 ↦⇘cat_CAT α⇙ 𝔅" 
    and "(∃𝔊. is_inverse (cat_CAT α) 𝔊 𝔉)"
    by simp_all
  then obtain 𝔊 where "is_inverse (cat_CAT α) 𝔊 𝔉" by clarsimp
  then obtain 𝔄' 𝔅' where 𝔊': "𝔊 : 𝔅' ↦⇘cat_CAT α⇙ 𝔄'"
    and 𝔉': "𝔉 : 𝔄' ↦⇘cat_CAT α⇙ 𝔅'"
    and 𝔊𝔉: "𝔊 ∘⇩A⇘cat_CAT α⇙ 𝔉 = cat_CAT α⦇CId⦈⦇𝔄'⦈"
    and 𝔉𝔊: "𝔉 ∘⇩A⇘cat_CAT α⇙ 𝔊 = cat_CAT α⦇CId⦈⦇𝔅'⦈"
    by auto
  from 𝔉 𝔉' have 𝔄': "𝔄' = 𝔄" and 𝔅': "𝔅' = 𝔅" by auto  
  from 𝔉 have 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" unfolding cat_CAT_is_arr_iff by simp
  then have 𝔄: "category α 𝔄" and 𝔅: "category α 𝔅" by auto
  from 𝔊' have "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄" unfolding 𝔄' 𝔅' cat_CAT_is_arr_iff by simp
  moreover from 𝔊𝔉 have "𝔊 ∘⇩C⇩F 𝔉 = cf_id 𝔄"
    unfolding 𝔄' cat_CAT_Comp_app[OF 𝔊' 𝔉'] cat_CAT_CId_app[OF 𝔄] by simp
  moreover from 𝔉𝔊 have "𝔉 ∘⇩C⇩F 𝔊 = cf_id 𝔅"
    unfolding 𝔅' cat_CAT_Comp_app[OF 𝔉' 𝔊'] cat_CAT_CId_app[OF 𝔅] by simp
  ultimately show ?thesis using 𝔉 by (elim is_iso_arr_is_iso_functor)
qed

lemma cat_CAT_is_iso_arrE: 
  assumes "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_CAT α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using assms by (auto dest: cat_CAT_is_iso_arrD)

lemma cat_CAT_is_iso_arr_iff[cat_CAT_simps]: 
  "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_CAT α⇙ 𝔅 ⟷ 𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using cat_CAT_is_iso_arrI cat_CAT_is_iso_arrD by auto



subsection‹Isomorphic objects›

lemma cat_CAT_obj_isoI: 
  assumes "𝔄 ≈⇩C⇘α⇙ 𝔅"
  shows "𝔄 ≈⇩o⇩b⇩j⇘cat_CAT α⇙ 𝔅"
proof-
  from iso_categoryD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
    by clarsimp
  from cat_CAT_is_iso_arrI[OF this] show ?thesis by (rule obj_isoI)
qed

lemma cat_CAT_obj_isoD: 
  assumes "𝔄 ≈⇩o⇩b⇩j⇘cat_CAT α⇙ 𝔅"
  shows "𝔄 ≈⇩C⇘α⇙ 𝔅"
proof-
  from obj_isoD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_CAT α⇙ 𝔅" 
    by clarsimp
  from cat_CAT_is_iso_arrD[OF this] show ?thesis by (rule iso_categoryI)
qed

lemma cat_CAT_obj_isoE: 
  assumes "𝔄 ≈⇩o⇩b⇩j⇘cat_CAT α⇙ 𝔅"
  obtains "𝔄 ≈⇩C⇘α⇙ 𝔅"
  using assms by (auto simp: cat_CAT_obj_isoD)

lemma cat_CAT_obj_iso_iff[cat_CAT_simps]: 
  "𝔄 ≈⇩o⇩b⇩j⇘cat_CAT α⇙ 𝔅 ⟷ 𝔄 ≈⇩C⇘α⇙ 𝔅"
  using cat_CAT_obj_isoI cat_CAT_obj_isoD by (intro iffI) auto

text‹\newpage›

end