Theory CZH_SMC_Small_Semicategory

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for semicategories›
theory CZH_SMC_Small_Semicategory
  imports 
    CZH_DG_Small_Digraph
    CZH_SMC_Semicategory
begin



subsection‹Background›


text‹
An explanation of the methodology chosen for the exposition of all
matters related to the size of the semicategories and associated entities
is given in the previous chapter.
›

named_theorems smc_small_cs_simps
named_theorems smc_small_cs_intros



subsection‹Tiny semicategory›


subsubsection‹Definition and elementary properties›

locale tiny_semicategory = 𝒵 α + vfsequence ℭ + Comp: vsv ‹ℭ⦇Comp⦈› for α ℭ +
  assumes tiny_smc_length[smc_cs_simps]: "vcard ℭ = 5⇩ℕ"
    and tiny_smc_tiny_digraph[slicing_intros]: "tiny_digraph α (smc_dg ℭ)"
    and tiny_smc_Comp_vdomain: "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and tiny_smc_Comp_is_arr[smc_cs_intros]: 
      "⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and tiny_smc_assoc[smc_cs_simps]:
      "⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
        (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"

lemmas [smc_cs_simps] = 
  tiny_semicategory.tiny_smc_length
  tiny_semicategory.tiny_smc_assoc

lemmas [slicing_intros] = 
  tiny_semicategory.tiny_smc_Comp_is_arr


text‹Rules.›

lemma (in tiny_semicategory) tiny_semicategory_axioms'[smc_small_cs_intros]:
  assumes "α' = α"
  shows "tiny_semicategory α' ℭ"
  unfolding assms by (rule tiny_semicategory_axioms)

mk_ide rf tiny_semicategory_def[unfolded tiny_semicategory_axioms_def]
  |intro tiny_semicategoryI|
  |dest tiny_semicategoryD[dest]|
  |elim tiny_semicategoryE[elim]|

lemma tiny_semicategoryI': 
  assumes "semicategory α ℭ" and "ℭ⦇Obj⦈ ∈⇩∘ Vset α" and "ℭ⦇Arr⦈ ∈⇩∘ Vset α"
  shows "tiny_semicategory α ℭ"
proof-
  interpret semicategory α ℭ by (rule assms(1))
  show ?thesis
  proof(intro tiny_semicategoryI)
    show "vfsequence ℭ" by (simp add: vfsequence_axioms)
    from assms show "tiny_digraph α (smc_dg ℭ)"
      by (intro tiny_digraphI') (auto simp: slicing_simps)
  qed (auto simp: smc_cs_simps intro: smc_cs_intros)
qed

lemma tiny_semicategoryI'':
  assumes "𝒵 α"
    and "vfsequence ℭ"
    and "vsv (ℭ⦇Comp⦈)"
    and "vcard ℭ = 5⇩ℕ"
    and "vsv (ℭ⦇Dom⦈)"
    and "vsv (ℭ⦇Cod⦈)"
    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 "⋀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 "ℭ⦇Obj⦈ ∈⇩∘ Vset α" 
    and "ℭ⦇Arr⦈ ∈⇩∘ Vset α"
  shows "tiny_semicategory α ℭ"
  by (intro tiny_semicategoryI tiny_digraphI, unfold slicing_simps) 
    (simp_all add: smc_dg_def nat_omega_simps assms)


text‹Slicing.›

context tiny_semicategory
begin

interpretation dg: tiny_digraph α ‹smc_dg ℭ› by (rule tiny_smc_tiny_digraph)

lemmas_with [unfolded slicing_simps]:
  tiny_smc_Obj_in_Vset[smc_small_cs_intros] = dg.tiny_dg_Obj_in_Vset
  and tiny_smc_Arr_in_Vset[smc_small_cs_intros] = dg.tiny_dg_Arr_in_Vset
  and tiny_smc_Dom_in_Vset[smc_small_cs_intros] = dg.tiny_dg_Dom_in_Vset
  and tiny_smc_Cod_in_Vset[smc_small_cs_intros] = dg.tiny_dg_Cod_in_Vset

end


text‹Elementary properties.›

sublocale tiny_semicategory ⊆ semicategory
  by (rule semicategoryI)
    (
      auto 
        simp: 
          vfsequence_axioms
          tiny_digraph.tiny_dg_digraph 
          tiny_smc_tiny_digraph
          tiny_smc_Comp_vdomain         
        intro: smc_cs_intros smc_cs_simps 
    )

lemmas (in tiny_semicategory) tiny_smc_semicategory = semicategory_axioms

lemmas [smc_small_cs_intros] = tiny_semicategory.tiny_smc_semicategory


text‹Size.›

lemma (in tiny_semicategory) tiny_smc_Comp_in_Vset: "ℭ⦇Comp⦈ ∈⇩∘ Vset α"
proof-
  have "ℭ⦇Arr⦈ ∈⇩∘ Vset α" by (simp add: tiny_smc_Arr_in_Vset)
  with Axiom_of_Infinity have "ℭ⦇Arr⦈ ^⇩× 2⇩ℕ ∈⇩∘ Vset α" 
    by (intro Limit_vcpower_in_VsetI) auto
  with Comp.pnop_vdomain have D: "𝒟⇩∘ (ℭ⦇Comp⦈) ∈⇩∘ Vset α" by auto
  moreover from tiny_smc_Arr_in_Vset smc_Comp_vrange have 
    "ℛ⇩∘ (ℭ⦇Comp⦈) ∈⇩∘ Vset α"
    by auto
  ultimately show ?thesis by (simp add: Comp.vbrelation_Limit_in_VsetI)
qed

lemma (in tiny_semicategory) tiny_smc_in_Vset: "ℭ ∈⇩∘ Vset α"
proof-
  note [smc_cs_intros] = 
    tiny_smc_Obj_in_Vset 
    tiny_smc_Arr_in_Vset
    tiny_smc_Dom_in_Vset
    tiny_smc_Cod_in_Vset
    tiny_smc_Comp_in_Vset
  show ?thesis 
    by (subst smc_def) (cs_concl cs_shallow cs_intro: smc_cs_intros V_cs_intros)
qed

lemma small_tiny_semicategories[simp]: "small {ℭ. tiny_semicategory α ℭ}"
proof(rule down)
  show "{ℭ. tiny_semicategory α ℭ} ⊆ elts (set {ℭ. semicategory α ℭ})" 
    by (auto intro: smc_small_cs_intros)
qed

lemma tiny_semicategories_vsubset_Vset: 
  "set {ℭ. tiny_semicategory α ℭ} ⊆⇩∘ Vset α" 
  by (rule vsubsetI) (simp add: tiny_semicategory.tiny_smc_in_Vset)

lemma (in semicategory) smc_tiny_semicategory_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_semicategory β ℭ"
proof(intro tiny_semicategoryI)
  show "tiny_digraph β (smc_dg ℭ)"
    by (rule digraph.dg_tiny_digraph_if_ge_Limit, rule smc_digraph; intro assms)
qed 
  (
    auto simp: 
      assms(1)
      smc_cs_simps 
      smc_cs_intros 
      smc_digraph digraph.dg_tiny_digraph_if_ge_Limit 
      smc_Comp_vdomain vfsequence_axioms
  )


subsubsection‹Opposite tiny semicategory›

lemma (in tiny_semicategory) tiny_semicategory_op: 
  "tiny_semicategory α (op_smc ℭ)"
  by (intro tiny_semicategoryI', unfold smc_op_simps)
    (auto simp: smc_op_intros smc_small_cs_intros)

lemmas tiny_semicategory_op[smc_op_intros] = 
  tiny_semicategory.tiny_semicategory_op



subsection‹Finite semicategory›


subsubsection‹Definition and elementary properties›


text‹
A finite semicategory is a generalization of the concept of a finite category,
as presented in nLab 
\<^cite>‹"noauthor_nlab_nodate"›
\footnote{\url{https://ncatlab.org/nlab/show/finite+category}}.
›

locale finite_semicategory = 𝒵 α + vfsequence ℭ + Comp: vsv ‹ℭ⦇Comp⦈› for α ℭ +
  assumes fin_smc_length[smc_cs_simps]: "vcard ℭ = 5⇩ℕ"
    and fin_smc_finite_digraph[slicing_intros]: "finite_digraph α (smc_dg ℭ)"
    and fin_smc_Comp_vdomain: "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and fin_smc_Comp_is_arr[smc_cs_intros]: 
      "⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and fin_smc_assoc[smc_cs_simps]:
      "⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
        (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"

lemmas [smc_cs_simps] = 
  finite_semicategory.fin_smc_length
  finite_semicategory.fin_smc_assoc

lemmas [slicing_intros] = 
  finite_semicategory.fin_smc_Comp_is_arr


text‹Rules.›

lemma (in finite_semicategory) finite_semicategory_axioms'[smc_small_cs_intros]:
  assumes "α' = α"
  shows "finite_semicategory α' ℭ"
  unfolding assms by (rule finite_semicategory_axioms)

mk_ide rf finite_semicategory_def[unfolded finite_semicategory_axioms_def]
  |intro finite_semicategoryI|
  |dest finite_semicategoryD[dest]|
  |elim finite_semicategoryE[elim]|

lemma finite_semicategoryI': 
  assumes "semicategory α ℭ" and "vfinite (ℭ⦇Obj⦈)" and "vfinite (ℭ⦇Arr⦈)"
  shows "finite_semicategory α ℭ"
proof-
  interpret semicategory α ℭ by (rule assms(1))
  show ?thesis
  proof(intro finite_semicategoryI)
    show "vfsequence ℭ" by (simp add: vfsequence_axioms)
    from assms show "finite_digraph α (smc_dg ℭ)"
      by (intro finite_digraphI) (auto simp: slicing_simps)
  qed (auto simp: smc_cs_simps intro: smc_cs_intros)
qed

lemma finite_semicategoryI'': 
  assumes "tiny_semicategory α ℭ" and "vfinite (ℭ⦇Obj⦈)" and "vfinite (ℭ⦇Arr⦈)"
  shows "finite_semicategory α ℭ"
  using assms by (intro finite_semicategoryI') 
    (auto intro: smc_cs_intros smc_small_cs_intros)


text‹Slicing.›

context finite_semicategory
begin

interpretation dg: finite_digraph α ‹smc_dg ℭ› by (rule fin_smc_finite_digraph)

lemmas_with [unfolded slicing_simps]:
  fin_smc_Obj_vfinite[smc_small_cs_intros] = dg.fin_dg_Obj_vfinite
  and fin_smc_Arr_vfinite[smc_small_cs_intros] = dg.fin_dg_Arr_vfinite

end


text‹Elementary properties.›

sublocale finite_semicategory ⊆ tiny_semicategory
  by (rule tiny_semicategoryI)
    (
      auto simp: 
        vfsequence_axioms
        fin_smc_Comp_vdomain         
        fin_smc_finite_digraph 
        finite_digraph.fin_dg_tiny_digraph
        intro: smc_cs_intros smc_cs_simps 
    )

lemmas (in finite_semicategory) fin_smc_tiny_semicategory = 
  tiny_semicategory_axioms

lemmas [smc_small_cs_intros] = finite_semicategory.fin_smc_tiny_semicategory

lemma (in finite_semicategory) fin_smc_in_Vset: "ℭ ∈⇩∘ Vset α"
  by (rule tiny_smc_in_Vset)


text‹Size.›

lemma small_finite_semicategories[simp]: "small {ℭ. finite_semicategory α ℭ}"
proof(rule down)
  show "{ℭ. finite_semicategory α ℭ} ⊆ elts (set {ℭ. semicategory α ℭ})" 
    by (auto intro: smc_small_cs_intros)
qed

lemma finite_semicategories_vsubset_Vset: 
  "set {ℭ. finite_semicategory α ℭ} ⊆⇩∘ Vset α" 
  by (rule vsubsetI) (simp add: finite_semicategory.fin_smc_in_Vset)
 

subsubsection‹Opposite finite semicategory›

lemma (in finite_semicategory) finite_semicategory_op: 
  "finite_semicategory α (op_smc ℭ)"
  by (intro finite_semicategoryI', unfold smc_op_simps)
    (auto simp: smc_op_intros smc_small_cs_intros)

lemmas finite_semicategory_op[smc_op_intros] = 
  finite_semicategory.finite_semicategory_op

text‹\newpage›

end