Theory CZH_DG_Small_Digraph

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for digraphs›
theory CZH_DG_Small_Digraph
  imports CZH_DG_Digraph
begin



subsection‹Background›

named_theorems dg_small_cs_simps
named_theorems dg_small_cs_intros



subsection‹Tiny digraph›


subsubsection‹Definition and elementary properties›

locale tiny_digraph = 𝒵 α + vfsequence ℭ + Dom: vsv ‹ℭ⦇Dom⦈› + Cod: vsv ‹ℭ⦇Cod⦈› 
  for α ℭ +
  assumes tiny_dg_length[dg_cs_simps]: "vcard ℭ = 4⇩ℕ"  
    and tiny_dg_Dom_vdomain[dg_cs_simps]: "𝒟⇩∘ (ℭ⦇Dom⦈) = ℭ⦇Arr⦈"    
    and tiny_dg_Dom_vrange: "ℛ⇩∘ (ℭ⦇Dom⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and tiny_dg_Cod_vdomain[dg_cs_simps]: "𝒟⇩∘ (ℭ⦇Cod⦈) = ℭ⦇Arr⦈"
    and tiny_dg_Cod_vrange: "ℛ⇩∘ (ℭ⦇Cod⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and tiny_dg_Obj_in_Vset[dg_small_cs_intros]: "ℭ⦇Obj⦈ ∈⇩∘ Vset α"
    and tiny_dg_Arr_in_Vset[dg_small_cs_intros]: "ℭ⦇Arr⦈ ∈⇩∘ Vset α"

lemmas [dg_small_cs_intros] = 
  tiny_digraph.tiny_dg_Obj_in_Vset
  tiny_digraph.tiny_dg_Arr_in_Vset


text‹Rules.›

lemma (in tiny_digraph) tiny_digraph_axioms'[dg_small_cs_intros]:
  assumes "α' = α"
  shows "tiny_digraph α' ℭ"
  unfolding assms by (rule tiny_digraph_axioms)

mk_ide rf tiny_digraph_def[unfolded tiny_digraph_axioms_def]
  |intro tiny_digraphI|
  |dest tiny_digraphD[dest]|
  |elim tiny_digraphE[elim]|

lemma tiny_digraphI':
  assumes "digraph α ℭ" and "ℭ⦇Obj⦈ ∈⇩∘ Vset α" and "ℭ⦇Arr⦈ ∈⇩∘ Vset α"
  shows "tiny_digraph α ℭ"
  using assms by (meson digraphD(5,6,7,8,9) digraph_def tiny_digraphI)


text‹Elementary properties.›

sublocale tiny_digraph ⊆ digraph 
proof(rule digraphI)
  from tiny_dg_Obj_in_Vset show "ℭ⦇Obj⦈ ⊆⇩∘ Vset α" by auto
  fix A B assume "A ⊆⇩∘ ℭ⦇Obj⦈" "B ⊆⇩∘ ℭ⦇Obj⦈" "A ∈⇩∘ Vset α" "B ∈⇩∘ Vset α" 
  then have "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom ℭ a b) ⊆⇩∘ ℭ⦇Arr⦈" by auto
  with tiny_dg_Arr_in_Vset show "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom ℭ a b) ∈⇩∘ Vset α" by blast
qed 
  (
    cs_concl cs_shallow
      cs_simp: dg_cs_simps  
      cs_intro: tiny_dg_Cod_vrange tiny_dg_Dom_vrange dg_cs_intros V_cs_intros
  )+

lemmas (in tiny_digraph) tiny_dg_digraph = digraph_axioms

lemmas [dg_small_cs_intros] = tiny_digraph.tiny_dg_digraph


text‹Size.›

lemma (in tiny_digraph) tiny_dg_Dom_in_Vset: "ℭ⦇Dom⦈ ∈⇩∘ Vset α"
proof-
  from 𝒵_Limit_αω have "𝒟⇩∘ (ℭ⦇Dom⦈) ∈⇩∘ Vset α"  
    by (simp add: tiny_dg_Arr_in_Vset dg_cs_simps)
  moreover from tiny_dg_Dom_vrange have "ℛ⇩∘ (ℭ⦇Dom⦈) ∈⇩∘ Vset α" 
    by (auto intro: tiny_dg_Obj_in_Vset)
  ultimately show ?thesis 
    by (simp add: Dom.vbrelation_Limit_in_VsetI 𝒵_Limit_αω)
qed

lemma (in tiny_digraph) tiny_dg_Cod_in_Vset: "ℭ⦇Cod⦈ ∈⇩∘ Vset α"
proof-
  from 𝒵_Limit_αω have "𝒟⇩∘ (ℭ⦇Cod⦈) ∈⇩∘ Vset α"  
    by (simp add: tiny_dg_Arr_in_Vset dg_cs_simps)
  moreover from tiny_dg_Cod_vrange have "ℛ⇩∘ (ℭ⦇Cod⦈) ∈⇩∘ Vset α" 
    by (auto intro: tiny_dg_Obj_in_Vset)
  ultimately show ?thesis 
    by (simp add: Cod.vbrelation_Limit_in_VsetI 𝒵_Limit_αω)
qed

lemma (in tiny_digraph) tiny_dg_in_Vset: "ℭ ∈⇩∘ Vset α"
proof-
  note [dg_cs_intros] = 
    tiny_dg_Obj_in_Vset 
    tiny_dg_Arr_in_Vset
    tiny_dg_Dom_in_Vset
    tiny_dg_Cod_in_Vset
  show ?thesis
    by (subst dg_def) (cs_concl cs_shallow cs_intro: dg_cs_intros V_cs_intros)
qed

lemma small_tiny_digraphs[simp]: "small {ℭ. tiny_digraph α ℭ}"
proof(rule down)
  show "{ℭ. tiny_digraph α ℭ} ⊆ elts (set {ℭ. digraph α ℭ})" 
    by (auto intro: dg_small_cs_intros)
qed

lemma tiny_digraphs_vsubset_Vset: "set {ℭ. tiny_digraph α ℭ} ⊆⇩∘ Vset α"
  by (rule vsubsetI) (simp add: tiny_digraph.tiny_dg_in_Vset)

lemma (in digraph) dg_tiny_digraph_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_digraph β ℭ"
proof(intro tiny_digraphI')
  interpret β: 𝒵 β by (rule assms(1))
  show "digraph β ℭ"
    by (intro dg_digraph_if_ge_Limit)
      (use assms(2) in ‹cs_concl cs_shallow cs_intro: dg_cs_intros›)+
  show "ℭ⦇Obj⦈ ∈⇩∘ Vset β" "ℭ⦇Arr⦈ ∈⇩∘ Vset β" 
    by (auto simp: β.𝒵_β assms(2) dg_Obj_in_Vset dg_Arr_in_Vset)
qed


subsubsection‹Opposite tiny digraph›

lemma (in tiny_digraph) tiny_digraph_op: "tiny_digraph α (op_dg ℭ)"
  by (intro tiny_digraphI', unfold dg_op_simps)
    (auto simp: tiny_dg_Obj_in_Vset tiny_dg_Arr_in_Vset dg_cs_simps dg_op_intros)

lemmas tiny_digraph_op[dg_op_intros] = tiny_digraph.tiny_digraph_op



subsection‹Finite digraph›


subsubsection‹Definition and elementary properties›


text‹
A finite digraph 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_digraph = digraph α ℭ for α ℭ +
  assumes fin_dg_Obj_vfinite[dg_small_cs_intros]: "vfinite (ℭ⦇Obj⦈)"
    and fin_dg_Arr_vfinite[dg_small_cs_intros]: "vfinite (ℭ⦇Arr⦈)"

lemmas [dg_small_cs_intros] = 
  finite_digraph.fin_dg_Obj_vfinite
  finite_digraph.fin_dg_Arr_vfinite


text‹Rules.›

lemma (in finite_digraph) finite_digraph_axioms'[dg_small_cs_intros]:
  assumes "α' = α"
  shows "finite_digraph α' ℭ"
  unfolding assms by (rule finite_digraph_axioms)

mk_ide rf finite_digraph_def[unfolded finite_digraph_axioms_def]
  |intro finite_digraphI|
  |dest finite_digraphD[dest]|
  |elim finite_digraphE[elim]|


text‹Elementary properties.›

sublocale finite_digraph ⊆ tiny_digraph 
proof(rule tiny_digraphI')
  show "ℭ⦇Obj⦈ ∈⇩∘ Vset α"
    by
      (
        cs_concl cs_shallow cs_intro: 
          dg_small_cs_intros V_cs_intros 
          dg_Obj_vsubset_Vset Limit_vfinite_in_VsetI
      )
  show "ℭ⦇Arr⦈ ∈⇩∘ Vset α"
    by 
      (
        cs_concl cs_shallow cs_intro: 
          dg_small_cs_intros V_cs_intros 
          dg_Arr_vsubset_Vset Limit_vfinite_in_VsetI
      )
qed (auto intro: dg_cs_intros)

lemmas (in finite_digraph) fin_dg_tiny_digraph = tiny_digraph_axioms

lemmas [dg_small_cs_intros] = finite_digraph.fin_dg_tiny_digraph


text‹Size.›

lemma small_finite_digraphs[simp]: "small {ℭ. finite_digraph α ℭ}"
proof(rule down)
  show "{ℭ. finite_digraph α ℭ} ⊆ elts (set {ℭ. digraph α ℭ})" 
    by (auto intro: dg_cs_intros)
qed 

lemma finite_digraphs_vsubset_Vset: "set {ℭ. finite_digraph α ℭ} ⊆⇩∘ Vset α"
  by 
    (
      force simp: 
        tiny_digraph.tiny_dg_in_Vset finite_digraph.fin_dg_tiny_digraph
    )


subsubsection‹Opposite finite digraph›

lemma (in finite_digraph) fininte_digraph_op: "finite_digraph α (op_dg ℭ)"
  by (intro finite_digraphI, unfold dg_op_simps)
    (auto simp: dg_small_cs_intros dg_op_intros)

lemmas fininte_digraph_op[dg_op_intros] = finite_digraph.fininte_digraph_op

text‹\newpage›

end