Theory CZH_DG_DGHM
section‹Homomorphism of digraphs›
theory CZH_DG_DGHM
imports CZH_DG_Digraph
begin
subsection‹Background›
named_theorems dghm_cs_simps
named_theorems dghm_cs_intros
named_theorems dg_cn_cs_simps
named_theorems dg_cn_cs_intros
named_theorems dghm_field_simps
definition ObjMap :: V where [dghm_field_simps]: "ObjMap = 0"
definition ArrMap :: V where [dghm_field_simps]: "ArrMap = 1⇩ℕ"
definition HomDom :: V where [dghm_field_simps]: "HomDom = 2⇩ℕ"
definition HomCod :: V where [dghm_field_simps]: "HomCod = 3⇩ℕ"
subsection‹Definition and elementary properties›
text‹
A homomorphism of digraphs, as presented in this work, can be seen as a
generalization of the concept of a functor between categories, as presented in
Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›, to digraphs.
The generalization is performed by removing the axioms (1) from the definition.
It is expected that the resulting definition is consistent with the conventional
notion of a homomorphism of digraphs in graph theory, but further details
are considered to be outside of the scope of this work.
The definition of a digraph homomorphism is parameterized by a limit ordinal
‹α› such that ‹ω < α›. Such digraph homomorphisms are referred to either as
‹α›-digraph homomorphisms or homomorphisms of ‹α›-digraphs.
Following \<^cite>‹"mac_lane_categories_2010"›, all digraph homomorphisms are
covariant (see Chapter II-2). However, a special notation is adapted for the
digraph homomorphisms from an opposite digraph. Normally, such
digraph homomorphisms will be referred to as the contravariant digraph
homomorphisms, but this convention will not be enforced.
›
locale is_dghm =
𝒵 α + vfsequence 𝔉 + HomDom: digraph α 𝔄 + HomCod: digraph α 𝔅
for α 𝔄 𝔅 𝔉 +
assumes dghm_length[dg_cs_simps]: "vcard 𝔉 = 4⇩ℕ"
and dghm_HomDom[dg_cs_simps]: "𝔉⦇HomDom⦈ = 𝔄"
and dghm_HomCod[dg_cs_simps]: "𝔉⦇HomCod⦈ = 𝔅"
and dghm_ObjMap_vsv: "vsv (𝔉⦇ObjMap⦈)"
and dghm_ArrMap_vsv: "vsv (𝔉⦇ArrMap⦈)"
and dghm_ObjMap_vdomain[dg_cs_simps]: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈"
and dghm_ObjMap_vrange: "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 𝔅⦇Obj⦈"
and dghm_ArrMap_vdomain[dg_cs_simps]: "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈"
and dghm_ArrMap_is_arr:
"f : a ↦⇘𝔄⇙ b ⟹ 𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
syntax "_is_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩D⇩Gı _)› [51, 51, 51] 51)
syntax_consts "_is_dghm" ⇌ is_dghm
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" ⇌ "CONST is_dghm α 𝔄 𝔅 𝔉"
abbreviation (input) is_cn_dghm :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "is_cn_dghm α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
syntax "_is_cn_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ⇩D⇩G↦↦ı _)› [51, 51, 51] 51)
syntax_consts "_is_cn_dghm" ⇌ is_cn_dghm
translations "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_dghm α 𝔄 𝔅 𝔉"
abbreviation all_dghms :: "V ⇒ V"
where "all_dghms α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
abbreviation dghms :: "V ⇒ V ⇒ V ⇒ V"
where "dghms α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
sublocale is_dghm ⊆ ObjMap: vsv ‹𝔉⦇ObjMap⦈›
rewrites "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈"
by (rule dghm_ObjMap_vsv) (simp add: dg_cs_simps)
sublocale is_dghm ⊆ ArrMap: vsv ‹𝔉⦇ArrMap⦈›
rewrites "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈"
by (rule dghm_ArrMap_vsv) (simp add: dg_cs_simps)
lemmas [dg_cs_simps] =
is_dghm.dghm_HomDom
is_dghm.dghm_HomCod
is_dghm.dghm_ObjMap_vdomain
is_dghm.dghm_ArrMap_vdomain
lemma (in is_dghm) dghm_ArrMap_is_arr''[dg_cs_intros]:
assumes "f : a ↦⇘𝔄⇙ b" and "𝔉f = 𝔉⦇ArrMap⦈⦇f⦈"
shows "𝔉f : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
using assms(1) unfolding assms(2) by (rule dghm_ArrMap_is_arr)
lemma (in is_dghm) dghm_ArrMap_is_arr'[dg_cs_intros]:
assumes "f : a ↦⇘𝔄⇙ b"
and "A = 𝔉⦇ObjMap⦈⦇a⦈"
and "B = 𝔉⦇ObjMap⦈⦇b⦈"
shows "𝔉⦇ArrMap⦈⦇f⦈ : A ↦⇘𝔅⇙ B"
using assms(1) unfolding assms(2,3) by (rule dghm_ArrMap_is_arr)
lemmas [dg_cs_intros] = is_dghm.dghm_ArrMap_is_arr'
text‹Rules.›
lemma (in is_dghm) is_dghm_axioms'[dg_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇘α'⇙ 𝔅'"
unfolding assms by (rule is_dghm_axioms)
mk_ide rf is_dghm_def[unfolded is_dghm_axioms_def]
|intro is_dghmI|
|dest is_dghmD[dest]|
|elim is_dghmE[elim]|
lemmas [dg_cs_intros] = is_dghmD(3,4)
text‹Elementary properties.›
lemma dghm_eqI:
assumes "𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
and "𝔉 : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
and "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
shows "𝔊 = 𝔉"
proof-
interpret L: is_dghm α 𝔄 𝔅 𝔊 by (rule assms(1))
interpret R: is_dghm α ℭ 𝔇 𝔉 by (rule assms(2))
show ?thesis
proof(rule vsv_eqI)
have dom: "𝒟⇩∘ 𝔊 = 4⇩ℕ"
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
from assms(5,6) have sup: "𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
by (simp_all add: dg_cs_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔊 ⟹ 𝔊⦇a⦈ = 𝔉⦇a⦈" for a
by (unfold dom, elim_in_numeral, insert assms(3,4) sup)
(auto simp: dghm_field_simps)
qed (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps cs_intro: V_cs_intros)+
qed
lemma (in is_dghm) dghm_def: "𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ 𝔉 = 4⇩ℕ"
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
have dom_rhs: "𝒟⇩∘ [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘ = 4⇩ℕ"
by (simp add: nat_omega_simps)
then show "𝒟⇩∘ 𝔉 = 𝒟⇩∘ [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"
unfolding dom_lhs dom_rhs by (simp add: nat_omega_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔉 ⟹ 𝔉⦇a⦈ = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘⦇a⦈"
for a
by (unfold dom_lhs, elim_in_numeral, unfold dghm_field_simps)
(simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)
lemma (in is_dghm) dghm_ObjMap_app_in_HomCod_Obj[dg_cs_intros]:
assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "𝔉⦇ObjMap⦈⦇a⦈ ∈⇩∘ 𝔅⦇Obj⦈"
using assms dghm_ObjMap_vrange by (blast dest: ObjMap.vsv_vimageI2)
lemmas [dg_cs_intros] = is_dghm.dghm_ObjMap_app_in_HomCod_Obj
lemma (in is_dghm) dghm_ArrMap_vrange: "ℛ⇩∘ (𝔉⦇ArrMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
fix f assume "f ∈⇩∘ 𝔄⦇Arr⦈"
then obtain a b where "f : a ↦⇘𝔄⇙ b" by auto
then have "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
then show "𝔉⦇ArrMap⦈⦇f⦈ ∈⇩∘ 𝔅⦇Arr⦈" by auto
qed auto
lemma (in is_dghm) dghm_ArrMap_app_in_HomCod_Arr[dg_cs_intros]:
assumes "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "𝔉⦇ArrMap⦈⦇a⦈ ∈⇩∘ 𝔅⦇Arr⦈"
using assms dghm_ArrMap_vrange by (blast dest: ArrMap.vsv_vimageI2)
lemmas [dg_cs_intros] = is_dghm.dghm_ArrMap_app_in_HomCod_Arr
text‹Size.›
lemma (in is_dghm) dghm_ObjMap_vsubset_Vset: "𝔉⦇ObjMap⦈ ⊆⇩∘ Vset α"
by
(
rule ObjMap.vbrelation_Limit_vsubset_VsetI,
insert dghm_ObjMap_vrange HomCod.dg_Obj_vsubset_Vset
)
(auto intro!: HomDom.dg_Obj_vsubset_Vset)
lemma (in is_dghm) dghm_ArrMap_vsubset_Vset: "𝔉⦇ArrMap⦈ ⊆⇩∘ Vset α"
by
(
rule ArrMap.vbrelation_Limit_vsubset_VsetI,
insert dghm_ArrMap_vrange HomCod.dg_Arr_vsubset_Vset
)
(auto intro!: HomDom.dg_Arr_vsubset_Vset)
lemma (in is_dghm) dghm_ObjMap_in_Vset:
assumes "α ∈⇩∘ β"
shows "𝔉⦇ObjMap⦈ ∈⇩∘ Vset β"
by (meson assms dghm_ObjMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)
lemma (in is_dghm) dghm_ArrMap_in_Vset:
assumes "α ∈⇩∘ β"
shows "𝔉⦇ArrMap⦈ ∈⇩∘ Vset β"
by (meson assms dghm_ArrMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)
lemma (in is_dghm) dghm_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "𝔉 ∈⇩∘ Vset β"
proof-
interpret β: 𝒵 β by (rule assms(1))
note [dg_cs_intros] =
dghm_ObjMap_in_Vset dghm_ArrMap_in_Vset HomDom.dg_in_Vset HomCod.dg_in_Vset
from assms(2) show ?thesis
by (subst dghm_def)
(
cs_concl cs_shallow
cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros
)
qed
lemma (in is_dghm) dghm_is_dghm_if_ge_Limit:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇘β⇙ 𝔅"
proof(rule is_dghmI)
from is_dghm_axioms assms show "digraph β 𝔄"
by (cs_concl cs_intro: digraph.dg_digraph_if_ge_Limit dg_cs_intros)
from is_dghm_axioms assms show "digraph β 𝔅"
by (cs_concl cs_intro: digraph.dg_digraph_if_ge_Limit dg_cs_intros)
qed
(
cs_concl
cs_simp: dg_cs_simps
cs_intro: assms(1) dg_cs_intros V_cs_intros dghm_ObjMap_vrange
)+
lemma small_all_dghms[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
case True
from is_dghm.dghm_in_Vset show ?thesis
by (intro down[of _ ‹Vset (α + ω)›] subsetI)
(auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
case False
then have "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅} = {}" by auto
then show ?thesis by simp
qed
lemma (in is_dghm) dghm_in_Vset_7: "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)"
proof-
note [folded VPow_iff, folded Vset_succ[OF Ord_α], dg_cs_intros] =
dghm_ObjMap_vsubset_Vset
dghm_ArrMap_vsubset_Vset
from HomDom.dg_digraph_in_Vset_4 have [dg_cs_intros]:
"𝔄 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
by (succ_of_numeral)
(cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
from HomCod.dg_digraph_in_Vset_4 have [dg_cs_intros]:
"𝔅 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
by (succ_of_numeral)
(cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
show ?thesis
by (subst dghm_def, succ_of_numeral)
(
cs_concl
cs_simp: plus_V_succ_right V_cs_simps dg_cs_simps
cs_intro: dg_cs_intros V_cs_intros
)
qed
lemma (in 𝒵) all_dghms_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "all_dghms α ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
interpret β: 𝒵 β by (rule assms(1))
show "all_dghms α ⊆⇩∘ Vset (α + 7⇩ℕ)"
proof(intro vsubsetI)
fix 𝔉 assume "𝔉 ∈⇩∘ all_dghms α"
then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" by clarsimp
interpret is_dghm α 𝔄 𝔅 𝔉 using 𝔉 by simp
show "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)" by (rule dghm_in_Vset_7)
qed
from assms(2) show "Vset (α + 7⇩ℕ) ∈⇩∘ Vset β"
by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed
lemma small_dghms[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
by (rule down[of _ ‹set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}›]) auto
text‹Further properties.›
lemma (in is_dghm) dghm_is_arr_HomCod:
assumes "f : a ↦⇘𝔄⇙ b"
shows "𝔉⦇ArrMap⦈⦇f⦈ ∈⇩∘ 𝔅⦇Arr⦈" "𝔉⦇ObjMap⦈⦇a⦈ ∈⇩∘ 𝔅⦇Obj⦈" "𝔉⦇ObjMap⦈⦇b⦈ ∈⇩∘ 𝔅⦇Obj⦈"
using assms by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
lemma (in is_dghm) dghm_vimage_dghm_ArrMap_vsubset_Hom:
assumes "a ∈⇩∘ 𝔄⦇Obj⦈" and "b ∈⇩∘ 𝔄⦇Obj⦈"
shows "𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b ⊆⇩∘ Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
proof(intro vsubsetI)
fix g assume "g ∈⇩∘ 𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b"
then obtain f where "f ∈⇩∘ Hom (𝔉⦇HomDom⦈) a b" and "g = 𝔉⦇ArrMap⦈⦇f⦈"
by (auto simp: dg_cs_simps)
then show "g ∈⇩∘ Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
by (simp add: dghm_ArrMap_is_arr dg_cs_simps)
qed
subsection‹Opposite digraph homomorphism›
subsubsection‹Definition and elementary properties›
text‹See Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.›
definition op_dghm :: "V ⇒ V"
where "op_dghm 𝔉 =
[𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, op_dg (𝔉⦇HomDom⦈), op_dg (𝔉⦇HomCod⦈)]⇩∘"
text‹Components.›
lemma op_dghm_components[dg_op_simps]:
shows "op_dghm 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "op_dghm 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "op_dghm 𝔉⦇HomDom⦈ = op_dg (𝔉⦇HomDom⦈)"
and "op_dghm 𝔉⦇HomCod⦈ = op_dg (𝔉⦇HomCod⦈)"
unfolding op_dghm_def dghm_field_simps by (auto simp: nat_omega_simps)
subsubsection‹Further properties›
lemma (in is_dghm) is_dghm_op: "op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ op_dg 𝔅"
proof(intro is_dghmI, unfold dg_op_simps)
show "vfsequence (op_dghm 𝔉)" unfolding op_dghm_def by simp
show "vcard (op_dghm 𝔉) = 4⇩ℕ"
unfolding op_dghm_def by (auto simp: nat_omega_simps)
qed
(
cs_concl cs_shallow
cs_intro: dghm_ObjMap_vrange dg_cs_intros dg_op_intros V_cs_intros
cs_simp: dg_cs_simps dg_op_simps
)+
lemma (in is_dghm) is_dghm_op'[dg_op_intros]:
assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅" and "α' = α"
shows "op_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇘α'⇙ 𝔅'"
unfolding assms by (rule is_dghm_op)
lemmas is_dghm_op[dg_op_intros] = is_dghm.is_dghm_op'
lemma (in is_dghm) dghm_op_dghm_op_dghm[dg_op_simps]: "op_dghm (op_dghm 𝔉) = 𝔉"
using is_dghm_axioms
by
(
cs_concl cs_shallow
cs_simp: dg_op_simps
cs_intro: dg_op_intros dghm_eqI[where 𝔉=𝔉]
)
lemmas dghm_op_dghm_op_dghm[dg_op_simps] = is_dghm.dghm_op_dghm_op_dghm
lemma eq_op_dghm_iff[dg_op_simps]:
assumes "𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" and "𝔉 : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
shows "op_dghm 𝔊 = op_dghm 𝔉 ⟷ 𝔊 = 𝔉"
proof
interpret L: is_dghm α 𝔄 𝔅 𝔊 by (rule assms(1))
interpret R: is_dghm α ℭ 𝔇 𝔉 by (rule assms(2))
assume prems: "op_dghm 𝔊 = op_dghm 𝔉"
show "𝔊 = 𝔉"
proof(rule dghm_eqI[OF assms])
from prems R.dghm_op_dghm_op_dghm L.dghm_op_dghm_op_dghm show
"𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
by metis+
from prems R.dghm_op_dghm_op_dghm L.dghm_op_dghm_op_dghm have
"𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
by auto
then show "𝔄 = ℭ" "𝔅 = 𝔇" by (auto simp: dg_cs_simps)
qed
qed auto
subsection‹Composition of covariant digraph homomorphisms›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
definition dghm_comp :: "V ⇒ V ⇒ V" (infixl ‹∘⇩D⇩G⇩H⇩M› 55)
where "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 =
[𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈, 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔊⦇HomCod⦈]⇩∘"
text‹Components.›
lemma dghm_comp_components:
shows "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈ = 𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
and "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ = 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈"
and [dg_shared_cs_simps, dg_cs_simps]: "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇HomDom⦈ = 𝔉⦇HomDom⦈"
and [dg_shared_cs_simps, dg_cs_simps]: "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇HomCod⦈ = 𝔊⦇HomCod⦈"
unfolding dghm_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map›
lemma dghm_comp_ObjMap_vsv[dg_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "vsv ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis by (cs_concl cs_simp: dghm_comp_components cs_intro: V_cs_intros)
qed
lemma dghm_comp_ObjMap_vdomain[dg_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
using assms
by
(
cs_concl
cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
cs_intro: is_dghm.dghm_ObjMap_vrange
)
lemma dghm_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
using assms
by
(
cs_concl cs_shallow
cs_simp: dghm_comp_components
cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros
)
lemma dghm_comp_ObjMap_app[dg_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
from assms(3) show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
cs_intro: V_cs_intros dg_cs_intros
)
qed
subsubsection‹Arrow map›
lemma dghm_comp_ArrMap_vsv[dg_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "vsv ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by (cs_concl cs_simp: dghm_comp_components cs_intro: V_cs_intros)
qed
lemma dghm_comp_ArrMap_vdomain[dg_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
using assms
by
(
cs_concl
cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
cs_intro: is_dghm.dghm_ArrMap_vrange
)
lemma dghm_comp_ArrMap_vrange[dg_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
using assms
by
(
cs_concl cs_shallow
cs_simp: dghm_comp_components
cs_intro: is_dghm.dghm_ArrMap_vrange V_cs_intros
)
lemma dghm_comp_ArrMap_app[dg_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" and "f ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
proof-
interpret L: is_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
from assms(3) show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
by
(
cs_concl
cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
cs_intro: V_cs_intros dg_cs_intros
)
qed
subsubsection‹Opposite of the composition of covariant digraph homomorphisms›
lemma op_dghm_dghm_comp[dg_op_simps]:
"op_dghm (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) = op_dghm 𝔊 ∘⇩D⇩G⇩H⇩M op_dghm 𝔉"
unfolding dghm_comp_def op_dghm_def dghm_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Further properties›
lemma dghm_comp_is_dghm[dg_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
proof-
interpret L: is_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
proof(intro is_dghmI is_dghmI, unfold dg_cs_simps)
show "vfsequence (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)" unfolding dghm_comp_def by simp
show "vcard (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) = 4⇩ℕ"
unfolding dghm_comp_def by (simp add: nat_omega_simps)
fix f a b assume "f : a ↦⇘𝔄⇙ b"
with assms show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇f⦈ :
(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇b⦈"
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed
(
use assms in
‹
cs_concl cs_shallow
cs_intro: dg_cs_intros dghm_comp_ObjMap_vrange
cs_simp: dg_cs_simps
›
)+
qed
lemma dghm_comp_assoc[dg_cs_simps]:
assumes "ℌ : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇" and "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "(ℌ ∘⇩D⇩G⇩H⇩M 𝔊) ∘⇩D⇩G⇩H⇩M 𝔉 = ℌ ∘⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)"
proof(rule dghm_eqI [of α 𝔄 𝔇 _ 𝔄 𝔇])
show "(ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈ = (ℌ ∘⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇ObjMap⦈"
proof(rule vsv_eqI)
show "(ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = (ℌ ∘⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝒟⇩∘ ((ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈)" for a
using that assms
by
(cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
(cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed (use assms in ‹cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros›)+
show "(ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ = (ℌ ∘⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇ArrMap⦈"
proof(rule vsv_eqI)
show "(ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇a⦈ = (ℌ ∘⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇ArrMap⦈⦇a⦈"
if "a ∈⇩∘ 𝒟⇩∘ ((ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈)" for a
using that assms
by
(cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
(cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed
(
use assms in
‹cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros›
)+
qed (use assms in ‹cs_concl cs_shallow cs_intro: dg_cs_intros›)+
subsection‹Composition of contravariant digraph homomorphisms›
subsubsection‹Definition and elementary properties›
text‹See section 1.2 in \<^cite>‹"bodo_categories_1970"›.›
definition dghm_cn_comp :: "V ⇒ V ⇒ V" (infixl ‹⇩D⇩G⇩H⇩M∘› 55)
where "𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉 =
[
𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈,
𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈,
op_dg (𝔉⦇HomDom⦈),
𝔊⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma dghm_cn_comp_components:
shows "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈ = 𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
and "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈ = 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈"
and [dg_cn_cs_simps]: "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇HomDom⦈ = op_dg (𝔉⦇HomDom⦈)"
and [dg_cn_cs_simps]: "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇HomCod⦈ = 𝔊⦇HomCod⦈"
unfolding dghm_cn_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map: two contravariant digraph homomorphisms›
lemma dghm_cn_comp_ObjMap_vsv[dg_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α ‹op_dg 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed
lemma dghm_cn_comp_ObjMap_vdomain[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
using assms
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
cs_intro: is_dghm.dghm_ObjMap_vrange
)
lemma dghm_cn_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
using assms
by
(
cs_concl cs_shallow
cs_simp: dghm_cn_comp_components
cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros
)
lemma dghm_cn_comp_ObjMap_app[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α ‹op_dg 𝔄› 𝔅 𝔉 by (rule assms(2))
from assms(3) show "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
cs_intro: V_cs_intros dg_cs_intros
)
qed
subsubsection‹Arrow map: two contravariant digraph homomorphisms›
lemma dghm_cn_comp_ArrMap_vsv[dg_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α ‹op_dg 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed
lemma dghm_cn_comp_ArrMap_vdomain[dg_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
using assms
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
cs_intro: is_dghm.dghm_ArrMap_vrange
)
lemma dghm_cn_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
using assms
by
(
cs_concl cs_shallow
cs_simp: dghm_cn_comp_components
cs_intro: is_dghm.dghm_ArrMap_vrange V_cs_intros
)
lemma dghm_cn_comp_ArrMap_app[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α ‹op_dg 𝔄› 𝔅 𝔉 by (rule assms(2))
from assms(3) show "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
cs_intro: V_cs_intros dg_cs_intros
)
qed
subsubsection‹Object map: contravariant and covariant digraph homomorphisms›
lemma dghm_cn_cov_comp_ObjMap_vsv[dg_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed
lemma dghm_cn_cov_comp_ObjMap_vdomain[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
using assms
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
cs_intro: is_dghm.dghm_ObjMap_vrange
)
lemma dghm_cn_cov_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
using assms
by
(
cs_concl cs_shallow
cs_simp: dghm_cn_comp_components
cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros
)
lemma dghm_cn_cov_comp_ObjMap_app[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
from assms show "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps V_cs_simps
cs_intro: V_cs_intros dg_op_intros dg_cs_intros
)
qed
subsubsection‹Arrow map: contravariant and covariant digraph homomorphisms›
lemma dghm_cn_cov_comp_ArrMap_vsv[dg_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed
lemma dghm_cn_cov_comp_ArrMap_vdomain[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
using assms
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
cs_intro: is_dghm.dghm_ArrMap_vrange
)
lemma dghm_cn_cov_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
using assms
by
(
cs_concl cs_shallow
cs_simp: dghm_cn_comp_components
cs_intro: is_dghm.dghm_ArrMap_vrange V_cs_intros
)
lemma dghm_cn_cov_comp_ArrMap_app[dg_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
from assms(3) show "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: dghm_cn_comp_components dg_cs_simps V_cs_simps
cs_intro: V_cs_intros dg_op_intros dg_cs_intros
)
qed
subsubsection‹
Opposite of the contravariant composition of the digraph homomorphisms
›
lemma op_dghm_dghm_cn_comp[dg_op_simps]:
"op_dghm (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉) = op_dghm 𝔊 ⇩D⇩G⇩H⇩M∘ op_dghm 𝔉"
unfolding op_dghm_def dghm_cn_comp_def dghm_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹Further properties›
lemma dghm_cn_comp_is_dghm[dg_cn_cs_intros]:
assumes "digraph α 𝔄" and "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
proof-
interpret 𝔄: digraph α 𝔄 by (rule assms(1))
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 using assms(2) by auto
interpret R: is_dghm α ‹op_dg 𝔄› 𝔅 𝔉 using assms(3) by auto
show ?thesis
proof(intro is_dghmI, unfold dg_op_simps dg_cs_simps dg_cn_cs_simps)
show "vfsequence (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)" unfolding dghm_cn_comp_def by auto
show "vcard (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉) = 4⇩ℕ"
unfolding dghm_cn_comp_def by (simp add: nat_omega_simps)
fix f a b assume "f : a ↦⇘𝔄⇙ b"
with assms show "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈⦇f⦈ :
(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇b⦈"
by
(
cs_concl
cs_simp: dg_cn_cs_simps
cs_intro: dg_cs_intros dg_op_intros
)
qed
(
cs_concl
cs_simp: dg_cs_simps dg_cn_cs_simps
cs_intro: dghm_cn_comp_ObjMap_vrange dg_cs_intros dg_cn_cs_intros
)+
qed
lemma dghm_cn_cov_comp_is_dghm[dg_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩D⇩G↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
shows "𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ ℭ"
proof-
interpret L: is_dghm α ‹op_dg 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
proof(intro is_dghmI, unfold dg_op_simps dg_cs_simps)
show "vfsequence (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)" unfolding dghm_cn_comp_def by simp
show "vcard (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉) = 4⇩ℕ"
unfolding dghm_cn_comp_def by (auto simp: nat_omega_simps)
fix f b a assume "f : b ↦⇘𝔄⇙ a"
with assms show "(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ArrMap⦈⦇f⦈ :
(𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ⇩D⇩G⇩H⇩M∘ 𝔉)⦇ObjMap⦈⦇b⦈"
by (cs_concl cs_simp: dg_cn_cs_simps dg_op_simps cs_intro: dg_cs_intros)
qed
(
cs_concl cs_shallow
cs_simp: dg_cs_simps dg_cn_cs_simps
cs_intro:
dghm_cn_cov_comp_ObjMap_vrange
dg_cs_intros dg_cn_cs_intros dg_op_intros
)+
qed
lemma dghm_cov_cn_comp_is_dghm:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ 𝔅"
shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ⇩D⇩G↦↦⇘α⇙ ℭ"
using assms by (rule dghm_comp_is_dghm)
subsection‹Identity digraph homomorphism›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
definition dghm_id :: "V ⇒ V"
where "dghm_id ℭ = [vid_on (ℭ⦇Obj⦈), vid_on (ℭ⦇Arr⦈), ℭ, ℭ]⇩∘"
text‹Components.›
lemma dghm_id_components:
shows "dghm_id ℭ⦇ObjMap⦈ = vid_on (ℭ⦇Obj⦈)"
and "dghm_id ℭ⦇ArrMap⦈ = vid_on (ℭ⦇Arr⦈)"
and [dg_shared_cs_simps, dg_cs_simps]: "dghm_id ℭ⦇HomDom⦈ = ℭ"
and [dg_shared_cs_simps, dg_cs_simps]: "dghm_id ℭ⦇HomCod⦈ = ℭ"
unfolding dghm_id_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map›
mk_VLambda dghm_id_components(1)[folded VLambda_vid_on]
|vsv dghm_id_ObjMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
|vdomain dghm_id_ObjMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
|app dghm_id_ObjMap_app[dg_shared_cs_simps, dg_cs_simps]|
lemma dghm_id_ObjMap_vrange[dg_shared_cs_simps, dg_cs_simps]:
"ℛ⇩∘ (dghm_id ℭ⦇ObjMap⦈) = ℭ⦇Obj⦈"
unfolding dghm_id_components by simp
subsubsection‹Arrow map›
mk_VLambda dghm_id_components(2)[folded VLambda_vid_on]
|vsv dghm_id_ArrMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
|vdomain dghm_id_ArrMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
|app dghm_id_ArrMap_app[dg_shared_cs_simps, dg_cs_simps]|
lemma dghm_id_ArrMap_vrange[dg_shared_cs_simps, dg_cs_simps]:
"ℛ⇩∘ (dghm_id ℭ⦇ArrMap⦈) = ℭ⦇Arr⦈"
unfolding dghm_id_components by simp
subsubsection‹Opposite identity digraph homomorphism›
lemma op_dghm_dghm_id[dg_op_simps]: "op_dghm (dghm_id ℭ) = dghm_id (op_dg ℭ)"
unfolding dghm_id_def op_dg_def op_dghm_def dghm_field_simps dg_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹An identity digraph homomorphism is a digraph homomorphism›
lemma (in digraph) dg_dghm_id_is_dghm: "dghm_id ℭ : ℭ ↦↦⇩D⇩G⇘α⇙ ℭ"
proof(intro is_dghmI, unfold dg_cs_simps)
show "vfsequence (dghm_id ℭ)" unfolding dghm_id_def by simp
show "vcard (dghm_id ℭ) = 4⇩ℕ"
unfolding dghm_id_def by (simp add: nat_omega_simps)
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
lemma (in digraph) dg_dghm_id_is_dghm':
assumes "𝔄 = ℭ" and "𝔅 = ℭ"
shows "dghm_id ℭ : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
unfolding assms by (rule dg_dghm_id_is_dghm)
lemmas [dg_cs_intros] = digraph.dg_dghm_id_is_dghm'
subsubsection‹Further properties›
lemma (in is_dghm) dghm_dghm_comp_dghm_id_left: "dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉 = 𝔉"
proof(rule dghm_eqI [of α 𝔄 𝔅 _ 𝔄 𝔅])
show "(dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
proof(rule vsv_eqI)
show "(dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝒟⇩∘ ((dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈)" for a
using that
by
(cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
(cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
show "(dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
proof(rule vsv_eqI)
show "(dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔉⦇ArrMap⦈⦇a⦈"
if "a ∈⇩∘ 𝒟⇩∘ ((dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈)" for a
using that
by
(cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
(cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
qed (cs_concl cs_shallow cs_simp: cs_intro: dg_cs_intros)+
lemmas [dg_cs_simps] = is_dghm.dghm_dghm_comp_dghm_id_left
lemma (in is_dghm) dghm_dghm_comp_dghm_id_right: "𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄 = 𝔉"
proof(rule dghm_eqI [of α 𝔄 𝔅 _ 𝔄 𝔅])
show "(𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
proof(rule vsv_eqI)
show "(𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝒟⇩∘ ((𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇ObjMap⦈)" for a
using that
by
(cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
(cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
show "(𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
proof(rule vsv_eqI)
show "(𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇ArrMap⦈⦇a⦈ = 𝔉⦇ArrMap⦈⦇a⦈"
if "a ∈⇩∘ 𝒟⇩∘ ((𝔉 ∘⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇ArrMap⦈)" for a
using that
by
(cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
(cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
lemmas [dg_cs_simps] = is_dghm.dghm_dghm_comp_dghm_id_right
subsection‹Constant digraph homomorphism›
subsubsection‹Definition and elementary properties›
text‹See Chapter III-3 in \<^cite>‹"mac_lane_categories_2010"›.›
definition dghm_const :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "dghm_const ℭ 𝔇 a f =
[vconst_on (ℭ⦇Obj⦈) a, vconst_on (ℭ⦇Arr⦈) f, ℭ, 𝔇]⇩∘"
text‹Components.›
lemma dghm_const_components:
shows "dghm_const ℭ 𝔇 a f⦇ObjMap⦈ = vconst_on (ℭ⦇Obj⦈) a"
and "dghm_const ℭ 𝔇 a f⦇ArrMap⦈ = vconst_on (ℭ⦇Arr⦈) f"
and [dg_shared_cs_simps, dg_cs_simps]: "dghm_const ℭ 𝔇 a f⦇HomDom⦈ = ℭ"
and [dg_shared_cs_simps, dg_cs_simps]: "dghm_const ℭ 𝔇 a f⦇HomCod⦈ = 𝔇"
unfolding dghm_const_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map›
mk_VLambda dghm_const_components(1)[folded VLambda_vconst_on]
|vsv dghm_const_ObjMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
|vdomain dghm_const_ObjMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
|app dghm_const_ObjMap_app[dg_shared_cs_simps, dg_cs_simps]|
subsubsection‹Arrow map›
mk_VLambda dghm_const_components(2)[folded VLambda_vconst_on]
|vsv dghm_const_ArrMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
|vdomain dghm_const_ArrMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
|app dghm_const_ArrMap_app[dg_shared_cs_simps, dg_cs_simps]|
subsubsection‹Opposite constant digraph homomorphism›
lemma op_dghm_dghm_const[dg_op_simps]:
"op_dghm (dghm_const ℭ 𝔇 a f) = dghm_const (op_dg ℭ) (op_dg 𝔇) a f"
unfolding dghm_const_def op_dg_def op_dghm_def dghm_field_simps dg_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹A constant digraph homomorphism is a digraph homomorphism›
lemma dghm_const_is_dghm:
assumes "digraph α ℭ" and "digraph α 𝔇" and "f : a ↦⇘𝔇⇙ a"
shows "dghm_const ℭ 𝔇 a f : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
proof-
interpret 𝔇: digraph α 𝔇 by (rule assms(2))
show ?thesis
proof(intro is_dghmI)
show "vfsequence (dghm_const ℭ 𝔇 a f)"
unfolding dghm_const_def by simp
show "vcard (dghm_const ℭ 𝔇 a f) = 4⇩ℕ"
unfolding dghm_const_def by (simp add: nat_omega_simps)
qed
(
use assms in
‹
cs_concl
cs_simp: dghm_const_components(1) dg_cs_simps
cs_intro: V_cs_intros dg_cs_intros
›
)+
qed
lemma dghm_const_is_dghm'[dg_cs_intros]:
assumes "digraph α ℭ"
and "digraph α 𝔇"
and "f : a ↦⇘𝔇⇙ a"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
shows "dghm_const ℭ 𝔇 a f : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
using assms(1-3) unfolding assms(4,5) by (rule dghm_const_is_dghm)
subsubsection‹Further properties›
lemma (in is_dghm) dghm_dghm_comp_dghm_const[dg_cs_simps]:
assumes "digraph α ℭ" and "f : a ↦⇘ℭ⇙ a"
shows "dghm_const 𝔅 ℭ a f ∘⇩D⇩G⇩H⇩M 𝔉 = dghm_const 𝔄 ℭ a f"
proof(rule dghm_eqI)
interpret ℭ: digraph α ℭ by (rule assms(1))
from assms(2) show "dghm_const 𝔅 ℭ a f ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
with assms(2) have ObjMap_dom_lhs:
"𝒟⇩∘ ((dghm_const 𝔅 ℭ a f ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
and ArrMap_dom_lhs: "𝒟⇩∘ ((dghm_const 𝔅 ℭ a f ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
by (cs_concl cs_simp: dg_cs_simps)+
from assms(2) show "dghm_const 𝔄 ℭ a f : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
with assms(2) have ObjMap_dom_rhs: "𝒟⇩∘ (dghm_const 𝔄 ℭ a f⦇ObjMap⦈) = 𝔄⦇Obj⦈"
and ArrMap_dom_rhs: "𝒟⇩∘ (dghm_const 𝔄 ℭ a f⦇ArrMap⦈) = 𝔄⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: dg_cs_simps)+
show "(dghm_const 𝔅 ℭ a f ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈ = dghm_const 𝔄 ℭ a f⦇ObjMap⦈"
by (rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
(
use assms(2) in
‹cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros›
)+
show "(dghm_const 𝔅 ℭ a f ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ = dghm_const 𝔄 ℭ a f⦇ArrMap⦈"
by (rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
(
use assms(2) in
‹cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros›
)+
qed simp_all
lemmas [dg_cs_simps] = is_dghm.dghm_dghm_comp_dghm_const
subsection‹Faithful digraph homomorphism›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
locale is_ft_dghm = is_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes ft_dghm_v11_on_Hom:
"⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
syntax "_is_ft_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩lı _)› [51, 51, 51] 51)
syntax_consts "_is_ft_dghm" ⇌ is_ft_dghm
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅" ⇌ "CONST is_ft_dghm α 𝔄 𝔅 𝔉"
text‹Rules.›
lemma (in is_ft_dghm) is_ft_dghm_axioms'[dghm_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α'⇙ 𝔅'"
unfolding assms by (rule is_ft_dghm_axioms)
mk_ide rf is_ft_dghm_def[unfolded is_ft_dghm_axioms_def]
|intro is_ft_dghmI|
|dest is_ft_dghmD[dest]|
|elim is_ft_dghmE[elim]|
lemmas [dghm_cs_intros] = is_ft_dghmD(1)
lemma is_ft_dghmI'':
assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
and "⋀a b g f.
⟦ g : a ↦⇘𝔄⇙ b; f : a ↦⇘𝔄⇙ b; 𝔉⦇ArrMap⦈⦇g⦈ = 𝔉⦇ArrMap⦈⦇f⦈ ⟧ ⟹ g = f"
shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
proof(intro is_ft_dghmI assms)
interpret 𝔉: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(1))
fix a b assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈" "b ∈⇩∘ 𝔄⦇Obj⦈"
have dom_def: "𝒟⇩∘ (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b) = Hom 𝔄 a b"
by (intro vdomain_vlrestriction_vsubset vsubsetI) (auto simp: dg_cs_simps)
show "v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
proof(intro vsv.vsv_valeq_v11I, unfold dom_def dg_cs_simps)
from prems show "vsv (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)" by auto
fix g f assume prems:
"g : a ↦⇘𝔄⇙ b"
"f : a ↦⇘𝔄⇙ b"
"(𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)⦇g⦈ = (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)⦇f⦈"
from prems(3,1,2) have 𝔉g_𝔉f: "𝔉⦇ArrMap⦈⦇g⦈ = 𝔉⦇ArrMap⦈⦇f⦈"
by
(
cs_prems
cs_simp: V_cs_simps dg_cs_simps
cs_intro: V_cs_intros dg_cs_intros
)
show "g = f" by (rule assms(2)[OF prems(1,2) 𝔉g_𝔉f])
qed
qed
subsubsection‹Opposite faithful digraph homomorphism›
lemma (in is_ft_dghm) ft_dghm_op_dghm_is_ft_dghm:
"op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_dg 𝔅"
by
(
rule is_ft_dghmI,
unfold dg_op_simps,
cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros
)
(auto simp: ft_dghm_v11_on_Hom)
lemma (in is_ft_dghm) ft_dghm_op_dghm_is_ft_dghm'[dg_op_intros]:
assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
shows "op_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule ft_dghm_op_dghm_is_ft_dghm)
lemmas ft_dghm_op_dghm_is_ft_dghm[dg_op_intros] =
is_ft_dghm.ft_dghm_op_dghm_is_ft_dghm'
subsubsection‹
The composition of faithful digraph homomorphisms is a faithful
digraph homomorphism.
›
lemma dghm_comp_is_ft_dghm[dghm_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ"
proof-
interpret L: is_ft_dghm α 𝔅 ℭ 𝔊 using assms(1) by auto
interpret R: is_ft_dghm α 𝔄 𝔅 𝔉 using assms(2) by auto
have inj:
"⟦ a ∈⇩∘ 𝔄⦇Obj⦈ ; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
for a b
proof-
assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈" "b ∈⇩∘ 𝔄⦇Obj⦈"
then have 𝔊_hom_𝔅:
"v11 (𝔊⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈))"
by (intro L.ft_dghm_v11_on_Hom)
(cs_concl cs_shallow cs_intro: dg_cs_intros)+
have "v11 (𝔊⦇ArrMap⦈ ↾⇧l⇩∘ (𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b))"
proof(intro v11_vlrestriction_vsubset[OF 𝔊_hom_𝔅] vsubsetI)
fix g assume "g ∈⇩∘ 𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b"
then obtain f where f: "f : a ↦⇘𝔄⇙ b" and g_def: "g = 𝔉⦇ArrMap⦈⦇f⦈"
by auto
from f show "g ∈⇩∘ Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
by (cs_concl cs_shallow cs_simp: g_def cs_intro: dg_cs_intros)
qed
then show "v11 ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
unfolding dghm_comp_components
by (intro v11_vlrestriction_vcomp) (auto simp: R.ft_dghm_v11_on_Hom prems)
qed
then show "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ"
by (intro is_ft_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros) auto
qed
subsubsection‹Further properties›
lemma (in is_ft_dghm) ft_dghm_ArrMap_eqD:
assumes "g : a ↦⇘𝔄⇙ b" and "f : a ↦⇘𝔄⇙ b" and "𝔉⦇ArrMap⦈⦇g⦈ = 𝔉⦇ArrMap⦈⦇f⦈"
shows "g = f"
proof-
from assms(1) have a: "a ∈⇩∘ 𝔄⦇Obj⦈" and b: "b ∈⇩∘ 𝔄⦇Obj⦈" by auto
interpret ArrMap: v11 ‹𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b›
by (rule ft_dghm_v11_on_Hom[OF a b])
have dom_def: "𝒟⇩∘ (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b) = Hom 𝔄 a b"
by (intro vdomain_vlrestriction_vsubset vsubsetI) (auto simp: dg_cs_simps)
show ?thesis
proof(rule ArrMap.v11_injective[unfolded dom_def dg_cs_simps, OF assms(1,2)])
from assms(1,2) show
"(𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)⦇g⦈ = (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)⦇f⦈"
by
(
cs_concl
cs_simp: dg_cs_simps assms(3) vsv.vlrestriction_atI
cs_intro: V_cs_intros dg_cs_intros
)
qed
qed
subsection‹Full digraph homomorphism›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
locale is_fl_dghm = is_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes fl_dghm_surj_on_Hom:
"⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
syntax "_is_fl_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩lı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" ⇌ "CONST is_fl_dghm α 𝔄 𝔅 𝔉"
text‹Rules.›
lemma (in is_fl_dghm) is_fl_dghm_axioms'[dghm_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α'⇙ 𝔅'"
unfolding assms by (rule is_fl_dghm_axioms)
mk_ide rf is_fl_dghm_def[unfolded is_fl_dghm_axioms_def]
|intro is_fl_dghmI|
|dest is_fl_dghmD[dest]|
|elim is_fl_dghmE[elim]|
lemmas [dghm_cs_intros] = is_fl_dghmD(1)
subsubsection‹Opposite full digraph homomorphism›
lemma (in is_fl_dghm) fl_dghm_op_dghm_is_fl_dghm:
"op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ op_dg 𝔅"
by
(
rule is_fl_dghmI,
unfold dg_op_simps,
cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros
)
(auto simp: fl_dghm_surj_on_Hom)
lemma (in is_fl_dghm) fl_dghm_op_dghm_is_fl_dghm'[dg_op_intros]:
assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
shows "op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ op_dg 𝔅"
unfolding assms by (rule fl_dghm_op_dghm_is_fl_dghm)
lemmas fl_dghm_op_dghm_is_fl_dghm[dg_op_intros] =
is_fl_dghm.fl_dghm_op_dghm_is_fl_dghm'
subsubsection‹
The composition of full digraph homomorphisms is a full digraph homomorphism
›
lemma dghm_comp_is_fl_dghm[dghm_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ"
proof-
interpret L: is_fl_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_fl_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
have surj:
"⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) =
Hom ℭ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈) ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇b⦈)"
for a b
proof-
assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈" "b ∈⇩∘ 𝔄⦇Obj⦈"
have surj_𝔉: "𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
by (rule R.fl_dghm_surj_on_Hom[OF prems])
from prems L.is_dghm_axioms R.is_dghm_axioms have comp_Obj:
"(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
"(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇b⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇b⦈⦈"
by (auto simp: dg_cs_simps)
have "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b = 𝔊⦇ArrMap⦈ `⇩∘ 𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b"
unfolding dghm_comp_components by (simp add: vcomp_vimage)
also from prems have
"… = Hom ℭ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈) ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇b⦈)"
unfolding surj_𝔉 comp_Obj
by
(
simp add:
prems(2) L.fl_dghm_surj_on_Hom R.dghm_ObjMap_app_in_HomCod_Obj
)
finally show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) =
Hom ℭ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈) ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇b⦈)"
by simp
qed
show ?thesis
by (rule is_fl_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros)
(auto simp: surj)
qed
subsection‹Fully faithful digraph homomorphism›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
locale is_ff_dghm = is_ft_dghm α 𝔄 𝔅 𝔉 + is_fl_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉
syntax "_is_ff_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩D⇩G⇩.⇩f⇩fı _)› [51, 51, 51] 51)
syntax_consts "_is_ff_dghm" ⇌ is_ff_dghm
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ 𝔅" ⇌ "CONST is_ff_dghm α 𝔄 𝔅 𝔉"
text‹Rules.›
lemma (in is_ff_dghm) is_ff_dghm_axioms'[dghm_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩f⇘α'⇙ 𝔅'"
unfolding assms by (rule is_ff_dghm_axioms)
mk_ide rf is_ff_dghm_def
|intro is_ff_dghmI|
|dest is_ff_dghmD[dest]|
|elim is_ff_dghmE[elim]|
lemmas [dghm_cs_intros] = is_ff_dghmD
subsubsection‹Opposite fully faithful digraph homomorphism.›
lemma (in is_ff_dghm) ff_dghm_op_dghm_is_ff_dghm:
"op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ op_dg 𝔅"
by (rule is_ff_dghmI) (cs_concl cs_shallow cs_intro: dg_op_intros)+
lemma (in is_ff_dghm) ff_dghm_op_dghm_is_ff_dghm'[dg_op_intros]:
assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
shows "op_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ 𝔅'"
unfolding assms by (rule ff_dghm_op_dghm_is_ff_dghm)
lemmas ff_dghm_op_dghm_is_ff_dghm[dg_op_intros] =
is_ff_dghm.ff_dghm_op_dghm_is_ff_dghm
subsubsection‹
The composition of fully faithful digraph homomorphisms is
a fully faithful digraph homomorphism.
›
lemma dghm_comp_is_ff_dghm[dghm_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ 𝔅"
shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ ℭ"
using assms
by (intro is_ff_dghmI, elim is_ff_dghmE) (cs_concl cs_intro: dghm_cs_intros)
subsection‹Isomorphism of digraphs›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
locale is_iso_dghm = is_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes iso_dghm_ObjMap_v11: "v11 (𝔉⦇ObjMap⦈)"
and iso_dghm_ArrMap_v11: "v11 (𝔉⦇ArrMap⦈)"
and iso_dghm_ObjMap_vrange[dghm_cs_simps]: "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
and iso_dghm_ArrMap_vrange[dghm_cs_simps]: "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
syntax "_is_iso_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩D⇩G⇩.⇩i⇩s⇩oı _)› [51, 51, 51] 51)
syntax_consts "_is_iso_dghm" ⇌ is_iso_dghm
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" ⇌ "CONST is_iso_dghm α 𝔄 𝔅 𝔉"
sublocale is_iso_dghm ⊆ ObjMap: v11 ‹𝔉⦇ObjMap⦈›
rewrites "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈" and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: dghm_cs_simps dg_cs_simps cs_intro: iso_dghm_ObjMap_v11
)+
sublocale is_iso_dghm ⊆ ArrMap: v11 ‹𝔉⦇ArrMap⦈›
rewrites "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈" and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_simp: dghm_cs_simps dg_cs_simps cs_intro: iso_dghm_ArrMap_v11
)+
lemmas [dghm_cs_simps] =
is_iso_dghm.iso_dghm_ObjMap_vrange
is_iso_dghm.iso_dghm_ArrMap_vrange
text‹Rules.›
lemma (in is_iso_dghm) is_iso_dghm_axioms'[dghm_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α'⇙ 𝔅'"
unfolding assms by (rule is_iso_dghm_axioms)
mk_ide rf is_iso_dghm_def[unfolded is_iso_dghm_axioms_def]
|intro is_iso_dghmI|
|dest is_iso_dghmD[dest]|
|elim is_iso_dghmE[elim]|
text‹Elementary properties.›
lemma (in is_iso_dghm) iso_dghm_Obj_HomDom_if_Obj_HomCod[elim]:
assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
obtains a where "a ∈⇩∘ 𝔄⦇Obj⦈" and "b = 𝔉⦇ObjMap⦈⦇a⦈"
using assms ObjMap.vrange_atD iso_dghm_ObjMap_vrange by blast
lemma (in is_iso_dghm) iso_dghm_Arr_HomDom_if_Arr_HomCod[elim]:
assumes "g ∈⇩∘ 𝔅⦇Arr⦈"
obtains f where "f ∈⇩∘ 𝔄⦇Arr⦈" and "g = 𝔉⦇ArrMap⦈⦇f⦈"
using assms ArrMap.vrange_atD iso_dghm_ArrMap_vrange by blast
lemma (in is_iso_dghm) iso_dghm_ObjMap_eqE[elim]:
assumes "𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇b⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
and "b ∈⇩∘ 𝔄⦇Obj⦈"
and "a = b ⟹ P"
shows P
using assms ObjMap.v11_eq_iff by auto
lemma (in is_iso_dghm) iso_dghm_ArrMap_eqE[elim]:
assumes "𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇g⦈"
and "f ∈⇩∘ 𝔄⦇Arr⦈"
and "g ∈⇩∘ 𝔄⦇Arr⦈"
and "f = g ⟹ P"
shows P
using assms ArrMap.v11_eq_iff by auto
sublocale is_iso_dghm ⊆ is_ft_dghm
by (intro is_ft_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros) auto
sublocale is_iso_dghm ⊆ is_fl_dghm
proof
fix a b assume [intro]: "a ∈⇩∘ 𝔄⦇Obj⦈" "b ∈⇩∘ 𝔄⦇Obj⦈"
show "𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
proof(intro vsubset_antisym vsubsetI)
fix g assume prems: "g ∈⇩∘ Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
then have g: "g : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈" by auto
then have dom_g: "𝔅⦇Dom⦈⦇g⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
and cod_g: "𝔅⦇Cod⦈⦇g⦈ = 𝔉⦇ObjMap⦈⦇b⦈"
by blast+
from prems obtain f
where [intro, simp]: "f ∈⇩∘ 𝔄⦇Arr⦈" and g_def: "g = 𝔉⦇ArrMap⦈⦇f⦈"
by auto
then obtain a' b' where f: "f : a' ↦⇘𝔄⇙ b'" by blast
then have "g : 𝔉⦇ObjMap⦈⦇a'⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b'⦈"
by (cs_concl cs_shallow cs_simp: g_def dg_cs_simps cs_intro: dg_cs_intros)
with g have "𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a'⦈" and "𝔉⦇ObjMap⦈⦇b⦈ = 𝔉⦇ObjMap⦈⦇b'⦈"
by (metis HomCod.dg_is_arrE cod_g)+
with f have "a = 𝔄⦇Dom⦈⦇f⦈" "b = 𝔄⦇Cod⦈⦇f⦈" by auto
with f show "g ∈⇩∘ 𝔉⦇ArrMap⦈ `⇩∘ Hom 𝔄 a b"
by (auto simp: g_def HomDom.dg_is_arrD(4,5) ArrMap.vsv_vimageI1)
qed (metis ArrMap.vsv_vimageE dghm_ArrMap_is_arr' in_Hom_iff)
qed
sublocale is_iso_dghm ⊆ is_ff_dghm by unfold_locales
lemmas (in is_iso_dghm) iso_dghm_is_ff_dghm = is_ff_dghm_axioms
lemmas [dghm_cs_intros] = is_iso_dghm.iso_dghm_is_ff_dghm
subsubsection‹Opposite digraph isomorphisms›
lemma (in is_iso_dghm) is_iso_dghm_op:
"op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ op_dg 𝔅"
by (intro is_iso_dghmI, unfold dg_op_simps)
(
cs_concl cs_shallow
cs_simp: dghm_cs_simps cs_intro: V_cs_intros dg_cs_intros dg_op_intros
)+
lemma (in is_iso_dghm) is_iso_dghm_op':
assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
shows "op_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅'"
unfolding assms by (rule is_iso_dghm_op)
lemmas is_iso_dghm_op[dg_op_intros] = is_iso_dghm.is_iso_dghm_op'
subsubsection‹
The composition of isomorphisms of digraphs is an isomorphism of digraphs
›
lemma dghm_comp_is_iso_dghm[dghm_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
proof-
interpret 𝔉: is_iso_dghm α 𝔄 𝔅 𝔉 using assms by auto
interpret 𝔊: is_iso_dghm α 𝔅 ℭ 𝔊 using assms by auto
show ?thesis
by (intro is_iso_dghmI, unfold dghm_comp_components)
(
cs_concl
cs_simp: V_cs_simps dg_cs_simps dghm_cs_simps
cs_intro: dg_cs_intros V_cs_intros
)+
qed
subsubsection‹An identity digraph homomorphism is an isomorphism of digraphs.›
lemma (in digraph) dg_dghm_id_is_iso_dghm: "dghm_id ℭ : ℭ ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
by (rule is_iso_dghmI) (simp_all add: dg_dghm_id_is_dghm dghm_id_components)
lemma (in digraph) dg_dghm_id_is_iso_dghm'[dghm_cs_intros]:
assumes "𝔄' = ℭ" and "𝔅' = ℭ"
shows "dghm_id ℭ : 𝔄' ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅'"
unfolding assms by (rule dg_dghm_id_is_iso_dghm)
lemmas [dghm_cs_intros] = digraph.dg_dghm_id_is_iso_dghm'
subsection‹Inverse digraph homomorphism›
subsubsection‹Definition and elementary properties›
definition inv_dghm :: "V ⇒ V"
where "inv_dghm 𝔉 = [(𝔉⦇ObjMap⦈)¯⇩∘, (𝔉⦇ArrMap⦈)¯⇩∘, 𝔉⦇HomCod⦈, 𝔉⦇HomDom⦈]⇩∘"
text‹Components.›
lemma inv_dghm_components:
shows "inv_dghm 𝔉⦇ObjMap⦈ = (𝔉⦇ObjMap⦈)¯⇩∘"
and "inv_dghm 𝔉⦇ArrMap⦈ = (𝔉⦇ArrMap⦈)¯⇩∘"
and [dghm_cs_simps]: "inv_dghm 𝔉⦇HomDom⦈ = 𝔉⦇HomCod⦈"
and [dghm_cs_simps]: "inv_dghm 𝔉⦇HomCod⦈ = 𝔉⦇HomDom⦈"
unfolding inv_dghm_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map›
lemma (in is_iso_dghm) inv_dghm_ObjMap_v11[dghm_cs_intros]:
"v11 (inv_dghm 𝔉⦇ObjMap⦈)"
unfolding inv_dghm_components by (cs_concl cs_shallow cs_intro: V_cs_intros)
lemmas [dghm_cs_intros] = is_iso_dghm.inv_dghm_ObjMap_v11
lemma (in is_iso_dghm) inv_dghm_ObjMap_vdomain[dghm_cs_simps]:
"𝒟⇩∘ (inv_dghm 𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
unfolding inv_dghm_components by (cs_concl cs_simp: dghm_cs_simps V_cs_simps)
lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ObjMap_vdomain
lemma (in is_iso_dghm) inv_dghm_ObjMap_app[dghm_cs_simps]:
assumes "a' = 𝔉⦇ObjMap⦈⦇a⦈" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "inv_dghm 𝔉⦇ObjMap⦈⦇a'⦈ = a"
unfolding inv_dghm_components
by (metis assms ObjMap.vconverse_atI ObjMap.vsv_vconverse vsv.vsv_appI)
lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ObjMap_app
lemma (in is_iso_dghm) inv_dghm_ObjMap_vrange[dghm_cs_simps]:
"ℛ⇩∘ (inv_dghm 𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈"
unfolding inv_dghm_components by (cs_concl cs_simp: dg_cs_simps V_cs_simps)
lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ObjMap_vrange
subsubsection‹Arrow map›
lemma (in is_iso_dghm) inv_dghm_ArrMap_v11[dghm_cs_intros]:
"v11 (inv_dghm 𝔉⦇ArrMap⦈)"
unfolding inv_dghm_components by (cs_concl cs_shallow cs_intro: V_cs_intros)
lemmas [dghm_cs_intros] = is_iso_dghm.inv_dghm_ArrMap_v11
lemma (in is_iso_dghm) inv_dghm_ArrMap_vdomain[dghm_cs_simps]:
"𝒟⇩∘ (inv_dghm 𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
unfolding inv_dghm_components by (cs_concl cs_simp: dghm_cs_simps V_cs_simps)
lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ArrMap_vdomain
lemma (in is_iso_dghm) inv_dghm_ArrMap_app[dghm_cs_simps]:
assumes "a' = 𝔉⦇ArrMap⦈⦇a⦈" and "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "inv_dghm 𝔉⦇ArrMap⦈⦇a'⦈ = a"
unfolding inv_dghm_components
by (metis assms ArrMap.vconverse_atI ArrMap.vsv_vconverse vsv.vsv_appI)
lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ArrMap_app
lemma (in is_iso_dghm) inv_dghm_ArrMap_vrange[dghm_cs_simps]:
"ℛ⇩∘ (inv_dghm 𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈"
unfolding inv_dghm_components by (cs_concl cs_simp: dg_cs_simps V_cs_simps)
lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ArrMap_vrange
subsubsection‹Further properties›
lemma (in is_iso_dghm) iso_dghm_ObjMap_inv_dghm_ObjMap_app[dghm_cs_simps]:
assumes "a ∈⇩∘ 𝔅⦇Obj⦈"
shows "𝔉⦇ObjMap⦈⦇inv_dghm 𝔉⦇ObjMap⦈⦇a⦈⦈ = a"
using assms by (cs_concl cs_simp: inv_dghm_components V_cs_simps)
lemmas [dghm_cs_simps] = is_iso_dghm.iso_dghm_ObjMap_inv_dghm_ObjMap_app
lemma (in is_iso_dghm) iso_dghm_ArrMap_inv_dghm_ArrMap_app[dghm_cs_simps]:
assumes "f : a ↦⇘𝔅⇙ b"
shows "𝔉⦇ArrMap⦈⦇inv_dghm 𝔉⦇ArrMap⦈⦇f⦈⦈ = f"
using assms
by (cs_concl cs_simp: inv_dghm_components V_cs_simps cs_intro: dg_cs_intros)
lemmas [dghm_cs_simps] = is_iso_dghm.iso_dghm_ArrMap_inv_dghm_ArrMap_app
lemma (in is_iso_dghm) iso_dghm_HomDom_is_arr_conv:
assumes "f ∈⇩∘ 𝔄⦇Arr⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
and "b ∈⇩∘ 𝔄⦇Obj⦈"
and "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
shows "f : a ↦⇘𝔄⇙ b"
by
(
metis
assms
HomDom.dg_is_arrE
is_arr_def
dghm_ArrMap_is_arr
iso_dghm_ObjMap_eqE
)
lemma (in is_iso_dghm) iso_dghm_HomCod_is_arr_conv:
assumes "f ∈⇩∘ 𝔅⦇Arr⦈"
and "a ∈⇩∘ 𝔅⦇Obj⦈"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
and "inv_dghm 𝔉⦇ArrMap⦈⦇f⦈ : inv_dghm 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ inv_dghm 𝔉⦇ObjMap⦈⦇b⦈"
shows "f : a ↦⇘𝔅⇙ b"
by
(
metis
assms
dghm_ArrMap_is_arr'
is_arrI
iso_dghm_ArrMap_inv_dghm_ArrMap_app
iso_dghm_ObjMap_inv_dghm_ObjMap_app
)
subsection‹An isomorphism of digraphs is an isomorphism in the category ‹GRPH››
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
lemma is_iso_arr_is_iso_dghm:
assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
and "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ 𝔄"
and "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 = dghm_id 𝔄"
and "𝔉 ∘⇩D⇩G⇩H⇩M 𝔊 = dghm_id 𝔅"
shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
proof(intro is_iso_dghmI)
interpret L: is_dghm α 𝔅 𝔄 𝔊 by (rule assms(2))
interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(1))
show "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" by (cs_concl cs_shallow cs_intro: dg_cs_intros)
show "v11 (𝔉⦇ObjMap⦈)"
proof(rule R.ObjMap.vsv_valeq_v11I)
fix a b assume prems[simp]:
"a ∈⇩∘ 𝔄⦇Obj⦈" "b ∈⇩∘ 𝔄⦇Obj⦈" "𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇b⦈"
from assms(1,2) have "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇b⦈"
by (simp add: dg_cs_simps)
then show "a = b" by (simp add: assms(3) dghm_id_components)
qed
show "v11 (𝔉⦇ArrMap⦈)"
proof(rule R.ArrMap.vsv_valeq_v11I)
fix a b
assume prems[simp]:
"a ∈⇩∘ 𝔄⦇Arr⦈" "b ∈⇩∘ 𝔄⦇Arr⦈" "𝔉⦇ArrMap⦈⦇a⦈ = 𝔉⦇ArrMap⦈⦇b⦈"
then have "𝔉⦇ArrMap⦈⦇a⦈ ∈⇩∘ 𝔅⦇Arr⦈"
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
with R.dghm_ArrMap_vsv L.dghm_ArrMap_vsv R.dghm_ArrMap_vrange have
"(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇a⦈ = (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇b⦈"
unfolding dghm_comp_components by (simp add: dg_cs_simps)
then show "a = b" by (simp add: assms(3) dghm_id_components)
qed
show "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
proof(intro vsubset_antisym vsubsetI)
from R.dghm_ObjMap_vrange show "a ∈⇩∘ ℛ⇩∘ (𝔉⦇ObjMap⦈) ⟹ a ∈⇩∘ 𝔅⦇Obj⦈" for a
by auto
next
fix a assume prems: "a ∈⇩∘ 𝔅⦇Obj⦈"
then have a_def[symmetric]: "(𝔉 ∘⇩D⇩G⇩H⇩M 𝔊)⦇ObjMap⦈⦇a⦈ = a"
unfolding assms(4) dghm_id_components by simp
from prems show "a ∈⇩∘ ℛ⇩∘ (𝔉⦇ObjMap⦈)"
by (subst a_def)
(
cs_concl cs_shallow
cs_intro: V_cs_intros dg_cs_intros cs_simp: dg_cs_simps
)
qed
show "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
proof(intro vsubset_antisym vsubsetI)
from R.dghm_ArrMap_vrange show "a ∈⇩∘ ℛ⇩∘ (𝔉⦇ArrMap⦈) ⟹ a ∈⇩∘ 𝔅⦇Arr⦈" for a
by auto
next
fix a assume prems: "a ∈⇩∘ 𝔅⦇Arr⦈"
then have a_def[symmetric]: "(𝔉 ∘⇩D⇩G⇩H⇩M 𝔊)⦇ArrMap⦈⦇a⦈ = a"
unfolding assms(4) dghm_id_components by simp
with prems show "a ∈⇩∘ ℛ⇩∘ (𝔉⦇ArrMap⦈)"
by (subst a_def)
(
cs_concl cs_shallow
cs_intro: V_cs_intros dg_cs_intros cs_simp: dg_cs_simps
)
qed
qed
lemma is_iso_dghm_is_iso_arr:
assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
shows [dghm_cs_intros]: "inv_dghm 𝔉 : 𝔅 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
and [dghm_cs_simps]: "inv_dghm 𝔉 ∘⇩D⇩G⇩H⇩M 𝔉 = dghm_id 𝔄"
and [dghm_cs_simps]: "𝔉 ∘⇩D⇩G⇩H⇩M inv_dghm 𝔉 = dghm_id 𝔅"
proof-
let ?𝔊 = ‹inv_dghm 𝔉›
interpret is_iso_dghm α 𝔄 𝔅 𝔉 by (rule assms(1))
show 𝔊: "?𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
proof(intro is_iso_dghmI is_dghmI, unfold dghm_cs_simps)
show "vfsequence (inv_dghm 𝔉)" unfolding inv_dghm_def by auto
show "vcard (inv_dghm 𝔉) = 4⇩ℕ"
unfolding inv_dghm_def by (simp add: nat_omega_simps)
show "inv_dghm 𝔉⦇ArrMap⦈⦇f⦈ : inv_dghm 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ inv_dghm 𝔉⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘𝔅⇙ b" for a b f
using that
by
(
intro iso_dghm_HomDom_is_arr_conv,
use nothing in ‹unfold inv_dghm_components›
)
(
cs_concl
cs_simp: V_cs_simps dghm_cs_simps dg_cs_simps
cs_intro: dg_cs_intros V_cs_intros
)+
qed
(
cs_concl cs_shallow
cs_simp: dg_cs_simps
cs_intro: dg_cs_intros V_cs_intros dghm_cs_intros
)+
show "inv_dghm 𝔉 ∘⇩D⇩G⇩H⇩M 𝔉 = dghm_id 𝔄"
proof(rule dghm_eqI[of α 𝔄 𝔄 _ 𝔄 𝔄])
show "(inv_dghm 𝔉 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈ = dghm_id 𝔄⦇ObjMap⦈"
unfolding inv_dghm_components dghm_comp_components dghm_id_components
by (rule ObjMap.v11_vcomp_vconverse)
show "(inv_dghm 𝔉 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ = dghm_id 𝔄⦇ArrMap⦈"
unfolding inv_dghm_components dghm_comp_components dghm_id_components
by (rule ArrMap.v11_vcomp_vconverse)
qed (use 𝔊 in ‹cs_concl cs_intro: dghm_cs_intros›)
show "𝔉 ∘⇩D⇩G⇩H⇩M inv_dghm 𝔉 = dghm_id 𝔅"
proof(rule dghm_eqI[of α 𝔅 𝔅 _ 𝔅 𝔅])
show "(𝔉 ∘⇩D⇩G⇩H⇩M inv_dghm 𝔉)⦇ObjMap⦈ = dghm_id 𝔅⦇ObjMap⦈"
unfolding inv_dghm_components dghm_comp_components dghm_id_components
by (rule ObjMap.v11_vcomp_vconverse')
show "(𝔉 ∘⇩D⇩G⇩H⇩M inv_dghm 𝔉)⦇ArrMap⦈ = dghm_id 𝔅⦇ArrMap⦈"
unfolding inv_dghm_components dghm_comp_components dghm_id_components
by (rule ArrMap.v11_vcomp_vconverse')
qed (use 𝔊 in ‹cs_concl cs_intro: dghm_cs_intros›)
qed
subsubsection‹Further properties›
lemma (in is_iso_dghm) iso_inv_dghm_ObjMap_dghm_ObjMap_app[dghm_cs_simps]:
assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "inv_dghm 𝔉⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈ = a"
proof-
from is_iso_dghm_is_iso_arr[OF is_iso_dghm_axioms] have
"(inv_dghm 𝔉 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ = dghm_id 𝔄⦇ObjMap⦈⦇a⦈"
by simp
from this assms show ?thesis
by
(
cs_prems cs_shallow
cs_simp: dg_cs_simps cs_intro: dg_cs_intros dghm_cs_intros
)
qed
lemmas [dghm_cs_simps] = is_iso_dghm.iso_inv_dghm_ObjMap_dghm_ObjMap_app
lemma (in is_iso_dghm) iso_inv_dghm_ArrMap_dghm_ArrMap_app[dghm_cs_simps]:
assumes "f : a ↦⇘𝔄⇙ b"
shows "inv_dghm 𝔉⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈ = f"
proof-
from is_iso_dghm_is_iso_arr[OF is_iso_dghm_axioms] have
"(inv_dghm 𝔉 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈⦇f⦈ = dghm_id 𝔄⦇ArrMap⦈⦇f⦈"
by simp
from this assms show ?thesis
by
(
cs_prems cs_shallow
cs_simp: dg_cs_simps cs_intro: dg_cs_intros dghm_cs_intros
)
qed
lemmas [dghm_cs_simps] = is_iso_dghm.iso_inv_dghm_ArrMap_dghm_ArrMap_app
subsection‹Isomorphic digraphs›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
locale iso_digraph =
fixes α 𝔄 𝔅 :: V
assumes iso_digraph_is_iso_dghm: "∃𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
notation iso_digraph (infixl ‹≈⇩D⇩Gı› 50)
sublocale iso_digraph ⊆ HomDom: digraph α 𝔄 + HomCod: digraph α 𝔅
using iso_digraph_is_iso_dghm by auto
text‹Rules.›
lemma iso_digraphI':
assumes "∃𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
shows "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
using assms iso_digraph.intro by auto
lemma iso_digraphI:
assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
shows "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
using assms unfolding iso_digraph_def by auto
lemma iso_digraphD[dest]:
assumes "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
shows "∃𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
using assms unfolding iso_digraph_def by simp_all
lemma iso_digraphE[elim]:
assumes "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
obtains 𝔉 where "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
using assms by auto
subsubsection‹A digraph isomorphism is an equivalence relation›
lemma iso_digraph_refl:
assumes "digraph α 𝔄"
shows "𝔄 ≈⇩D⇩G⇘α⇙ 𝔄"
proof(rule iso_digraphI[of _ _ _ ‹dghm_id 𝔄›])
interpret digraph α 𝔄 by (rule assms)
show "dghm_id 𝔄 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔄" by (rule dg_dghm_id_is_iso_dghm)
qed
lemma iso_digraph_sym[sym]:
assumes "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅"
shows "𝔅 ≈⇩D⇩G⇘α⇙ 𝔄"
proof-
interpret iso_digraph α 𝔄 𝔅 by (rule assms)
from iso_digraph_is_iso_dghm obtain 𝔉 where "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
by clarsimp
then have "inv_dghm 𝔉 : 𝔅 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
by (simp add: is_iso_dghm_is_iso_arr(1))
then show ?thesis
by (cs_concl cs_shallow cs_intro: dghm_cs_intros iso_digraphI)
qed
lemma iso_digraph_trans[trans]:
assumes "𝔄 ≈⇩D⇩G⇘α⇙ 𝔅" and "𝔅 ≈⇩D⇩G⇘α⇙ ℭ"
shows "𝔄 ≈⇩D⇩G⇘α⇙ ℭ"
proof-
interpret L: iso_digraph α 𝔄 𝔅 by (rule assms(1))
interpret R: iso_digraph α 𝔅 ℭ by (rule assms(2))
from L.iso_digraph_is_iso_dghm R.iso_digraph_is_iso_dghm show ?thesis
by (meson dghm_comp_is_iso_dghm iso_digraph.intro)
qed
text‹\newpage›
end