Theory CZH_DG_PDigraph

(* Copyright 2021 (C) Mihails Milehins *)

section‹Product digraph›
theory CZH_DG_PDigraph
  imports 
    CZH_DG_TDGHM
    CZH_DG_Small_Digraph
begin



subsection‹Background›


text‹
The concept of a product digraph, as presented in this work, 
is a generalization of the concept of a product category,
as presented in Chapter II-3 in cite‹"mac_lane_categories_2010"›.
›

named_theorems dg_prod_cs_simps
named_theorems dg_prod_cs_intros



subsection‹Product digraph: definition and elementary properties›

definition dg_prod :: "V ⇒ (V ⇒ V) ⇒ V"
  where "dg_prod I 𝔄 =
    [
      (∏∘i∈∘I. 𝔄 i⦇Obj⦈),
      (∏∘i∈∘I. 𝔄 i⦇Arr⦈),
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈)),
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈))
    ]∘"

syntax "_PDIGRAPH" :: "pttrn ⇒ V ⇒ (V ⇒ V) ⇒ V"
  (‹(3∏DG_∈∘_./ _)› [0, 0, 10] 10)
translations "∏DGi∈∘I. 𝔄" ⇌ "CONST dg_prod I (λi. 𝔄)"


text‹Components.›

lemma dg_prod_components:
  shows "(∏DGi∈∘I. 𝔄 i)⦇Obj⦈ = (∏∘i∈∘I. 𝔄 i⦇Obj⦈)"
    and "(∏DGi∈∘I. 𝔄 i)⦇Arr⦈ = (∏∘i∈∘I. 𝔄 i⦇Arr⦈)"
    and "(∏DGi∈∘I. 𝔄 i)⦇Dom⦈ =
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈))"
    and "(∏DGi∈∘I. 𝔄 i)⦇Cod⦈ =
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈))"
  unfolding dg_prod_def dg_field_simps by (simp_all add: nat_omega_simps)



subsection‹Local assumptions for a product digraph›

locale pdigraph_base = 𝒵 α for α I and 𝔄 :: "V ⇒ V" +
  assumes pdg_digraphs[dg_prod_cs_intros]: "i ∈∘ I ⟹ digraph α (𝔄 i)"
    and pdg_index_in_Vset[dg_cs_intros]: "I ∈∘ Vset α"


text‹Rules.›

lemma (in pdigraph_base) pdigraph_base_axioms'[dg_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "pdigraph_base α' I' 𝔄"
  unfolding assms by (rule pdigraph_base_axioms)

mk_ide rf pdigraph_base_def[unfolded pdigraph_base_axioms_def]
  |intro pdigraph_baseI|
  |dest pdigraph_baseD[dest]|
  |elim pdigraph_baseE[elim]|


text‹Elementary properties.›

lemma (in pdigraph_base) pdg_Obj_in_Vset: 
  assumes "𝒵 β" and "α ∈∘ β" 
  shows "(∏∘i∈∘I. 𝔄 i⦇Obj⦈) ∈∘ Vset β"
proof(rule Vset_trans)
  interpret β: 𝒵 β by (rule assms(1))
  show "(∏∘i∈∘I. 𝔄 i⦇Obj⦈) ∈∘ Vset (succ (succ α))"
  proof
    (
      rule vsubset_in_VsetI,
      rule Limit_vproduct_vsubset_Vset_succI,
      rule Limit_α,
      intro dg_cs_intros
    )
    show "Vset (succ α) ∈∘ Vset (succ (succ α))" 
      by (cs_concl cs_shallow cs_intro: V_cs_intros)
    fix i assume "i ∈∘ I"
    then interpret digraph α ‹𝔄 i›
      by (cs_concl cs_shallow cs_intro: dg_cs_intros dg_prod_cs_intros)
    show "𝔄 i⦇Obj⦈ ⊆∘ Vset α" by (rule dg_Obj_vsubset_Vset)
  qed
  from assms(2) show "Vset (succ (succ α)) ∈∘ Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros succ_in_Limit_iff[THEN iffD2])
qed

lemma (in pdigraph_base) pdg_Arr_in_Vset: 
  assumes "𝒵 β" and "α ∈∘ β" 
  shows "(∏∘i∈∘I. 𝔄 i⦇Arr⦈) ∈∘ Vset β"
proof(rule Vset_trans)
  interpret β: 𝒵 β by (rule assms(1))
  show "(∏∘i∈∘I. 𝔄 i⦇Arr⦈) ∈∘ Vset (succ (succ α))"
  proof
    (
      rule vsubset_in_VsetI,
      rule Limit_vproduct_vsubset_Vset_succI,
      rule Limit_α,
      intro dg_cs_intros
    )
    fix i assume "i ∈∘ I"
    then interpret digraph α ‹𝔄 i› 
      by (cs_concl cs_shallow cs_intro: dg_prod_cs_intros)
    show "𝔄 i⦇Arr⦈ ⊆∘ Vset α" by (rule dg_Arr_vsubset_Vset)
  qed (cs_concl cs_shallow cs_intro: V_cs_intros)
  from assms(2) show "Vset (succ (succ α)) ∈∘ Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros succ_in_Limit_iff[THEN iffD2])
qed

lemmas_with (in pdigraph_base) [folded dg_prod_components]:
  pdg_dg_prod_Obj_in_Vset[dg_cs_intros] = pdg_Obj_in_Vset
  and pdg_dg_prod_Arr_in_Vset[dg_cs_intros] = pdg_Arr_in_Vset

lemma (in pdigraph_base) pdg_vsubset_index_pdigraph_base:
  assumes "J ⊆∘ I"
  shows "pdigraph_base α J 𝔄"
  using assms
  by (intro pdigraph_baseI)
    (auto simp: vsubset_in_VsetI dg_cs_intros intro: dg_prod_cs_intros)


subsubsection‹Object›

lemma dg_prod_ObjI:
  assumes "vsv a" and "𝒟∘ a = I" and "⋀i. i ∈∘ I ⟹ a⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
  shows "a ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
  using assms unfolding dg_prod_components by auto

lemma dg_prod_ObjD:
  assumes "a ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈" 
  shows "vsv a" and "𝒟∘ a = I" and "⋀i. i ∈∘ I ⟹ a⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
  using assms unfolding dg_prod_components by auto

lemma dg_prod_ObjE:
  assumes "a ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈" 
  obtains "vsv a" and "𝒟∘ a = I" and "⋀i. i ∈∘ I ⟹ a⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
  using assms by (auto dest: dg_prod_ObjD)

lemma dg_prod_Obj_cong:
  assumes "g ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
    and "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
    and "⋀i. i ∈∘ I ⟹ g⦇i⦈ = f⦇i⦈"
  shows "g = f"
  using assms by (intro vsv_eqI[of g f]) (force simp: dg_prod_components)+


subsubsection‹Arrow›

lemma dg_prod_ArrI:
  assumes "vsv f" and "𝒟∘ f = I" and "⋀i. i ∈∘ I ⟹ f⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
  shows "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
  using assms unfolding dg_prod_components by auto

lemma dg_prod_ArrD:
  assumes "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈" 
  shows "vsv f" and "𝒟∘ f = I" and "⋀i. i ∈∘ I ⟹ f⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
  using assms unfolding dg_prod_components by auto

lemma dg_prod_ArrE:
  assumes "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈" 
  obtains "vsv f" and "𝒟∘ f = I" and "⋀i. i ∈∘ I ⟹ f⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
  using assms by (auto dest: dg_prod_ArrD)

lemma dg_prod_Arr_cong:
  assumes "g ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    and "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    and "⋀i. i ∈∘ I ⟹ g⦇i⦈ = f⦇i⦈"
  shows "g = f"
  using assms by (intro vsv_eqI[of g f]) (force simp: dg_prod_components)+


subsubsection‹Domain›

mk_VLambda dg_prod_components(3)
  |vsv dg_prod_Dom_vsv[dg_cs_intros]|
  |vdomain dg_prod_Dom_vdomain[folded dg_prod_components, dg_cs_simps]|
  |app dg_prod_Dom_app[folded dg_prod_components]|

lemma (in pdigraph_base) dg_prod_Dom_app_in_Obj[dg_cs_intros]:
  assumes "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
  shows "(∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈ ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
  unfolding dg_prod_components(1) dg_prod_Dom_app[OF assms]
proof(intro vproductI ballI)
  fix i assume prems: "i ∈∘ I" 
  interpret digraph α ‹𝔄 i› 
    by (auto simp: prems intro: dg_prod_cs_intros)
  from assms prems show "(λi∈∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
    unfolding dg_prod_components(2) by force
qed simp_all

lemma dg_prod_Dom_app_component_app[dg_cs_simps]:
  assumes "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈" and "i ∈∘ I"
  shows "(∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈⦇i⦈ = 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈"
  using assms(2) unfolding dg_prod_Dom_app[OF assms(1)] by simp


subsubsection‹Codomain›

mk_VLambda dg_prod_components(4)
  |vsv dg_prod_Cod_vsv[dg_cs_intros]|
  |vdomain dg_prod_Cod_vdomain[folded dg_prod_components, dg_cs_simps]|
  |app dg_prod_Cod_app[folded dg_prod_components]|

lemma (in pdigraph_base) dg_prod_Cod_app_in_Obj[dg_cs_intros]:
  assumes "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
  shows "(∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈ ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
  unfolding dg_prod_components(1) dg_prod_Cod_app[OF assms]
proof(rule vproductI)
  show "∀i∈∘I. (λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
  proof(intro ballI)
    fix i assume prems: "i ∈∘ I" 
    then interpret digraph α ‹𝔄 i› 
      by (auto intro: dg_prod_cs_intros)
    from assms prems show "(λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
      unfolding dg_prod_components(2) by force
  qed
qed simp_all

lemma dg_prod_Cod_app_component_app[dg_cs_simps]:
  assumes "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈" and "i ∈∘ I"
  shows "(∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈⦇i⦈ = 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈"
  using assms(2) unfolding dg_prod_Cod_app[OF assms(1)] by simp


subsubsection‹A product ‹α›-digraph is a tiny ‹β›-digraph›

lemma (in pdigraph_base) pdg_tiny_digraph_dg_prod:
  assumes "𝒵 β" and "α ∈∘ β" 
  shows "tiny_digraph β (∏DGi∈∘I. 𝔄 i)"
proof(intro tiny_digraphI)
  show "vfsequence (∏DGi∈∘I. 𝔄 i)" unfolding dg_prod_def by simp
  show "vcard (∏DGi∈∘I. 𝔄 i) = 4ℕ"
    unfolding dg_prod_def by (simp add: nat_omega_simps)
  show vsv_dg_prod_Dom: "vsv ((∏DGi∈∘I. 𝔄 i)⦇Dom⦈)" 
    unfolding dg_prod_components by simp
  show vdomain_dg_prod_Dom: "𝒟∘ ((∏DGi∈∘I. 𝔄 i)⦇Dom⦈) = (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    unfolding dg_prod_components by simp
  show "ℛ∘ ((∏DGi∈∘I. 𝔄 i)⦇Dom⦈) ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"  
    by (rule vsubsetI)
      (
        metis 
          dg_prod_Dom_app_in_Obj 
          dg_prod_Dom_vdomain 
          vsv.vrange_atE 
          vsv_dg_prod_Dom
      )
  show vsv_dg_prod_Cod: "vsv ((∏DGi∈∘I. 𝔄 i)⦇Cod⦈)" 
    unfolding dg_prod_components by auto
  show vdomain_dg_prod_Cod: "𝒟∘ ((∏DGi∈∘I. 𝔄 i)⦇Cod⦈) = (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    unfolding dg_prod_components by auto
  show "ℛ∘ ((∏DGi∈∘I. 𝔄 i)⦇Cod⦈) ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"  
    by (rule vsubsetI)
      (
        metis 
          dg_prod_Cod_app_in_Obj 
          vdomain_dg_prod_Cod 
          vsv.vrange_atE 
          vsv_dg_prod_Cod
      )
qed 
  (
    auto simp:
      dg_cs_intros
      assms 
      pdg_dg_prod_Arr_in_Vset[OF assms(1,2)]
      pdg_dg_prod_Obj_in_Vset[OF assms(1,2)]
  )


lemma (in pdigraph_base) pdg_tiny_digraph_dg_prod': 
  "tiny_digraph (α + ω) (∏DGi∈∘I. 𝔄 i)"
  by (rule pdg_tiny_digraph_dg_prod)
    (simp_all add: 𝒵_α_αω 𝒵.intro 𝒵_Limit_αω 𝒵_ω_αω)


subsubsection‹Arrow with a domain and a codomain›

lemma (in pdigraph_base) dg_prod_is_arrI:
  assumes "vsv f"
    and "𝒟∘ f = I"
    and "vsv a"
    and "𝒟∘ a = I"
    and "vsv b"
    and "𝒟∘ b = I"
    and "⋀i. i ∈∘ I ⟹ f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈"
  shows "f : a ↦⇘∏DGi∈∘I. 𝔄 i⇙ b"
proof(intro is_arrI)
  interpret f: vsv f by (rule assms(1))
  interpret a: vsv a by (rule assms(3))
  interpret b: vsv b by (rule assms(5))
  from assms(7) have f_components: "⋀i. i ∈∘ I ⟹ f⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈" by auto
  from assms(7) have a_components: "⋀i. i ∈∘ I ⟹ a⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
    by (meson digraph.dg_is_arrD(2) pdg_digraphs)
  from assms(7) have b_components: "⋀i. i ∈∘ I ⟹ b⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
    by (meson digraph.dg_is_arrD(3) pdg_digraphs)
  show f_in_Arr: "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    unfolding dg_prod_components
    by (intro vproductI)
      (auto simp: f_components assms(2) f.vsv_vrange_vsubset_vifunion_app)
  show "(∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈ = a"
  proof(rule vsv_eqI)
    from dg_prod_Dom_app_in_Obj[OF f_in_Arr] show "vsv ((∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈)"
      unfolding dg_prod_components by clarsimp
    from dg_prod_Dom_app_in_Obj[OF f_in_Arr] assms(4) show [simp]:
      "𝒟∘ ((∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈) = 𝒟∘ a"
      unfolding dg_prod_components by clarsimp
    fix i assume "i ∈∘ 𝒟∘ ((∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈)"
    then have i: "i ∈∘ I" by (simp add: assms(4))
    from a_components assms(7) i show "(∏DGi∈∘I. 𝔄 i)⦇Dom⦈⦇f⦈⦇i⦈ = a⦇i⦈"
      unfolding dg_prod_Dom_app_component_app[OF f_in_Arr i] by auto
  qed auto
  show "(∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈ = b"
  proof(rule vsv_eqI)
    from dg_prod_Cod_app_in_Obj[OF f_in_Arr] show "vsv ((∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈)"
      unfolding dg_prod_components by clarsimp
    from dg_prod_Cod_app_in_Obj[OF f_in_Arr] assms(6) show [simp]:
      "𝒟∘ ((∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈) = 𝒟∘ b"
      unfolding dg_prod_components by clarsimp
    fix i assume "i ∈∘ 𝒟∘ ((∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈)"
    then have i: "i ∈∘ I" by (simp add: assms(6))
    from b_components assms(7) i show "(∏DGi∈∘I. 𝔄 i)⦇Cod⦈⦇f⦈⦇i⦈ = b⦇i⦈"
      unfolding dg_prod_Cod_app_component_app[OF f_in_Arr i] by auto
  qed auto
qed

lemma (in pdigraph_base) dg_prod_is_arrD[dest]:
  assumes "f : a ↦⇘∏DGi∈∘I. 𝔄 i⇙ b"
  shows "vsv f"
    and "𝒟∘ f = I"
    and "vsv a"
    and "𝒟∘ a = I"
    and "vsv b"
    and "𝒟∘ b = I"
    and "⋀i. i ∈∘ I ⟹ f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈"
proof-
  from is_arrD[OF assms] have f: "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    and a: "a ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈" 
    and b: "b ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈" 
    by (auto intro: dg_cs_intros)
  then show "𝒟∘ f = I" "𝒟∘ a = I" "𝒟∘ b = I" "vsv f" "vsv a" "vsv b"
    unfolding dg_prod_components by auto
  fix i assume prems: "i ∈∘ I"
  show "f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈"
  proof(intro is_arrI)
    from assms(1) have f: "f ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
      and a: "a ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
      and b: "b ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
    by (auto intro: dg_cs_intros)
    from f prems show "f⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
      unfolding dg_prod_components by clarsimp
    from a b assms(1) prems dg_prod_components(2,3,4) show 
      "𝔄 i⦇Dom⦈⦇f⦇i⦈⦈ = a⦇i⦈" "𝔄 i⦇Cod⦈⦇f⦇i⦈⦈ = b⦇i⦈"
      by fastforce+
  qed
qed

lemma (in pdigraph_base) dg_prod_is_arrE[elim]:
  assumes "f : a ↦⇘∏DGi∈∘I. 𝔄 i⇙ b"
  obtains "vsv f"
    and "𝒟∘ f = I"
    and "vsv a"
    and "𝒟∘ a = I"
    and "vsv b"
    and "𝒟∘ b = I"
    and "⋀i. i ∈∘ I ⟹ f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈"
  using assms by auto



subsection‹Further local assumptions for product digraphs›


subsubsection‹Definition and elementary properties›

locale pdigraph = pdigraph_base α I 𝔄 for α I 𝔄 +
  assumes pdg_Obj_vsubset_Vset: "J ⊆∘ I ⟹ (∏DGi∈∘J. 𝔄 i)⦇Obj⦈ ⊆∘ Vset α"
    and pdg_Hom_vifunion_in_Vset: 
      "⟦
        J ⊆∘ I;
        A ⊆∘ (∏DGi∈∘J. 𝔄 i)⦇Obj⦈;
        B ⊆∘ (∏DGi∈∘J. 𝔄 i)⦇Obj⦈;
        A ∈∘ Vset α;
        B ∈∘ Vset α
      ⟧ ⟹ (⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘J. 𝔄 i) a b) ∈∘ Vset α"


text‹Rules.›

lemma (in pdigraph) pdigraph_axioms'[dg_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "pdigraph α' I' 𝔄"
  unfolding assms by (rule pdigraph_axioms)

mk_ide rf pdigraph_def[unfolded pdigraph_axioms_def]
  |intro pdigraphI|
  |dest pdigraphD[dest]|
  |elim pdigraphE[elim]|

lemmas [dg_prod_cs_intros] = pdigraphD(1)


text‹Elementary properties.›

lemma (in pdigraph) pdg_Obj_vsubset_Vset': "(∏DGi∈∘I. 𝔄 i)⦇Obj⦈ ⊆∘ Vset α"
  by (rule pdg_Obj_vsubset_Vset) simp

lemma (in pdigraph) pdg_Hom_vifunion_in_Vset':
  assumes "A ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
    and "B ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
    and "A ∈∘ Vset α"
    and "B ∈∘ Vset α"
  shows "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘I. 𝔄 i) a b) ∈∘ Vset α"
  using assms by (intro pdg_Hom_vifunion_in_Vset) simp_all

lemma (in pdigraph) pdg_vsubset_index_pdigraph:
  assumes "J ⊆∘ I"
  shows "pdigraph α J 𝔄"
proof(intro pdigraphI)
  show "dg_prod J' 𝔄⦇Obj⦈ ⊆∘ Vset α" if ‹J' ⊆∘ J› for J'
  proof-
    from that assms have "J' ⊆∘ I" by simp
    then show "dg_prod J' 𝔄⦇Obj⦈ ⊆∘ Vset α" by (rule pdg_Obj_vsubset_Vset)
  qed
  fix A B J' assume prems: 
    "J' ⊆∘ J"
    "A ⊆∘ (∏DGi∈∘J'. 𝔄 i)⦇Obj⦈"
    "B ⊆∘ (∏DGi∈∘J'. 𝔄 i)⦇Obj⦈"
    "A ∈∘ Vset α" 
    "B ∈∘ Vset α"
  show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘J'. 𝔄 i) a b) ∈∘ Vset α"
  proof-
    from prems(1) assms have "J' ⊆∘ I" by simp
    from pdg_Hom_vifunion_in_Vset[OF this prems(2-5)] show ?thesis.
  qed
qed (rule pdg_vsubset_index_pdigraph_base[OF assms])


subsubsection‹A product ‹α›-digraph is an ‹α›-digraph›

lemma (in pdigraph) pdg_digraph_dg_prod: "digraph α (∏DGi∈∘I. 𝔄 i)"
proof-
  interpret tiny_digraph ‹α + ω› ‹∏DGi∈∘I. 𝔄 i›
    by (intro pdg_tiny_digraph_dg_prod) 
      (auto simp: 𝒵_α_αω 𝒵.intro 𝒵_Limit_αω 𝒵_ω_αω)
  show ?thesis
    by (rule digraph_if_digraph)  
      (
        auto 
          intro!: pdg_Hom_vifunion_in_Vset pdg_Obj_vsubset_Vset
          intro: dg_cs_intros
      )
qed



subsection‹Local assumptions for a finite product digraph›


subsubsection‹Definition and elementary properties›

locale finite_pdigraph = pdigraph_base α I 𝔄 for α I 𝔄 +
  assumes fin_pdg_index_vfinite: "vfinite I"


text‹Rules.›

lemma (in finite_pdigraph) finite_pdigraph_axioms'[dg_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "finite_pdigraph α' I' 𝔄"
  unfolding assms by (rule finite_pdigraph_axioms)

mk_ide rf finite_pdigraph_def[unfolded finite_pdigraph_axioms_def]
  |intro finite_pdigraphI|
  |dest finite_pdigraphD[dest]|
  |elim finite_pdigraphE[elim]|

lemmas [dg_prod_cs_intros] = finite_pdigraphD(1)


subsubsection‹
Local assumptions for a finite product digraph and local
assumptions for an arbitrary product digraph
›

sublocale finite_pdigraph ⊆ pdigraph α I 𝔄
proof(intro pdigraphI)
  show "(∏DGi∈∘J. 𝔄 i)⦇Obj⦈ ⊆∘ Vset α" if "J ⊆∘ I" for J
    unfolding dg_prod_components
  proof-
    from that fin_pdg_index_vfinite have J: "vfinite J"
      by (cs_concl cs_shallow cs_intro: vfinite_vsubset)
    show "(∏∘i∈∘J. 𝔄 i⦇Obj⦈) ⊆∘ Vset α"
    proof(intro vsubsetI)
      fix A assume prems: "A ∈∘ (∏∘i∈∘J. 𝔄 i⦇Obj⦈)"
      note A = vproductD[OF prems, rule_format]
      show "A ∈∘ Vset α"
      proof(rule vsv.vsv_Limit_vsv_in_VsetI)
        from that show "𝒟∘ A ∈∘ Vset α" 
          unfolding A(2) by (auto intro: pdg_index_in_Vset)
        show "ℛ∘ A ⊆∘ Vset α"
        proof(intro vsv.vsv_vrange_vsubset, unfold A(2))
          fix i assume prems': "i ∈∘ J"
          with that have i: "i ∈∘ I" by auto
          interpret digraph α ‹𝔄 i›
            by (cs_concl cs_shallow cs_intro: dg_prod_cs_intros i)
          have "A⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈" by (rule A(3)[OF prems'])
          then show "A⦇i⦈ ∈∘ Vset α" by (cs_concl cs_intro: dg_cs_intros)
        qed (intro A(1))
      qed (auto simp: A(2) intro!: J A(1))
    qed
  qed
  show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘J. 𝔄 i) a b) ∈∘ Vset α"
    if J: "J ⊆∘ I"
      and A: "A ⊆∘ (∏DGi∈∘J. 𝔄 i)⦇Obj⦈"
      and B: "B ⊆∘ (∏DGi∈∘J. 𝔄 i)⦇Obj⦈"
      and A_in_Vset: "A ∈∘ Vset α"
      and B_in_Vset: "B ∈∘ Vset α"
    for J A B 
  proof-
    interpret J: pdigraph_base α J 𝔄 
      by (intro J pdg_vsubset_index_pdigraph_base)
    let ?UA = ‹⋃∘(⋃∘(⋃∘A))› and ?UB = ‹⋃∘(⋃∘(⋃∘B))›
    from that(4) have UA: "?UA ∈∘ Vset α" by (intro VUnion_in_VsetI)
    from that(5) have UB: "?UB ∈∘ Vset α" by (intro VUnion_in_VsetI)
    have "(∏∘i∈∘J. (⋃∘a∈∘?UA. ⋃∘b∈∘?UB. Hom (𝔄 i) a b)) ∈∘ Vset α"
    proof(intro Limit_vproduct_in_VsetI)
      from that(1) show "J ∈∘ Vset α" by (auto intro!: pdg_index_in_Vset)
      show "(⋃∘a∈∘?UA. ⋃∘b∈∘?UB. Hom (𝔄 i) a b) ∈∘ Vset α" if i: "i ∈∘ J" for i
      proof-
        from i J have i: "i ∈∘ I" by auto
        interpret digraph α ‹𝔄 i› 
          using i by (cs_concl cs_intro: dg_prod_cs_intros)
        have [dg_cs_simps]: "(⋃∘a∈∘?UA. ⋃∘b∈∘?UB. Hom (𝔄 i) a b) ⊆∘
          (⋃∘a∈∘?UA ∩∘ 𝔄 i⦇Obj⦈. ⋃∘b∈∘?UB ∩∘ 𝔄 i⦇Obj⦈. Hom (𝔄 i) a b)"
        proof(intro vsubsetI)
          fix f assume "f ∈∘ (⋃∘a∈∘?UA. ⋃∘b∈∘?UB. Hom (𝔄 i) a b)"
          then obtain a b
            where a: "a ∈∘ ?UA" and b: "b ∈∘ ?UB" and f: "f : a ↦⇘𝔄 i⇙ b" 
            by (elim vifunionE, unfold in_Hom_iff)
          then show
            "f ∈∘ (⋃∘a∈∘?UA ∩∘ 𝔄 i⦇Obj⦈. ⋃∘b∈∘?UB ∩∘ 𝔄 i⦇Obj⦈. Hom (𝔄 i) a b)"
            by (intro vifunionI, unfold in_Hom_iff) (auto intro!: f b a)
        qed
        moreover from UA UB have 
          "(⋃∘a∈∘?UA ∩∘ 𝔄 i⦇Obj⦈. ⋃∘b∈∘?UB ∩∘ 𝔄 i⦇Obj⦈. Hom (𝔄 i) a b) ∈∘ 
            Vset α"
          by (intro dg_Hom_vifunion_in_Vset) auto
        ultimately show ?thesis by auto
      qed
      from J show "vfinite J"
        by (rule vfinite_vsubset[OF fin_pdg_index_vfinite])
    qed auto
    moreover have 
      "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘J. 𝔄 i) a b) ⊆∘
        (∏∘i∈∘J. (⋃∘a∈∘?UA. ⋃∘b∈∘?UB. Hom (𝔄 i) a b))"
    proof(intro vsubsetI)
      fix f assume "f ∈∘ (⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘J. 𝔄 i) a b)"
      then obtain a b 
        where a: "a ∈∘ A" and b: "b ∈∘ B" and f: "f ∈∘ Hom (∏DGi∈∘J. 𝔄 i) a b"
        by auto
      from f have f: "f : a ↦⇘(∏DGi∈∘J. 𝔄 i)⇙ b" by simp
      show "f ∈∘ (∏∘i∈∘J. (⋃∘a∈∘?UA. ⋃∘b∈∘?UB. Hom (𝔄 i) a b))"
      proof
        (
          intro vproductI, 
          unfold Ball_def; 
          (intro allI impI)?;
          (intro vifunionI)?;
          (unfold in_Hom_iff)?
        )
        from f show "vsv f" by (auto simp: dg_prod_components(2))
        from f show "𝒟∘ f = J" by (auto simp: dg_prod_components(2))
        fix i assume i: "i ∈∘ J"
        show "a⦇i⦈ ∈∘ ?UA"
          by 
            (
              intro vprojection_in_VUnionI, 
              rule that(2)[unfolded dg_prod_components(1)]; 
              intro a i
            )
        show "b⦇i⦈ ∈∘ ?UB"
          by 
            (
              intro vprojection_in_VUnionI, 
              rule that(3)[unfolded dg_prod_components(1)]; 
              intro b i
            )
        show "f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈" by (rule J.dg_prod_is_arrD(7)[OF f i])
      qed
    qed
    ultimately show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏DGi∈∘J. 𝔄 i) a b) ∈∘ Vset α" 
      by blast
  qed
qed (intro pdigraph_base_axioms)



subsection‹Binary union and complement›


subsubsection‹Application-specific methods›

method vdiff_of_vunion uses rule assms subset = 
  (
    rule 
      rule
        [
          OF vintersection_complement assms, 
          unfolded vunion_complement[OF subset]
        ]
  )

method vdiff_of_vunion' uses rule assms subset = 
  (
    rule 
      rule
        [
          OF vintersection_complement complement_vsubset subset assms, 
          unfolded vunion_complement[OF subset]
        ]
  )


subsubsection‹Results›

lemma dg_prod_vunion_Obj_in_Obj:
  assumes "vdisjnt J K"
    and "b ∈∘ (∏DGj∈∘J. 𝔄 j)⦇Obj⦈" 
    and "c ∈∘ (∏DGk∈∘K. 𝔄 k)⦇Obj⦈"
  shows "b ∪∘ c ∈∘ (∏DGi∈∘J ∪∘ K. 𝔄 i)⦇Obj⦈"
proof-

  interpret b: vsv b using assms(2) unfolding dg_prod_components by clarsimp
  interpret c: vsv c using assms(3) unfolding dg_prod_components by clarsimp

  from assms(2,3) have dom_b: "𝒟∘ b = J" and dom_c: "𝒟∘ c = K"
    unfolding dg_prod_components by auto
  from assms(1) have disjnt: "𝒟∘ b ∩∘ 𝒟∘ c = 0" unfolding dom_b dom_c by auto

  show ?thesis
    unfolding dg_prod_components
  proof(intro vproductI)
    show "𝒟∘ (b ∪∘ c) = J ∪∘ K" by (auto simp: vdomain_vunion dom_b dom_c)
    show "∀i∈∘J ∪∘ K. (b ∪∘ c)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
    proof(intro ballI)
      fix i assume prems: "i ∈∘ J ∪∘ K" 
      then consider (ib) ‹i ∈∘ 𝒟∘ b› | (ic) ‹i ∈∘ 𝒟∘ c› 
        unfolding dom_b dom_c by auto
      then show "(b ∪∘ c)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
      proof cases
        case ib
        with prems disjnt have bc_i: "(b ∪∘ c)⦇i⦈ = b⦇i⦈"
          by (auto intro!: vsv_vunion_app_left)
        from assms(2) ib show ?thesis unfolding bc_i dg_prod_components by auto
      next
        case ic 
        with prems disjnt have bc_i: "(b ∪∘ c)⦇i⦈ = c⦇i⦈"
          by (auto intro!: vsv_vunion_app_right)
        from assms(3) ic show ?thesis unfolding bc_i dg_prod_components by auto
      qed 
    qed
  qed (auto simp: disjnt)

qed

lemma dg_prod_vdiff_vunion_Obj_in_Obj:
  assumes "J ⊆∘ I"
    and "b ∈∘ (∏DGk∈∘I -∘ J. 𝔄 k)⦇Obj⦈" 
    and "c ∈∘ (∏DGj∈∘J. 𝔄 j)⦇Obj⦈"
  shows "b ∪∘ c ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
  by 
    (
      vdiff_of_vunion 
        rule: dg_prod_vunion_Obj_in_Obj assms: assms(2,3) subset: assms(1)
    )

lemma dg_prod_vunion_Arr_in_Arr:
  assumes "vdisjnt J K" 
    and "b ∈∘ (∏DGj∈∘J. 𝔄 j)⦇Arr⦈" 
    and "c ∈∘ (∏DGk∈∘K. 𝔄 k)⦇Arr⦈"
  shows "b ∪∘ c ∈∘ (∏DGi∈∘J ∪∘ K. 𝔄 i)⦇Arr⦈"
  unfolding dg_prod_components
proof(intro vproductI)

  interpret b: vsv b using assms(2) unfolding dg_prod_components by clarsimp
  interpret c: vsv c using assms(3) unfolding dg_prod_components by clarsimp

  from assms have dom_b: "𝒟∘ b = J" and dom_c: "𝒟∘ c = K" 
    unfolding dg_prod_components by auto
  from assms have disjnt: "𝒟∘ b ∩∘ 𝒟∘ c = 0" unfolding dom_b dom_c by auto

  from disjnt show "vsv (b ∪∘ c)" by auto
  show dom_bc: "𝒟∘ (b ∪∘ c) = J ∪∘ K" 
    unfolding vdomain_vunion dom_b dom_c by auto

  show "∀i∈∘J ∪∘ K. (b ∪∘ c)⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
  proof(intro ballI)
    fix i assume prems: "i ∈∘ J ∪∘ K" 
    then consider (ib) ‹i ∈∘ 𝒟∘ b› | (ic) ‹i ∈∘ 𝒟∘ c› 
      unfolding dom_b dom_c by auto
    then show "(b ∪∘ c)⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
    proof cases
      case ib
      with prems disjnt have bc_i: "(b ∪∘ c)⦇i⦈ = b⦇i⦈"
        by (auto intro!: vsv_vunion_app_left)
      from assms(2) ib show ?thesis unfolding bc_i dg_prod_components by auto
    next
      case ic 
      with prems disjnt have bc_i: "(b ∪∘ c)⦇i⦈ = c⦇i⦈"
        by (auto intro!: vsv_vunion_app_right)
      from assms(3) ic show ?thesis unfolding bc_i dg_prod_components by auto
    qed 
  qed

qed

lemma dg_prod_vdiff_vunion_Arr_in_Arr:
  assumes "J ⊆∘ I"
    and "b ∈∘ (∏DGk∈∘I -∘ J. 𝔄 k)⦇Arr⦈" 
    and "c ∈∘ (∏DGj∈∘J. 𝔄 j)⦇Arr⦈"
  shows "b ∪∘ c ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
  by 
    (
      vdiff_of_vunion 
        rule: dg_prod_vunion_Arr_in_Arr assms: assms(2,3) subset: assms(1)
    )

lemma (in pdigraph) pdg_dg_prod_vunion_is_arr:
  assumes "vdisjnt J K"
    and "J ⊆∘ I"
    and "K ⊆∘ I"
    and "g : a ↦⇘(∏DGj∈∘J. 𝔄 j)⇙ b" 
    and "f : c ↦⇘(∏DGk∈∘K. 𝔄 k)⇙ d"
  shows "g ∪∘ f : a ∪∘ c ↦⇘(∏DGi∈∘J ∪∘ K. 𝔄 i)⇙ b ∪∘ d"
proof-

  interpret J𝔄: pdigraph α J 𝔄 
    using assms(2) by (simp add: pdg_vsubset_index_pdigraph)
  interpret K𝔄: pdigraph α K 𝔄 
    using assms(3) by (simp add: pdg_vsubset_index_pdigraph)
  interpret JK𝔄: pdigraph α ‹J ∪∘ K› 𝔄 
    using assms(2,3) by (simp add: pdg_vsubset_index_pdigraph)

  show ?thesis
  proof(intro JK𝔄.dg_prod_is_arrI)

    note gD = J𝔄.dg_prod_is_arrD[OF assms(4)]
      and fD = K𝔄.dg_prod_is_arrD[OF assms(5)]

    from assms(1) gD fD show
      "vsv (g ∪∘ f)"
      "𝒟∘ (g ∪∘ f) = J ∪∘ K"
      "vsv (a ∪∘ c)"
      "𝒟∘ (a ∪∘ c) = J ∪∘ K"
      "vsv (b ∪∘ d)" 
      "𝒟∘ (b ∪∘ d) = J ∪∘ K"
      by (auto simp: vdomain_vunion)

    fix i assume "i ∈∘ J ∪∘ K"
    then consider (iJ) ‹i ∈∘ J› | (iK) ‹i ∈∘ K› by auto
    then show "(g ∪∘ f)⦇i⦈ : (a ∪∘ c)⦇i⦈ ↦⇘𝔄 i⇙ (b ∪∘ d)⦇i⦈" 
    proof cases
      case iJ
      have gf_i: "(g ∪∘ f)⦇i⦈ = g⦇i⦈" by (simp add: iJ assms(1) gD(1,2) fD(1,2))        
      have ac_i: "(a ∪∘ c)⦇i⦈ = a⦇i⦈" by (simp add: iJ assms(1) gD(3,4) fD(3,4))
      have bd_i: "(b ∪∘ d)⦇i⦈ = b⦇i⦈" by (simp add: iJ assms(1) gD(5,6) fD(5,6))
      show ?thesis unfolding gf_i ac_i bd_i by (rule gD(7)[OF iJ])
    next
      case iK
      have gf_i: "(g ∪∘ f)⦇i⦈ = f⦇i⦈" by (simp add: iK assms(1) gD(1,2) fD(1,2))        
      have ac_i: "(a ∪∘ c)⦇i⦈ = c⦇i⦈" by (simp add: iK assms(1) gD(3,4) fD(3,4))
      have bd_i: "(b ∪∘ d)⦇i⦈ = d⦇i⦈" by (simp add: iK assms(1) gD(5,6) fD(5,6))
      show ?thesis unfolding gf_i ac_i bd_i by (rule fD(7)[OF iK])
    qed

  qed

qed

lemma (in pdigraph) pdg_dg_prod_vdiff_vunion_is_arr:
  assumes "J ⊆∘ I"  
    and "g : a ↦⇘(∏DGk∈∘I -∘ J. 𝔄 k)⇙ b" 
    and "f : c ↦⇘(∏DGj∈∘J. 𝔄 j)⇙ d"
  shows "g ∪∘ f : a ∪∘ c ↦⇘∏DGi∈∘I. 𝔄 i⇙ b ∪∘ d"
  by 
    (
      vdiff_of_vunion' 
        rule: pdg_dg_prod_vunion_is_arr assms: assms(2,3) subset: assms(1)
    )



subsection‹Projection›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-3 in cite‹"mac_lane_categories_2010"›.›

definition dghm_proj :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V" (‹πDG›)
  where "πDG I 𝔄 i =
    [
      (λa∈∘((∏DGi∈∘I. 𝔄 i)⦇Obj⦈). a⦇i⦈),
      (λf∈∘((∏DGi∈∘I. 𝔄 i)⦇Arr⦈). f⦇i⦈),
      (∏DGi∈∘I. 𝔄 i),
      𝔄 i
    ]∘"


text‹Components.›

lemma dghm_proj_components:
  shows "πDG I 𝔄 i⦇ObjMap⦈ = (λa∈∘((∏DGi∈∘I. 𝔄 i)⦇Obj⦈). a⦇i⦈)"
    and "πDG I 𝔄 i⦇ArrMap⦈ = (λf∈∘((∏DGi∈∘I. 𝔄 i)⦇Arr⦈). f⦇i⦈)"
    and "πDG I 𝔄 i⦇HomDom⦈ = (∏DGi∈∘I. 𝔄 i)"
    and "πDG I 𝔄 i⦇HomCod⦈ = 𝔄 i"
  unfolding dghm_proj_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Object map.›

mk_VLambda dghm_proj_components(1)
  |vsv dghm_proj_ObjMap_vsv[dg_cs_intros]|
  |vdomain dghm_proj_ObjMap_vdomain[dg_cs_simps]|
  |app dghm_proj_ObjMap_app[dg_cs_simps]|

lemma (in pdigraph) dghm_proj_ObjMap_vrange: 
  assumes "i ∈∘ I"
  shows "ℛ∘ (πDG I 𝔄 i⦇ObjMap⦈) ⊆∘ 𝔄 i⦇Obj⦈"
  using assms 
  unfolding dghm_proj_components
  by (intro vrange_VLambda_vsubset) (clarsimp simp: dg_prod_components)


text‹Arrow map.›

mk_VLambda dghm_proj_components(2)
  |vsv dghm_proj_ArrMap_vsv[dg_cs_intros]|
  |vdomain dghm_proj_ArrMap_vdomain[dg_cs_simps]|
  |app dghm_proj_ArrMap_app[dg_cs_simps]|

lemma (in pdigraph) dghm_proj_ArrMap_vrange: 
  assumes "i ∈∘ I"
  shows "ℛ∘ (πDG I 𝔄 i⦇ArrMap⦈) ⊆∘ 𝔄 i⦇Arr⦈"
  using assms 
  unfolding dghm_proj_components
  by (intro vrange_VLambda_vsubset) (clarsimp simp: dg_prod_components)


subsubsection‹A projection digraph homomorphism is a digraph homomorphism›

lemma (in pdigraph) pdg_dghm_proj_is_dghm: 
  assumes "i ∈∘ I" 
  shows "πDG I 𝔄 i : (∏DGi∈∘I. 𝔄 i) ↦↦DG⇘α⇙ 𝔄 i"
proof(intro is_dghmI)
  show "vfsequence (πDG I 𝔄 i)" unfolding dghm_proj_def by auto
  show "vcard (πDG I 𝔄 i) = 4ℕ"
    unfolding dghm_proj_def by (simp add: nat_omega_simps)
  show "πDG I 𝔄 i⦇HomDom⦈ = (∏DGi∈∘I. 𝔄 i)"
    unfolding dghm_proj_components by simp
  show "πDG I 𝔄 i⦇HomCod⦈ = 𝔄 i" 
    unfolding dghm_proj_components by simp
  fix f a b assume "f : a ↦⇘∏DGi∈∘I. 𝔄 i⇙ b"
  with assms pdg_digraph_dg_prod show 
    "πDG I 𝔄 i⦇ArrMap⦈⦇f⦈ : πDG I 𝔄 i⦇ObjMap⦈⦇a⦈ ↦⇘𝔄 i⇙ πDG I 𝔄 i⦇ObjMap⦈⦇b⦈"
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_is_arrD(7))
qed 
  (
    auto simp: 
      dg_cs_simps dg_cs_intros dg_prod_cs_intros
      assms pdg_digraph_dg_prod dghm_proj_ObjMap_vrange
  )

lemma (in pdigraph) pdg_dghm_proj_is_dghm':
  assumes "i ∈∘ I" and "ℭ = (∏DGi∈∘I. 𝔄 i)" and "𝔇 = 𝔄 i"
  shows "πDG I 𝔄 i : ℭ ↦↦DG⇘α⇙ 𝔇"
  using assms(1) unfolding assms(2,3) by (rule pdg_dghm_proj_is_dghm)

lemmas [dg_cs_intros] = pdigraph.pdg_dghm_proj_is_dghm'



subsection‹Digraph product universal property digraph homomorphism›


subsubsection‹Definition and elementary properties›


text‹
The following digraph homomorphism is used in the 
proof of the universal property of the product digraph 
later in this work.
›

definition dghm_up :: "V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "dghm_up I 𝔄 ℭ φ =
    [
      (λa∈∘ℭ⦇Obj⦈. (λi∈∘I. φ i⦇ObjMap⦈⦇a⦈)),
      (λf∈∘ℭ⦇Arr⦈. (λi∈∘I. φ i⦇ArrMap⦈⦇f⦈)),
      ℭ,
      (∏DGi∈∘I. 𝔄 i)
    ]∘"


text‹Components.›

lemma dghm_up_components: 
  shows "dghm_up I 𝔄 ℭ φ⦇ObjMap⦈ = (λa∈∘ℭ⦇Obj⦈. (λi∈∘I. φ i⦇ObjMap⦈⦇a⦈))"
    and "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈ = (λf∈∘ℭ⦇Arr⦈. (λi∈∘I. φ i⦇ArrMap⦈⦇f⦈))"
    and "dghm_up I 𝔄 ℭ φ⦇HomDom⦈ = ℭ"
    and "dghm_up I 𝔄 ℭ φ⦇HomCod⦈ = (∏DGi∈∘I. 𝔄 i)"
  unfolding dghm_up_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda dghm_up_components(1)
  |vsv dghm_up_ObjMap_vsv[dg_cs_intros]|
  |vdomain dghm_up_ObjMap_vdomain[dg_cs_simps]|
  |app dghm_up_ObjMap_app|

lemma dghm_up_ObjMap_vrange: 
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i"
  shows "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈) ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
  unfolding dghm_up_components dg_prod_components
proof(intro vrange_VLambda_vsubset vproductI)
  fix a assume prems: "a ∈∘ ℭ⦇Obj⦈"
  show "∀i∈∘I. (λi∈∘I. φ i⦇ObjMap⦈⦇a⦈)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
  proof(intro ballI)
    fix i assume prems': "i ∈∘ I"
    interpret φ: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms[OF prems'])
    from prems prems' show "(λi∈∘I. φ i⦇ObjMap⦈⦇a⦈)⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈" 
      by (simp add: φ.dghm_ObjMap_app_in_HomCod_Obj)
  qed
qed auto

lemma dghm_up_ObjMap_app_vdomain[dg_cs_simps]: 
  assumes "a ∈∘ ℭ⦇Obj⦈"
  shows "𝒟∘ (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈) = I"
  unfolding dghm_up_ObjMap_app[OF assms] by simp

lemma dghm_up_ObjMap_app_component[dg_cs_simps]: 
  assumes "a ∈∘ ℭ⦇Obj⦈" and "i ∈∘ I"
  shows "dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈⦇i⦈ = φ i⦇ObjMap⦈⦇a⦈"
  using assms unfolding dghm_up_components by simp

lemma dghm_up_ObjMap_app_vrange: 
  assumes "a ∈∘ ℭ⦇Obj⦈" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i"
  shows "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. 𝔄 i⦇Obj⦈)"
proof(intro vsubsetI)
  fix b assume prems: "b ∈∘ ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈)"
  have "vsv (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈)"
    unfolding dghm_up_ObjMap_app[OF assms(1)] by auto
  with prems obtain i where b_def: "b = dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈⦇i⦈" 
    and i: "i ∈∘ I"
    by (auto elim: vsv.vrange_atE simp: dghm_up_ObjMap_app[OF assms(1)])
  interpret φi: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF i])
  from dghm_up_ObjMap_app_component[OF assms(1) i] b_def have b_def':
    "b = φ i⦇ObjMap⦈⦇a⦈"
    by simp
  from assms(1) have "b ∈∘ 𝔄 i⦇Obj⦈" 
    unfolding b_def' by (auto intro: dg_cs_intros)
  with i show "b ∈∘ (⋃∘i∈∘I. 𝔄 i⦇Obj⦈)" by force
qed


subsubsection‹Arrow map›

mk_VLambda dghm_up_components(2)
  |vsv dghm_up_ArrMap_vsv[dg_cs_intros]|
  |vdomain dghm_up_ArrMap_vdomain[dg_cs_simps]|
  |app dghm_up_ArrMap_app|

lemma (in pdigraph) dghm_up_ArrMap_vrange: 
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i"
  shows "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈) ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
  unfolding dghm_up_components dg_prod_components
proof(intro vrange_VLambda_vsubset vproductI)
  fix a assume prems: "a ∈∘ ℭ⦇Arr⦈"
  show "∀i∈∘I. (λi∈∘I. φ i⦇ArrMap⦈⦇a⦈)⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
  proof(intro ballI)
    fix i assume prems': "i ∈∘ I"
    interpret φ: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms[OF prems'])
    from prems prems' show "(λi∈∘I. φ i⦇ArrMap⦈⦇a⦈)⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈" 
      by (auto intro: dg_cs_intros)
  qed
qed auto

lemma dghm_up_ArrMap_vrange: 
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i"
  shows "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈) ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
proof(intro vsubsetI)
  fix A assume "A ∈∘ ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈)"
  then obtain a where A_def: "A = dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈" 
    and a: "a ∈∘ ℭ⦇Arr⦈"
    unfolding dghm_up_ArrMap_vdomain dghm_up_components by auto
  have "(λi∈∘I. φ i⦇ArrMap⦈⦇a⦈) ∈∘ (∏∘i∈∘I. 𝔄 i⦇Arr⦈)"
  proof(intro vproductI)
    show "∀i∈∘I. (λi∈∘I. φ i⦇ArrMap⦈⦇a⦈)⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈"
    proof(intro ballI)
      fix i assume prems: "i ∈∘ I"
      interpret φ: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms[OF prems])
      from prems a show "(λi∈∘I. φ i⦇ArrMap⦈⦇a⦈)⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈" 
        by (auto intro: dg_cs_intros)
    qed
  qed simp_all
  with a show "A ∈∘ (∏DGi∈∘I. 𝔄 i)⦇Arr⦈"
    unfolding A_def dg_prod_components dghm_up_components by simp
qed

lemma dghm_up_ArrMap_app_vdomain[dg_cs_simps]: 
  assumes "a ∈∘ ℭ⦇Arr⦈"
  shows "𝒟∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈) = I"
  unfolding dghm_up_ArrMap_app[OF assms] by simp

lemma dghm_up_ArrMap_app_component[dg_cs_simps]: 
  assumes "a ∈∘ ℭ⦇Arr⦈" and "i ∈∘ I"
  shows "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈⦇i⦈ = φ i⦇ArrMap⦈⦇a⦈"
  using assms unfolding dghm_up_components by simp

lemma dghm_up_ArrMap_app_vrange: 
  assumes "a ∈∘ ℭ⦇Arr⦈" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i"
  shows "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. 𝔄 i⦇Arr⦈)"
proof(intro vsubsetI)
  fix b assume prems: "b ∈∘ ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈)"
  have "vsv (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈)"
    unfolding dghm_up_ArrMap_app[OF assms(1)] by auto
  with prems obtain i where b_def: "b = dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈⦇i⦈" 
    and i: "i ∈∘ I"
    by (auto elim: vsv.vrange_atE simp: dghm_up_ArrMap_app[OF assms(1)])
  interpret φi: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF i])
  from dghm_up_ArrMap_app_component[OF assms(1) i] b_def have b_def':
    "b = φ i⦇ArrMap⦈⦇a⦈"
    by simp
  from assms(1) have "b ∈∘ 𝔄 i⦇Arr⦈" 
    unfolding b_def' by (auto intro: dg_cs_intros)
  with i show "b ∈∘ (⋃∘i∈∘I. 𝔄 i⦇Arr⦈)" by force
qed


subsubsection‹
Digraph product universal property 
digraph homomorphism is a digraph homomorphism
›

lemma (in pdigraph) pdg_dghm_up_is_dghm:
  assumes "digraph α ℭ" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i"
  shows "dghm_up I 𝔄 ℭ φ : ℭ ↦↦DG⇘α⇙ (∏DGi∈∘I. 𝔄 i)"
proof-
  interpret ℭ: digraph α ℭ by (rule assms(1))
  show ?thesis
  proof(intro is_dghmI, unfold dghm_up_components(3,4))
    show "vfsequence (dghm_up I 𝔄 ℭ φ)" unfolding dghm_up_def by simp
    show "vcard (dghm_up I 𝔄 ℭ φ) = 4ℕ"
      unfolding dghm_up_def by (simp add: nat_omega_simps)
    from assms(2) show "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈) ⊆∘ (∏DGi∈∘I. 𝔄 i)⦇Obj⦈"
      by (intro dghm_up_ObjMap_vrange) blast
    fix f a b assume prems: "f : a ↦⇘ℭ⇙ b"
    then have f: "f ∈∘ ℭ⦇Arr⦈" and a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" by auto
    show "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇f⦈ :
      dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈ ↦⇘∏DGi∈∘I. 𝔄 i⇙ dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇b⦈"
    proof(rule dg_prod_is_arrI)
      fix i assume prems': "i ∈∘ I"
      interpret φ: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF prems'])
      from φ.is_dghm_axioms ℭ.digraph_axioms prems pdigraph_axioms prems prems' 
      show "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇f⦈⦇i⦈ : 
        dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈⦇i⦈ ↦⇘𝔄 i⇙ dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇b⦈⦇i⦈"
        by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
    qed (simp_all add: f a b dghm_up_ArrMap_app dghm_up_ObjMap_app)
  qed (auto simp: dghm_up_components pdg_digraph_dg_prod dg_cs_intros)
qed


subsubsection‹Further properties›

lemma (in pdigraph) pdg_dghm_comp_dghm_proj_dghm_up: 
  assumes "digraph α ℭ"
    and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i" 
    and "i ∈∘ I" 
  shows "φ i = πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ"
proof(rule dghm_eqI[of α ℭ ‹𝔄 i› _ ℭ ‹𝔄 i›])
  
  interpret φ: is_dghm α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF assms(3)])
  
  show "φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i" by (auto intro: dg_cs_intros)

  from assms(1,2) have dghm_up: "dghm_up I 𝔄 ℭ φ : ℭ ↦↦DG⇘α⇙ (∏DGi∈∘I. 𝔄 i)"
    by (simp add: pdg_dghm_up_is_dghm)
  note dghm_proj = pdg_dghm_proj_is_dghm[OF assms(3)]

  from assms(3) pdg_dghm_proj_is_dghm show
    "πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ : ℭ ↦↦DG⇘α⇙ 𝔄 i"
    by (intro dghm_comp_is_dghm[of α ‹(∏DGi∈∘I. 𝔄 i)›]) 
      (auto simp: assms dghm_up)
  
  show "φ i⦇ObjMap⦈ = (πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ObjMap⦈"
  proof(rule vsv_eqI)
    show "vsv ((πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ObjMap⦈)"
      unfolding dghm_comp_components dghm_proj_components dghm_up_components 
      by (rule vsv_vcomp) simp_all
    from 
      dghm_up_ObjMap_vrange[
        OF assms(2), simplified, unfolded dg_prod_components
        ]
    have rd: "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ObjMap⦈) ⊆∘ 𝒟∘ (πDG I 𝔄 i⦇ObjMap⦈)"
      by (simp add: dg_prod_components dg_cs_simps)
    show "𝒟∘ (φ i⦇ObjMap⦈) = 𝒟∘ ((πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ObjMap⦈)"
      unfolding dghm_comp_components vdomain_vcomp_vsubset[OF rd] 
      by (simp add: dg_cs_simps)
    fix a assume "a ∈∘ 𝒟∘ (φ i⦇ObjMap⦈)"
    then have a: "a ∈∘ ℭ⦇Obj⦈" by (simp add: dg_cs_simps) 
    with dghm_up dghm_proj assms(3) show 
      "φ i⦇ObjMap⦈⦇a⦈ = (πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ObjMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed auto

  show "φ i⦇ArrMap⦈ = (πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ArrMap⦈"
  proof(rule vsv_eqI)
    show "vsv ((πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ArrMap⦈)"
      unfolding dghm_comp_components dghm_proj_components dghm_up_components 
      by (rule vsv_vcomp) simp_all
    from 
      dghm_up_ArrMap_vrange[
        OF assms(2), simplified, unfolded dg_prod_components
        ]
    have rd: "ℛ∘ (dghm_up I 𝔄 ℭ φ⦇ArrMap⦈) ⊆∘ 𝒟∘ (πDG I 𝔄 i⦇ArrMap⦈)"
      by (simp add: dg_prod_components dg_cs_simps)
    show "𝒟∘ (φ i⦇ArrMap⦈) = 𝒟∘ ((πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ArrMap⦈)"
      unfolding dghm_comp_components vdomain_vcomp_vsubset[OF rd] 
      by (simp add: dg_cs_simps)
    fix a assume "a ∈∘ 𝒟∘ (φ i⦇ArrMap⦈)"
    then have a: "a ∈∘ ℭ⦇Arr⦈" by (simp add: dg_cs_simps)
    with dghm_up dghm_proj assms(3) show 
      "φ i⦇ArrMap⦈⦇a⦈ = (πDG I 𝔄 i ∘DGHM dghm_up I 𝔄 ℭ φ)⦇ArrMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed auto

qed simp_all
      
lemma (in pdigraph) pdg_dghm_up_eq_dghm_proj:
  assumes "𝔉 : ℭ ↦↦DG⇘α⇙ (∏DGi∈∘I. 𝔄 i)"
    and "⋀i. i ∈∘ I ⟹ φ i = πDG I 𝔄 i ∘DGHM 𝔉"
  shows "dghm_up I 𝔄 ℭ φ = 𝔉"
proof(rule dghm_eqI)

  interpret 𝔉: is_dghm α ℭ ‹(∏DGi∈∘I. 𝔄 i)› 𝔉 by (rule assms(1))

  show "dghm_up I 𝔄 ℭ φ : ℭ ↦↦DG⇘α⇙ (∏DGi∈∘I. 𝔄 i)"
  proof(rule pdg_dghm_up_is_dghm)
    fix i assume prems: "i ∈∘ I"
    interpret π: is_dghm α ‹(∏DGi∈∘I. 𝔄 i)› ‹𝔄 i› ‹πDG I 𝔄 i›
      using prems by (rule pdg_dghm_proj_is_dghm)
    show "φ i : ℭ ↦↦DG⇘α⇙ 𝔄 i" 
      unfolding assms(2)[OF prems] by (auto intro: dg_cs_intros)
  qed (auto intro: dg_cs_intros)

  show "dghm_up I 𝔄 ℭ φ⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
  proof(rule vsv_eqI, unfold dghm_up_ObjMap_vdomain)
    fix a assume prems: "a ∈∘ ℭ⦇Obj⦈"
    show "dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
    proof(rule vsv_eqI, unfold dghm_up_ObjMap_app_vdomain[OF prems])
      fix i assume prems': "i ∈∘ I"
      with pdg_dghm_proj_is_dghm[OF prems'] 𝔉.is_dghm_axioms prems show 
        "dghm_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈⦇i⦈ = 𝔉⦇ObjMap⦈⦇a⦈⦇i⦈"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: dg_cs_simps assms(2) cs_intro: dg_cs_intros
          )
    qed 
      (
        use 𝔉.dghm_ObjMap_app_in_HomCod_Obj prems in 
          ‹auto simp: dg_prod_components dghm_up_ObjMap_app›
      )
  qed (auto simp: dghm_up_components dg_cs_simps)

  show "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold dghm_up_ArrMap_vdomain)
    fix a assume prems: "a ∈∘ ℭ⦇Arr⦈"
    show "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈ = 𝔉⦇ArrMap⦈⦇a⦈"
    proof(rule vsv_eqI, unfold dghm_up_ArrMap_app_vdomain[OF prems])
      fix i assume prems': "i ∈∘ I"
      with pdg_dghm_proj_is_dghm[OF prems'] 𝔉.is_dghm_axioms prems show 
        "dghm_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈⦇i⦈ = 𝔉⦇ArrMap⦈⦇a⦈⦇i⦈"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: dg_cs_simps assms(2) cs_intro: dg_cs_intros
          )
    qed 
      (
        use 𝔉.dghm_ArrMap_app_in_HomCod_Arr prems in 
          ‹auto simp: dg_prod_components dghm_up_ArrMap_app›
      )+
  qed (auto simp: dghm_up_components dg_cs_simps)

qed (simp_all add: assms(1))



subsection‹Singleton digraph›


subsubsection‹Object›

lemma dg_singleton_ObjI: 
  assumes "A = set {⟨j, a⟩}" and "a ∈∘ ℭ⦇Obj⦈"
  shows "A ∈∘ (∏DGi∈∘set {j}. ℭ)⦇Obj⦈"
  using assms unfolding dg_prod_components by auto

lemma dg_singleton_ObjE: 
  assumes "A ∈∘ (∏DGi∈∘set {j}. ℭ)⦇Obj⦈"
  obtains a where "A = set {⟨j, a⟩}" and "a ∈∘ ℭ⦇Obj⦈"
proof-
  from vproductD[OF assms[unfolded dg_prod_components], rule_format] 
  have "vsv A" and [simp]: "𝒟∘ A = set {j}" and Aj: "A⦇j⦈ ∈∘ ℭ⦇Obj⦈"
    by simp_all
  then interpret A: vsv A by simp
  from A.vsv_is_VLambda have "A = set {⟨j, A⦇j⦈⟩}" 
    by (auto simp: VLambda_vsingleton)
  with Aj show ?thesis using that by simp
qed


subsubsection‹Arrow›

lemma dg_singleton_ArrI: 
  assumes "F = set {⟨j, a⟩}" and "a ∈∘ ℭ⦇Arr⦈"
  shows "F ∈∘ (∏DGj∈∘set {j}. ℭ)⦇Arr⦈"
  using assms unfolding dg_prod_components by auto

lemma dg_singleton_ArrE: 
  assumes "F ∈∘ (∏DGj∈∘set {j}. ℭ)⦇Arr⦈"
  obtains a where "F = set {⟨j, a⟩}" and "a ∈∘ ℭ⦇Arr⦈"
proof-
  from vproductD[OF assms[unfolded dg_prod_components], rule_format] 
  have "vsv F" and [simp]: "𝒟∘ F = set {j}" and Fj: "F⦇j⦈ ∈∘ ℭ⦇Arr⦈"
    by simp_all
  then interpret F: vsv F by simp
  from F.vsv_is_VLambda have "F = set {⟨j, F⦇j⦈⟩}" 
    by (auto simp: VLambda_vsingleton)
  with Fj show ?thesis using that by simp
qed


subsubsection‹Singleton digraph is a digraph›

lemma (in digraph) dg_finite_pdigraph_dg_singleton: 
  assumes "j ∈∘ Vset α"
  shows "finite_pdigraph α (set {j}) (λi. ℭ)"
  by (intro finite_pdigraphI pdigraph_baseI)
    (auto simp: digraph_axioms Limit_vsingleton_in_VsetI assms)

lemma (in digraph) dg_digraph_dg_singleton:
  assumes "j ∈∘ Vset α"
  shows "digraph α (∏DGj∈∘set {j}. ℭ)"
proof-
  interpret finite_pdigraph α ‹set {j}› ‹λi. ℭ›
    using assms by (rule dg_finite_pdigraph_dg_singleton)
  show ?thesis by (rule pdg_digraph_dg_prod)
qed


subsubsection‹Arrow with a domain and a codomain›

lemma (in digraph) dg_singleton_is_arrI:
  assumes "j ∈∘ Vset α" and "f : a ↦⇘ℭ⇙ b"
  shows "set {⟨j, f⟩} : set {⟨j, a⟩} ↦⇘(∏DGj∈∘set {j}. ℭ)⇙ set {⟨j, b⟩}"
proof-
  interpret finite_pdigraph α ‹set {j}› ‹λi. ℭ›
    by (rule dg_finite_pdigraph_dg_singleton[OF assms(1)])
  from assms(2) show ?thesis by (intro dg_prod_is_arrI) auto
qed

lemma (in digraph) dg_singleton_is_arrD:
  assumes "set {⟨j, f⟩} : set {⟨j, a⟩} ↦⇘(∏DGj∈∘set {j}. ℭ)⇙ set {⟨j, b⟩}" 
    and "j ∈∘ Vset α"
  shows "f : a ↦⇘ℭ⇙ b"
proof-
  interpret finite_pdigraph α ‹set {j}› ‹λi. ℭ›
    by (rule dg_finite_pdigraph_dg_singleton[OF assms(2)])
  from dg_prod_is_arrD(7)[OF assms(1)] show ?thesis by simp
qed

lemma (in digraph) dg_singleton_is_arrE:
  assumes "set {⟨j, f⟩} : set {⟨j, a⟩} ↦⇘(∏DGj∈∘set {j}. ℭ)⇙ set {⟨j, b⟩}" 
    and "j ∈∘ Vset α"
  obtains "f : a ↦⇘ℭ⇙ b"
  using assms dg_singleton_is_arrD by auto



subsection‹Singleton digraph homomorphism›

definition dghm_singleton :: "V ⇒ V ⇒ V"
  where "dghm_singleton j ℭ = 
    [
      (λa∈∘ℭ⦇Obj⦈. set {⟨j, a⟩}), 
      (λf∈∘ℭ⦇Arr⦈. set {⟨j, f⟩}), 
      ℭ,
      (∏DGj∈∘set {j}. ℭ)
    ]∘"


text‹Components.›

lemma dghm_singleton_components:
  shows "dghm_singleton j ℭ⦇ObjMap⦈ = (λa∈∘ℭ⦇Obj⦈. set {⟨j, a⟩})"
    and "dghm_singleton j ℭ⦇ArrMap⦈ = (λf∈∘ℭ⦇Arr⦈. set {⟨j, f⟩})"
    and "dghm_singleton j ℭ⦇HomDom⦈ = ℭ"
    and "dghm_singleton j ℭ⦇HomCod⦈ = (∏DGj∈∘set {j}. ℭ)"
  unfolding dghm_singleton_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda dghm_singleton_components(1)
  |vsv dghm_singleton_ObjMap_vsv[dg_cs_intros]|
  |vdomain dghm_singleton_ObjMap_vdomain[dg_cs_simps]|
  |app dghm_singleton_ObjMap_app[dg_prod_cs_simps]|

lemma dghm_singleton_ObjMap_vrange[dg_cs_simps]: 
  "ℛ∘ (dghm_singleton j ℭ⦇ObjMap⦈) = (∏DGj∈∘set {j}. ℭ)⦇Obj⦈"
proof(intro vsubset_antisym vsubsetI)
  fix A assume "A ∈∘ ℛ∘ (dghm_singleton j ℭ⦇ObjMap⦈)"
  then obtain a where A_def: "A = set {⟨j, a⟩}" and a: "a ∈∘ ℭ⦇Obj⦈" 
    unfolding dghm_singleton_components by auto
  then show "A ∈∘ (∏DGj∈∘set {j}. ℭ)⦇Obj⦈"
    unfolding dg_prod_components by auto
next
  fix A assume "A ∈∘ (∏DGj∈∘set {j}. ℭ)⦇Obj⦈" 
  from vproductD[OF this[unfolded dg_prod_components], rule_format] 
  have "vsv A"
    and [simp]: "𝒟∘ A = set {j}" 
    and Ai: "⋀i. i ∈∘ set {j} ⟹ A⦇i⦈ ∈∘ ℭ⦇Obj⦈"
    by auto
  then interpret A: vsv A by simp
  from Ai have "A⦇j⦈ ∈∘ ℭ⦇Obj⦈" using Ai by auto
  moreover with A.vsv_is_VLambda have "A = (λf∈∘ℭ⦇Obj⦈. set {⟨j, f⟩})⦇A⦇j⦈⦈"
    by (simp add: VLambda_vsingleton)
  ultimately show "A ∈∘ ℛ∘ (dghm_singleton j ℭ⦇ObjMap⦈)"
    unfolding dghm_singleton_components
    by 
      (
        metis 
          dghm_singleton_ObjMap_vdomain 
          dghm_singleton_ObjMap_vsv 
          dghm_singleton_components(1) 
          vsv.vsv_vimageI2
      )
qed


subsubsection‹Arrow map›

mk_VLambda dghm_singleton_components(2)
  |vsv dghm_singleton_ArrMap_vsv[dg_cs_intros]|
  |vdomain dghm_singleton_ArrMap_vdomain[dg_cs_simps]|
  |app dghm_singleton_ArrMap_app[dg_prod_cs_simps]|

lemma dghm_singleton_ArrMap_vrange[dg_cs_simps]: 
  "ℛ∘ (dghm_singleton j ℭ⦇ArrMap⦈) = (∏DGj∈∘set {j}. ℭ)⦇Arr⦈"
proof(intro vsubset_antisym vsubsetI)
  fix F assume "F ∈∘ ℛ∘ (dghm_singleton j ℭ⦇ArrMap⦈)"
  then obtain f where "F = set {⟨j, f⟩}" and "f ∈∘ ℭ⦇Arr⦈" 
    unfolding dghm_singleton_components by auto
  then show "F ∈∘ (∏DGj∈∘set {j}. ℭ)⦇Arr⦈"
    unfolding dg_prod_components by auto
next
  fix F assume "F ∈∘ (∏DGj∈∘set {j}. ℭ)⦇Arr⦈" 
  from vproductD[OF this[unfolded dg_prod_components], rule_format] 
  have "vsv F"
    and [simp]: "𝒟∘ F = set {j}" 
    and Fi: "⋀i. i ∈∘ set {j} ⟹ F⦇i⦈ ∈∘ ℭ⦇Arr⦈"
    by auto
  then interpret F: vsv F by simp
  from Fi have "F⦇j⦈ ∈∘ ℭ⦇Arr⦈" using Fi by auto
  moreover with F.vsv_is_VLambda have "F = (λf∈∘ℭ⦇Arr⦈. set {⟨j, f⟩})⦇F⦇j⦈⦈"
    by (simp add: VLambda_vsingleton)
  ultimately show "F ∈∘ ℛ∘ (dghm_singleton j ℭ⦇ArrMap⦈)"
    unfolding dghm_singleton_components
    by 
      (
        metis 
          dghm_singleton_ArrMap_vdomain 
          dghm_singleton_ArrMap_vsv 
          dghm_singleton_components(2) 
          vsv.vsv_vimageI2
      )
qed


subsubsection‹Singleton digraph homomorphism is an isomorphism of digraphs›

lemma (in digraph) dg_dghm_singleton_is_dghm:
  assumes "j ∈∘ Vset α"
  shows "dghm_singleton j ℭ : ℭ ↦↦DG.iso⇘α⇙ (∏DGj∈∘set {j}. ℭ)"
proof-
  interpret finite_pdigraph α ‹set {j}› ‹λi. ℭ›
    by (rule dg_finite_pdigraph_dg_singleton[OF assms])
  show ?thesis
  proof(intro is_iso_dghmI is_dghmI)
    show "vfsequence (dghm_singleton j ℭ)" unfolding dghm_singleton_def by simp
    show "vcard (dghm_singleton j ℭ) = 4ℕ"
      unfolding dghm_singleton_def by (simp add: nat_omega_simps)
    show "ℛ∘ (dghm_singleton j ℭ⦇ObjMap⦈) ⊆∘ (∏DGj∈∘set {j}. ℭ)⦇Obj⦈"
      by (simp add: dg_cs_simps)
    show "dghm_singleton j ℭ⦇ArrMap⦈⦇f⦈ :
      dghm_singleton j ℭ⦇ObjMap⦈⦇a⦈ ↦⇘∏DGj∈∘set {j}. ℭ⇙ 
      dghm_singleton j ℭ⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘ℭ⇙ b" for f a b
      using that
    proof(intro dg_prod_is_arrI)
      fix k assume "k ∈∘ set {j}"
      then have k_def: "k = j" by simp
      from that show "dghm_singleton j ℭ⦇ArrMap⦈⦇f⦈⦇k⦈ :
        dghm_singleton j ℭ⦇ObjMap⦈⦇a⦈⦇k⦈ ↦⇘ℭ⇙ dghm_singleton j ℭ⦇ObjMap⦈⦇b⦈⦇k⦈"
        by 
          (
            cs_concl 
              cs_simp: k_def V_cs_simps dg_cs_simps dg_prod_cs_simps
              cs_intro: dg_cs_intros
          )
    qed 
      (
        cs_concl  
          cs_simp: V_cs_simps dg_prod_cs_simps 
          cs_intro: V_cs_intros dg_cs_intros
      )+
    show "ℛ∘ (dghm_singleton j ℭ⦇ObjMap⦈) = (∏DGj∈∘set {j}. ℭ)⦇Obj⦈" 
      by (simp add: dg_cs_simps)
    show "ℛ∘ (dghm_singleton j ℭ⦇ArrMap⦈) = (∏DGj∈∘set {j}. ℭ)⦇Arr⦈" 
      by (simp add: dg_cs_simps)
  qed 
    (
      auto simp: 
        dg_cs_intros 
        dg_digraph_dg_singleton[OF assms] 
        dghm_singleton_components
    )
qed



subsection‹Product of two digraphs›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-3 in cite‹"mac_lane_categories_2010"›.›

definition dg_prod_2 :: "V ⇒ V ⇒ V" (infixr ‹×DG› 80)
  where "𝔄 ×DG 𝔅