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 𝔅 ≡ dg_prod (2ℕ) (if2 𝔄 𝔅)"


subsubsection‹Product of two digraphs is a digraph›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

interpretation 𝒵 α by (rule digraphD[OF 𝔄(1)])
interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)

lemma finite_pdigraph_dg_prod_2: "finite_pdigraph α (2ℕ) (if2 𝔄 𝔅)"
proof(intro finite_pdigraphI pdigraph_baseI)
  from Axiom_of_Infinity show z1_in_Vset: "2ℕ ∈∘ Vset α" by blast
  show "digraph α (i = 0 ? 𝔄 : 𝔅)" if "i ∈∘ 2ℕ" for i
    by (auto intro: dg_cs_intros)
qed auto

interpretation finite_pdigraph α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_pdigraph_dg_prod_2 𝔄 𝔅)

lemma digraph_dg_prod_2[dg_cs_intros]: "digraph α (𝔄 ×DG 𝔅)"
proof-
  show ?thesis unfolding dg_prod_2_def by (rule pdg_digraph_dg_prod)
qed

end


subsubsection‹Object›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma dg_prod_2_ObjI:
  assumes "a ∈∘ 𝔄⦇Obj⦈" and "b ∈∘ 𝔅⦇Obj⦈"
  shows "[a, b]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
  unfolding dg_prod_2_def dg_prod_components
proof(intro vproductI ballI)
  show "𝒟∘ [a, b]∘ = 2ℕ" by (simp add: nat_omega_simps two)
  fix i assume "i ∈∘ 2ℕ"
  then consider ‹i = 0› | ‹i = 1ℕ› unfolding two by auto 
  then show "[a, b]∘⦇i⦈ ∈∘ (if i = 0 then 𝔄 else 𝔅)⦇Obj⦈"
    by cases (simp_all add: nat_omega_simps assms(1,2))
qed auto

lemma dg_prod_2_ObjI'[dg_prod_cs_intros]:
  assumes "ab = [a, b]∘" and "a ∈∘ 𝔄⦇Obj⦈" and "b ∈∘ 𝔅⦇Obj⦈"
  shows "ab ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
  using assms(2,3) unfolding assms(1) by (rule dg_prod_2_ObjI)

lemma dg_prod_2_ObjE:
  assumes "ab ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
  obtains a b where "ab = [a, b]∘" and "a ∈∘ 𝔄⦇Obj⦈" and "b ∈∘ 𝔅⦇Obj⦈"
proof-
  from vproductD[OF assms[unfolded dg_prod_2_def dg_prod_components]]
  have vsv_ab: "vsv ab"
    and dom_ab: "𝒟∘ ab = 2ℕ"
    and ab_app: "⋀i. i ∈∘ 2ℕ ⟹ ab⦇i⦈ ∈∘ (if i = 0 then 𝔄 else 𝔅)⦇Obj⦈"
    by auto
  have dom_ab[simp]: "𝒟∘ ab = 2ℕ"
    unfolding dom_ab by (simp add: nat_omega_simps two)
  interpret vsv ab by (rule vsv_ab)
  have "ab = [vpfst ab, vpsnd ab]∘"
    by (rule vsv_vfsequence_two[symmetric]) auto
  moreover from ab_app[of 0] have "vpfst ab ∈∘ 𝔄⦇Obj⦈" by simp
  moreover from ab_app[of ‹1ℕ›] have "vpsnd ab ∈∘ 𝔅⦇Obj⦈" by simp
  ultimately show ?thesis using that by auto
qed

end


subsubsection‹Arrow›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma dg_prod_2_ArrI:
  assumes "g ∈∘ 𝔄⦇Arr⦈" and "f ∈∘ 𝔅⦇Arr⦈"
  shows "[g, f]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  unfolding dg_prod_2_def dg_prod_components
proof(intro vproductI ballI)
  show "𝒟∘ [g, f]∘ = 2ℕ" by (simp add: nat_omega_simps two)
  fix i assume "i ∈∘ 2ℕ"
  then consider ‹i = 0› | ‹i = 1ℕ› unfolding two by auto 
  then show "[g, f]∘⦇i⦈ ∈∘ (if i = 0 then 𝔄 else 𝔅)⦇Arr⦈"
    by cases (simp_all add: nat_omega_simps assms(1,2))
qed auto

lemma dg_prod_2_ArrI'[dg_prod_cs_intros]:
  assumes "gf = [g, f]∘" and "g ∈∘ 𝔄⦇Arr⦈" and "f ∈∘ 𝔅⦇Arr⦈"
  shows "[g, f]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  using assms(2,3) unfolding assms(1) by (rule dg_prod_2_ArrI)

lemma dg_prod_2_ArrE:
  assumes "gf ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  obtains g f where "gf = [g, f]∘" and "g ∈∘ 𝔄⦇Arr⦈" and "f ∈∘ 𝔅⦇Arr⦈"
proof-
  from vproductD[OF assms[unfolded dg_prod_2_def dg_prod_components]]
  have vsv_gf: "vsv gf"
    and dom_gf: "𝒟∘ gf = 2ℕ"
    and gf_app: "⋀i. i ∈∘ 2ℕ ⟹ gf⦇i⦈ ∈∘ (if i = 0 then 𝔄 else 𝔅)⦇Arr⦈"
    by auto
  have dom_gf[simp]: "𝒟∘ gf = 2ℕ" unfolding dom_gf by (simp add: two)
  interpret vsv gf by (rule vsv_gf)
  have "gf = [vpfst gf, vpsnd gf]∘"
    by (rule vsv_vfsequence_two[symmetric]) auto
  moreover from gf_app[of 0] have "vpfst gf ∈∘ 𝔄⦇Arr⦈" by simp
  moreover from gf_app[of ‹1ℕ›] have "vpsnd gf ∈∘ 𝔅⦇Arr⦈" by simp
  ultimately show ?thesis using that by auto
qed

end


subsubsection‹Arrow with a domain and a codomain›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

interpretation 𝒵 α by (rule digraphD[OF 𝔄(1)])
interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)
interpretation finite_pdigraph α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_pdigraph_dg_prod_2 𝔄 𝔅)

lemma dg_prod_2_is_arrI:
  assumes "g : a ↦⇘𝔄⇙ c" and "f : b ↦⇘𝔅⇙ d"
  shows "[g, f]∘ : [a, b]∘ ↦⇘𝔄 ×DG 𝔅⇙ [c, d]∘"
  unfolding dg_prod_2_def
proof(rule dg_prod_is_arrI)
  show "[g, f]∘⦇i⦈ : [a, b]∘⦇i⦈ ↦⇘if i = 0 then 𝔄 else 𝔅⇙ [c, d]∘⦇i⦈"
    if "i ∈∘ 2ℕ" for i
  proof-
    from that consider ‹i = 0› | ‹i = 1ℕ› unfolding two by auto 
    then show "[g, f]∘⦇i⦈ : [a, b]∘⦇i⦈ ↦⇘if i = 0 then 𝔄 else 𝔅⇙ [c, d]∘⦇i⦈"
      by cases (simp_all add: nat_omega_simps assms)
  qed
qed (auto simp: nat_omega_simps two)

lemma dg_prod_2_is_arrI'[dg_prod_cs_intros]:
  assumes "gf = [g, f]∘"
    and "ab = [a, b]∘"
    and "cd = [c, d]∘"
    and "g : a ↦⇘𝔄⇙ c" 
    and "f : b ↦⇘𝔅⇙ d"
  shows "gf : ab ↦⇘𝔄 ×DG 𝔅⇙ cd"
  using assms(4,5) unfolding assms(1,2,3) by (rule dg_prod_2_is_arrI)

lemma dg_prod_2_is_arrE:
  assumes "gf : ab ↦⇘𝔄 ×DG 𝔅⇙ cd"
  obtains g f a b c d 
    where "gf = [g, f]∘"
      and "ab = [a, b]∘"
      and "cd = [c, d]∘"
      and "g : a ↦⇘𝔄⇙ c"
      and "f : b ↦⇘𝔅⇙ d"
proof-
  from dg_prod_is_arrD[OF assms[unfolded dg_prod_2_def]] 
  have [simp]: "vsv gf" "𝒟∘ gf = 2ℕ" "vsv ab" "𝒟∘ ab = 2ℕ" "vsv cd" "𝒟∘ cd = 2ℕ"
    and gf_app: 
      "⋀i. i ∈∘ 2ℕ ⟹ gf⦇i⦈ : ab⦇i⦈ ↦⇘if i = 0 then 𝔄 else 𝔅⇙ cd⦇i⦈"
    by (auto simp: two)
  have "gf = [vpfst gf, vpsnd gf]∘" by (simp add: vsv_vfsequence_two)
  moreover have "ab = [vpfst ab, vpsnd ab]∘" by (simp add: vsv_vfsequence_two)
  moreover have "cd = [vpfst cd, vpsnd cd]∘" by (simp add: vsv_vfsequence_two)
  moreover from gf_app[of 0] have "vpfst gf : vpfst ab ↦⇘𝔄⇙ vpfst cd" by simp
  moreover from gf_app[of ‹1ℕ›] have "vpsnd gf : vpsnd ab ↦⇘𝔅⇙ vpsnd cd" 
    by (simp add: nat_omega_simps)
  ultimately show ?thesis using that by auto
qed

end


subsubsection‹Domain›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma dg_prod_2_Dom_vsv: "vsv ((𝔄 ×DG 𝔅)⦇Dom⦈)"
  unfolding dg_prod_2_def dg_prod_components by simp

lemma dg_prod_2_Dom_vdomain[dg_cs_simps]: 
  "𝒟∘ ((𝔄 ×DG 𝔅)⦇Dom⦈) = (𝔄 ×DG 𝔅)⦇Arr⦈"
  unfolding dg_prod_2_def dg_prod_components by simp

lemma dg_prod_2_Dom_app[dg_prod_cs_simps]:
  assumes "[g, f]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  shows "(𝔄 ×DG 𝔅)⦇Dom⦈⦇g, f⦈∙ = [𝔄⦇Dom⦈⦇g⦈, 𝔅⦇Dom⦈⦇f⦈]∘"
proof-
  from assms obtain ab cd where gf: "[g, f]∘ : ab ↦⇘𝔄 ×DG 𝔅⇙ cd" 
    by (auto intro: is_arrI)
  then have Dom_gf: "(𝔄 ×DG 𝔅)⦇Dom⦈⦇g, f⦈∙ = ab" 
    by (simp add: dg_cs_simps)
  from gf obtain a b c d 
    where ab_def: "ab = [a, b]∘" 
      and "cd = [c, d]∘" 
      and "g : a ↦⇘𝔄⇙ c"
      and "f : b ↦⇘𝔅⇙ d"
    by (elim dg_prod_2_is_arrE[OF 𝔄 𝔅]) simp
  then have Dom_g: "𝔄⦇Dom⦈⦇g⦈ = a" and Dom_f: "𝔅⦇Dom⦈⦇f⦈ = b" 
    by (simp_all add: dg_cs_simps)
  show ?thesis unfolding Dom_gf ab_def Dom_g Dom_f ..
qed

lemma dg_prod_2_Dom_vrange: "ℛ∘ ((𝔄 ×DG 𝔅)⦇Dom⦈) ⊆∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
  show "vsv ((𝔄 ×DG 𝔅)⦇Dom⦈)" by (rule dg_prod_2_Dom_vsv)
  fix gf assume prems: "gf ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  then obtain g f where gf_def: "gf = [g, f]∘" 
    and g: "g ∈∘ 𝔄⦇Arr⦈" 
    and f: "f ∈∘ 𝔅⦇Arr⦈"
    by (elim dg_prod_2_ArrE[OF 𝔄 𝔅]) simp
  from g f obtain a b c d where g: "g : a ↦⇘𝔄⇙ c" and f: "f : b ↦⇘𝔅⇙ d"
    by (auto intro!: is_arrI)
  from 𝔄 𝔅 g f show "(𝔄 ×DG 𝔅)⦇Dom⦈⦇gf⦈ ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
    unfolding gf_def dg_prod_2_Dom_app[OF prems[unfolded gf_def]]
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros)
qed

end


subsubsection‹Codomain›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma dg_prod_2_Cod_vsv: "vsv ((𝔄 ×DG 𝔅)⦇Cod⦈)"
  unfolding dg_prod_2_def dg_prod_components by simp

lemma dg_prod_2_Cod_vdomain[dg_cs_simps]: 
  "𝒟∘ ((𝔄 ×DG 𝔅)⦇Cod⦈) = (𝔄 ×DG 𝔅)⦇Arr⦈"
  unfolding dg_prod_2_def dg_prod_components by simp

lemma dg_prod_2_Cod_app[dg_prod_cs_simps]:
  assumes "[g, f]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  shows "(𝔄 ×DG 𝔅)⦇Cod⦈⦇g, f⦈∙ = [𝔄⦇Cod⦈⦇g⦈, 𝔅⦇Cod⦈⦇f⦈]∘"
proof-
  from assms obtain ab cd where gf: "[g, f]∘ : ab ↦⇘𝔄 ×DG 𝔅⇙ cd" 
    by (auto intro: is_arrI)
  then have Cod_gf: "(𝔄 ×DG 𝔅)⦇Cod⦈⦇g, f⦈∙ = cd"
    by (simp add: dg_cs_simps)
  from gf obtain a b c d 
    where "ab = [a, b]∘" 
      and cd_def: "cd = [c, d]∘" 
      and "g : a ↦⇘𝔄⇙ c"
      and "f : b ↦⇘𝔅⇙ d"
    by (elim dg_prod_2_is_arrE[OF 𝔄 𝔅]) simp
  then have Cod_g: "𝔄⦇Cod⦈⦇g⦈ = c" and Cod_f: "𝔅⦇Cod⦈⦇f⦈ = d"
    by (simp_all add: dg_cs_simps)
  show ?thesis unfolding Cod_gf cd_def Cod_g Cod_f ..
qed

lemma dg_prod_2_Cod_vrange: "ℛ∘ ((𝔄 ×DG 𝔅)⦇Cod⦈) ⊆∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
  show "vsv ((𝔄 ×DG 𝔅)⦇Cod⦈)" by (rule dg_prod_2_Cod_vsv)
  fix gf assume prems: "gf ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  then obtain g f where gf_def: "gf = [g, f]∘" 
    and g: "g ∈∘ 𝔄⦇Arr⦈" 
    and f: "f ∈∘ 𝔅⦇Arr⦈"
    by (elim dg_prod_2_ArrE[OF 𝔄 𝔅]) simp
  from g f obtain a b c d where g: "g : a ↦⇘𝔄⇙ c" and f: "f : b ↦⇘𝔅⇙ d"
    by (auto intro!: is_arrI)
  from 𝔄 𝔅 g f show "(𝔄 ×DG 𝔅)⦇Cod⦈⦇gf⦈ ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
    unfolding gf_def dg_prod_2_Cod_app[OF prems[unfolded gf_def]]
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros
      )
qed

end


subsubsection‹Opposite product digraph›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)

lemma dg_prod_2_op_dg_dg_Obj[dg_op_simps]: 
  "(op_dg 𝔄 ×DG 𝔅)⦇Obj⦈ = (𝔄 ×DG 𝔅)⦇Obj⦈"
proof
  (
    intro vsubset_antisym vsubsetI; 
    elim dg_prod_2_ObjE[OF 𝔄.digraph_op 𝔅] dg_prod_2_ObjE[OF 𝔄 𝔅],
    (unfold dg_op_simps)?
  )
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Obj⦈" "b ∈∘ 𝔅⦇Obj⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
    unfolding prems(1) dg_op_simps
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
next
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Obj⦈" "b ∈∘ 𝔅⦇Obj⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (op_dg 𝔄 ×DG 𝔅)⦇Obj⦈"
    unfolding prems(1) dg_op_simps
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_op_intros dg_prod_cs_intros
      )
qed

lemma dg_prod_2_dg_op_dg_Obj[dg_op_simps]: 
  "(𝔄 ×DG op_dg 𝔅)⦇Obj⦈ = (𝔄 ×DG 𝔅)⦇Obj⦈"
proof
  (
    intro vsubset_antisym vsubsetI; 
    elim dg_prod_2_ObjE[OF 𝔄 𝔅.digraph_op] dg_prod_2_ObjE[OF 𝔄 𝔅],
    (unfold dg_op_simps)?
  )
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Obj⦈" "b ∈∘ 𝔅⦇Obj⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
    unfolding prems(1) dg_op_simps
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
next
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Obj⦈" "b ∈∘ 𝔅⦇Obj⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (𝔄 ×DG op_dg 𝔅)⦇Obj⦈"
    unfolding prems(1) dg_op_simps
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros dg_op_intros
      ) 
qed

lemma dg_prod_2_op_dg_dg_Arr[dg_op_simps]: 
  "(op_dg 𝔄 ×DG 𝔅)⦇Arr⦈ = (𝔄 ×DG 𝔅)⦇Arr⦈"
proof
  (
    intro vsubset_antisym vsubsetI; 
    elim dg_prod_2_ArrE[OF 𝔄.digraph_op 𝔅] dg_prod_2_ArrE[OF 𝔄 𝔅],
    (unfold dg_op_simps)?
  )
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Arr⦈" "b ∈∘ 𝔅⦇Arr⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
    unfolding prems(1) dg_op_simps
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
next
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Arr⦈" "b ∈∘ 𝔅⦇Arr⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (op_dg 𝔄 ×DG 𝔅)⦇Arr⦈"
    unfolding prems(1) dg_op_simps
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros dg_op_intros
      ) 
qed

lemma dg_prod_2_dg_op_dg_Arr[dg_op_simps]: 
  "(𝔄 ×DG op_dg 𝔅)⦇Arr⦈ = (𝔄 ×DG 𝔅)⦇Arr⦈"
proof
  (
    intro vsubset_antisym vsubsetI; 
    elim dg_prod_2_ArrE[OF 𝔄 𝔅.digraph_op] dg_prod_2_ArrE[OF 𝔄 𝔅],
    (unfold dg_op_simps)?
  )
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Arr⦈" "b ∈∘ 𝔅⦇Arr⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
    unfolding prems(1) dg_op_simps
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
next
  fix ab a b assume prems: "ab = [a, b]∘" "a ∈∘ 𝔄⦇Arr⦈" "b ∈∘ 𝔅⦇Arr⦈"
  from 𝔄 𝔅 prems(2,3) show "ab ∈∘ (𝔄 ×DG op_dg 𝔅)⦇Arr⦈"
    unfolding prems(1) dg_op_simps
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros dg_op_intros
      ) 
qed

end

context
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma op_dg_dg_prod_2[dg_op_simps]: "op_dg (𝔄 ×DG 𝔅) = op_dg 𝔄 ×DG op_dg 𝔅"
proof(rule vsv_eqI)

  show "vsv (op_dg (𝔄 ×DG 𝔅))" unfolding op_dg_def by auto
  show "vsv (op_dg 𝔄 ×DG op_dg 𝔅)" unfolding dg_prod_2_def dg_prod_def by auto
  have dom_lhs: "𝒟∘ (op_dg (𝔄 ×DG 𝔅)) = 4ℕ" 
    by (simp add: op_dg_def nat_omega_simps)
  show "𝒟∘ (op_dg (𝔄 ×DG 𝔅)) = 𝒟∘ (op_dg 𝔄 ×DG op_dg 𝔅)"
    unfolding dom_lhs by (simp add: dg_prod_2_def dg_prod_def nat_omega_simps)

  have Cod_Dom: "(𝔄 ×DG 𝔅)⦇Cod⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Dom⦈"
  proof(rule vsv_eqI)
    from 𝔄 𝔅 show "vsv ((𝔄 ×DG 𝔅)⦇Cod⦈)" by (rule dg_prod_2_Cod_vsv)
    from 𝔄 𝔅 show "vsv ((op_dg 𝔄 ×DG op_dg 𝔅)⦇Dom⦈)"
      by (cs_concl cs_shallow cs_intro: dg_prod_2_Dom_vsv dg_op_intros)+
    from 𝔄 𝔅 have dom_lhs: "𝒟∘ ((𝔄 ×DG 𝔅)⦇Cod⦈) = (𝔄 ×DG 𝔅)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps)
    from 𝔄 𝔅 show "𝒟∘ ((𝔄 ×DG 𝔅)⦇Cod⦈) = 𝒟∘ ((op_dg 𝔄 ×DG op_dg 𝔅)⦇Dom⦈)"
      unfolding dom_lhs
      by 
        (
          cs_concl cs_shallow 
            cs_simp: dg_cs_simps dg_op_simps cs_intro: dg_op_intros
        )
    show "(𝔄 ×DG 𝔅)⦇Cod⦈⦇gf⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Dom⦈⦇gf⦈"
      if "gf ∈∘ 𝒟∘ ((𝔄 ×DG 𝔅)⦇Cod⦈)" for gf
      using that unfolding dom_lhs
    proof-
      assume "gf ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
      then obtain g f 
        where gf_def: "gf = [g, f]∘" 
          and g: "g ∈∘ 𝔄⦇Arr⦈" 
          and f: "f ∈∘ 𝔅⦇Arr⦈"
        by (rule dg_prod_2_ArrE[OF 𝔄 𝔅]) simp
      from 𝔄 𝔅 g f show "(𝔄 ×DG 𝔅)⦇Cod⦈⦇gf⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Dom⦈⦇gf⦈"
        unfolding gf_def
        by 
          (
            cs_concl cs_shallow
              cs_simp: dg_prod_cs_simps dg_op_simps 
              cs_intro: dg_prod_cs_intros dg_op_intros
          )
    qed
  qed

  have Dom_Cod: "(𝔄 ×DG 𝔅)⦇Dom⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Cod⦈"
  proof(rule vsv_eqI)
    from 𝔄 𝔅 show "vsv ((op_dg 𝔄 ×DG op_dg 𝔅)⦇Cod⦈)"
      by (cs_concl cs_shallow cs_intro: dg_prod_2_Cod_vsv dg_op_intros)+
    from 𝔄 𝔅 have dom_lhs: "𝒟∘ ((𝔄 ×DG 𝔅)⦇Dom⦈) = (𝔄 ×DG 𝔅)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps)
    from 𝔄 𝔅 show "𝒟∘ ((𝔄 ×DG 𝔅)⦇Dom⦈) = 𝒟∘ ((op_dg 𝔄 ×DG op_dg 𝔅)⦇Cod⦈)"
      unfolding dom_lhs
      by 
        (
          cs_concl cs_shallow 
            cs_simp: dg_cs_simps dg_op_simps cs_intro: dg_op_intros
        )
    show "(𝔄 ×DG 𝔅)⦇Dom⦈⦇gf⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Cod⦈⦇gf⦈"
      if "gf ∈∘ 𝒟∘ ((𝔄 ×DG 𝔅)⦇Dom⦈)" for gf
      using that unfolding dom_lhs
    proof-
      assume "gf ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
      then obtain g f 
        where gf_def: "gf = [g, f]∘" 
          and g: "g ∈∘ 𝔄⦇Arr⦈" 
          and f: "f ∈∘ 𝔅⦇Arr⦈"
        by (rule dg_prod_2_ArrE[OF 𝔄 𝔅]) simp
      from 𝔄 𝔅 g f show "(𝔄 ×DG 𝔅)⦇Dom⦈⦇gf⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Cod⦈⦇gf⦈"
        unfolding gf_def
        by 
          (
            cs_concl cs_shallow 
              cs_simp: dg_cs_simps dg_prod_cs_simps dg_op_simps 
              cs_intro: dg_op_intros dg_prod_cs_intros
          )
    qed
  qed (auto intro: 𝔄 𝔅 dg_prod_2_Dom_vsv)

  show "a ∈∘ 𝒟∘ (op_dg (𝔄 ×DG 𝔅)) ⟹
    op_dg (𝔄 ×DG 𝔅)⦇a⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇a⦈" 
    for a
  proof
    (
      unfold dom_lhs, 
      elim_in_numeral, 
      fold dg_field_simps, 
      unfold op_dg_components
    )
    from 𝔄 𝔅 show "(𝔄 ×DG 𝔅)⦇Obj⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: dg_op_simps cs_intro: dg_op_intros) 
    from 𝔄 𝔅 show "(𝔄 ×DG 𝔅)⦇Arr⦈ = (op_dg 𝔄 ×DG op_dg 𝔅)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: dg_op_simps cs_intro: dg_op_intros) 
  qed (auto simp: 𝔄 𝔅 Cod_Dom Dom_Cod)

qed

end



subsection‹Projections for the product of two digraphs›


subsubsection‹Definition and elementary properties›

definition dghm_proj_fst :: "V ⇒ V ⇒ V" (‹πDG.1›)
  where "πDG.1 𝔄 𝔅 = dghm_proj (2ℕ) (if2 𝔄 𝔅) 0"
definition dghm_proj_snd :: "V ⇒ V ⇒ V" (‹πDG.2›)
  where "πDG.2 𝔄 𝔅 = dghm_proj (2ℕ) (if2 𝔄 𝔅) (1ℕ)"


subsubsection‹Object map for a projection of a product of two digraphs›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma dghm_proj_fst_ObjMap_app[dg_cs_simps]:
  assumes "[a, b]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
  shows "πDG.1 𝔄 𝔅⦇ObjMap⦈⦇a, b⦈∙ = a"
proof-
  from assms have "[a, b]∘ ∈∘ (∏∘i∈∘2ℕ. (if i = 0 then 𝔄 else 𝔅)⦇Obj⦈)"
    unfolding dg_prod_2_def dg_prod_components by simp
  then show "πDG.1 𝔄 𝔅⦇ObjMap⦈⦇a, b⦈∙ = a"
    unfolding dghm_proj_fst_def dghm_proj_components dg_prod_components by simp
qed

lemma dghm_proj_snd_ObjMap_app[dg_cs_simps]:
  assumes "[a, b]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Obj⦈"
  shows "πDG.2 𝔄 𝔅⦇ObjMap⦈⦇a, b⦈∙ = b"
proof-
  from assms have "[a, b]∘ ∈∘ (∏∘i∈∘2ℕ. (if i = 0 then 𝔄 else 𝔅)⦇Obj⦈)"
    unfolding dg_prod_2_def dg_prod_components by simp
  then show "πDG.2 𝔄 𝔅⦇ObjMap⦈⦇a, b⦈∙ = b"
    unfolding dghm_proj_snd_def dghm_proj_components dg_prod_components
    by (simp add: nat_omega_simps)
qed

end


subsubsection‹Arrow map for a projection of a product of two digraphs›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

lemma dghm_proj_fst_ArrMap_app[dg_cs_simps]:
  assumes "[g, f]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  shows "πDG.1 𝔄 𝔅⦇ArrMap⦈⦇g, f⦈∙ = g"
proof-
  from assms have "[g, f]∘ ∈∘ (∏∘i∈∘2ℕ. (if i = 0 then 𝔄 else 𝔅)⦇Arr⦈)"
    unfolding dg_prod_2_def dg_prod_components by simp
  then show "πDG.1 𝔄 𝔅⦇ArrMap⦈⦇g, f⦈∙ = g"
    unfolding dghm_proj_fst_def dghm_proj_components dg_prod_components by simp
qed

lemma dghm_proj_snd_ArrMap_app[dg_cs_simps]:
  assumes "[g, f]∘ ∈∘ (𝔄 ×DG 𝔅)⦇Arr⦈"
  shows "πDG.2 𝔄 𝔅⦇ArrMap⦈⦇g, f⦈∙ = f"
proof-
  from assms have "[g, f]∘ ∈∘ (∏∘i∈∘2ℕ. (if i = 0 then 𝔄 else 𝔅)⦇Arr⦈)"
    unfolding dg_prod_2_def dg_prod_components by simp
  then show "πDG.2 𝔄 𝔅⦇ArrMap⦈⦇g, f⦈∙ = f"
    unfolding dghm_proj_snd_def dghm_proj_components dg_prod_components
    by (simp add: nat_omega_simps)
qed

end


subsubsection‹Domain and codomain of a projection of a product of two digraphs›

lemma dghm_proj_fst_HomDom: "πDG.1 𝔄 𝔅⦇HomDom⦈ = 𝔄 ×DG 𝔅"
  unfolding dghm_proj_fst_def dghm_proj_components dg_prod_2_def ..

lemma dghm_proj_fst_HomCod: "πDG.1 𝔄 𝔅⦇HomCod⦈ = 𝔄"
  unfolding dghm_proj_fst_def dghm_proj_components dg_prod_2_def by simp
  
lemma dghm_proj_snd_HomDom: "πDG.2 𝔄 𝔅⦇HomDom⦈ = 𝔄 ×DG 𝔅"
  unfolding dghm_proj_snd_def dghm_proj_components dg_prod_2_def ..

lemma dghm_proj_snd_HomCod: "πDG.2 𝔄 𝔅⦇HomCod⦈ = 𝔅"
  unfolding dghm_proj_snd_def dghm_proj_components dg_prod_2_def by simp


subsubsection‹Projection of a product of two digraphs is a digraph homomorphism›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅"
begin

interpretation finite_pdigraph α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_pdigraph_dg_prod_2 𝔄 𝔅)

lemma dghm_proj_fst_is_dghm: 
  assumes "i ∈∘ I" 
  shows "πDG.1 𝔄 𝔅 : 𝔄 ×DG 𝔅 ↦↦DG⇘α⇙ 𝔄"
  by 
    (
      rule pdg_dghm_proj_is_dghm[
        where i=0, simplified, folded dghm_proj_fst_def dg_prod_2_def
        ]
    )

lemma dghm_proj_fst_is_dghm'[dg_cs_intros]:
  assumes "i ∈∘ I" and "ℭ = 𝔄 ×DG 𝔅" and "𝔇 = 𝔄"
  shows "πDG.1 𝔄 𝔅 : ℭ ↦↦DG⇘α⇙ 𝔇"
  using assms(1) unfolding assms(2,3) by (rule dghm_proj_fst_is_dghm)

lemma dghm_proj_snd_is_dghm:
  assumes "i ∈∘ I"
  shows "πDG.2 𝔄 𝔅 : 𝔄 ×DG 𝔅 ↦↦DG⇘α⇙ 𝔅"
  by
    (
      rule pdg_dghm_proj_is_dghm[
        where i=‹1ℕ›, simplified, folded dghm_proj_snd_def dg_prod_2_def
        ]
    )

lemma dghm_proj_snd_is_dghm'[dg_cs_intros]:  
  assumes "i ∈∘ I" and "ℭ = 𝔄 ×DG 𝔅" and "𝔇 = 𝔅"
  shows "πDG.2 𝔄 𝔅 : ℭ ↦↦DG⇘α⇙ 𝔇"
  using assms(1) unfolding assms(2,3) by (rule dghm_proj_snd_is_dghm)

end



subsection‹Product of three digraphs›
(*TODO: find a way to generalize to the product of n digraphs*)

definition dg_prod_3 :: "V ⇒ V ⇒ V ⇒ V" ("(_ ×DG3 _ ×DG3 _)" [81, 81, 81] 80)
  where "𝔄 ×DG3 𝔅 ×DG3 ℭ = (∏DGi∈∘3ℕ. if3 𝔄 𝔅 ℭ i)"


subsubsection‹Product of three digraphs is a digraph›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" and ℭ: "digraph α ℭ"
begin

interpretation 𝒵 α by (rule digraphD[OF 𝔄(1)])
interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)
interpretation 𝔅: digraph α ℭ by (rule ℭ)

lemma finite_pdigraph_dg_prod_3: 
  "finite_pdigraph α (3ℕ) (if3 𝔄 𝔅 ℭ)"
proof(intro finite_pdigraphI pdigraph_baseI)
  from Axiom_of_Infinity show z1_in_Vset: "3ℕ ∈∘ Vset α" by blast
  show "digraph α (if3 𝔄 𝔅 ℭ i)" if "i ∈∘ 3ℕ" for i
    by (auto intro: dg_cs_intros)
qed auto

interpretation finite_pdigraph α ‹3ℕ› ‹if3 𝔄 𝔅 ℭ›
  by (intro finite_pdigraph_dg_prod_3 𝔄 𝔅)

lemma digraph_dg_prod_3[dg_cs_intros]: "digraph α (𝔄 ×DG3 𝔅 ×DG3 ℭ)"
proof-
  show ?thesis unfolding dg_prod_3_def by (rule pdg_digraph_dg_prod)
qed

end


subsubsection‹Object›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" and ℭ: "digraph α ℭ"
begin

lemma dg_prod_3_ObjI:
  assumes "a ∈∘ 𝔄⦇Obj⦈" and "b ∈∘ 𝔅⦇Obj⦈" and "c ∈∘ ℭ⦇Obj⦈"
  shows "[a, b, c]∘ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
  unfolding dg_prod_3_def dg_prod_components
proof(intro vproductI ballI)
  show "𝒟∘ [a, b, c]∘ = 3ℕ" by (simp add: nat_omega_simps)
  fix i assume "i ∈∘ 3ℕ"
  then consider ‹i = 0› | ‹i = 1ℕ› | ‹i = 2ℕ› unfolding three by auto 
  then show "[a, b, c]∘⦇i⦈ ∈∘ (if3 𝔄 𝔅 ℭ i)⦇Obj⦈"
    by cases (simp_all add: nat_omega_simps assms)
qed auto

lemma dg_prod_3_ObjI'[dg_prod_cs_intros]:
  assumes "abc = [a, b, c]∘" and "a ∈∘ 𝔄⦇Obj⦈" and "b ∈∘ 𝔅⦇Obj⦈" and "c ∈∘ ℭ⦇Obj⦈"
  shows "abc ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
  using assms(2-4) unfolding assms(1) by (rule dg_prod_3_ObjI)

lemma dg_prod_3_ObjE:
  assumes "abc ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
  obtains a b c
    where "abc = [a, b, c]∘" 
      and "a ∈∘ 𝔄⦇Obj⦈" 
      and "b ∈∘ 𝔅⦇Obj⦈"
      and "c ∈∘ ℭ⦇Obj⦈"
proof-
  from vproductD[OF assms[unfolded dg_prod_3_def dg_prod_components]]
  have vsv_abc: "vsv abc"
    and dom_abc: "𝒟∘ abc = 3ℕ"
    and abc_app: "⋀i. i ∈∘ 3ℕ ⟹ abc⦇i⦈ ∈∘ (if3 𝔄 𝔅 ℭ i)⦇Obj⦈"
    by auto
  have dom_abc[simp]: "𝒟∘ abc = 3ℕ"
    unfolding dom_abc by (simp add: nat_omega_simps two)
  interpret vsv abc by (rule vsv_abc)
  have "abc = [vpfst abc, vpsnd abc, vpthrd abc]∘"
    by (rule vsv_vfsequence_three[symmetric]) auto
  moreover from abc_app[of 0] have "vpfst abc ∈∘ 𝔄⦇Obj⦈" by simp
  moreover from abc_app[of ‹1ℕ›] have "vpsnd abc ∈∘ 𝔅⦇Obj⦈" by simp
  moreover from abc_app[of ‹2ℕ›] have "vpthrd abc ∈∘ ℭ⦇Obj⦈" by simp
  ultimately show ?thesis using that by auto
qed

end


subsubsection‹Arrow›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" and ℭ: "digraph α ℭ"
begin

lemma dg_prod_3_ArrI:
  assumes "h ∈∘ 𝔄⦇Arr⦈" and "g ∈∘ 𝔅⦇Arr⦈" and "f ∈∘ ℭ⦇Arr⦈"
  shows "[h, g, f]∘ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  unfolding dg_prod_3_def dg_prod_components
proof(intro vproductI ballI)
  show "𝒟∘ [h, g, f]∘ = 3ℕ" by (simp add: nat_omega_simps three)
  fix i assume "i ∈∘ 3ℕ"
  then consider ‹i = 0› | ‹i = 1ℕ› | ‹i = 2ℕ› unfolding three by auto 
  then show "[h, g, f]∘⦇i⦈ ∈∘ (if3 𝔄 𝔅 ℭ i)⦇Arr⦈"
    by cases (simp_all add: nat_omega_simps assms)
qed auto

lemma dg_prod_3_ArrI'[dg_prod_cs_intros]:
  assumes "hgf = [h, g, f]∘" 
    and "h ∈∘ 𝔄⦇Arr⦈" 
    and "g ∈∘ 𝔅⦇Arr⦈"
    and "f ∈∘ ℭ⦇Arr⦈"
  shows "[h, g, f]∘ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  using assms(2-4) unfolding assms(1) by (rule dg_prod_3_ArrI)

lemma dg_prod_3_ArrE:
  assumes "hgf ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  obtains h g f 
    where "hgf = [h, g, f]∘" 
      and "h ∈∘ 𝔄⦇Arr⦈" 
      and "g ∈∘ 𝔅⦇Arr⦈" 
      and "f ∈∘ ℭ⦇Arr⦈"
proof-
  from vproductD[OF assms[unfolded dg_prod_3_def dg_prod_components]]
  have vsv_hgf: "vsv hgf"
    and dom_hgf: "𝒟∘ hgf = 3ℕ"
    and hgf_app: "⋀i. i ∈∘ 3ℕ ⟹ hgf⦇i⦈ ∈∘ (if3 𝔄 𝔅 ℭ i)⦇Arr⦈"
    by auto
  have dom_hgf[simp]: "𝒟∘ hgf = 3ℕ" unfolding dom_hgf by (simp add: three)
  interpret vsv hgf by (rule vsv_hgf)
  have "hgf = [vpfst hgf, vpsnd hgf, vpthrd hgf]∘"
    by (rule vsv_vfsequence_three[symmetric]) auto
  moreover from hgf_app[of 0] have "vpfst hgf ∈∘ 𝔄⦇Arr⦈" by simp
  moreover from hgf_app[of ‹1ℕ›] have "vpsnd hgf ∈∘ 𝔅⦇Arr⦈" by simp
  moreover from hgf_app[of ‹2ℕ›] have "vpthrd hgf ∈∘ ℭ⦇Arr⦈" by simp
  ultimately show ?thesis using that by auto
qed

end


subsubsection‹Arrow with a domain and a codomain›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" and ℭ: "digraph α ℭ"
begin

interpretation 𝒵 α by (rule digraphD[OF 𝔄(1)])
interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)
interpretation ℭ: digraph α ℭ by (rule ℭ)
interpretation finite_pdigraph α ‹3ℕ› ‹if3 𝔄 𝔅 ℭ›
  by (intro finite_pdigraph_dg_prod_3 𝔄 𝔅 ℭ)

lemma dg_prod_3_is_arrI:
  assumes "f : a ↦⇘𝔄⇙ b" and "f' : a' ↦⇘𝔅⇙ b'" and "f'' : a'' ↦⇘ℭ⇙ b''"
  shows "[f, f', f'']∘ : [a, a', a'']∘ ↦⇘𝔄 ×DG3 𝔅 ×DG3 ℭ⇙ [b, b', b'']∘"
  unfolding dg_prod_3_def
proof(rule dg_prod_is_arrI)
  show "[f, f', f'']∘⦇i⦈ : [a, a', a'']∘⦇i⦈ ↦⇘if3 𝔄 𝔅 ℭ i⇙ [b, b', b'']∘⦇i⦈"
    if "i ∈∘ 3ℕ" for i
  proof-
    from that consider ‹i = 0› | ‹i = 1ℕ› | ‹i = 2ℕ› unfolding three by auto 
    then show 
      "[f, f', f'']∘⦇i⦈ : [a, a', a'']∘⦇i⦈ ↦⇘if3 𝔄 𝔅 ℭ i⇙ [b, b', b'']∘⦇i⦈"
      by cases (simp_all add: nat_omega_simps assms)
  qed
qed (auto simp: nat_omega_simps three)

lemma dg_prod_3_is_arrI'[dg_prod_cs_intros]:
  assumes "F = [f, f', f'']∘"
    and "A = [a, a', a'']∘"
    and "B = [b, b', b'']∘"
    and "f : a ↦⇘𝔄⇙ b"
    and "f' : a' ↦⇘𝔅⇙ b'"  
    and "f'' : a'' ↦⇘ℭ⇙ b''"
  shows "F : A ↦⇘𝔄 ×DG3 𝔅 ×DG3 ℭ⇙ B"
  using assms(4,5,6) unfolding assms(1,2,3) by (rule dg_prod_3_is_arrI)

lemma dg_prod_3_is_arrE:
  assumes "F : A ↦⇘𝔄 ×DG3 𝔅 ×DG3 ℭ⇙ B"
  obtains f f' f'' a a' a'' b b' b'' 
    where "F = [f, f', f'']∘"
      and "A = [a, a', a'']∘"
      and "B = [b, b', b'']∘"
      and "f : a ↦⇘𝔄⇙ b"
      and "f' : a' ↦⇘𝔅⇙ b'"
      and "f'' : a'' ↦⇘ℭ⇙ b''"
proof-
  from dg_prod_is_arrD[OF assms[unfolded dg_prod_3_def]] 
  have [simp]: "vsv F" "𝒟∘ F = 3ℕ" "vsv A" "𝒟∘ A = 3ℕ" "vsv B" "𝒟∘ B = 3ℕ"
    and F_app: "⋀i. i ∈∘ 3ℕ ⟹ F⦇i⦈ : A⦇i⦈ ↦⇘if3 𝔄 𝔅 ℭ i⇙ B⦇i⦈"
    by (auto simp: three)
  have "F = [vpfst F, vpsnd F, vpthrd F]∘" 
    by (simp add: vsv_vfsequence_three)
  moreover have "A = [vpfst A, vpsnd A, vpthrd A]∘" 
    by (simp add: vsv_vfsequence_three)
  moreover have "B = [vpfst B, vpsnd B, vpthrd B]∘" 
    by (simp add: vsv_vfsequence_three)
  moreover from F_app[of 0] have "vpfst F : vpfst A ↦⇘𝔄⇙ vpfst B" by simp
  moreover from F_app[of ‹1ℕ›] have "vpsnd F : vpsnd A ↦⇘𝔅⇙ vpsnd B" 
    by (simp add: nat_omega_simps)
  moreover from F_app[of ‹2ℕ›] have "vpthrd F : vpthrd A ↦⇘ℭ⇙ vpthrd B" 
    by (simp add: nat_omega_simps)
  ultimately show ?thesis using that by auto
qed

end


subsubsection‹Domain›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" and ℭ: "digraph α ℭ"
begin

interpretation 𝒵 α by (rule digraphD[OF 𝔄(1)])
interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)
interpretation ℭ: digraph α ℭ by (rule ℭ)

lemma dg_prod_3_Dom_vsv: "vsv ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈)"
  unfolding dg_prod_3_def dg_prod_components by simp

lemma dg_prod_3_Dom_vdomain[dg_cs_simps]: 
  "𝒟∘ ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈) = (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  unfolding dg_prod_3_def dg_prod_components by simp

lemma dg_prod_3_Dom_app[dg_prod_cs_simps]:
  assumes "[f, f', f'']∘ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  shows "(𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈⦇f, f', f''⦈∙ =
    [𝔄⦇Dom⦈⦇f⦈, 𝔅⦇Dom⦈⦇f'⦈, ℭ⦇Dom⦈⦇f''⦈]∘"
proof-
  from assms obtain A B where F: "[f, f', f'']∘ : A ↦⇘𝔄 ×DG3 𝔅 ×DG3 ℭ⇙ B" 
    by (auto intro: is_arrI)
  then have Dom_F: "(𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈⦇f, f', f''⦈∙ = A" 
    by (simp add: dg_cs_simps)
  from F obtain a a' a'' b b' b'' 
    where A_def: "A = [a, a', a'']∘" 
      and "B = [b, b', b'']∘" 
      and "f : a ↦⇘𝔄⇙ b"
      and "f' : a' ↦⇘𝔅⇙ b'"
      and "f'' : a'' ↦⇘ℭ⇙ b''"
    by (elim dg_prod_3_is_arrE[OF 𝔄 𝔅 ℭ]) simp
  then have Dom_f: "𝔄⦇Dom⦈⦇f⦈ = a"   
    and Dom_f': "𝔅⦇Dom⦈⦇f'⦈ = a'" 
    and Dom_f'': "ℭ⦇Dom⦈⦇f''⦈ = a''" 
    by (simp_all add: dg_cs_simps)
  show ?thesis unfolding Dom_F A_def Dom_f Dom_f' Dom_f'' ..
qed

lemma dg_prod_3_Dom_vrange: 
  "ℛ∘ ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈) ⊆∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
  show "vsv ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈)" by (rule dg_prod_3_Dom_vsv)
  fix F assume prems: "F ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  then obtain f f' f'' where F_def: "F = [f, f', f'']∘" 
    and f: "f ∈∘ 𝔄⦇Arr⦈" 
    and f': "f' ∈∘ 𝔅⦇Arr⦈"
    and f'': "f'' ∈∘ ℭ⦇Arr⦈"
    by (elim dg_prod_3_ArrE[OF 𝔄 𝔅 ℭ]) simp
  from f f' f'' obtain a a' a'' b b' b''
    where f: "f : a ↦⇘𝔄⇙ b" 
      and f': "f' : a' ↦⇘𝔅⇙ b'" 
      and f'': "f'' : a'' ↦⇘ℭ⇙ b''" 
    by (meson is_arrI)
  from 𝔄 𝔅 f f' f'' show "(𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Dom⦈⦇F⦈ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
    unfolding F_def dg_prod_3_Dom_app[OF prems[unfolded F_def]]
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros)
qed

end


subsubsection‹Codomain›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "digraph α 𝔄" and 𝔅: "digraph α 𝔅" and ℭ: "digraph α ℭ"
begin

interpretation 𝒵 α by (rule digraphD[OF 𝔄(1)])
interpretation 𝔄: digraph α 𝔄 by (rule 𝔄)
interpretation 𝔅: digraph α 𝔅 by (rule 𝔅)
interpretation ℭ: digraph α ℭ by (rule ℭ)

lemma dg_prod_3_Cod_vsv: "vsv ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈)"
  unfolding dg_prod_3_def dg_prod_components by simp

lemma dg_prod_3_Cod_vdomain[dg_cs_simps]: 
  "𝒟∘ ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈) = (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  unfolding dg_prod_3_def dg_prod_components by simp

lemma dg_prod_3_Cod_app[dg_prod_cs_simps]:
  assumes "[f, f', f'']∘ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  shows 
    "(𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈⦇f, f', f''⦈∙ =
      [𝔄⦇Cod⦈⦇f⦈, 𝔅⦇Cod⦈⦇f'⦈, ℭ⦇Cod⦈⦇f''⦈]∘"
proof-
  from assms obtain A B where F: "[f, f', f'']∘ : A ↦⇘𝔄 ×DG3 𝔅 ×DG3 ℭ⇙ B" 
    by (auto intro: is_arrI)
  then have Cod_F: "(𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈⦇f, f', f''⦈∙ = B"
    by (simp add: dg_cs_simps)
  from F obtain a a' a'' b b' b'' 
    where "A = [a, a', a'']∘" 
      and B_def: "B = [b, b', b'']∘" 
      and "f : a ↦⇘𝔄⇙ b"
      and "f' : a' ↦⇘𝔅⇙ b'"
      and "f'' : a'' ↦⇘ℭ⇙ b''"
    by (elim dg_prod_3_is_arrE[OF 𝔄 𝔅 ℭ]) simp
  then have Cod_f: "𝔄⦇Cod⦈⦇f⦈ = b"
    and Cod_f': "𝔅⦇Cod⦈⦇f'⦈ = b'"
    and Cod_f'': "ℭ⦇Cod⦈⦇f''⦈ = b''"
    by (simp_all add: dg_cs_simps)
  show ?thesis unfolding Cod_F B_def Cod_f Cod_f' Cod_f'' ..
qed

lemma dg_prod_3_Cod_vrange: 
  "ℛ∘ ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈) ⊆∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
  show "vsv ((𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈)" by (rule dg_prod_3_Cod_vsv)
  fix F assume prems: "F ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Arr⦈"
  then obtain f f' f'' where F_def: "F = [f, f', f'']∘" 
    and f: "f ∈∘ 𝔄⦇Arr⦈" 
    and f': "f' ∈∘ 𝔅⦇Arr⦈" 
    and f'': "f'' ∈∘ ℭ⦇Arr⦈"
    by (elim dg_prod_3_ArrE[OF 𝔄 𝔅 ℭ]) simp
  from f f' f'' obtain a a' a'' b b' b'' 
    where f: "f : a ↦⇘𝔄⇙ b" 
      and f': "f' : a' ↦⇘𝔅⇙ b'"
      and f'': "f'' : a'' ↦⇘ℭ⇙ b''"
    by (metis is_arrI)
  from 𝔄 𝔅 ℭ f f' f'' show 
    "(𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Cod⦈⦇F⦈ ∈∘ (𝔄 ×DG3 𝔅 ×DG3 ℭ)⦇Obj⦈"
    unfolding F_def dg_prod_3_Cod_app[OF prems[unfolded F_def]]
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros
      )
qed

end

text‹\newpage›

end