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  CIda : a a"
    and tiny_cat_CId_left_left[cat_cs_simps]:
      "f : a b  CIdb Af = f"
    and tiny_cat_CId_right_left[cat_cs_simps]:
      "f : b c  f ACIdb = 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 Af : a c"
    and "c d h b g a f.  h : c d; g : b c; f : a b  
      (h Ag) Af = h A(g Af)"
    and "a. a  Obj  CIda : a a"
    and "a b f. f : a b  CIdb Af = f"
    and "b c f. f : b c  f ACIdb = 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  CIda : a a"
    and fin_cat_CId_left_left[cat_cs_simps]:
      "f : a b  CIdb Af = f"
    and fin_cat_CId_right_left[cat_cs_simps]:
      "f : b c  f ACIdb = 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