Theory CZH_SMC_GRPH
section‹‹GRPH› as a semicategory›
theory CZH_SMC_GRPH
imports
CZH_DG_Simple
CZH_DG_GRPH
CZH_SMC_Small_Semicategory
begin
subsection‹Background›
text‹
The methodology for the exposition of ‹GRPH› as a semicategory is analogous
to the one used in the previous chapter for the exposition of ‹GRPH›
as a digraph.
›
named_theorems smc_GRPH_cs_simps
named_theorems smc_GRPH_cs_intros
subsection‹Definition and elementary properties›
definition smc_GRPH :: "V ⇒ V"
where "smc_GRPH α =
[
set {ℭ. digraph α ℭ},
all_dghms α,
(λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomDom⦈),
(λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomCod⦈),
(λ𝔊𝔉∈⇩∘composable_arrs (dg_GRPH α). 𝔊𝔉⦇0⦈ ∘⇩D⇩G⇩H⇩M 𝔊𝔉⦇1⇩ℕ⦈)
]⇩∘"
text‹Components.›
lemma smc_GRPH_components:
shows "smc_GRPH α⦇Obj⦈ = set {ℭ. digraph α ℭ}"
and "smc_GRPH α⦇Arr⦈ = all_dghms α"
and "smc_GRPH α⦇Dom⦈ = (λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomDom⦈)"
and "smc_GRPH α⦇Cod⦈ = (λ𝔉∈⇩∘all_dghms α. 𝔉⦇HomCod⦈)"
and "smc_GRPH α⦇Comp⦈ =
(λ𝔊𝔉∈⇩∘composable_arrs (dg_GRPH α). 𝔊𝔉⦇0⦈ ∘⇩D⇩G⇩H⇩M 𝔊𝔉⦇1⇩ℕ⦈)"
unfolding smc_GRPH_def dg_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma smc_dg_GRPH: "smc_dg (smc_GRPH α) = dg_GRPH α"
proof(rule vsv_eqI)
show "vsv (smc_dg (smc_GRPH α))" unfolding smc_dg_def by auto
show "vsv (dg_GRPH α)" unfolding dg_GRPH_def by auto
have dom_lhs: "𝒟⇩∘ (smc_dg (smc_GRPH α)) = 4⇩ℕ"
unfolding smc_dg_def by (simp add: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ (dg_GRPH α) = 4⇩ℕ"
unfolding dg_GRPH_def by (simp add: nat_omega_simps)
show "𝒟⇩∘ (smc_dg (smc_GRPH α)) = 𝒟⇩∘ (dg_GRPH α)"
unfolding dom_lhs dom_rhs by simp
show "a ∈⇩∘ 𝒟⇩∘ (smc_dg (smc_GRPH α)) ⟹ smc_dg (smc_GRPH α)⦇a⦈ = dg_GRPH α⦇a⦈"
for a
by
(
unfold dom_lhs,
elim_in_numeral,
unfold smc_dg_def dg_field_simps smc_GRPH_def dg_GRPH_def
)
(auto simp: nat_omega_simps)
qed
lemmas_with [folded smc_dg_GRPH, unfolded slicing_simps]:
smc_GRPH_ObjI = dg_GRPH_ObjI
and smc_GRPH_ObjD = dg_GRPH_ObjD
and smc_GRPH_ObjE = dg_GRPH_ObjE
and smc_GRPH_Obj_iff[smc_GRPH_cs_simps] = dg_GRPH_Obj_iff
and smc_GRPH_Dom_app[smc_GRPH_cs_simps] = dg_GRPH_Dom_app
and smc_GRPH_Cod_app[smc_GRPH_cs_simps] = dg_GRPH_Cod_app
and smc_GRPH_is_arrI = dg_GRPH_is_arrI
and smc_GRPH_is_arrD = dg_GRPH_is_arrD
and smc_GRPH_is_arrE = dg_GRPH_is_arrE
and smc_GRPH_is_arr_iff[smc_GRPH_cs_simps] = dg_GRPH_is_arr_iff
subsection‹Composable arrows›
lemma smc_GRPH_composable_arrs_dg_GRPH:
"composable_arrs (dg_GRPH α) = composable_arrs (smc_GRPH α)"
unfolding composable_arrs_def smc_dg_GRPH[symmetric] slicing_simps by auto
lemma smc_GRPH_Comp:
"smc_GRPH α⦇Comp⦈ = (λ𝔊𝔉∈⇩∘composable_arrs (smc_GRPH α). 𝔊𝔉⦇0⦈ ∘⇩D⇩G⇩H⇩M 𝔊𝔉⦇1⇩ℕ⦈)"
unfolding smc_GRPH_components smc_GRPH_composable_arrs_dg_GRPH ..
subsection‹Composition›
lemma smc_GRPH_Comp_app:
assumes "𝔊 : 𝔅 ↦⇘smc_GRPH α⇙ ℭ" and "𝔉 : 𝔄 ↦⇘smc_GRPH α⇙ 𝔅"
shows "𝔊 ∘⇩A⇘smc_GRPH α⇙ 𝔉 = 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉"
proof-
from assms have "[𝔊, 𝔉]⇩∘ ∈⇩∘ composable_arrs (smc_GRPH α)"
by (auto intro: smc_cs_intros)
then show "𝔊 ∘⇩A⇘smc_GRPH α⇙ 𝔉 = 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉"
unfolding smc_GRPH_Comp by (simp add: nat_omega_simps)
qed
lemma smc_GRPH_Comp_vdomain:
"𝒟⇩∘ (smc_GRPH α⦇Comp⦈) = composable_arrs (smc_GRPH α)"
unfolding smc_GRPH_Comp by auto
subsection‹‹GRPH› is a semicategory›
lemma (in 𝒵) tiny_semicategory_smc_GRPH:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "tiny_semicategory β (smc_GRPH α)"
proof(intro tiny_semicategoryI, unfold smc_GRPH_is_arr_iff)
show "vfsequence (smc_GRPH α)" unfolding smc_GRPH_def by auto
show "vcard (smc_GRPH α) = 5⇩ℕ"
unfolding smc_GRPH_def by (simp add: nat_omega_simps)
show "(gf ∈⇩∘ 𝒟⇩∘ (smc_GRPH α⦇Comp⦈)) ⟷
(∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦↦⇩D⇩G⇘α⇙ c ∧ f : a ↦↦⇩D⇩G⇘α⇙ b)"
for gf
unfolding smc_GRPH_Comp_vdomain
proof
show "gf ∈⇩∘ composable_arrs (smc_GRPH α) ⟹
∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦↦⇩D⇩G⇘α⇙ c ∧ f : a ↦↦⇩D⇩G⇘α⇙ b"
by (elim composable_arrsE) (auto simp: smc_GRPH_is_arr_iff)
next
assume "∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦↦⇩D⇩G⇘α⇙ c ∧ f : a ↦↦⇩D⇩G⇘α⇙ b"
with smc_GRPH_is_arr_iff show "gf ∈⇩∘ composable_arrs (smc_GRPH α)"
unfolding smc_GRPH_Comp_vdomain by (auto intro: smc_cs_intros)
qed
show "⟦ g : b ↦↦⇩D⇩G⇘α⇙ c; f : a ↦↦⇩D⇩G⇘α⇙ b ⟧ ⟹
g ∘⇩A⇘smc_GRPH α⇙ f : a ↦↦⇩D⇩G⇘α⇙ c"
for g b c f a
by (auto simp: smc_GRPH_Comp_app dghm_comp_is_dghm smc_GRPH_cs_simps)
fix h c d g b f a
assume "h : c ↦↦⇩D⇩G⇘α⇙ d" "g : b ↦↦⇩D⇩G⇘α⇙ c" "f : a ↦↦⇩D⇩G⇘α⇙ b"
moreover then have "g ∘⇩D⇩G⇩H⇩M f : a ↦↦⇩D⇩G⇘α⇙ c" "h ∘⇩D⇩G⇩H⇩M g : b ↦↦⇩D⇩G⇘α⇙ d"
by (auto simp: dghm_comp_is_dghm smc_GRPH_cs_simps)
ultimately show
"h ∘⇩A⇘smc_GRPH α⇙ g ∘⇩A⇘smc_GRPH α⇙ f =
h ∘⇩A⇘smc_GRPH α⇙ (g ∘⇩A⇘smc_GRPH α⇙ f)"
by (simp add: smc_GRPH_is_arr_iff smc_GRPH_Comp_app dghm_comp_assoc)
qed (simp_all add: assms smc_dg_GRPH tiny_digraph_dg_GRPH smc_GRPH_components)
subsection‹Initial object›
lemma (in 𝒵) smc_GRPH_obj_initialI: "obj_initial (smc_GRPH α) dg_0"
unfolding obj_initial_def
proof
(
intro obj_terminalI,
unfold smc_op_simps smc_GRPH_is_arr_iff smc_GRPH_Obj_iff
)
show "digraph α dg_0" by (intro digraph_dg_0)
fix 𝔄 assume "digraph α 𝔄"
then interpret digraph α 𝔄 .
show "∃!f. f : dg_0 ↦↦⇩D⇩G⇘α⇙ 𝔄"
proof
show dghm_0: "dghm_0 𝔄 : dg_0 ↦↦⇩D⇩G⇘α⇙ 𝔄"
by (simp add: dghm_0_is_ft_dghm digraph_axioms is_ft_dghm.axioms(1))
fix 𝔉 assume prems: "𝔉 : dg_0 ↦↦⇩D⇩G⇘α⇙ 𝔄"
then interpret 𝔉: is_dghm α dg_0 𝔄 𝔉 .
show "𝔉 = dghm_0 𝔄"
proof(rule dghm_eqI)
from dghm_0 show "dghm_0 𝔄 : dg_0 ↦↦⇩D⇩G⇘α⇙ 𝔄"
unfolding smc_GRPH_is_arr_iff by simp
have [simp]: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 0" by (simp add: dg_cs_simps dg_0_components)
with 𝔉.ObjMap.vdomain_vrange_is_vempty show "𝔉⦇ObjMap⦈ = dghm_0 𝔄⦇ObjMap⦈"
by
(
auto
intro: 𝔉.ObjMap.vsv_vrange_vempty
simp: dg_0_components dghm_0_components
)
from 𝔉.dghm_ObjMap_vdomain have "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 0"
by
(
auto
simp: 𝔉.dghm_ArrMap_vdomain
intro: 𝔉.HomDom.dg_Arr_vempty_if_Obj_vempty
)
then show "𝔉⦇ArrMap⦈ = dghm_0 𝔄⦇ArrMap⦈"
by
(
metis
𝔉.ArrMap.vsv_axioms
dghm_0_components(2)
vsv.vdomain_vrange_is_vempty
vsv.vsv_vrange_vempty
)
qed (auto simp: dghm_0_components prems)
qed
qed
lemma (in 𝒵) smc_GRPH_obj_initialD:
assumes "obj_initial (smc_GRPH α) 𝔄"
shows "𝔄 = dg_0"
using assms unfolding obj_initial_def
proof
(
elim obj_terminalE,
unfold smc_op_simps smc_GRPH_is_arr_iff smc_GRPH_Obj_iff
)
assume prems: "digraph α 𝔄" "digraph α 𝔅 ⟹ ∃!𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" for 𝔅
from prems(2)[OF digraph_dg_0] obtain 𝔉 where 𝔉: "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ dg_0"
by meson
interpret 𝔉: is_dghm α 𝔄 dg_0 𝔉 by (rule 𝔉)
have "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 0"
unfolding dg_0_components(1)[symmetric] by (simp add: 𝔉.dghm_ObjMap_vrange)
then have "𝔉⦇ObjMap⦈ = 0" by (auto intro: 𝔉.ObjMap.vsv_vrange_vempty)
with 𝔉.dghm_ObjMap_vdomain have Obj[simp]: "𝔄⦇Obj⦈ = 0" by auto
have "ℛ⇩∘ (𝔉⦇ArrMap⦈) ⊆⇩∘ 0"
unfolding dg_0_components(2)[symmetric]
by (simp add: 𝔉.dghm_ArrMap_vrange)
then have "𝔉⦇ArrMap⦈ = 0" by (auto intro: 𝔉.ArrMap.vsv_vrange_vempty)
with 𝔉.dghm_ArrMap_vdomain have Arr[simp]: "𝔄⦇Arr⦈ = 0" by auto
from Arr 𝔉.HomDom.dg_Dom_vempty_if_Arr_vempty have [simp]: "𝔄⦇Dom⦈ = 0"
by auto
from Arr 𝔉.HomDom.dg_Cod_vempty_if_Arr_vempty have [simp]: "𝔄⦇Cod⦈ = 0"
by auto
show "𝔄 = dg_0"
by (rule dg_eqI[of α]) (simp_all add: prems(1) dg_0_components digraph_dg_0)
qed
lemma (in 𝒵) smc_GRPH_obj_initialE:
assumes "obj_initial (smc_GRPH α) 𝔄"
obtains "𝔄 = dg_0"
using assms by (auto dest: smc_GRPH_obj_initialD)
lemma (in 𝒵) smc_GRPH_obj_initial_iff[smc_GRPH_cs_simps]:
"obj_initial (smc_GRPH α) 𝔄 ⟷ 𝔄 = dg_0"
using smc_GRPH_obj_initialI smc_GRPH_obj_initialD by auto
subsection‹Terminal object›
lemma (in 𝒵) smc_GRPH_obj_terminalI[smc_GRPH_cs_intros]:
assumes "a ∈⇩∘ Vset α" and "f ∈⇩∘ Vset α"
shows "obj_terminal (smc_GRPH α) (dg_1 a f)"
proof
(
intro obj_terminalI,
unfold smc_op_simps smc_GRPH_is_arr_iff smc_GRPH_Obj_iff
)
fix 𝔄 assume "digraph α 𝔄"
then interpret digraph α 𝔄 .
show "∃!𝔉'. 𝔉' : 𝔄 ↦↦⇩D⇩G⇘α⇙ dg_1 a f"
proof
show dghm_1: "dghm_const 𝔄 (dg_1 a f) a f : 𝔄 ↦↦⇩D⇩G⇘α⇙ dg_1 a f"
by
(
auto simp:
assms
dg_1_is_arr_iff
dghm_const_is_dghm
digraph_axioms'
digraph_dg_1
)
fix 𝔉' assume prems: "𝔉' : 𝔄 ↦↦⇩D⇩G⇘α⇙ dg_1 a f"
then interpret 𝔉': is_dghm α 𝔄 ‹dg_1 a f› 𝔉' .
show "𝔉' = dghm_const 𝔄 (dg_1 a f) a f"
proof(rule dghm_eqI, unfold dghm_const_components)
show "dghm_const 𝔄 (dg_1 a f) a f : 𝔄 ↦↦⇩D⇩G⇘α⇙ dg_1 a f" by (rule dghm_1)
show "𝔉'⦇ObjMap⦈ = vconst_on (𝔄⦇Obj⦈) a"
proof(cases‹𝔄⦇Obj⦈ = 0›)
case True
then have "𝔉'⦇ObjMap⦈ = 0"
by
(
simp add:
𝔉'.ObjMap.vdomain_vrange_is_vempty
𝔉'.dghm_ObjMap_vsv
vsv.vsv_vrange_vempty
)
with True show ?thesis by simp
next
case False
then have "𝒟⇩∘ (𝔉'⦇ObjMap⦈) ≠ 0" by (auto simp: 𝔉'.dghm_ObjMap_vdomain)
with False have "ℛ⇩∘ (𝔉'⦇ObjMap⦈) ≠ 0" by fastforce
moreover from 𝔉'.dghm_ObjMap_vrange have "ℛ⇩∘ (𝔉'⦇ObjMap⦈) ⊆⇩∘ set {a}"
by (simp add: dg_1_components)
ultimately have "ℛ⇩∘ (𝔉'⦇ObjMap⦈) = set {a}" by auto
with 𝔉'.dghm_ObjMap_vdomain show ?thesis
by (intro vsv.vsv_is_vconst_onI) blast+
qed
show "𝔉'⦇ArrMap⦈ = vconst_on (𝔄⦇Arr⦈) f"
proof(cases‹𝔄⦇Arr⦈ = 0›)
case True
then have "𝔉'⦇ArrMap⦈ = 0"
by
(
simp add:
𝔉'.ArrMap.vdomain_vrange_is_vempty
𝔉'.dghm_ArrMap_vsv
vsv.vsv_vrange_vempty
)
with True show ?thesis by simp
next
case False
then have "𝒟⇩∘ (𝔉'⦇ArrMap⦈) ≠ 0" by (auto simp: 𝔉'.dghm_ArrMap_vdomain)
with False have "ℛ⇩∘ (𝔉'⦇ArrMap⦈) ≠ 0"
by (force simp: 𝔉'.ArrMap.vdomain_vrange_is_vempty)
moreover from 𝔉'.dghm_ArrMap_vrange have "ℛ⇩∘ (𝔉'⦇ArrMap⦈) ⊆⇩∘ set {f}"
by (simp add: dg_1_components)
ultimately have "ℛ⇩∘ (𝔉'⦇ArrMap⦈) = set {f}" by auto
then show ?thesis
by (intro vsv.vsv_is_vconst_onI) (auto simp: 𝔉'.dghm_ArrMap_vdomain)
qed
qed (auto intro: prems)
qed
qed (simp add: assms digraph_dg_1)
lemma (in 𝒵) smc_GRPH_obj_terminalE:
assumes "obj_terminal (smc_GRPH α) 𝔅"
obtains a f where "a ∈⇩∘ Vset α" and "f ∈⇩∘ Vset α" and "𝔅 = dg_1 a f"
using assms
proof
(
elim obj_terminalE;
unfold smc_op_simps smc_GRPH_is_arr_iff smc_GRPH_Obj_iff
)
assume prems: "digraph α 𝔅" "digraph α 𝔄 ⟹ ∃!𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" for 𝔄
then interpret 𝔅: digraph α 𝔅 by simp
obtain a where 𝔅_Obj: "𝔅⦇Obj⦈ = set {a}" and a: "a ∈⇩∘ Vset α"
proof-
have dg_10: "digraph α (dg_10 0)" by (rule digraph_dg_10) auto
from prems(2)[OF dg_10] obtain 𝔉
where 𝔉: "𝔉 : dg_10 0 ↦↦⇩D⇩G⇘α⇙ 𝔅"
and 𝔊𝔉: "𝔊 : dg_10 0 ↦↦⇩D⇩G⇘α⇙ 𝔅 ⟹ 𝔊 = 𝔉" for 𝔊
by fastforce
interpret 𝔉: is_dghm α ‹dg_10 0› 𝔅 𝔉 by (rule 𝔉)
have "𝒟⇩∘ (𝔉⦇ObjMap⦈) = set {0}"
by (simp add: dg_cs_simps dg_10_components)
then obtain a where vrange_𝔉[simp]: "ℛ⇩∘ (𝔉⦇ObjMap⦈) = set {a}"
by
(
auto
simp: dg_cs_simps
intro: 𝔉.ObjMap.vsv_vdomain_vsingleton_vrange_vsingleton
)
with 𝔅.dg_Obj_vsubset_Vset 𝔉.dghm_ObjMap_vrange have [simp]: "a ∈⇩∘ Vset α"
by auto
from 𝔉.dghm_ObjMap_vrange have "set {a} ⊆⇩∘ 𝔅⦇Obj⦈" by simp
moreover have "𝔅⦇Obj⦈ ⊆⇩∘ set {a}"
proof(rule ccontr)
assume "¬𝔅⦇Obj⦈ ⊆⇩∘ set {a}"
then obtain b where ba: "b ≠ a" and b: "b ∈⇩∘ 𝔅⦇Obj⦈" by force
define 𝔊 where "𝔊 = [set {⟨0, b⟩}, 0, dg_10 0, 𝔅]⇩∘"
have 𝔊_components:
"𝔊⦇ObjMap⦈ = set {⟨0, b⟩}"
"𝔊⦇ArrMap⦈ = 0"
"𝔊⦇HomDom⦈ = dg_10 0"
"𝔊⦇HomCod⦈ = 𝔅"
unfolding 𝔊_def dghm_field_simps by (simp_all add: nat_omega_simps)
have 𝔊: "𝔊 : dg_10 0 ↦↦⇩D⇩G⇘α⇙ 𝔅"
by (rule is_dghmI, unfold 𝔊_components dg_10_components)
(
auto simp:
dg_cs_intros
nat_omega_simps
digraph_dg_10
𝔊_def
dg_10_is_arr_iff
b
vsubset_vsingleton_leftI
)
then have 𝔊_def: "𝔊 = 𝔉" by (rule 𝔊𝔉)
have "ℛ⇩∘ (𝔊⦇ObjMap⦈) = set {b}" unfolding 𝔊_components by simp
with vrange_𝔉 ba show False unfolding 𝔊_def by simp
qed
ultimately have "𝔅⦇Obj⦈ = set {a}" by simp
with that show ?thesis by simp
qed
obtain f where 𝔅_Arr: "𝔅⦇Arr⦈ = set {f}" and f: "f ∈⇩∘ Vset α"
proof-
from prems(2)[OF digraph_dg_1, of 0 0] obtain 𝔉
where 𝔉: "𝔉 : dg_1 0 0 ↦↦⇩D⇩G⇘α⇙ 𝔅"
and 𝔊𝔉: "𝔊 : dg_1 0 0 ↦↦⇩D⇩G⇘α⇙ 𝔅 ⟹ 𝔊 = 𝔉" for 𝔊
by fastforce
interpret 𝔉: is_dghm α ‹dg_1 0 0› 𝔅 𝔉 by (rule 𝔉)
have "𝒟⇩∘ (𝔉⦇ObjMap⦈) = set {0}"
by (simp add: dg_cs_simps dg_1_components)
then obtain a' where "ℛ⇩∘ (𝔉⦇ObjMap⦈) = set {a'}"
by
(
auto
simp: dg_cs_simps
intro: 𝔉.ObjMap.vsv_vdomain_vsingleton_vrange_vsingleton
)
with 𝔅_Obj 𝔉.dghm_ObjMap_vrange have "ℛ⇩∘ (𝔉⦇ObjMap⦈) = set {a}" by auto
have "𝒟⇩∘ (𝔉⦇ArrMap⦈) = set {0}" by (simp add: dg_cs_simps dg_1_components)
then obtain f where vrange_𝔉[simp]: "ℛ⇩∘ (𝔉⦇ArrMap⦈) = set {f}"
by
(
auto
simp: dg_cs_simps
intro: 𝔉.ArrMap.vsv_vdomain_vsingleton_vrange_vsingleton
)
with 𝔅.dg_Arr_vsubset_Vset 𝔉.dghm_ArrMap_vrange have [simp]: "f ∈⇩∘ Vset α"
by auto
from 𝔉.dghm_ArrMap_vrange have "set {f} ⊆⇩∘ 𝔅⦇Arr⦈" by simp
moreover have "𝔅⦇Arr⦈ ⊆⇩∘ set {f}"
proof(rule ccontr)
assume "¬𝔅⦇Arr⦈ ⊆⇩∘ set {f}"
then obtain g where gf: "g ≠ f" and g: "g ∈⇩∘ 𝔅⦇Arr⦈" by force
have g: "g : a ↦⇘𝔅⇙ a"
proof(intro is_arrI)
from g 𝔅_Obj show "𝔅⦇Dom⦈⦇g⦈ = a"
by (metis 𝔅.dg_is_arrD(2) is_arr_def vsingleton_iff)
from g 𝔅_Obj show "𝔅⦇Cod⦈⦇g⦈ = a"
by (metis 𝔅.dg_is_arrD(3) is_arr_def vsingleton_iff)
qed (auto simp: g)
define 𝔊 where "𝔊 = [set {⟨0, a⟩}, set {⟨0, g⟩}, dg_1 0 0, 𝔅]⇩∘"
have 𝔊_components:
"𝔊⦇ObjMap⦈ = set {⟨0, a⟩}"
"𝔊⦇ArrMap⦈ = set {⟨0, g⟩}"
"𝔊⦇HomDom⦈ = dg_1 0 0"
"𝔊⦇HomCod⦈ = 𝔅"
unfolding 𝔊_def dghm_field_simps by (simp_all add: nat_omega_simps)
have 𝔊: "𝔊 : dg_1 0 0 ↦↦⇩D⇩G⇘α⇙ 𝔅"
by (rule is_dghmI, unfold 𝔊_components dg_1_components)
(
auto simp:
dg_cs_intros nat_omega_simps 𝔊_def dg_1_is_arr_iff 𝔅_Obj g
)
then have 𝔊_def: "𝔊 = 𝔉" by (rule 𝔊𝔉)
have "ℛ⇩∘ (𝔊⦇ArrMap⦈) = set {g}" unfolding 𝔊_components by simp
with vrange_𝔉 gf show False unfolding 𝔊_def by simp
qed
ultimately have "𝔅⦇Arr⦈ = set {f}" by simp
with that show ?thesis by simp
qed
have "𝔅 = dg_1 a f"
proof(rule dg_eqI[of α], unfold dg_1_components)
show "𝔅⦇Obj⦈ = set {a}" by (simp add: 𝔅_Obj)
moreover show "𝔅⦇Arr⦈ = set {f}" by (simp add: 𝔅_Arr)
ultimately have "𝔅⦇Dom⦈⦇f⦈ = a" "𝔅⦇Cod⦈⦇f⦈ = a"
by (metis 𝔅.dg_is_arrE is_arr_def vsingleton_iff)+
have "𝒟⇩∘ (𝔅⦇Dom⦈) = set {f}" by (simp add: dg_cs_simps 𝔅_Arr)
moreover from 𝔅.Dom.vsv_vrange_vempty 𝔅.dg_Dom_vdomain 𝔅.dg_Dom_vrange
have "ℛ⇩∘ (𝔅⦇Dom⦈) = set {a}" by (fastforce simp: 𝔅_Arr 𝔅_Obj)
ultimately show "𝔅⦇Dom⦈ = set {⟨f, a⟩}"
using 𝔅.Dom.vsv_vdomain_vrange_vsingleton by simp
have "𝒟⇩∘ (𝔅⦇Cod⦈) = set {f}" by (simp add: dg_cs_simps 𝔅_Arr)
moreover from 𝔅.Cod.vsv_vrange_vempty 𝔅.dg_Cod_vdomain 𝔅.dg_Cod_vrange
have "ℛ⇩∘ (𝔅⦇Cod⦈) = set {a}"
by (fastforce simp: 𝔅_Arr 𝔅_Obj)
ultimately show "𝔅⦇Cod⦈ = set {⟨f, a⟩}"
using assms 𝔅.Cod.vsv_vdomain_vrange_vsingleton by simp
qed (auto simp: dg_cs_intros 𝔅_Obj digraph_dg_1 a f)
with a f that show ?thesis by auto
qed
text‹\newpage›
end