(* Copyright 2021 (C) Mihails Milehins *) section‹Subdigraph› theory CZH_DG_Subdigraph imports CZH_DG_Digraph CZH_DG_DGHM begin subsection‹Background› text‹ In this body of work, a subdigraph is a natural generalization of the concept of a subcategory, as defined in Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›, to digraphs. It should be noted that a similar concept also exists in the conventional graph theory, but further details are considered to be outside of the scope of this work. › named_theorems dg_sub_cs_intros named_theorems dg_sub_bw_cs_intros named_theorems dg_sub_fw_cs_intros named_theorems dg_sub_bw_cs_simps subsection‹Simple subdigraph› subsubsection‹Definition and elementary properties› locale subdigraph = sdg: digraph α 𝔅 + dg: digraph α ℭ for α 𝔅 ℭ + assumes subdg_Obj_vsubset[dg_sub_fw_cs_intros]: "a ∈⇩_{∘}𝔅⦇Obj⦈ ⟹ a ∈⇩_{∘}ℭ⦇Obj⦈" and subdg_is_arr_vsubset[dg_sub_fw_cs_intros]: "f : a ↦⇘𝔅⇙ b ⟹ f : a ↦⇘ℭ⇙ b" abbreviation is_subdigraph ("(_/ ⊆⇩_{D}⇩_{G}ı _)" [51, 51] 50) where "𝔅 ⊆⇩_{D}⇩_{G}⇘α⇙ ℭ ≡ subdigraph α 𝔅 ℭ" lemmas [dg_sub_fw_cs_intros] = subdigraph.subdg_Obj_vsubset subdigraph.subdg_is_arr_vsubset text‹Rules.› lemma (in subdigraph) subdigraph_axioms'[dg_cs_intros]: assumes "α' = α" and "𝔅' = 𝔅" shows "𝔅' ⊆⇩_{D}⇩_{G}⇘α'⇙ ℭ" unfolding assms by (rule subdigraph_axioms) lemma (in subdigraph) subdigraph_axioms''[dg_cs_intros]: assumes "α' = α" and "ℭ' = ℭ" shows "𝔅 ⊆⇩_{D}⇩_{G}⇘α'⇙ ℭ'" unfolding assms by (rule subdigraph_axioms) mk_ide rf subdigraph_def[unfolded subdigraph_axioms_def] |intro subdigraphI| |dest subdigraphD[dest]| |elim subdigraphE[elim!]| lemmas [dg_sub_cs_intros] = subdigraphD(1,2) text‹The opposite subdigraph.› lemma (in subdigraph) subdg_subdigraph_op_dg_op_dg: "op_dg 𝔅 ⊆⇩_{D}⇩_{G}⇘α⇙ op_dg ℭ" proof(rule subdigraphI) show "a ∈⇩_{∘}op_dg 𝔅⦇Obj⦈ ⟹ a ∈⇩_{∘}op_dg ℭ⦇Obj⦈" for a by (auto simp: dg_op_simps subdg_Obj_vsubset) show "f : a ↦⇘op_dg 𝔅⇙ b ⟹ f : a ↦⇘op_dg ℭ⇙ b" for f a b by (auto simp: dg_op_simps subdg_is_arr_vsubset) qed (auto simp: dg_op_simps intro: dg_op_intros) lemmas subdg_subdigraph_op_dg_op_dg[dg_op_intros] = subdigraph.subdg_subdigraph_op_dg_op_dg text‹Further rules.› lemma (in subdigraph) subdg_objD: assumes "a ∈⇩_{∘}𝔅⦇Obj⦈" shows "a ∈⇩_{∘}ℭ⦇Obj⦈" using assms by (auto intro: subdg_Obj_vsubset) lemmas [dg_sub_fw_cs_intros] = subdigraph.subdg_objD lemma (in subdigraph) subdg_arrD[dg_sub_fw_cs_intros]: assumes "f ∈⇩_{∘}𝔅⦇Arr⦈" shows "f ∈⇩_{∘}ℭ⦇Arr⦈" proof- from assms obtain a b where "f : a ↦⇘𝔅⇙ b" by auto then show "f ∈⇩_{∘}ℭ⦇Arr⦈" by (cs_concl cs_shallow cs_intro: subdg_is_arr_vsubset dg_cs_intros) qed lemmas [dg_sub_fw_cs_intros] = subdigraph.subdg_arrD lemma (in subdigraph) subdg_dom_simp: assumes "f ∈⇩_{∘}𝔅⦇Arr⦈" shows "𝔅⦇Dom⦈⦇f⦈ = ℭ⦇Dom⦈⦇f⦈" proof- from assms obtain a b where "f : a ↦⇘𝔅⇙ b" by auto then show "𝔅⦇Dom⦈⦇f⦈ = ℭ⦇Dom⦈⦇f⦈" by (force dest: subdg_is_arr_vsubset simp: dg_cs_simps) qed lemmas [dg_sub_bw_cs_simps] = subdigraph.subdg_dom_simp lemma (in subdigraph) subdg_cod_simp: assumes "f ∈⇩_{∘}𝔅⦇Arr⦈" shows "𝔅⦇Cod⦈⦇f⦈ = ℭ⦇Cod⦈⦇f⦈" proof- from assms obtain a b where "f : a ↦⇘𝔅⇙ b" by auto then show "𝔅⦇Cod⦈⦇f⦈ = ℭ⦇Cod⦈⦇f⦈" by (force dest: subdg_is_arr_vsubset simp: dg_cs_simps) qed lemmas [dg_sub_bw_cs_simps] = subdigraph.subdg_cod_simp lemma (in subdigraph) subdg_is_arrD: assumes "f : a ↦⇘𝔅⇙ b" shows "f : a ↦⇘ℭ⇙ b" using assms subdg_is_arr_vsubset by simp lemmas [dg_sub_fw_cs_intros] = subdigraph.subdg_is_arrD subsubsection‹The subdigraph relation is a partial order› lemma subdg_refl: assumes "digraph α 𝔄" shows "𝔄 ⊆⇩_{D}⇩_{G}⇘α⇙ 𝔄" proof- interpret digraph α 𝔄 by (rule assms) show ?thesis by unfold_locales simp qed lemma subdg_trans[trans]: assumes "𝔄 ⊆⇩_{D}⇩_{G}⇘α⇙ 𝔅" and "𝔅 ⊆⇩_{D}⇩_{G}⇘α⇙ ℭ" shows "𝔄 ⊆⇩_{D}⇩_{G}⇘α⇙ ℭ" proof- interpret 𝔄𝔅: subdigraph α 𝔄 𝔅 by (rule assms(1)) interpret 𝔅ℭ: subdigraph α 𝔅 ℭ by (rule assms(2)) show ?thesis by unfold_locales ( insert 𝔄𝔅.subdigraph_axioms, auto simp: 𝔅ℭ.subdg_Obj_vsubset 𝔄𝔅.subdg_Obj_vsubset subdigraph.subdg_is_arr_vsubset 𝔅ℭ.subdg_is_arr_vsubset ) qed lemma subdg_antisym: assumes "𝔄 ⊆⇩_{D}⇩_{G}⇘α⇙ 𝔅" and "𝔅 ⊆⇩_{D}⇩_{G}⇘α⇙ 𝔄" shows "𝔄 = 𝔅" proof- interpret 𝔄𝔅: subdigraph α 𝔄 𝔅 by (rule assms(1)) interpret 𝔅𝔄: subdigraph α 𝔅 𝔄 by (rule assms(2)) show ?thesis proof(rule dg_eqI) from assms show Arr: "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" by (intro vsubset_antisym vsubsetI) (auto simp: dg_sub_bw_cs_simps intro: dg_sub_fw_cs_intros) from assms show "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" by (intro vsubset_antisym vsubsetI) (auto simp: dg_sub_bw_cs_simps intro: dg_sub_fw_cs_intros) show "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" by (rule vsv_eqI) (auto simp: 𝔄𝔅.subdg_dom_simp Arr dg_cs_simps) show "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈" by (rule vsv_eqI) (auto simp: 𝔄𝔅.subdg_cod_simp Arr dg_cs_simps) qed (cs_concl cs_shallow cs_intro: dg_cs_intros)+ qed subsection‹Inclusion digraph homomorphism› subsubsection‹Definition and elementary properties› text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.› definition dghm_inc :: "V ⇒ V ⇒ V" where "dghm_inc 𝔅 ℭ = [vid_on (𝔅⦇Obj⦈), vid_on (𝔅⦇Arr⦈), 𝔅, ℭ]⇩_{∘}" text‹Components.› lemma dghm_inc_components: shows "dghm_inc 𝔅 ℭ⦇ObjMap⦈ = vid_on (𝔅⦇Obj⦈)" and "dghm_inc 𝔅 ℭ⦇ArrMap⦈ = vid_on (𝔅⦇Arr⦈)" and [dg_cs_simps]: "dghm_inc 𝔅 ℭ⦇HomDom⦈ = 𝔅" and [dg_cs_simps]: "dghm_inc 𝔅 ℭ⦇HomCod⦈ = ℭ" unfolding dghm_inc_def dghm_field_simps by (simp_all add: nat_omega_simps) subsubsection‹Object map› mk_VLambda dghm_inc_components(1)[folded VLambda_vid_on] |vsv dghm_inc_ObjMap_vsv[dg_cs_intros]| |vdomain dghm_inc_ObjMap_vdomain[dg_cs_simps]| |app dghm_inc_ObjMap_app[dg_cs_simps]| subsubsection‹Arrow map› mk_VLambda dghm_inc_components(2)[folded VLambda_vid_on] |vsv dghm_inc_ArrMap_vsv[dg_cs_intros]| |vdomain dghm_inc_ArrMap_vdomain[dg_cs_simps]| |app dghm_inc_ArrMap_app[dg_cs_simps]| subsubsection‹ Canonical inclusion digraph homomorphism associated with a subdigraph › sublocale subdigraph ⊆ inc: is_ft_dghm α 𝔅 ℭ ‹dghm_inc 𝔅 ℭ› proof(intro is_ft_dghmI is_dghmI) show "vfsequence (dghm_inc 𝔅 ℭ)" unfolding dghm_inc_def by auto show "vcard (dghm_inc 𝔅 ℭ) = 4⇩_{ℕ}" unfolding dghm_inc_def by (simp add: nat_omega_simps) show "ℛ⇩_{∘}(dghm_inc 𝔅 ℭ⦇ObjMap⦈) ⊆⇩_{∘}ℭ⦇Obj⦈" unfolding dghm_inc_components by (auto dest: subdg_objD) show "dghm_inc 𝔅 ℭ⦇ArrMap⦈⦇f⦈ : dghm_inc 𝔅 ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ dghm_inc 𝔅 ℭ⦇ObjMap⦈⦇b⦈" if "f : a ↦⇘𝔅⇙ b" for a b f using that by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_sub_fw_cs_intros) show "v11 (dghm_inc 𝔅 ℭ⦇ArrMap⦈ ↾⇧^{l}⇩_{∘}Hom 𝔅 a b)" if "a ∈⇩_{∘}𝔅⦇Obj⦈" and "b ∈⇩_{∘}𝔅⦇Obj⦈" for a b using that unfolding dghm_inc_components by simp qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+ lemmas (in subdigraph) subdg_dghm_inc_is_ft_dghm = inc.is_ft_dghm_axioms subsubsection‹The inclusion digraph homomorphism for the opposite digraphs› lemma (in subdigraph) subdg_dghm_inc_op_dg_is_dghm[dg_sub_cs_intros]: "dghm_inc (op_dg 𝔅) (op_dg ℭ) : op_dg 𝔅 ↦↦⇩_{D}⇩_{G}⇩_{.}⇩_{f}⇩_{a}⇩_{i}⇩_{t}⇩_{h}⇩_{f}⇩_{u}⇩_{l}⇘α⇙ op_dg ℭ" by (intro subdigraph.subdg_dghm_inc_is_ft_dghm subdg_subdigraph_op_dg_op_dg) lemmas [dg_sub_cs_intros] = subdigraph.subdg_dghm_inc_op_dg_is_dghm lemma (in subdigraph) subdg_op_dg_dghm_inc[dg_op_simps]: "op_dghm (dghm_inc 𝔅 ℭ) = dghm_inc (op_dg 𝔅) (op_dg ℭ)" by (rule dghm_eqI, unfold dg_op_simps dghm_inc_components id_def) ( auto simp: subdg_dghm_inc_op_dg_is_dghm is_ft_dghmD intro: dg_op_intros dg_cs_intros ) lemmas [dg_op_simps] = subdigraph.subdg_op_dg_dghm_inc subsection‹Full subdigraph› text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.› locale fl_subdigraph = subdigraph + assumes fl_subdg_is_fl_dghm_inc: "dghm_inc 𝔅 ℭ : 𝔅 ↦↦⇩_{D}⇩_{G}⇩_{.}⇩_{f}⇩_{u}⇩_{l}⇩_{l}⇘α⇙ ℭ" abbreviation is_fl_subdigraph ("(_/ ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{f}⇩_{u}⇩_{l}⇩_{l}ı _)" [51, 51] 50) where "𝔅 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{f}⇩_{u}⇩_{l}⇩_{l}⇘α⇙ ℭ ≡ fl_subdigraph α 𝔅 ℭ" sublocale fl_subdigraph ⊆ inc: is_fl_dghm α 𝔅 ℭ ‹dghm_inc 𝔅 ℭ› by (rule fl_subdg_is_fl_dghm_inc) text‹Rules.› lemma (in fl_subdigraph) fl_subdigraph_axioms'[dg_cs_intros]: assumes "α' = α" and "𝔅' = 𝔅" shows "𝔅' ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{f}⇩_{u}⇩_{l}⇩_{l}⇘α'⇙ ℭ" unfolding assms by (rule fl_subdigraph_axioms) lemma (in fl_subdigraph) fl_subdigraph_axioms''[dg_cs_intros]: assumes "α' = α" and "ℭ' = ℭ" shows "𝔅 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{f}⇩_{u}⇩_{l}⇩_{l}⇘α'⇙ ℭ'" unfolding assms by (rule fl_subdigraph_axioms) mk_ide rf fl_subdigraph_def[unfolded fl_subdigraph_axioms_def] |intro fl_subdigraphI| |dest fl_subdigraphD[dest]| |elim fl_subdigraphE[elim!]| lemmas [dg_sub_cs_intros] = fl_subdigraphD(1) text‹Elementary properties.› lemma (in fl_subdigraph) fl_subdg_Hom_eq: assumes "A ∈⇩_{∘}𝔅⦇Obj⦈" and "B ∈⇩_{∘}𝔅⦇Obj⦈" shows "Hom 𝔅 A B = Hom ℭ A B" proof- from assms have Arr_AB: "𝔅⦇Arr⦈ ∩⇩_{∘}Hom 𝔅 A B = Hom 𝔅 A B" by ( intro vsubset_antisym vsubsetI, unfold vintersection_iff in_Hom_iff; (elim conjE)?; (intro conjI)? ) (auto intro: dg_cs_intros) from assms have A: "vid_on (𝔅⦇Obj⦈)⦇A⦈ = A" and B: "vid_on (𝔅⦇Obj⦈)⦇B⦈ = B" by simp_all from inc.fl_dghm_surj_on_Hom[OF assms, unfolded dghm_inc_components] show "Hom 𝔅 A B = Hom ℭ A B" by (auto simp: Arr_AB A B) qed subsection‹Wide subdigraph› subsubsection‹Definition and elementary properties› text‹ See \<^cite>‹"noauthor_nlab_nodate"›\footnote{ \url{https://ncatlab.org/nlab/show/wide+subcategory} }). › locale wide_subdigraph = subdigraph + assumes wide_subdg_Obj[dg_sub_bw_cs_intros]: "a ∈⇩_{∘}ℭ⦇Obj⦈ ⟹ a ∈⇩_{∘}𝔅⦇Obj⦈" abbreviation is_wide_subdigraph ("(_/ ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}ı _)" [51, 51] 50) where "𝔅 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ ℭ ≡ wide_subdigraph α 𝔅 ℭ" lemmas [dg_sub_bw_cs_intros] = wide_subdigraph.wide_subdg_Obj text‹Rules.› lemma (in wide_subdigraph) wide_subdigraph_axioms'[dg_cs_intros]: assumes "α' = α" and "𝔅' = 𝔅" shows "𝔅' ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α'⇙ ℭ" unfolding assms by (rule wide_subdigraph_axioms) lemma (in wide_subdigraph) wide_subdigraph_axioms''[dg_cs_intros]: assumes "α' = α" and "ℭ' = ℭ" shows "𝔅 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α'⇙ ℭ'" unfolding assms by (rule wide_subdigraph_axioms) mk_ide rf wide_subdigraph_def[unfolded wide_subdigraph_axioms_def] |intro wide_subdigraphI| |dest wide_subdigraphD[dest]| |elim wide_subdigraphE[elim!]| lemmas [dg_sub_cs_intros] = wide_subdigraphD(1) text‹Elementary properties.› lemma (in wide_subdigraph) wide_subdg_obj_eq[dg_sub_bw_cs_simps]: "𝔅⦇Obj⦈ = ℭ⦇Obj⦈" using subdg_Obj_vsubset wide_subdg_Obj by auto lemmas [dg_sub_bw_cs_simps] = wide_subdigraph.wide_subdg_obj_eq subsubsection‹The wide subdigraph relation is a partial order› lemma wide_subdg_refl: assumes "digraph α 𝔄" shows "𝔄 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ 𝔄" proof- interpret digraph α 𝔄 by (rule assms) show ?thesis by unfold_locales simp qed lemma wide_subdg_trans[trans]: assumes "𝔄 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ 𝔅" and "𝔅 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ ℭ" shows "𝔄 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ ℭ" proof- interpret 𝔄𝔅: wide_subdigraph α 𝔄 𝔅 by (rule assms(1)) interpret 𝔅ℭ: wide_subdigraph α 𝔅 ℭ by (rule assms(2)) interpret 𝔄ℭ: subdigraph α 𝔄 ℭ by (rule subdg_trans) (cs_concl cs_shallow cs_intro: dg_cs_intros)+ show ?thesis by (cs_concl cs_intro: dg_sub_bw_cs_intros dg_cs_intros wide_subdigraphI) qed lemma wide_subdg_antisym: assumes "𝔄 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ 𝔅" and "𝔅 ⊆⇩_{D}⇩_{G}⇩_{.}⇩_{w}⇩_{i}⇩_{d}⇩_{e}⇘α⇙ 𝔄" shows "𝔄 = 𝔅" proof- interpret 𝔄𝔅: wide_subdigraph α 𝔄 𝔅 by (rule assms(1)) interpret 𝔅𝔄: wide_subdigraph α 𝔅 𝔄 by (rule assms(2)) show ?thesis by (rule subdg_antisym[OF 𝔄𝔅.subdigraph_axioms 𝔅𝔄.subdigraph_axioms]) qed text‹\newpage› end