Theory CZH_ECAT_SemiCAT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹SemiCAT››
theory CZH_ECAT_SemiCAT
  imports 
    CZH_Foundations.CZH_SMC_SemiCAT
    CZH_ECAT_Small_Category
    CZH_ECAT_Simple
begin



subsection‹Background›


text‹
The methodology for the exposition of ‹SemiCAT› as a category 
is analogous to the one used in \<^cite>‹"milehins_category_2021"› 
for the exposition of ‹SemiCAT› as a semicategory.
›

named_theorems cat_SemiCAT_simps
named_theorems cat_SemiCAT_intros



subsection‹Definition and elementary properties›

definition cat_SemiCAT :: "V ⇒ V"
  where "cat_SemiCAT α =
    [
      set {ℭ. semicategory α ℭ}, 
      all_smcfs α, 
      (λ𝔉∈⇩∘all_smcfs α. 𝔉⦇HomDom⦈), 
      (λ𝔉∈⇩∘all_smcfs α. 𝔉⦇HomCod⦈),
      (λ𝔊𝔉∈⇩∘composable_arrs (dg_SemiCAT α). 𝔊𝔉⦇0⦈ ∘⇩S⇩M⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈),
      (λℭ∈⇩∘set {ℭ. semicategory α ℭ}. smcf_id ℭ)
    ]⇩∘"


text‹Components.›

lemma cat_SemiCAT_components:
  shows "cat_SemiCAT α⦇Obj⦈ = set {ℭ. semicategory α ℭ}"
    and "cat_SemiCAT α⦇Arr⦈ = all_smcfs α"
    and "cat_SemiCAT α⦇Dom⦈ = (λ𝔉∈⇩∘all_smcfs α. 𝔉⦇HomDom⦈)"
    and "cat_SemiCAT α⦇Cod⦈ = (λ𝔉∈⇩∘all_smcfs α. 𝔉⦇HomCod⦈)"
    and "cat_SemiCAT α⦇Comp⦈ = 
      (λ𝔊𝔉∈⇩∘composable_arrs (dg_SemiCAT α). 𝔊𝔉⦇0⦈ ∘⇩S⇩M⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈)"
    and "cat_SemiCAT α⦇CId⦈ = (λℭ∈⇩∘set {ℭ. semicategory α ℭ}. smcf_id ℭ)"
  unfolding cat_SemiCAT_def dg_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_SemiCAT: "cat_smc (cat_SemiCAT α) = smc_SemiCAT α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ (cat_smc (cat_SemiCAT α)) = 5⇩ℕ" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smc_SemiCAT α) = 5⇩ℕ"
    unfolding smc_SemiCAT_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cat_smc (cat_SemiCAT α)) = 𝒟⇩∘ (smc_SemiCAT α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_SemiCAT α)) ⟹ 
    cat_smc (cat_SemiCAT α)⦇a⦈ = smc_SemiCAT α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        unfold cat_smc_def dg_field_simps cat_SemiCAT_def smc_SemiCAT_def
      )
      (auto simp: nat_omega_simps)
qed (auto simp: cat_smc_def smc_SemiCAT_def)

lemmas_with [folded cat_smc_SemiCAT, unfolded slicing_simps]: 
  ―‹Digraph›
  cat_SemiCAT_ObjI = smc_SemiCAT_ObjI
  and cat_SemiCAT_ObjD = smc_SemiCAT_ObjD
  and cat_SemiCAT_ObjE = smc_SemiCAT_ObjE
  and cat_SemiCAT_Obj_iff[cat_SemiCAT_simps] = smc_SemiCAT_Obj_iff  
  and cat_SemiCAT_Dom_app[cat_SemiCAT_simps] = smc_SemiCAT_Dom_app
  and cat_SemiCAT_Cod_app[cat_SemiCAT_simps] = smc_SemiCAT_Cod_app
  and cat_SemiCAT_is_arrI = smc_SemiCAT_is_arrI
  and cat_SemiCAT_is_arrD = smc_SemiCAT_is_arrD
  and cat_SemiCAT_is_arrE = smc_SemiCAT_is_arrE
  and cat_SemiCAT_is_arr_iff[cat_SemiCAT_simps] = smc_SemiCAT_is_arr_iff

lemmas_with [
    folded cat_smc_SemiCAT, unfolded slicing_simps, unfolded cat_smc_SemiCAT
    ]: 
  ―‹Semicategory›
  cat_SemiCAT_Comp_vdomain = smc_SemiCAT_Comp_vdomain
  and cat_SemiCAT_composable_arrs_dg_SemiCAT = 
    smc_SemiCAT_composable_arrs_dg_SemiCAT
  and cat_SemiCAT_Comp = smc_SemiCAT_Comp
  and cat_SemiCAT_Comp_app[cat_SemiCAT_simps] = smc_SemiCAT_Comp_app
  and cat_SemiCAT_Comp_vrange = smc_SemiCAT_Comp_vrange

lemmas_with (in 𝒵) [folded cat_smc_SemiCAT, unfolded slicing_simps]: 
  ―‹Semicategory›
  cat_SemiCAT_obj_initialI = smc_SemiCAT_obj_initialI
  and cat_SemiCAT_obj_initialD = smc_SemiCAT_obj_initialD
  and cat_SemiCAT_obj_initialE = smc_SemiCAT_obj_initialE
  and cat_SemiCAT_obj_initial_iff[cat_SemiCAT_simps] = 
    smc_SemiCAT_obj_initial_iff
  and cat_SemiCAT_obj_terminalI = smc_SemiCAT_obj_terminalI
  and cat_SemiCAT_obj_terminalE = smc_SemiCAT_obj_terminalE



subsection‹Identity›

lemma cat_SemiCAT_CId_app[cat_SemiCAT_simps]: 
  assumes "semicategory α ℭ"
  shows "cat_SemiCAT α⦇CId⦈⦇ℭ⦈ = smcf_id ℭ"
  using assms unfolding cat_SemiCAT_components by simp

lemma cat_SemiCAT_CId_vdomain[cat_SemiCAT_simps]: 
  "𝒟⇩∘ (cat_SemiCAT α⦇CId⦈) = set {ℭ. semicategory α ℭ}"
  unfolding cat_SemiCAT_components by auto

lemma cat_SemiCAT_CId_vrange: "ℛ⇩∘ (cat_SemiCAT α⦇CId⦈) ⊆⇩∘ all_smcfs α"
proof(rule vsubsetI)
  fix ℌ assume "ℌ ∈⇩∘ ℛ⇩∘ (cat_SemiCAT α⦇CId⦈)"
  then obtain 𝔄 
    where ℌ_def: "ℌ = cat_SemiCAT α⦇CId⦈⦇𝔄⦈" 
      and 𝔄: "𝔄 ∈⇩∘ 𝒟⇩∘ (cat_SemiCAT α⦇CId⦈)"
    unfolding cat_SemiCAT_components by auto
  from 𝔄 have ℌ_def': "ℌ = smcf_id 𝔄" 
    unfolding ℌ_def cat_SemiCAT_CId_vdomain by (auto simp: cat_SemiCAT_CId_app)
  from 𝔄 semicategory.smc_smcf_id_is_semifunctor show "ℌ ∈⇩∘ all_smcfs α"
    unfolding ℌ_def' cat_SemiCAT_CId_vdomain by force
qed



subsection‹‹SemiCAT› is a category›

lemma (in 𝒵) tiny_category_cat_SemiCAT: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_category β (cat_SemiCAT α)"
proof(intro tiny_categoryI)
  interpret β: 𝒵 β by (rule assms(1))
  show "vfsequence (cat_SemiCAT α)" unfolding cat_SemiCAT_def by simp
  show "vcard (cat_SemiCAT α) = 6⇩ℕ"
    unfolding cat_SemiCAT_def by (simp add: nat_omega_simps)
  show "cat_SemiCAT α⦇CId⦈⦇𝔅⦈ ∘⇩A⇘cat_SemiCAT α⇙ 𝔉 = 𝔉"
    if "𝔉 : 𝔄 ↦⇘cat_SemiCAT α⇙ 𝔅" for 𝔉 𝔄 𝔅
    using that 
    unfolding cat_SemiCAT_is_arr_iff
    by (cs_concl cs_simp: smc_cs_simps cat_SemiCAT_simps cs_intro: smc_cs_intros)
  show "𝔉 ∘⇩A⇘cat_SemiCAT α⇙ cat_SemiCAT α⦇CId⦈⦇𝔅⦈ = 𝔉"
    if "𝔉 : 𝔅 ↦⇘cat_SemiCAT α⇙ ℭ" for 𝔉 𝔅 ℭ
    using that 
    unfolding cat_SemiCAT_is_arr_iff
    by (cs_concl cs_simp: smc_cs_simps cat_SemiCAT_simps cs_intro: smc_cs_intros)
qed 
  (
    simp_all add: 
      assms
      cat_smc_SemiCAT
      cat_SemiCAT_components
      cat_SemiCAT_is_arr_iff
      tiny_semicategory_smc_SemiCAT
      semicategory.smc_smcf_id_is_semifunctor
  )



subsection‹Isomorphism›

lemma cat_SemiCAT_is_iso_arrI: 
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_SemiCAT α⇙ 𝔅"
proof(intro is_iso_arrI is_inverseI)
  interpret is_iso_semifunctor α 𝔄 𝔅 𝔉 by (rule assms)
  from assms show 𝔉: "𝔉 : 𝔄 ↦⇘cat_SemiCAT α⇙ 𝔅"
    unfolding cat_SemiCAT_is_arr_iff by auto
  note iso_thms = is_iso_semifunctor_is_iso_arr[OF assms]
  from iso_thms(1) show inv_𝔉: "inv_smcf 𝔉 : 𝔅 ↦⇘cat_SemiCAT α⇙ 𝔄"
    unfolding cat_SemiCAT_is_arr_iff by auto
  from assms show "𝔉 : 𝔄 ↦⇘cat_SemiCAT α⇙ 𝔅"
    unfolding cat_SemiCAT_is_arr_iff by auto
  from assms have 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅" by auto
  show "inv_smcf 𝔉 ∘⇩A⇘cat_SemiCAT α⇙ 𝔉 = cat_SemiCAT α⦇CId⦈⦇𝔄⦈"
    unfolding cat_SemiCAT_CId_app[OF 𝔄] cat_SemiCAT_Comp_app[OF inv_𝔉 𝔉]
    by (rule iso_thms(2))
  show "𝔉 ∘⇩A⇘cat_SemiCAT α⇙ inv_smcf 𝔉 = cat_SemiCAT α⦇CId⦈⦇𝔅⦈"
    unfolding cat_SemiCAT_CId_app[OF 𝔅] cat_SemiCAT_Comp_app[OF 𝔉 inv_𝔉]
    by (rule iso_thms(3))
qed

lemma cat_SemiCAT_is_iso_arrD: 
  assumes "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_SemiCAT α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
proof-
  from is_iso_arrD[OF assms] have 𝔉: "𝔉 : 𝔄 ↦⇘cat_SemiCAT α⇙ 𝔅" 
    and "(∃𝔊. is_inverse (cat_SemiCAT α) 𝔊 𝔉)"
    by simp_all
  then obtain 𝔊 where 𝔊𝔉: "is_inverse (cat_SemiCAT α) 𝔊 𝔉" by clarsimp
  then obtain 𝔄' 𝔅' where 𝔊': "𝔊 : 𝔅' ↦⇘cat_SemiCAT α⇙ 𝔄'"
    and 𝔉': "𝔉 : 𝔄' ↦⇘cat_SemiCAT α⇙ 𝔅'"
    and 𝔊𝔉: "𝔊 ∘⇩A⇘cat_SemiCAT α⇙ 𝔉 = cat_SemiCAT α⦇CId⦈⦇𝔄'⦈"
    and 𝔉𝔊: "𝔉 ∘⇩A⇘cat_SemiCAT α⇙ 𝔊 = cat_SemiCAT α⦇CId⦈⦇𝔅'⦈"
    by auto
  from 𝔉 𝔉' have 𝔄': "𝔄' = 𝔄" and 𝔅': "𝔅' = 𝔅" by auto  
  from 𝔉 have 𝔉: "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" unfolding cat_SemiCAT_is_arr_iff by simp
  interpret is_semifunctor α 𝔄 𝔅 𝔉 by (rule 𝔉)
  have 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅" 
    by (cs_concl cs_intro: smc_cs_intros)+
  from 𝔊' have 𝔊: "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔄" 
    unfolding 𝔄' 𝔅' cat_SemiCAT_is_arr_iff by simp
  moreover from 𝔊𝔉 have "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 = smcf_id 𝔄"
    unfolding 𝔄' cat_SemiCAT_Comp_app[OF 𝔊' 𝔉'] cat_SemiCAT_CId_app[OF 𝔄] 
    by simp
  moreover from 𝔉𝔊 have "𝔉 ∘⇩S⇩M⇩C⇩F 𝔊 = smcf_id 𝔅"
    unfolding 𝔅' cat_SemiCAT_Comp_app[OF 𝔉' 𝔊'] cat_SemiCAT_CId_app[OF 𝔅] 
    by simp
  ultimately show ?thesis 
    using 𝔉 by (elim is_iso_arr_is_iso_semifunctor)
qed

lemma cat_SemiCAT_is_iso_arrE: 
  assumes "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_SemiCAT α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using assms by (auto dest: cat_SemiCAT_is_iso_arrD)

lemma cat_SemiCAT_is_iso_arr_iff[cat_SemiCAT_simps]: 
  "𝔉 : 𝔄 ↦⇩i⇩s⇩o⇘cat_SemiCAT α⇙ 𝔅 ⟷ 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using cat_SemiCAT_is_iso_arrI cat_SemiCAT_is_iso_arrD by auto



subsection‹Isomorphic objects›

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

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

lemma cat_SemiCAT_obj_isoE: 
  assumes "𝔄 ≈⇩o⇩b⇩j⇘cat_SemiCAT α⇙ 𝔅"
  obtains "𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔅"
  using assms by (auto simp: cat_SemiCAT_obj_isoD)

lemma cat_SemiCAT_obj_iso_iff[cat_SemiCAT_simps]: 
  "𝔄 ≈⇩o⇩b⇩j⇘cat_SemiCAT α⇙ 𝔅 ⟷ 𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔅"
  using cat_SemiCAT_obj_isoI cat_SemiCAT_obj_isoD by (intro iffI) auto

text‹\newpage›

end