Theory CZH_ECAT_Par

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Par››
theory CZH_ECAT_Par
  imports 
    CZH_Foundations.CZH_SMC_Par
    CZH_ECAT_Rel
    CZH_ECAT_Subcategory
begin



subsection‹Background›


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

named_theorems cat_Par_cs_simps
named_theorems cat_Par_cs_intros

lemmas (in arr_Par) [cat_Par_cs_simps] = 
  dg_Rel_shared_cs_simps

lemmas (in arr_Par) [cat_cs_intros, cat_Par_cs_intros] = 
  arr_Par_axioms'

lemmas [cat_Par_cs_simps] = 
  dg_Rel_shared_cs_simps
  arr_Par.arr_Par_length
  arr_Par_comp_Par_id_Par_left
  arr_Par_comp_Par_id_Par_right

lemmas [cat_Par_cs_intros] = 
  arr_Par_comp_Par



subsection‹‹Par› as a category›


subsubsection‹Definition and elementary properties›

definition cat_Par :: "V ⇒ V"
  where "cat_Par α =
    [
      Vset α,
      set {T. arr_Par α T},
      (λT∈⇩∘set {T. arr_Par α T}. T⦇ArrDom⦈),
      (λT∈⇩∘set {T. arr_Par α T}. T⦇ArrCod⦈),
      (λST∈⇩∘composable_arrs (dg_Par α). ST⦇0⦈ ∘⇩R⇩e⇩l ST⦇1⇩ℕ⦈),
      VLambda (Vset α) id_Par 
    ]⇩∘"


text‹Components.›

lemma cat_Par_components:
  shows "cat_Par α⦇Obj⦈ = Vset α"
    and "cat_Par α⦇Arr⦈ = set {T. arr_Par α T}"
    and "cat_Par α⦇Dom⦈ = (λT∈⇩∘set {T. arr_Par α T}. T⦇ArrDom⦈)"
    and "cat_Par α⦇Cod⦈ = (λT∈⇩∘set {T. arr_Par α T}. T⦇ArrCod⦈)"
    and "cat_Par α⦇Comp⦈ = (λST∈⇩∘composable_arrs (dg_Par α). ST⦇0⦈ ∘⇩P⇩a⇩r ST⦇1⇩ℕ⦈)"
    and "cat_Par α⦇CId⦈ = VLambda (Vset α) id_Par"
  unfolding cat_Par_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_cat_Par: "cat_smc (cat_Par α) = smc_Par α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ (cat_smc (cat_Par α)) = 5⇩ℕ" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smc_Par α) = 5⇩ℕ"
    unfolding smc_Par_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cat_smc (cat_Par α)) = 𝒟⇩∘ (smc_Par α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_Par α)) ⟹ cat_smc (cat_Par α)⦇a⦈ = smc_Par α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold cat_smc_def dg_field_simps cat_Par_def smc_Par_def
      )
      (auto simp: nat_omega_simps)
qed (auto simp: cat_smc_def smc_Par_def)

lemmas_with [folded cat_smc_cat_Par, unfolded slicing_simps]:
  cat_Par_Obj_iff = smc_Par_Obj_iff
  and cat_Par_Arr_iff[cat_Par_cs_simps] = smc_Par_Arr_iff
  and cat_Par_Dom_vsv[cat_Par_cs_intros] = smc_Par_Dom_vsv
  and cat_Par_Dom_vdomain[cat_Par_cs_simps] = smc_Par_Dom_vdomain
  and cat_Par_Dom_vrange = smc_Par_Dom_vrange
  and cat_Par_Dom_app[cat_Par_cs_simps] = smc_Par_Dom_app
  and cat_Par_Cod_vsv[cat_Par_cs_intros] = smc_Par_Cod_vsv
  and cat_Par_Cod_vdomain[cat_Par_cs_simps] = smc_Par_Cod_vdomain
  and cat_Par_Cod_vrange = smc_Par_Cod_vrange
  and cat_Par_Cod_app[cat_Par_cs_simps] = smc_Par_Cod_app
  and cat_Par_is_arrI = smc_Par_is_arrI
  and cat_Par_is_arrD = smc_Par_is_arrD
  and cat_Par_is_arrE = smc_Par_is_arrE

lemmas_with [folded cat_smc_cat_Par, unfolded slicing_simps]: 
  cat_Par_composable_arrs_dg_Par = smc_Par_composable_arrs_dg_Par
  and cat_Par_Comp = smc_Par_Comp
  and cat_Par_Comp_app[cat_Par_cs_simps] = smc_Par_Comp_app
  and cat_Par_Comp_vdomain[cat_Par_cs_simps] = smc_Par_Comp_vdomain
  and cat_Par_is_monic_arrI = smc_Par_is_monic_arrI
  and cat_Par_is_monic_arrD = smc_Par_is_monic_arrD
  and cat_Par_is_monic_arr = smc_Par_is_monic_arr
  and cat_Par_is_epic_arrI = smc_Par_is_epic_arrI
  and cat_Par_is_epic_arrD = smc_Par_is_epic_arrD
  and cat_Par_is_epic_arr = smc_Par_is_epic_arr

lemmas [cat_cs_simps] = cat_Par_is_arrD(2,3)

lemmas [cat_Par_cs_intros] = cat_Par_is_arrI

lemmas_with (in 𝒵) [folded cat_smc_cat_Par, unfolded slicing_simps]:
  cat_Par_Hom_vifunion_in_Vset = smc_Par_Hom_vifunion_in_Vset
  and cat_Par_incl_Par_is_arr = smc_Par_incl_Par_is_arr
  and cat_Par_incl_Par_is_arr'[cat_Par_cs_intros] = smc_Par_incl_Par_is_arr'
  and cat_Par_Comp_vrange = smc_Par_Comp_vrange
  and cat_Par_obj_terminal = smc_Par_obj_terminal
  and cat_Par_obj_initial = smc_Par_obj_initial
  and cat_Par_obj_terminal_obj_initial = smc_Par_obj_terminal_obj_initial
  and cat_Par_obj_null = smc_Par_obj_null
  and cat_Par_is_zero_arr = smc_Par_is_zero_arr

lemmas [cat_Par_cs_intros] = 𝒵.cat_Par_incl_Par_is_arr'


subsubsection‹Identity›

lemma cat_Par_CId_app[cat_Par_cs_simps]:
  assumes "A ∈⇩∘ Vset α"
  shows "cat_Par α⦇CId⦈⦇A⦈ = id_Par A"
  using assms unfolding cat_Par_components by simp

lemma id_Par_CId_app_app[cat_cs_simps]:
  assumes "A ∈⇩∘ Vset α" and "a ∈⇩∘ A"
  shows "cat_Par α⦇CId⦈⦇A⦈⦇ArrVal⦈⦇a⦈ = a"
  unfolding cat_Par_CId_app[OF assms(1)] id_Rel_ArrVal_app[OF assms(2)] by simp


subsubsection‹‹Par› is a category›

lemma (in 𝒵) category_cat_Par: "category α (cat_Par α)"
proof(intro categoryI, unfold cat_smc_cat_Rel cat_smc_cat_Par cat_op_simps)

  interpret Par: semicategory α ‹cat_smc (cat_Par α)›
    unfolding cat_smc_cat_Par by (simp add: semicategory_smc_Par)

  show "vfsequence (cat_Par α)" unfolding cat_Par_def by simp
  show "vcard (cat_Par α) = 6⇩ℕ" 
    unfolding cat_Par_def by (simp add: nat_omega_simps)
  show "cat_Par α⦇CId⦈⦇A⦈ : A ↦⇘cat_Par α⇙ A" if "A ∈⇩∘ cat_Par α⦇Obj⦈" for A
    using that
    unfolding cat_Par_Obj_iff
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_Par_cs_simps cs_intro: cat_Par_cs_intros arr_Par_id_ParI
      )

  show "cat_Par α⦇CId⦈⦇B⦈ ∘⇩A⇘cat_Par α⇙ F = F"
    if "F : A ↦⇘cat_Par α⇙ B" for F A B
  proof-
    from that have "arr_Par α F" "B ∈⇩∘ Vset α"
      by (auto elim: cat_Par_is_arrE simp: cat_Par_cs_simps)
    with that 𝒵_axioms show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Par_cs_simps
            cs_intro: cat_Par_cs_intros arr_Par_id_ParI
        )
  qed

  show "F ∘⇩A⇘cat_Par α⇙ cat_Par α⦇CId⦈⦇B⦈ = F"
    if "F : B ↦⇘cat_Par α⇙ C" for F B C
  proof-
    from that have "arr_Par α F" "B ∈⇩∘ Vset α"
      by (auto elim: cat_Par_is_arrE simp: cat_Par_cs_simps)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Par_cs_simps
            cs_intro: cat_Par_cs_intros arr_Par_id_ParI
        )
  qed

qed (auto simp: semicategory_smc_Par cat_Par_components)


subsubsection‹‹Par› is a wide replete subcategory of ‹Rel››

lemma (in 𝒵) wide_replete_subcategory_cat_Par_cat_Rel: 
  "cat_Par α ⊆⇩C⇩.⇩w⇩r⇘α⇙ cat_Rel α"
proof(intro wide_replete_subcategoryI)
  show wide_subcategory_cat_Par_cat_Rel: "cat_Par α ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ cat_Rel α"
  proof(intro wide_subcategoryI, unfold cat_smc_cat_Rel cat_smc_cat_Par)
    interpret Rel: category α ‹cat_Rel α› by (rule category_cat_Rel)
    interpret Par: category α ‹cat_Par α› by (rule category_cat_Par)
    interpret wide_subsemicategory α ‹smc_Par α› ‹smc_Rel α›
      by (simp add: wide_subsemicategory_smc_Par_smc_Rel)
    show "cat_Par α ⊆⇩C⇘α⇙ cat_Rel α"
    proof(intro subcategoryI, unfold cat_smc_cat_Rel cat_smc_cat_Par)
      show "smc_Par α ⊆⇩S⇩M⇩C⇘α⇙ smc_Rel α" by (simp add: subsemicategory_axioms)
      fix A assume "A ∈⇩∘ cat_Par α⦇Obj⦈"
      then show "cat_Par α⦇CId⦈⦇A⦈ = cat_Rel α⦇CId⦈⦇A⦈"
        unfolding cat_Par_components cat_Rel_components by simp
    qed 
      (
        auto simp: 
          subsemicategory_axioms Rel.category_axioms Par.category_axioms
      )
  qed (rule wide_subsemicategory_smc_Par_smc_Rel)
  show "cat_Par α ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ cat_Rel α"
  proof(intro replete_subcategoryI)
    interpret wide_subcategory α ‹cat_Par α› ‹cat_Rel α›
      by (rule wide_subcategory_cat_Par_cat_Rel)
    show "cat_Par α ⊆⇩C⇘α⇙ cat_Rel α" by (rule subcategory_axioms)    
    fix A B F assume prems: "A ∈⇩∘ cat_Par α⦇Obj⦈" "F : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
    note arr_Rel = cat_Rel_is_iso_arrD[OF prems(2)]
    from arr_Rel(2) show "F : A ↦⇘cat_Par α⇙ B"
      by (intro cat_Par_is_arrI arr_Par_arr_RelI cat_Rel_is_arrD[OF arr_Rel(1)])
        auto
  qed
qed



subsection‹Isomorphism›

lemma cat_Par_is_iso_arrI[intro]:
  assumes "T : A ↦⇘cat_Par α⇙ B" 
    and "v11 (T⦇ArrVal⦈)"
    and "𝒟⇩∘ (T⦇ArrVal⦈) = A"
    and "ℛ⇩∘ (T⦇ArrVal⦈) = B"
  shows "T : A ↦⇩i⇩s⇩o⇘cat_Par α⇙ B"
proof-
  interpret T: arr_Par α T by (intro cat_Par_is_arrD(1)[OF assms(1)])
  note [cat_cs_intros] = cat_Rel_is_iso_arrI
  from T.wide_replete_subcategory_cat_Par_cat_Rel assms have 
    "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
    by (cs_concl cs_intro: cat_cs_intros cat_sub_cs_intros cat_sub_fw_cs_intros)
  with T.wide_replete_subcategory_cat_Par_cat_Rel assms show 
    "T : A ↦⇩i⇩s⇩o⇘cat_Par α⇙ B"
    by (cs_concl cs_shallow cs_simp: cat_sub_bw_cs_simps)
qed

lemma cat_Par_is_iso_arrD[dest]:
  assumes "T : A ↦⇩i⇩s⇩o⇘cat_Par α⇙ B"
  shows "T : A ↦⇘cat_Par α⇙ B"
    and "v11 (T⦇ArrVal⦈)"
    and "𝒟⇩∘ (T⦇ArrVal⦈) = A"
    and "ℛ⇩∘ (T⦇ArrVal⦈) = B"
proof-
  interpret T: arr_Par α T 
    by (intro cat_Par_is_arrD(1)[OF is_iso_arrD(1)[OF assms(1)]])
  from T.wide_replete_subcategory_cat_Par_cat_Rel assms have T: 
    "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
    by (cs_concl cs_shallow cs_intro: cat_sub_cs_intros cat_sub_fw_cs_intros)
  show "v11 (T⦇ArrVal⦈)" "𝒟⇩∘ (T⦇ArrVal⦈) = A" "ℛ⇩∘ (T⦇ArrVal⦈) = B"
    by (intro cat_Rel_is_iso_arrD[OF T])+
qed (rule is_iso_arrD(1)[OF assms])

lemma cat_Par_is_iso_arr:
  "T : A ↦⇩i⇩s⇩o⇘cat_Par α⇙ B ⟷
    T : A ↦⇘cat_Par α⇙ B ∧
    v11 (T⦇ArrVal⦈) ∧
    𝒟⇩∘ (T⦇ArrVal⦈) = A ∧
    ℛ⇩∘ (T⦇ArrVal⦈) = B"
  by auto



subsection‹The inverse arrow›

abbreviation (input) converse_Par :: "V ⇒ V" (‹(_¯⇩P⇩a⇩r)› [1000] 999)
  where "a¯⇩P⇩a⇩r ≡ a¯⇩R⇩e⇩l"

lemma cat_Par_the_inverse[cat_Par_cs_simps]:
  assumes "T : A ↦⇩i⇩s⇩o⇘cat_Par α⇙ B"
  shows "T¯⇩C⇘cat_Par α⇙ = T¯⇩P⇩a⇩r"
proof-
  interpret T: arr_Par α T 
    by (intro cat_Par_is_arrD(1)[OF is_iso_arrD(1)[OF assms(1)]])
  from T.wide_replete_subcategory_cat_Par_cat_Rel assms have T:
    "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
    by (cs_concl cs_shallow cs_intro: cat_sub_cs_intros cat_sub_fw_cs_intros)
  from T.wide_replete_subcategory_cat_Par_cat_Rel assms 
  have [symmetric, cat_cs_simps]: "T¯⇩C⇘cat_Rel α⇙ = T¯⇩C⇘cat_Par α⇙"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_sub_bw_cs_simps cs_intro: cat_sub_cs_intros
      )
  from T show "T¯⇩C⇘cat_Par α⇙ = T¯⇩P⇩a⇩r"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_Rel_cs_simps cat_cs_simps cs_intro: cat_cs_intros
      )
qed

text‹\newpage›

end