Theory CZH_DG_Subdigraph

(* 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