Theory CZH_ECAT_Small_Category

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for categories›
theory CZH_ECAT_Small_Category
  imports 
    CZH_Foundations.CZH_SMC_Small_Semicategory
    CZH_ECAT_Category
begin



subsection‹Background›


text‹
An explanation of the methodology chosen for the exposition of all
matters related to the size of the categories and associated entities
is given in \<^cite>‹"milehins_category_2021"›.
›

named_theorems cat_small_cs_simps
named_theorems cat_small_cs_intros



subsection‹Tiny category›


subsubsection‹Definition and elementary properties›

locale tiny_category = 𝒵 α + vfsequence ℭ + CId: vsv ‹ℭ⦇CId⦈› for α ℭ +
  assumes tiny_cat_length[cat_cs_simps]: "vcard ℭ = 6⇩ℕ"
    and tiny_cat_tiny_semicategory[slicing_intros]: 
      "tiny_semicategory α (cat_smc ℭ)"
    and tiny_cat_CId_vdomain[cat_cs_simps]: "𝒟⇩∘ (ℭ⦇CId⦈) = ℭ⦇Obj⦈"
    and tiny_cat_CId_is_arr[cat_cs_intros]: 
      "a ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and tiny_cat_CId_left_left[cat_cs_simps]:
      "f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and tiny_cat_CId_right_left[cat_cs_simps]:
      "f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = f"

lemmas [slicing_intros] = tiny_category.tiny_cat_tiny_semicategory


text‹Rules.›

lemma (in tiny_category) tiny_category_axioms'[cat_small_cs_intros]:
  assumes "α' = α"
  shows "tiny_category α' ℭ"
  unfolding assms by (rule tiny_category_axioms)

mk_ide rf tiny_category_def[unfolded tiny_category_axioms_def]
  |intro tiny_categoryI|
  |dest tiny_categoryD[dest]|
  |elim tiny_categoryE[elim]|

lemma tiny_categoryI':
  assumes "category α ℭ" and "ℭ⦇Obj⦈ ∈⇩∘ Vset α" and "ℭ⦇Arr⦈ ∈⇩∘ Vset α"
  shows "tiny_category α ℭ"
proof-
  interpret category α ℭ by (rule assms(1))
  show ?thesis
  proof(intro tiny_categoryI)
    from assms show "tiny_semicategory α (cat_smc ℭ)"
      by (intro tiny_semicategoryI') (auto simp: slicing_simps)
  qed (auto simp: vfsequence_axioms cat_cs_simps cat_cs_intros)
qed

lemma tiny_categoryI'':
  assumes "𝒵 α"
    and "vfsequence ℭ"
    and "vcard ℭ = 6⇩ℕ"
    and "vsv (ℭ⦇Dom⦈)"
    and "vsv (ℭ⦇Cod⦈)"
    and "vsv (ℭ⦇Comp⦈)"
    and "vsv (ℭ⦇CId⦈)"
    and "𝒟⇩∘ (ℭ⦇Dom⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Dom⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "𝒟⇩∘ (ℭ⦇Cod⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Cod⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "⋀gf. gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and "𝒟⇩∘ (ℭ⦇CId⦈) = ℭ⦇Obj⦈"
    and "⋀b c g a f. ⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
      (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "⋀a. a ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and "⋀a b f. f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and "⋀b c f. f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = f"
    and "ℭ⦇Obj⦈ ∈⇩∘ Vset α" 
    and "ℭ⦇Arr⦈ ∈⇩∘ Vset α"
  shows "tiny_category α ℭ"
  by (intro tiny_categoryI tiny_semicategoryI'', unfold slicing_simps) 
    (simp_all add: cat_smc_def nat_omega_simps assms)


text‹Slicing.›

context tiny_category
begin

interpretation smc: tiny_semicategory α ‹cat_smc ℭ›
  by (rule tiny_cat_tiny_semicategory) 

lemmas_with [unfolded slicing_simps]:
  tiny_cat_semicategory = smc.semicategory_axioms
  and tiny_cat_Obj_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Obj_in_Vset
  and tiny_cat_Arr_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Arr_in_Vset
  and tiny_cat_Dom_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Dom_in_Vset
  and tiny_cat_Cod_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Cod_in_Vset
  and tiny_cat_Comp_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Comp_in_Vset

end


text‹Elementary properties.›

sublocale tiny_category ⊆ category
  by (rule categoryI) 
    (
      auto simp: 
        vfsequence_axioms tiny_cat_semicategory cat_cs_intros cat_cs_simps
    )

lemmas (in tiny_category) tiny_cat_category = category_axioms

lemmas [cat_small_cs_intros] = tiny_category.tiny_cat_category


text‹Size.›

lemma (in tiny_category) tiny_cat_CId_in_Vset: "ℭ⦇CId⦈ ∈⇩∘ Vset α"
proof-
  from tiny_cat_Obj_in_Vset have "𝒟⇩∘ (ℭ⦇CId⦈) ∈⇩∘ Vset α"
    by (simp add: tiny_cat_Obj_in_Vset cat_cs_simps)
  moreover from tiny_cat_Arr_in_Vset cat_CId_vrange tiny_cat_Arr_in_Vset have 
    "ℛ⇩∘ (ℭ⦇CId⦈) ∈⇩∘ Vset α"  
    by auto
  ultimately show ?thesis by (blast intro: 𝒵_Limit_αω)
qed

lemma (in tiny_category) tiny_cat_in_Vset: "ℭ ∈⇩∘ Vset α"
proof-
  note [cat_cs_intros] = 
    tiny_cat_Obj_in_Vset 
    tiny_cat_Arr_in_Vset
    tiny_cat_Dom_in_Vset
    tiny_cat_Cod_in_Vset
    tiny_cat_Comp_in_Vset
    tiny_cat_CId_in_Vset
  show ?thesis 
    by (subst cat_def) (cs_concl cs_shallow cs_intro: cat_cs_intros V_cs_intros)
qed

lemma tiny_category[simp]: "small {ℭ. tiny_category α ℭ}"
proof(rule down)
  show "{ℭ. tiny_category α ℭ} ⊆ elts (set {ℭ. category α ℭ})" 
    by (auto intro: cat_small_cs_intros)
qed

lemma small_categories_vsubset_Vset: "set {ℭ. tiny_category α ℭ} ⊆⇩∘ Vset α" 
  by (rule vsubsetI) (simp_all add: tiny_category.tiny_cat_in_Vset)

lemma (in category) cat_tiny_category_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_category β ℭ"
proof(intro tiny_categoryI)
  show "tiny_semicategory β (cat_smc ℭ)"
    by 
      (
        rule semicategory.smc_tiny_semicategory_if_ge_Limit, 
        rule cat_semicategory;
        intro assms
      )
qed (auto simp:  assms(1) cat_cs_simps cat_cs_intros vfsequence_axioms)


subsubsection‹Opposite tiny category›

lemma (in tiny_category) tiny_category_op: "tiny_category α (op_cat ℭ)"
  by (intro tiny_categoryI') 
    (auto simp: cat_op_simps cat_cs_intros cat_small_cs_intros)

lemmas tiny_category_op[cat_op_intros] = tiny_category.tiny_category_op



subsection‹Finite category›


subsubsection‹Definition and elementary properties›


text‹
A definition of a finite category can be found in nLab 
\<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/finite+category}
}.
›

(*TODO: implicit redundant assumption*)
locale finite_category = 𝒵 α + vfsequence ℭ + CId: vsv ‹ℭ⦇CId⦈› for α ℭ +
  assumes fin_cat_length[cat_cs_simps]: "vcard ℭ = 6⇩ℕ"
    and fin_cat_finite_semicategory[slicing_intros]: 
      "finite_semicategory α (cat_smc ℭ)"
    and fin_cat_CId_vdomain[cat_cs_simps]: "𝒟⇩∘ (ℭ⦇CId⦈) = ℭ⦇Obj⦈"
    and fin_cat_CId_is_arr[cat_cs_intros]: 
      "a ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and fin_cat_CId_left_left[cat_cs_simps]:
      "f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and fin_cat_CId_right_left[cat_cs_simps]:
      "f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = f"

lemmas [slicing_intros] = finite_category.fin_cat_finite_semicategory


text‹Rules.›

lemma (in finite_category) fin_category_axioms'[cat_small_cs_intros]:
  assumes "α' = α"
  shows "finite_category α' ℭ"
  unfolding assms by (rule finite_category_axioms)

mk_ide rf finite_category_def[unfolded finite_category_axioms_def]
  |intro finite_categoryI|
  |dest finite_categoryD[dest]|
  |elim finite_categoryE[elim]|

lemma finite_categoryI':
  assumes "category α ℭ"  and "vfinite (ℭ⦇Obj⦈)" and "vfinite (ℭ⦇Arr⦈)"
  shows "finite_category α ℭ"
proof-
  interpret category α ℭ by (rule assms(1))
  show ?thesis
  proof(intro finite_categoryI)
    from assms show "finite_semicategory α (cat_smc ℭ)"
      by (intro finite_semicategoryI') (auto simp: slicing_simps)
  qed (auto simp: vfsequence_axioms cat_cs_simps cat_cs_intros)
qed

lemma finite_categoryI'': 
  assumes "tiny_category α ℭ" and "vfinite (ℭ⦇Obj⦈)" and "vfinite (ℭ⦇Arr⦈)"
  shows "finite_category α ℭ"
  using assms by (intro finite_categoryI') (auto intro: cat_small_cs_intros)


text‹Slicing.›

context finite_category
begin

interpretation smc: finite_semicategory α ‹cat_smc ℭ›
  by (rule fin_cat_finite_semicategory) 

lemmas_with [unfolded slicing_simps]:
  fin_cat_tiny_semicategory = smc.tiny_semicategory_axioms
  and fin_smc_Obj_vfinite[cat_small_cs_intros] = smc.fin_smc_Obj_vfinite
  and fin_smc_Arr_vfinite[cat_small_cs_intros] = smc.fin_smc_Arr_vfinite

end


text‹Elementary properties.›

sublocale finite_category ⊆ tiny_category
  by (rule tiny_categoryI) 
    (
      auto 
        simp: vfsequence_axioms 
        intro:
          cat_cs_intros cat_cs_simps cat_small_cs_intros
          finite_category.fin_cat_tiny_semicategory
    )

lemmas (in finite_category) fin_cat_tiny_category = tiny_category_axioms

lemmas [cat_small_cs_intros] = finite_category.fin_cat_tiny_category

lemma (in finite_category) fin_cat_in_Vset: "ℭ ∈⇩∘ Vset α"
  by (rule tiny_cat_in_Vset)


text‹Size.›

lemma small_finite_categories[simp]: "small {ℭ. finite_category α ℭ}"
proof(rule down)
  show "{ℭ. finite_category α ℭ} ⊆ elts (set {ℭ. tiny_category  α ℭ})" 
    by (auto intro: cat_small_cs_intros)
qed

lemma small_finite_categories_vsubset_Vset: 
  "set {ℭ. finite_category α ℭ} ⊆⇩∘ Vset α" 
  by (rule vsubsetI) (simp_all add: finite_category.fin_cat_in_Vset)


subsubsection‹Opposite finite category›

lemma (in finite_category) finite_category_op: "finite_category α (op_cat ℭ)"
  by (intro finite_categoryI', unfold cat_op_simps) 
    (auto simp: cat_cs_intros cat_small_cs_intros)

lemmas finite_category_op[cat_op_intros] = finite_category.finite_category_op

text‹\newpage›

end