Theory CZH_ECAT_Small_Category
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}
}.
›
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