Theory CZH_DG_TDGHM

(* Copyright 2021 (C) Mihails Milehins *)

section‹Transformation of digraph homomorphisms›
theory CZH_DG_TDGHM
  imports CZH_DG_DGHM
begin



subsection‹Background›

named_theorems tdghm_cs_simps
named_theorems tdghm_cs_intros
named_theorems nt_field_simps

definition NTMap :: V where [nt_field_simps]: "NTMap = 0"
definition NTDom :: V where [nt_field_simps]: "NTDom = 1⇩ℕ"
definition NTCod :: V where [nt_field_simps]: "NTCod = 2⇩ℕ"
definition NTDGDom :: V where [nt_field_simps]: "NTDGDom = 3⇩ℕ"
definition NTDGCod :: V where [nt_field_simps]: "NTDGCod = 4⇩ℕ"



subsection‹Definition and elementary properties›


text‹
A transformation of digraph homomorphisms, as presented in this work, 
is a generalization of the concept of a natural transformation, as presented in
Chapter I-4 in \<^cite>‹"mac_lane_categories_2010"›, to digraphs and digraph
homomorphisms. The generalization is performed by excluding the commutativity 
axiom from the definition. 

The definition of a transformation of digraph homomorphisms is 
parameterized by a limit ordinal ‹α› such that ‹ω < α›. 
Such transformations of digraph homomorphisms are referred to either as
‹α›-transformations of digraph homomorphisms or 
transformations of ‹α›-digraph homomorphisms.
›

locale is_tdghm = 
  𝒵 α + 
  vfsequence 𝔑 + 
  NTDom: is_dghm α 𝔄 𝔅 𝔉 +
  NTCod: is_dghm α 𝔄 𝔅 𝔊 
  for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes tdghm_length[dg_cs_simps]: "vcard 𝔑 = 5⇩ℕ"
    and tdghm_NTMap_vsv: "vsv (𝔑⦇NTMap⦈)"
    and tdghm_NTMap_vdomain[dg_cs_simps]: "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
    and tdghm_NTDom[dg_cs_simps]: "𝔑⦇NTDom⦈ = 𝔉"
    and tdghm_NTCod[dg_cs_simps]: "𝔑⦇NTCod⦈ = 𝔊"
    and tdghm_NTDGDom[dg_cs_simps]: "𝔑⦇NTDGDom⦈ = 𝔄"
    and tdghm_NTDGCod[dg_cs_simps]: "𝔑⦇NTDGCod⦈ = 𝔅"
    and tdghm_NTMap_is_arr: 
      "a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"

syntax "_is_tdghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦⇩D⇩G⇩H⇩M _ :/ _ ↦↦⇩D⇩Gı _)› [51, 51, 51, 51, 51] 51)
translations "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" ⇌
  "CONST is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑"

abbreviation all_tdghms :: "V ⇒ V"
  where "all_tdghms α ≡ set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"

abbreviation tdghms :: "V ⇒ V ⇒ V ⇒ V"
  where "tdghms α 𝔄 𝔅 ≡ set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"

abbreviation these_tdghms :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "these_tdghms α 𝔄 𝔅 𝔉 𝔊 ≡ set {𝔑. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"

sublocale is_tdghm ⊆ NTMap: vsv ‹𝔑⦇NTMap⦈›
  rewrites "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
  by (rule tdghm_NTMap_vsv) (simp add: dg_cs_simps)

lemmas [dg_cs_simps] =  
  is_tdghm.tdghm_length
  is_tdghm.tdghm_NTMap_vdomain
  is_tdghm.tdghm_NTDom
  is_tdghm.tdghm_NTCod
  is_tdghm.tdghm_NTDGDom
  is_tdghm.tdghm_NTDGCod

lemma (in is_tdghm) tdghm_NTMap_is_arr'[dg_cs_intros]:
  assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
    and "A = 𝔉⦇ObjMap⦈⦇a⦈"
    and "B = 𝔊⦇ObjMap⦈⦇a⦈"
  shows "𝔑⦇NTMap⦈⦇a⦈ : A ↦⇘𝔅⇙ B"
  using assms(1) unfolding assms(2,3) by (rule tdghm_NTMap_is_arr)

lemmas [dg_cs_intros] = is_tdghm.tdghm_NTMap_is_arr'


text‹Rules.›

lemma (in is_tdghm) is_tdghm_axioms'[dg_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "𝔑 : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄' ↦↦⇩D⇩G⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tdghm_axioms)

mk_ide rf is_tdghm_def[unfolded is_tdghm_axioms_def]
  |intro is_tdghmI|
  |dest is_tdghmD[dest]|
  |elim is_tdghmE[elim]|

lemmas [dg_cs_intros] =
  is_tdghmD(3,4)


text‹Elementary properties.›

lemma tdghm_eqI:
  assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
    and "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈"
    and "𝔉 = 𝔉'"
    and "𝔊 = 𝔊'"
    and "𝔄 = 𝔄'"
    and "𝔅 = 𝔅'"
  shows "𝔑 = 𝔑'"
proof-
  interpret L: is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret R: is_tdghm α 𝔄' 𝔅' 𝔉' 𝔊' 𝔑' by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟⇩∘ 𝔑 = 5⇩ℕ" 
      by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
    show "𝒟⇩∘ 𝔑 = 𝒟⇩∘ 𝔑'"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
    from assms(4-7) have sup: 
      "𝔑⦇NTDom⦈ = 𝔑'⦇NTDom⦈" "𝔑⦇NTCod⦈ = 𝔑'⦇NTCod⦈" 
      "𝔑⦇NTDGDom⦈ = 𝔑'⦇NTDGDom⦈" "𝔑⦇NTDGCod⦈ = 𝔑'⦇NTDGCod⦈" 
      by (simp_all add: dg_cs_simps)
    show "a ∈⇩∘ 𝒟⇩∘ 𝔑 ⟹ 𝔑⦇a⦈ = 𝔑'⦇a⦈" for a 
      by (unfold dom, elim_in_numeral, insert assms(3) sup)
        (auto simp: nt_field_simps)
  qed (auto simp: L.vsv_axioms R.vsv_axioms)
qed

lemma (in is_tdghm) tdghm_def:
  "𝔑 = [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ 𝔑 = 5⇩ℕ" 
    by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
  have dom_rhs:
    "𝒟⇩∘ [𝔑⦇NTMap⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈]⇩∘ = 5⇩ℕ"
    by (simp add: nat_omega_simps)
  then show 
    "𝒟⇩∘ 𝔑 = 𝒟⇩∘ [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘"
    unfolding dom_lhs dom_rhs by (simp add: nat_omega_simps)
  show "a ∈⇩∘ 𝒟⇩∘ 𝔑 ⟹
    𝔑⦇a⦈ = [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘⦇a⦈" 
    for a
    by (unfold dom_lhs, elim_in_numeral, unfold nt_field_simps)
      (simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)

lemma (in is_tdghm) tdghm_NTMap_app_in_Arr[dg_cs_intros]:
  assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "𝔑⦇NTMap⦈⦇a⦈ ∈⇩∘ 𝔅⦇Arr⦈"
  using assms using tdghm_NTMap_is_arr by auto

lemmas [dg_cs_intros] = is_tdghm.tdghm_NTMap_app_in_Arr

lemma (in is_tdghm) tdghm_NTMap_vrange_vifunion:
  "ℛ⇩∘ (𝔑⦇NTMap⦈) ⊆⇩∘ (⋃⇩∘a∈⇩∘ℛ⇩∘ (𝔉⦇ObjMap⦈). ⋃⇩∘b∈⇩∘ℛ⇩∘ (𝔊⦇ObjMap⦈). Hom 𝔅 a b)"
proof(intro NTMap.vsv_vrange_vsubset)
  fix x assume prems: "x ∈⇩∘ 𝔄⦇Obj⦈"
  note 𝔑x = tdghm_NTMap_is_arr[OF prems]
  from prems show 
    "𝔑⦇NTMap⦈⦇x⦈ ∈⇩∘ (⋃⇩∘a∈⇩∘ℛ⇩∘ (𝔉⦇ObjMap⦈). ⋃⇩∘b∈⇩∘ℛ⇩∘ (𝔊⦇ObjMap⦈). Hom 𝔅 a b)"
    by (intro vifunionI, unfold in_Hom_iff) 
      (
        auto intro: 
          dg_cs_intros NTDom.ObjMap.vsv_vimageI2' NTCod.ObjMap.vsv_vimageI2' 
      )
qed

lemma (in is_tdghm) tdghm_NTMap_vrange: "ℛ⇩∘ (𝔑⦇NTMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈"
proof(intro NTMap.vsv_vrange_vsubset)
  fix x assume "x ∈⇩∘ 𝔄⦇Obj⦈"
  with is_tdghm_axioms show "𝔑⦇NTMap⦈⦇x⦈ ∈⇩∘ 𝔅⦇Arr⦈"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
qed


text‹Size.›

lemma (in is_tdghm) tdghm_NTMap_vsubset_Vset: "𝔑⦇NTMap⦈ ⊆⇩∘ Vset α"
proof(intro NTMap.vbrelation_Limit_vsubset_VsetI)
  show "ℛ⇩∘ (𝔑⦇NTMap⦈) ⊆⇩∘ Vset α"
    by 
      (
        rule vsubset_transitive, 
        rule tdghm_NTMap_vrange,
        rule NTDom.HomCod.dg_Arr_vsubset_Vset
      )
qed (simp_all add: NTDom.HomDom.dg_Obj_vsubset_Vset)

lemma (in is_tdghm) tdghm_NTMap_in_Vset: 
  assumes "α ∈⇩∘ β"
  shows "𝔑⦇NTMap⦈ ∈⇩∘ Vset β"
  by (meson assms tdghm_NTMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in is_tdghm) tdghm_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 ∈⇩∘ Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [dg_cs_intros] = 
    tdghm_NTMap_in_Vset
    NTDom.dghm_in_Vset
    NTCod.dghm_in_Vset
    NTDom.HomDom.dg_in_Vset
    NTDom.HomCod.dg_in_Vset
  from assms(2) show ?thesis
    by (subst tdghm_def) 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros
      )
qed

lemma (in is_tdghm) tdghm_is_tdghm_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘β⇙ 𝔅"
proof(rule is_tdghmI)
  show "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈" if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
    using that by (cs_concl cs_shallow cs_intro: dg_cs_intros)
qed 
  (
    cs_concl cs_shallow 
      cs_simp: dg_cs_simps 
      cs_intro:
        V_cs_intros
        assms NTDom.dghm_is_dghm_if_ge_Limit NTCod.dghm_is_dghm_if_ge_Limit  
   )+

lemma small_all_tdghms[simp]: 
  "small {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
  case True
  from is_tdghm.tdghm_in_Vset show ?thesis
    by (intro down[of _ ‹Vset (α + ω)›]) 
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅} = {}" by auto
  then show ?thesis by simp
qed

lemma small_tdghms[simp]: "small {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
  by (rule down[of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}›])
    auto

lemma small_these_tdghms[simp]: "small {𝔑. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}"
  by (rule down[of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅}›]) 
    auto


text‹Further elementary results.›

lemma these_tdghms_iff(*not simp*): 
  "𝔑 ∈⇩∘ these_tdghms α 𝔄 𝔅 𝔉 𝔊 ⟷ 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  by auto



subsection‹Opposite transformation of digraph homomorphisms›


subsubsection‹Definition and elementary properties›


text‹See section 1.5 in \<^cite>‹"bodo_categories_1970"›.›

definition op_tdghm :: "V ⇒ V"
  where "op_tdghm 𝔑 =
    [
      𝔑⦇NTMap⦈,
      op_dghm (𝔑⦇NTCod⦈),
      op_dghm (𝔑⦇NTDom⦈),
      op_dg (𝔑⦇NTDGDom⦈),
      op_dg (𝔑⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›

lemma op_tdghm_components[dg_op_simps]:
  shows "op_tdghm 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "op_tdghm 𝔑⦇NTDom⦈ = op_dghm (𝔑⦇NTCod⦈)"
    and "op_tdghm 𝔑⦇NTCod⦈ = op_dghm (𝔑⦇NTDom⦈)"
    and "op_tdghm 𝔑⦇NTDGDom⦈ = op_dg (𝔑⦇NTDGDom⦈)"
    and "op_tdghm 𝔑⦇NTDGCod⦈ = op_dg (𝔑⦇NTDGCod⦈)"
  unfolding op_tdghm_def nt_field_simps by (auto simp: nat_omega_simps)


subsubsection‹Further properties›

lemma (in is_tdghm) is_tdghm_op: 
  "op_tdghm 𝔑 : op_dghm 𝔊 ↦⇩D⇩G⇩H⇩M op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ op_dg 𝔅"
proof(rule is_tdghmI, unfold dg_op_simps)
  show "vfsequence (op_tdghm 𝔑)" by (simp add: op_tdghm_def)
  show "vcard (op_tdghm 𝔑) = 5⇩ℕ" by (simp add: op_tdghm_def nat_omega_simps)
  show "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈" if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
    using that by (cs_concl cs_shallow cs_intro: dg_cs_intros)
qed 
  (
    cs_concl cs_shallow
      cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_op_intros V_cs_intros
  )+

lemma (in is_tdghm) is_tdghm_op'[dg_op_intros]: 
  assumes "𝔊' = op_dghm 𝔊"
    and "𝔉' = op_dghm 𝔉"
    and "𝔄' = op_dg 𝔄"
    and "𝔅' = op_dg 𝔅"
  shows "op_tdghm 𝔑 : 𝔊' ↦⇩D⇩G⇩H⇩M 𝔉' : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tdghm_op)

lemmas is_tdghm_op[dg_op_intros] = is_tdghm.is_tdghm_op'

lemma (in is_tdghm) tdghm_op_tdghm_op_tdghm[dg_op_simps]: 
  "op_tdghm (op_tdghm 𝔑) = 𝔑"
proof(rule tdghm_eqI[of α 𝔄 𝔅 𝔉 𝔊 _ 𝔄 𝔅 𝔉 𝔊], unfold dg_op_simps)
  interpret op: 
    is_tdghm α ‹op_dg 𝔄› ‹op_dg 𝔅› ‹op_dghm 𝔊› ‹op_dghm 𝔉› ‹op_tdghm 𝔑›
    by (rule is_tdghm_op)
  from op.is_tdghm_op show 
    "op_tdghm (op_tdghm 𝔑) : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    by (simp add: dg_op_simps)
qed (auto simp: dg_cs_intros)

lemmas tdghm_op_tdghm_op_tdghm[dg_op_simps] = 
  is_tdghm.tdghm_op_tdghm_op_tdghm

lemma eq_op_tdghm_iff: 
  assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
  shows "op_tdghm 𝔑 = op_tdghm 𝔑' ⟷ 𝔑 = 𝔑'"
proof
  interpret L: is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret R: is_tdghm α 𝔄' 𝔅' 𝔉' 𝔊' 𝔑' by (rule assms(2))
  assume prems: "op_tdghm 𝔑 = op_tdghm 𝔑'"
  show "𝔑 = 𝔑'"
  proof(rule tdghm_eqI[OF assms])
    from prems L.tdghm_op_tdghm_op_tdghm R.tdghm_op_tdghm_op_tdghm show 
      "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈"
      by metis+
    from prems L.tdghm_op_tdghm_op_tdghm R.tdghm_op_tdghm_op_tdghm 
    have "𝔑⦇NTDom⦈ = 𝔑'⦇NTDom⦈" 
      and "𝔑⦇NTCod⦈ = 𝔑'⦇NTCod⦈" 
      and "𝔑⦇NTDGDom⦈ = 𝔑'⦇NTDGDom⦈" 
      and "𝔑⦇NTDGCod⦈ = 𝔑'⦇NTDGCod⦈" 
      by metis+
    then show "𝔉 = 𝔉'" "𝔊 = 𝔊'" "𝔄 = 𝔄'" "𝔅 = 𝔅'" by (auto simp: dg_cs_simps)
  qed
qed auto



subsection‹
Composition of a transformation of digraph homomorphisms 
and a digraph homomorphism
›


subsubsection‹Definition and elementary properties›

definition tdghm_dghm_comp :: "V ⇒ V ⇒ V" (infixl ‹∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M› 55)
  where "𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ =
    [
      (λa∈⇩∘ℌ⦇HomDom⦈⦇Obj⦈. 𝔑⦇NTMap⦈⦇ℌ⦇ObjMap⦈⦇a⦈⦈),
      𝔑⦇NTDom⦈ ∘⇩D⇩G⇩H⇩M ℌ,
      𝔑⦇NTCod⦈ ∘⇩D⇩G⇩H⇩M ℌ,
      ℌ⦇HomDom⦈,
      𝔑⦇NTDGCod⦈
    ]⇩∘"


text‹Components.›

lemma tdghm_dghm_comp_components:
  shows "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTMap⦈ =
    (λa∈⇩∘ℌ⦇HomDom⦈⦇Obj⦈. 𝔑⦇NTMap⦈⦇ℌ⦇ObjMap⦈⦇a⦈⦈)"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTDom⦈ = 𝔑⦇NTDom⦈ ∘⇩D⇩G⇩H⇩M ℌ"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTCod⦈ = 𝔑⦇NTCod⦈ ∘⇩D⇩G⇩H⇩M ℌ"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTDGDom⦈ = ℌ⦇HomDom⦈"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTDGCod⦈ = 𝔑⦇NTDGCod⦈"
  unfolding tdghm_dghm_comp_def nt_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Transformation map›

mk_VLambda tdghm_dghm_comp_components(1)
  |vsv tdghm_dghm_comp_NTMap_vsv[dg_shared_cs_intros, dg_cs_intros]|

mk_VLambda (in is_dghm) 
  tdghm_dghm_comp_components(1)[where ℌ=𝔉, unfolded dghm_HomDom]
  |vdomain tdghm_dghm_comp_NTMap_vdomain|
  |app tdghm_dghm_comp_NTMap_app|

lemmas [dg_cs_simps] = 
  is_dghm.tdghm_dghm_comp_NTMap_vdomain
  is_dghm.tdghm_dghm_comp_NTMap_app

lemma tdghm_dghm_comp_NTMap_vrange: 
  assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret 𝔑: is_tdghm α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_dghm α 𝔄 𝔅 ℌ by (rule assms(2))
  show ?thesis 
    unfolding tdghm_dghm_comp_components
  proof(rule vrange_VLambda_vsubset, unfold dg_cs_simps)
    fix x assume "x ∈⇩∘ 𝔄⦇Obj⦈"
    then show "𝔑⦇NTMap⦈⦇ℌ⦇ObjMap⦈⦇x⦈⦈ ∈⇩∘ ℭ⦇Arr⦈"
      by (cs_concl cs_shallow cs_intro: dg_cs_intros)
  qed
qed


subsubsection‹
Opposite of the composition of a transformation of 
digraph homomorphisms and a digraph homomorphism
›

lemma op_tdghm_tdghm_dghm_comp[dg_op_simps]: 
  "op_tdghm (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ) = op_tdghm 𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M op_dghm ℌ"
  unfolding 
    tdghm_dghm_comp_def 
    dghm_comp_def 
    op_tdghm_def 
    op_dghm_def 
    op_dg_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹
Composition of a transformation of digraph homomorphisms and a digraph
homomorphism is a transformation of digraph homomorphisms
›

lemma tdghm_dghm_comp_is_tdghm:
  assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  shows "𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ : 𝔉 ∘⇩D⇩G⇩H⇩M ℌ ↦⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M ℌ : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_tdghm α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_dghm α 𝔄 𝔅 ℌ by (rule assms(2))
  show ?thesis
  proof(rule is_tdghmI)
    show "vfsequence (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)" unfolding tdghm_dghm_comp_def by simp
    show "vcard (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ) = 5⇩ℕ"
      unfolding tdghm_dghm_comp_def by (simp add: nat_omega_simps)
    show "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ)⦇NTMap⦈⦇a⦈ :
      (𝔉 ∘⇩D⇩G⇩H⇩M ℌ)⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ∘⇩D⇩G⇩H⇩M ℌ)⦇ObjMap⦈⦇a⦈"
      if "a ∈⇩∘ 𝔄⦇Obj⦈" for a 
      by 
        (
          use that in 
            ‹cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros›
        )
  qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
qed

lemma tdghm_dghm_comp_is_tdghm'[dg_cs_intros]:
  assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" 
    and "ℌ : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    and "𝔉' = 𝔉 ∘⇩D⇩G⇩H⇩M ℌ"
    and "𝔊' = 𝔊 ∘⇩D⇩G⇩H⇩M ℌ"
  shows "𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M ℌ : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule tdghm_dghm_comp_is_tdghm)


subsubsection‹Further properties›

lemma tdghm_dghm_comp_tdghm_dghm_comp_assoc:
  assumes "𝔑 : ℌ ↦⇩D⇩G⇩H⇩M ℌ' : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇" 
    and "𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" 
    and "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  shows "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔊) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔉 = 𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)"
proof-
  interpret 𝔑: is_tdghm α ℭ 𝔇 ℌ ℌ' 𝔑 by (rule assms(1))
  interpret 𝔊: is_dghm α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret 𝔉: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(3))
  show ?thesis  
  proof(rule tdghm_eqI)
    from assms show 
      "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔊) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔉 :
        ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ↦⇩D⇩G⇩H⇩M ℌ' ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 :
        𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔇"
      by (cs_concl cs_shallow cs_intro: dg_cs_intros)
    then have dom_lhs: "𝒟⇩∘ (((𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔊) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔉)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_simp: dg_cs_simps)
    show "𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) :
      ℌ ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ↦⇩D⇩G⇩H⇩M ℌ' ∘⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 :
      𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔇"
      by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
    then have dom_rhs: "𝒟⇩∘ ((𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_simp: dg_cs_simps)
    show 
      "((𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔊) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔉)⦇NTMap⦈ = 
        (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      with assms show 
        "((𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔊) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔉)⦇NTMap⦈⦇a⦈ =
          (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉))⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
    qed (cs_concl cs_shallow cs_intro: dg_cs_intros)
  qed simp_all
qed

lemma (in is_tdghm) tdghm_tdghm_dghm_comp_dghm_id[dg_cs_simps]:
  "𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M dghm_id 𝔄 = 𝔑"
proof(rule tdghm_eqI)
  show "𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M dghm_id 𝔄 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  show "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  have dom_lhs: "𝒟⇩∘ ((𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  show "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dg_cs_simps)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    then show "(𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M dghm_id 𝔄)⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed (cs_concl cs_intro: dg_cs_intros V_cs_intros)+
qed simp_all

lemmas [dg_cs_simps] = is_tdghm.tdghm_tdghm_dghm_comp_dghm_id



subsection‹
Composition of a digraph homomorphism and a transformation of
digraph homomorphisms
›


subsubsection‹Definition and elementary properties›

definition dghm_tdghm_comp :: "V ⇒ V ⇒ V" (infixl ‹∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M› 55)
  where "ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 =
    [
      (λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈. ℌ⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈),
      ℌ ∘⇩D⇩G⇩H⇩M 𝔑⦇NTDom⦈,
      ℌ ∘⇩D⇩G⇩H⇩M 𝔑⦇NTCod⦈,
      𝔑⦇NTDGDom⦈,
      ℌ⦇HomCod⦈
    ]⇩∘"


text‹Components.›

lemma dghm_tdghm_comp_components:
  shows "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈ =
    (λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈. ℌ⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈)"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTDom⦈ = ℌ ∘⇩D⇩G⇩H⇩M 𝔑⦇NTDom⦈"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTCod⦈ = ℌ ∘⇩D⇩G⇩H⇩M 𝔑⦇NTCod⦈"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTDGDom⦈ = 𝔑⦇NTDGDom⦈"
    and [dg_shared_cs_simps, dg_cs_simps]: 
      "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTDGCod⦈ = ℌ⦇HomCod⦈"
  unfolding dghm_tdghm_comp_def nt_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Transformation map›

mk_VLambda dghm_tdghm_comp_components(1)
  |vsv dghm_tdghm_comp_NTMap_vsv[dg_shared_cs_intros, dg_cs_intros]|

mk_VLambda (in is_tdghm) 
  dghm_tdghm_comp_components(1)[where 𝔑=𝔑, unfolded tdghm_NTDGDom]
  |vdomain dghm_tdghm_comp_NTMap_vdomain|
  |app dghm_tdghm_comp_NTMap_app|

lemmas [dg_cs_simps] = 
  is_tdghm.dghm_tdghm_comp_NTMap_vdomain
  is_tdghm.dghm_tdghm_comp_NTMap_app

lemma dghm_tdghm_comp_NTMap_vrange: 
  assumes "ℌ : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret ℌ: is_dghm α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis 
    unfolding dghm_tdghm_comp_components
  proof(rule vrange_VLambda_vsubset, unfold dg_cs_simps)
    fix x assume "x ∈⇩∘ 𝔄⦇Obj⦈"
    then show "ℌ⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇x⦈⦈ ∈⇩∘ ℭ⦇Arr⦈"
      by (cs_concl cs_shallow cs_intro: dg_cs_intros)
  qed
qed


subsubsection‹
Opposite of the composition of a digraph homomorphism 
and a transformation of digraph homomorphisms
›

lemma op_tdghm_dghm_tdghm_comp[dg_op_simps]: 
  "op_tdghm (ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) = op_dghm ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M op_tdghm 𝔑"
  unfolding 
    dghm_tdghm_comp_def
    dghm_comp_def
    op_tdghm_def
    op_dghm_def
    op_dg_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹
Composition of a digraph homomorphism and a transformation of
digraph homomorphisms is a transformation of digraph homomorphisms
›

lemma dghm_tdghm_comp_is_tdghm:
  assumes "ℌ : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  shows "ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 : ℌ ∘⇩D⇩G⇩H⇩M 𝔉 ↦⇩D⇩G⇩H⇩M ℌ ∘⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
proof-
  interpret ℌ: is_dghm α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
  proof(rule is_tdghmI)
    show "vfsequence (ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)"
      unfolding dghm_tdghm_comp_def by simp
    show "vcard (ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) = 5⇩ℕ"
      unfolding dghm_tdghm_comp_def  by (simp add: nat_omega_simps)
    show "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈⦇a⦈ : 
      (ℌ ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (ℌ ∘⇩D⇩G⇩H⇩M 𝔊)⦇ObjMap⦈⦇a⦈"
      if "a ∈⇩∘ 𝔄⦇Obj⦈" for a 
      by (use that in ‹cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros›)
  qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
qed

lemma dghm_tdghm_comp_is_tdghm'[dg_cs_intros]:
  assumes "ℌ : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    and "𝔉' = ℌ ∘⇩D⇩G⇩H⇩M 𝔉"
    and "𝔊' = ℌ ∘⇩D⇩G⇩H⇩M 𝔊"
  shows "ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄 ↦↦⇩D⇩G⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule dghm_tdghm_comp_is_tdghm)


subsubsection‹Further properties›

lemma dghm_comp_dghm_tdghm_comp_assoc:
  assumes "𝔑 : ℌ ↦⇩D⇩G⇩H⇩M ℌ' : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    and "𝔉 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ"
    and "𝔊 : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
  shows "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 = 𝔊 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)"
proof(rule tdghm_eqI)
  interpret 𝔑: is_tdghm α 𝔄 𝔅 ℌ ℌ' 𝔑 by (rule assms(1))
  interpret 𝔉: is_dghm α 𝔅 ℭ 𝔉 by (rule assms(2))
  interpret 𝔊: is_dghm α ℭ 𝔇 𝔊 by (rule assms(3))
  from assms show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 :
    𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ∘⇩D⇩G⇩H⇩M ℌ ↦⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ∘⇩D⇩G⇩H⇩M ℌ' : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔇"
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: dg_cs_simps)
  from assms show "𝔊 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) :
    𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ∘⇩D⇩G⇩H⇩M ℌ ↦⇩D⇩G⇩H⇩M 𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ∘⇩D⇩G⇩H⇩M ℌ' : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔇"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  then have dom_rhs: 
    "𝒟⇩∘ ((𝔊 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑))⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: dg_cs_simps)
  show 
    "((𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈ = 
      (𝔊 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑))⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    then show 
      "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈⦇a⦈ =
        (𝔊 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔉 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑))⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
qed simp_all

lemma (in is_tdghm) tdghm_dghm_tdghm_comp_dghm_id[dg_cs_simps]:
  "dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 = 𝔑"
proof(rule tdghm_eqI)
  show "dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: dg_cs_simps)
  show "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  show "(dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dg_cs_simps)
    show "vsv (𝔑⦇NTMap⦈)" by auto
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    then show "(dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑)⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed (cs_concl cs_shallow cs_intro: dg_cs_intros)+
qed simp_all

lemmas [dg_cs_simps] = is_tdghm.tdghm_dghm_tdghm_comp_dghm_id

lemma dghm_tdghm_comp_tdghm_dghm_comp_assoc:
  assumes "𝔑 : 𝔉 ↦⇩D⇩G⇩H⇩M 𝔊 : 𝔅 ↦↦⇩D⇩G⇘α⇙ ℭ"
    and "ℌ : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
    and "𝔎 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
  shows "(ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎 = ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎)"
proof-
  interpret 𝔑: is_tdghm α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_dghm α ℭ 𝔇 ℌ by (rule assms(2))
  interpret 𝔎: is_dghm α 𝔄 𝔅 𝔎 by (rule assms(3))
  show ?thesis
  proof(rule tdghm_eqI)
    from assms have dom_lhs: 
      "𝒟⇩∘ (((ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps)
    from assms have dom_rhs: 
      "𝒟⇩∘ ((ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎))⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
    show 
      "((ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎)⦇NTMap⦈ =
        (ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎))⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      then show 
        "((ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎)⦇NTMap⦈⦇a⦈ =
          ((ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M (𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M 𝔎)))⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
    qed (cs_concl cs_shallow cs_intro: dg_cs_intros)
  qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
qed

text‹\newpage›

end