Theory CZH_DG_Simple
section‹Simple digraphs›
theory CZH_DG_Simple
imports CZH_DG_TDGHM
begin
subsection‹Background›
text‹
The section presents a variety of simple digraphs, such as the empty digraph ‹0›
and a digraph with one object and one arrow ‹1›. All of the entities
presented in this section are generalizations of certain simple categories,
whose definitions can be found in \<^cite>‹"mac_lane_categories_2010"›.
›
subsection‹Empty digraph ‹0››
subsubsection‹Definition and elementary properties›
text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›
definition dg_0 :: V
where "dg_0 = [0, 0, 0, 0]⇩∘"
text‹Components.›
lemma dg_0_components:
shows "dg_0⦇Obj⦈ = 0"
and "dg_0⦇Arr⦈ = 0"
and "dg_0⦇Dom⦈ = 0"
and "dg_0⦇Cod⦈ = 0"
unfolding dg_0_def dg_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹‹0› is a digraph›
lemma (in 𝒵) digraph_dg_0[dg_cs_intros]: "digraph α dg_0"
proof(intro digraphI)
show "vfsequence dg_0" unfolding dg_0_def by (simp add: nat_omega_simps)
show "vcard dg_0 = 4⇩ℕ" unfolding dg_0_def by (simp add: nat_omega_simps)
qed (auto simp: dg_0_components)
lemmas [dg_cs_intros] = 𝒵.digraph_dg_0
subsubsection‹Opposite of the digraph ‹0››
lemma op_dg_dg_0[dg_op_simps]: "op_dg (dg_0) = dg_0"
proof(rule dg_eqI, unfold dg_op_simps)
define β where "β = ω + ω"
interpret β: 𝒵 β unfolding β_def by (rule 𝒵_ωω)
show "digraph β (op_dg dg_0)"
by (cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros)
show "digraph β dg_0" by (cs_concl cs_shallow cs_intro: dg_cs_intros)
qed (simp_all add: dg_0_components op_dg_components)
subsubsection‹Arrow with a domain and a codomain›
lemma dg_0_is_arr_iff[simp]: "𝔉 : 𝔄 ↦⇘dg_0⇙ 𝔅 ⟷ False"
by (rule iffI; (elim is_arrE)?) (auto simp: dg_0_components)
subsubsection‹A digraph without objects is empty›
lemma (in digraph) dg_dg_0_if_Obj_0:
assumes "ℭ⦇Obj⦈ = 0"
shows "ℭ = dg_0"
by (rule dg_eqI[of α])
(
auto simp:
dg_cs_intros
assms
digraph_dg_0
dg_0_components
dg_Arr_vempty_if_Obj_vempty
dg_Cod_vempty_if_Arr_vempty
dg_Dom_vempty_if_Arr_vempty
)
subsection‹Empty digraph homomorphism›
subsubsection‹Definition and elementary properties›
definition dghm_0 :: "V ⇒ V"
where "dghm_0 𝔄 = [0, 0, dg_0, 𝔄]⇩∘"
text‹Components.›
lemma dghm_0_components:
shows "dghm_0 𝔄⦇ObjMap⦈ = 0"
and "dghm_0 𝔄⦇ArrMap⦈ = 0"
and "dghm_0 𝔄⦇HomDom⦈ = dg_0"
and "dghm_0 𝔄⦇HomCod⦈ = 𝔄"
unfolding dghm_0_def dghm_field_simps by (simp_all add: nat_omega_simps)
text‹Opposite empty digraph homomorphism.›
lemma op_dghm_dghm_0: "op_dghm (dghm_0 ℭ) = dghm_0 (op_dg ℭ)"
unfolding
dghm_0_def op_dg_def op_dghm_def dg_0_def dghm_field_simps dg_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Object map›
lemma dghm_0_ObjMap_vsv[dg_cs_intros]: "vsv (dghm_0 ℭ⦇ObjMap⦈)"
unfolding dghm_0_components by simp
subsubsection‹Arrow map›
lemma dghm_0_ArrMap_vsv[dg_cs_intros]: "vsv (dghm_0 ℭ⦇ArrMap⦈)"
unfolding dghm_0_components by simp
subsubsection‹Empty digraph homomorphism is a faithful digraph homomorphism›
lemma (in 𝒵) dghm_0_is_ft_dghm:
assumes "digraph α 𝔄"
shows "dghm_0 𝔄 : dg_0 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔄"
proof(rule is_ft_dghmI)
show "dghm_0 𝔄 : dg_0 ↦↦⇩D⇩G⇘α⇙ 𝔄"
proof(rule is_dghmI)
show "vfsequence (dghm_0 𝔄)" unfolding dghm_0_def by simp
show "vcard (dghm_0 𝔄) = 4⇩ℕ"
unfolding dghm_0_def by (simp add: nat_omega_simps)
qed (auto simp: assms digraph_dg_0 dghm_0_components dg_0_components)
qed (auto simp: dg_0_components dghm_0_components)
lemma (in 𝒵) dghm_0_is_ft_dghm'[dghm_cs_intros]:
assumes "digraph α 𝔄"
and "𝔅' = 𝔄"
and "𝔄' = dg_0"
shows "dghm_0 𝔄 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule dghm_0_is_ft_dghm)
lemmas [dghm_cs_intros] = 𝒵.dghm_0_is_ft_dghm'
lemma (in 𝒵) dghm_0_is_dghm:
assumes "digraph α 𝔄"
shows "dghm_0 𝔄 : dg_0 ↦↦⇩D⇩G⇘α⇙ 𝔄"
using dghm_0_is_ft_dghm[OF assms] by auto
lemma (in 𝒵) dghm_0_is_dghm'[dg_cs_intros]:
assumes "digraph α 𝔄"
and "𝔅' = 𝔄"
and "𝔄' = dg_0"
shows "dghm_0 𝔄 : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule dghm_0_is_dghm)
lemmas [dg_cs_intros] = 𝒵.dghm_0_is_dghm'
subsubsection‹Further properties›
lemma is_dghm_is_dghm_0_if_dg_0:
assumes "𝔉 : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ"
shows "𝔉 = dghm_0 ℭ"
proof(rule dghm_eqI)
interpret 𝔉: is_dghm α dg_0 ℭ 𝔉 by (rule assms(1))
show "𝔉 : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ" by (rule assms(1))
then have dom_lhs: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 0" "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 0"
by (cs_concl cs_simp: dg_cs_simps dg_0_components)+
show "dghm_0 ℭ : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ" by (cs_concl cs_intro: dg_cs_intros)
then have dom_rhs: "𝒟⇩∘ (dghm_0 ℭ⦇ObjMap⦈) = 0" "𝒟⇩∘ (dghm_0 ℭ⦇ArrMap⦈) = 0"
by (cs_concl cs_simp: dg_cs_simps dg_0_components)+
show "𝔉⦇ObjMap⦈ = dghm_0 ℭ⦇ObjMap⦈"
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: dg_cs_intros)
show "𝔉⦇ArrMap⦈ = dghm_0 ℭ⦇ArrMap⦈"
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: dg_cs_intros)
qed simp_all
subsection‹Empty transformation of digraph homomorphisms›
subsubsection‹Definition and elementary properties›
definition tdghm_0 :: "V ⇒ V"
where "tdghm_0 ℭ = [0, dghm_0 ℭ, dghm_0 ℭ, dg_0, ℭ]⇩∘"
text‹Components.›
lemma tdghm_0_components:
shows "tdghm_0 ℭ⦇NTMap⦈ = 0"
and [dg_cs_simps]: "tdghm_0 ℭ⦇NTDom⦈ = dghm_0 ℭ"
and [dg_cs_simps]: "tdghm_0 ℭ⦇NTCod⦈ = dghm_0 ℭ"
and [dg_cs_simps]: "tdghm_0 ℭ⦇NTDGDom⦈ = dg_0"
and [dg_cs_simps]: "tdghm_0 ℭ⦇NTDGCod⦈ = ℭ"
unfolding tdghm_0_def nt_field_simps by (simp_all add: nat_omega_simps)
text‹Duality.›
lemma op_tdghm_tdghm_0: "op_tdghm (tdghm_0 ℭ) = tdghm_0 (op_dg ℭ)"
by
(
simp_all add:
tdghm_0_def op_tdghm_def op_dg_def dg_0_def op_dghm_dghm_0
nt_field_simps dg_field_simps nat_omega_simps
)
subsubsection‹Transformation map›
lemma tdghm_0_NTMap_vsv[dg_cs_intros]: "vsv (tdghm_0 ℭ⦇NTMap⦈)"
unfolding tdghm_0_components by simp
lemma tdghm_0_NTMap_vdomain[dg_cs_simps]: "𝒟⇩∘ (tdghm_0 ℭ⦇NTMap⦈) = 0"
unfolding tdghm_0_components by simp
lemma tdghm_0_NTMap_vrange[dg_cs_simps]: "ℛ⇩∘ (tdghm_0 ℭ⦇NTMap⦈) = 0"
unfolding tdghm_0_components by simp
subsubsection‹
Empty transformation of digraph homomorphisms
is a transformation of digraph homomorphisms
›
lemma (in digraph) dg_tdghm_0_is_tdghmI:
"tdghm_0 ℭ : dghm_0 ℭ ↦⇩D⇩G⇩H⇩M dghm_0 ℭ : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ"
proof(intro is_tdghmI)
show "vfsequence (tdghm_0 ℭ)" unfolding tdghm_0_def by simp
show "vcard (tdghm_0 ℭ) = 5⇩ℕ"
unfolding tdghm_0_def by (simp add: nat_omega_simps)
show "tdghm_0 ℭ⦇NTMap⦈⦇a⦈ : dghm_0 ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ dghm_0 ℭ⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ dg_0⦇Obj⦈" for a
using that unfolding dg_0_components by simp
qed
(
cs_concl cs_shallow
cs_simp: dg_cs_simps dg_0_components(1) cs_intro: dg_cs_intros
)+
lemma (in digraph) dg_tdghm_0_is_tdghmI'[dg_cs_intros]:
assumes "𝔉' = dghm_0 ℭ"
and "𝔊' = dghm_0 ℭ"
and "𝔄' = dg_0"
and "𝔅' = ℭ"
and "𝔉' = 𝔉"
and "𝔊' = 𝔊"
shows "tdghm_0 ℭ : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
unfolding assms by (rule dg_tdghm_0_is_tdghmI)
lemmas [dg_cs_intros] = digraph.dg_tdghm_0_is_tdghmI'
lemma is_tdghm_is_tdghm_0_if_dg_0:
assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ"
shows "𝔑 = tdghm_0 ℭ" and "𝔉 = dghm_0 ℭ" and "𝔊 = dghm_0 ℭ"
proof-
interpret 𝔑: is_tdghm α dg_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
show 𝔉_def: "𝔉 = dghm_0 ℭ" and 𝔊_def: "𝔊 = dghm_0 ℭ"
by (auto intro: is_dghm_is_dghm_0_if_dg_0 dg_cs_intros)
show "𝔑 = tdghm_0 ℭ"
proof(rule tdghm_eqI)
show "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ" by (rule assms(1))
then have dom_lhs: "𝒟⇩∘ (𝔑⦇NTMap⦈) = 0"
by (cs_concl cs_simp: dg_cs_simps dg_0_components(1))
show "tdghm_0 ℭ : dghm_0 ℭ ↦⇩D⇩G⇩H⇩M dghm_0 ℭ : dg_0 ↦↦⇩D⇩G⇘α⇙ ℭ"
by (cs_concl cs_intro: dg_cs_intros)
then have dom_rhs: "𝒟⇩∘ (tdghm_0 ℭ⦇NTMap⦈) = 0"
by (cs_concl cs_simp: dg_cs_simps dg_0_components(1))
show "𝔑⦇NTMap⦈ = tdghm_0 ℭ⦇NTMap⦈"
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: dg_cs_intros)
qed (auto simp: 𝔉_def 𝔊_def)
qed
subsection‹‹10›: digraph with one object and no arrows›
subsubsection‹Definition and elementary properties›
definition dg_10 :: "V ⇒ V"
where "dg_10 𝔞 = [set {𝔞}, 0, 0, 0]⇩∘"
text‹Components.›
lemma dg_10_components:
shows "dg_10 𝔞⦇Obj⦈ = set {𝔞}"
and "dg_10 𝔞⦇Arr⦈ = 0"
and "dg_10 𝔞⦇Dom⦈ = 0"
and "dg_10 𝔞⦇Cod⦈ = 0"
unfolding dg_10_def dg_field_simps by (auto simp: nat_omega_simps)
subsubsection‹‹10› is a digraph›
lemma (in 𝒵) digraph_dg_10:
assumes "𝔞 ∈⇩∘ Vset α"
shows "digraph α (dg_10 𝔞)"
proof(intro digraphI)
show "vfsequence (dg_10 𝔞)" unfolding dg_10_def by (simp add: nat_omega_simps)
show "vcard (dg_10 𝔞) = 4⇩ℕ" unfolding dg_10_def by (simp add: nat_omega_simps)
show "(⋃⇩∘a'∈⇩∘A. ⋃⇩∘b'∈⇩∘B. Hom (dg_10 𝔞) a' b') ∈⇩∘ Vset α" for A B
proof-
have "(⋃⇩∘a'∈⇩∘A. ⋃⇩∘b'∈⇩∘B. Hom (dg_10 𝔞) a' b') ⊆⇩∘ dg_10 𝔞⦇Arr⦈" by auto
moreover have "dg_10 𝔞⦇Arr⦈ ⊆⇩∘ 0" unfolding dg_10_components by auto
ultimately show ?thesis using vempty_is_zet vsubset_in_VsetI by presburger
qed
qed (auto simp: assms dg_10_components vsubset_vsingleton_leftI)
subsubsection‹Arrow with a domain and a codomain›
lemma dg_10_is_arr_iff: "𝔉 : 𝔄 ↦⇘dg_10 𝔞⇙ 𝔅 ⟷ False"
unfolding is_arr_def dg_10_components by simp
subsection‹‹1›: digraph with one object and one arrow›
subsubsection‹Definition and elementary properties›
definition dg_1 :: "V ⇒ V ⇒ V"
where "dg_1 𝔞 𝔣 = [set {𝔞}, set {𝔣}, set {⟨𝔣, 𝔞⟩}, set {⟨𝔣, 𝔞⟩}]⇩∘"
text‹Components.›
lemma dg_1_components:
shows "dg_1 𝔞 𝔣⦇Obj⦈ = set {𝔞}"
and "dg_1 𝔞 𝔣⦇Arr⦈ = set {𝔣}"
and "dg_1 𝔞 𝔣⦇Dom⦈ = set {⟨𝔣, 𝔞⟩}"
and "dg_1 𝔞 𝔣⦇Cod⦈ = set {⟨𝔣, 𝔞⟩}"
unfolding dg_1_def dg_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹‹1› is a digraph›
lemma (in 𝒵) digraph_dg_1:
assumes "𝔞 ∈⇩∘ Vset α" and "𝔣 ∈⇩∘ Vset α"
shows "digraph α (dg_1 𝔞 𝔣)"
proof(intro digraphI)
show "vfsequence (dg_1 𝔞 𝔣)" unfolding dg_1_def by (simp add: nat_omega_simps)
show "vcard (dg_1 𝔞 𝔣) = 4⇩ℕ" unfolding dg_1_def by (simp add: nat_omega_simps)
show "(⋃⇩∘a'∈⇩∘A. ⋃⇩∘b'∈⇩∘B. Hom (dg_1 𝔞 𝔣) a' b') ∈⇩∘ Vset α" for A B
proof-
have "(⋃⇩∘a'∈⇩∘A. ⋃⇩∘b'∈⇩∘B. Hom (dg_1 𝔞 𝔣) a' b') ⊆⇩∘ dg_1 𝔞 𝔣⦇Arr⦈" by auto
moreover have "dg_1 𝔞 𝔣⦇Arr⦈ ⊆⇩∘ set {𝔣}" unfolding dg_1_components by auto
moreover from assms(2) have "set {𝔣} ∈⇩∘ Vset α"
by (simp add: Limit_vsingleton_in_VsetI)
ultimately show ?thesis
unfolding dg_1_components by (auto simp: vsubset_in_VsetI)
qed
qed (auto simp: assms dg_1_components vsubset_vsingleton_leftI)
subsubsection‹Arrow with a domain and a codomain›
lemma dg_1_is_arrI:
assumes "a = 𝔞" and "b = 𝔞" and "f = 𝔣"
shows "f : a ↦⇘dg_1 𝔞 𝔣⇙ b"
using assms by (intro is_arrI) (auto simp: dg_1_components)
lemma dg_1_is_arrD:
assumes "f : a ↦⇘dg_1 𝔞 𝔣⇙ b"
shows "a = 𝔞" and "b = 𝔞" and "f = 𝔣"
using assms by (all‹elim is_arrE›) (auto simp: dg_1_components)
lemma dg_1_is_arrE:
assumes "f : a ↦⇘dg_1 𝔞 𝔣⇙ b"
obtains "a = 𝔞" and "b = 𝔞" and "f = 𝔣"
using assms by (elim is_arrE) (force simp: dg_1_components)
lemma dg_1_is_arr_iff: "f : a ↦⇘dg_1 𝔞 𝔣⇙ b ⟷ (a = 𝔞 ∧ b = 𝔞 ∧ f = 𝔣)"
by (rule iffI; (elim is_arrE)?)
(auto simp: dg_1_components intro: dg_1_is_arrI)
text‹\newpage›
end