Theory CZH_DG_DGHM

(* Copyright 2021 (C) Mihails Milehins *)

section‹Homomorphism of digraphs›
theory CZH_DG_DGHM
  imports CZH_DG_Digraph
begin



subsection‹Background›

named_theorems dghm_cs_simps
named_theorems dghm_cs_intros

named_theorems dg_cn_cs_simps
named_theorems dg_cn_cs_intros

named_theorems dghm_field_simps

definition ObjMap :: V where [dghm_field_simps]: "ObjMap = 0"
definition ArrMap :: V where [dghm_field_simps]: "ArrMap = 1"
definition HomDom :: V where [dghm_field_simps]: "HomDom = 2"
definition HomCod :: V where [dghm_field_simps]: "HomCod = 3"



subsection‹Definition and elementary properties›


text‹
A homomorphism of digraphs, as presented in this work, can be seen as a
generalization of the concept of a functor between categories, as presented in
Chapter I-3 in cite"mac_lane_categories_2010", to digraphs. 
The generalization is performed by removing the axioms (1) from the definition.
It is expected that the resulting definition is consistent with the conventional
notion of a homomorphism of digraphs in graph theory, but further details 
are considered to be outside of the scope of this work.

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

Following cite"mac_lane_categories_2010", all digraph homomorphisms are 
covariant (see Chapter II-2). However, a special notation is adapted for the 
digraph homomorphisms from an opposite digraph. Normally, such 
digraph homomorphisms will be referred to as the contravariant digraph 
homomorphisms, but this convention will not be enforced.
›

locale is_dghm = 
  𝒵 α + vfsequence 𝔉 + HomDom: digraph α 𝔄 + HomCod: digraph α 𝔅 
  for α 𝔄 𝔅 𝔉 +
  assumes dghm_length[dg_cs_simps]: "vcard 𝔉 = 4"  
    and dghm_HomDom[dg_cs_simps]: "𝔉HomDom = 𝔄"
    and dghm_HomCod[dg_cs_simps]: "𝔉HomCod = 𝔅"
    and dghm_ObjMap_vsv: "vsv (𝔉ObjMap)"
    and dghm_ArrMap_vsv: "vsv (𝔉ArrMap)"
    and dghm_ObjMap_vdomain[dg_cs_simps]: "𝒟 (𝔉ObjMap) = 𝔄Obj"
    and dghm_ObjMap_vrange: " (𝔉ObjMap)  𝔅Obj"
    and dghm_ArrMap_vdomain[dg_cs_simps]: "𝒟 (𝔉ArrMap) = 𝔄Arr"
    and dghm_ArrMap_is_arr: 
      "f : a 𝔄b  𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"

syntax "_is_dghm" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦DGı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦DGα𝔅"  "CONST is_dghm α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_dghm :: "V  V  V  V  bool"
  where "is_cn_dghm α 𝔄 𝔅 𝔉  𝔉 : op_dg 𝔄 ↦↦DGα𝔅"

syntax "_is_cn_dghm" :: "V  V  V  V  bool" 
  ((_ :/ _ DG↦↦ı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 DG↦↦α𝔅"  "CONST is_cn_dghm α 𝔄 𝔅 𝔉"

abbreviation all_dghms :: "V  V"
  where "all_dghms α  set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦DGα𝔅}"

abbreviation dghms :: "V  V  V  V"
  where "dghms α 𝔄 𝔅  set {𝔉. 𝔉 : 𝔄 ↦↦DGα𝔅}"

sublocale is_dghm  ObjMap: vsv 𝔉ObjMap
  rewrites "𝒟 (𝔉ObjMap) = 𝔄Obj"
  by (rule dghm_ObjMap_vsv) (simp add: dg_cs_simps)

sublocale is_dghm  ArrMap: vsv 𝔉ArrMap
  rewrites "𝒟 (𝔉ArrMap) = 𝔄Arr"
  by (rule dghm_ArrMap_vsv) (simp add: dg_cs_simps)

lemmas [dg_cs_simps] =
  is_dghm.dghm_HomDom
  is_dghm.dghm_HomCod
  is_dghm.dghm_ObjMap_vdomain
  is_dghm.dghm_ArrMap_vdomain

lemma (in is_dghm) dghm_ArrMap_is_arr''[dg_cs_intros]:
  assumes "f : a 𝔄b" and "𝔉f = 𝔉ArrMapf"
  shows "𝔉f : 𝔉ObjMapa 𝔅𝔉ObjMapb"
  using assms(1) unfolding assms(2) by (rule dghm_ArrMap_is_arr)

lemma (in is_dghm) dghm_ArrMap_is_arr'[dg_cs_intros]:
  assumes "f : a 𝔄b"
    and "A = 𝔉ObjMapa"
    and "B = 𝔉ObjMapb"
  shows "𝔉ArrMapf : A 𝔅B"
  using assms(1) unfolding assms(2,3) by (rule dghm_ArrMap_is_arr) 

lemmas [dg_cs_intros] = is_dghm.dghm_ArrMap_is_arr'


text‹Rules.›

lemma (in is_dghm) is_dghm_axioms'[dg_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦DGα'𝔅'"
  unfolding assms by (rule is_dghm_axioms)

mk_ide rf is_dghm_def[unfolded is_dghm_axioms_def]
  |intro is_dghmI|
  |dest is_dghmD[dest]|
  |elim is_dghmE[elim]|

lemmas [dg_cs_intros] = is_dghmD(3,4)


text‹Elementary properties.›

lemma dghm_eqI:
  assumes "𝔊 : 𝔄 ↦↦DGα𝔅" 
    and "𝔉 :  ↦↦DGα𝔇"
    and "𝔊ObjMap = 𝔉ObjMap"
    and "𝔊ArrMap = 𝔉ArrMap"
    and "𝔄 = "
    and "𝔅 = 𝔇"
  shows "𝔊 = 𝔉"
proof-
  interpret L: is_dghm α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret R: is_dghm α  𝔇 𝔉 by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟 𝔊 = 4" 
      by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
    from assms(5,6) have sup: "𝔊HomDom = 𝔉HomDom" "𝔊HomCod = 𝔉HomCod" 
      by (simp_all add: dg_cs_simps)
    show "a  𝒟 𝔊  𝔊a = 𝔉a" for a 
      by (unfold dom, elim_in_numeral, insert assms(3,4) sup)
        (auto simp: dghm_field_simps)
  qed (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps cs_intro: V_cs_intros)+
qed

lemma (in is_dghm) dghm_def: "𝔉 = [𝔉ObjMap, 𝔉ArrMap, 𝔉HomDom, 𝔉HomCod]"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟 𝔉 = 4" 
    by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
  have dom_rhs: "𝒟 [𝔉ObjMap, 𝔉ArrMap, 𝔉HomDom, 𝔉HomCod] = 4"
    by (simp add: nat_omega_simps)
  then show "𝒟 𝔉 = 𝒟 [𝔉ObjMap, 𝔉ArrMap, 𝔉HomDom, 𝔉HomCod]"
    unfolding dom_lhs dom_rhs by (simp add: nat_omega_simps)
  show "a  𝒟 𝔉  𝔉a = [𝔉ObjMap, 𝔉ArrMap, 𝔉HomDom, 𝔉HomCod]a" 
    for a
    by (unfold dom_lhs, elim_in_numeral, unfold dghm_field_simps)
      (simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)

lemma (in is_dghm) dghm_ObjMap_app_in_HomCod_Obj[dg_cs_intros]:
  assumes "a  𝔄Obj"
  shows "𝔉ObjMapa  𝔅Obj"
  using assms dghm_ObjMap_vrange by (blast dest: ObjMap.vsv_vimageI2)

lemmas [dg_cs_intros] = is_dghm.dghm_ObjMap_app_in_HomCod_Obj

lemma (in is_dghm) dghm_ArrMap_vrange: " (𝔉ArrMap)  𝔅Arr"
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
  fix f assume "f  𝔄Arr"
  then obtain a b where "f : a 𝔄b" by auto
  then have "𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb" 
    by (cs_concl cs_shallow cs_intro: dg_cs_intros)
  then show "𝔉ArrMapf  𝔅Arr" by auto
qed auto

lemma (in is_dghm) dghm_ArrMap_app_in_HomCod_Arr[dg_cs_intros]:
  assumes "a  𝔄Arr"
  shows "𝔉ArrMapa  𝔅Arr"
  using assms dghm_ArrMap_vrange by (blast dest: ArrMap.vsv_vimageI2)

lemmas [dg_cs_intros] = is_dghm.dghm_ArrMap_app_in_HomCod_Arr


text‹Size.›

lemma (in is_dghm) dghm_ObjMap_vsubset_Vset: "𝔉ObjMap  Vset α"
  by 
    (
      rule ObjMap.vbrelation_Limit_vsubset_VsetI, 
      insert dghm_ObjMap_vrange HomCod.dg_Obj_vsubset_Vset
    )
    (auto intro!: HomDom.dg_Obj_vsubset_Vset)

lemma (in is_dghm) dghm_ArrMap_vsubset_Vset: "𝔉ArrMap  Vset α"
  by 
    (
      rule ArrMap.vbrelation_Limit_vsubset_VsetI, 
      insert dghm_ArrMap_vrange HomCod.dg_Arr_vsubset_Vset
    )
    (auto intro!: HomDom.dg_Arr_vsubset_Vset)

lemma (in is_dghm) dghm_ObjMap_in_Vset: 
  assumes "α  β"
  shows "𝔉ObjMap  Vset β" 
  by (meson assms dghm_ObjMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in is_dghm) dghm_ArrMap_in_Vset:
  assumes  "α  β"
  shows "𝔉ArrMap  Vset β"
  by (meson assms dghm_ArrMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in is_dghm) dghm_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "𝔉  Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [dg_cs_intros] = 
    dghm_ObjMap_in_Vset dghm_ArrMap_in_Vset HomDom.dg_in_Vset HomCod.dg_in_Vset
  from assms(2) show ?thesis
    by (subst dghm_def) 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros
      )
qed

lemma (in is_dghm) dghm_is_dghm_if_ge_Limit:
  assumes "𝒵 β" and "α  β"
  shows "𝔉 : 𝔄 ↦↦DGβ𝔅"
proof(rule is_dghmI)
  from is_dghm_axioms assms show "digraph β 𝔄"
    by (cs_concl cs_intro: digraph.dg_digraph_if_ge_Limit dg_cs_intros)
  from is_dghm_axioms assms show "digraph β 𝔅"
    by (cs_concl cs_intro: digraph.dg_digraph_if_ge_Limit dg_cs_intros)
qed 
  (
    cs_concl 
      cs_simp: dg_cs_simps 
      cs_intro: assms(1) dg_cs_intros V_cs_intros dghm_ObjMap_vrange
  )+

lemma small_all_dghms[simp]: "small {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦DGα𝔅}"
proof(cases 𝒵 α)
  case True
  from is_dghm.dghm_in_Vset show ?thesis
    by (intro down[of _ Vset (α + ω)] subsetI)
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦DGα𝔅} = {}" by auto
  then show ?thesis by simp
qed

lemma (in is_dghm) dghm_in_Vset_7: "𝔉  Vset (α + 7)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], dg_cs_intros] =
    dghm_ObjMap_vsubset_Vset 
    dghm_ArrMap_vsubset_Vset 
  from HomDom.dg_digraph_in_Vset_4 have [dg_cs_intros]:
    "𝔄  Vset (succ (succ (succ (succ α))))"
    by (succ_of_numeral) 
      (cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
  from HomCod.dg_digraph_in_Vset_4 have [dg_cs_intros]:
    "𝔅  Vset (succ (succ (succ (succ α))))"
    by (succ_of_numeral) 
      (cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
  show ?thesis
    by (subst dghm_def, succ_of_numeral)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps dg_cs_simps 
          cs_intro: dg_cs_intros V_cs_intros
      )
qed

lemma (in 𝒵) all_dghms_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "all_dghms α  Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "all_dghms α  Vset (α + 7)"
  proof(intro vsubsetI)
    fix 𝔉 assume "𝔉  all_dghms α"
    then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦DGα𝔅" by clarsimp
    interpret is_dghm α 𝔄 𝔅 𝔉 using 𝔉 by simp
    show "𝔉  Vset (α + 7)" by (rule dghm_in_Vset_7)
  qed
  from assms(2) show "Vset (α + 7)  Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma small_dghms[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦DGα𝔅}"
  by (rule down[of _ set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦DGα𝔅}]) auto


text‹Further properties.›

lemma (in is_dghm) dghm_is_arr_HomCod: 
  assumes "f : a 𝔄b"
  shows "𝔉ArrMapf  𝔅Arr" "𝔉ObjMapa  𝔅Obj" "𝔉ObjMapb  𝔅Obj" 
  using assms by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+ 

lemma (in is_dghm) dghm_vimage_dghm_ArrMap_vsubset_Hom:
  assumes "a  𝔄Obj" and "b  𝔄Obj"
  shows "𝔉ArrMap ` Hom 𝔄 a b  Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
proof(intro vsubsetI)
  fix g assume "g  𝔉ArrMap ` Hom 𝔄 a b"
  then obtain f where "f  Hom (𝔉HomDom) a b" and "g = 𝔉ArrMapf" 
    by (auto simp: dg_cs_simps)
  then show "g  Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
    by (simp add: dghm_ArrMap_is_arr dg_cs_simps)
qed



subsection‹Opposite digraph homomorphism›


subsubsection‹Definition and elementary properties›


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

definition op_dghm :: "V  V"
  where "op_dghm 𝔉 =
    [𝔉ObjMap, 𝔉ArrMap, op_dg (𝔉HomDom), op_dg (𝔉HomCod)]"


text‹Components.›

lemma op_dghm_components[dg_op_simps]:
  shows "op_dghm 𝔉ObjMap = 𝔉ObjMap"
    and "op_dghm 𝔉ArrMap = 𝔉ArrMap"
    and "op_dghm 𝔉HomDom = op_dg (𝔉HomDom)"
    and "op_dghm 𝔉HomCod = op_dg (𝔉HomCod)"
  unfolding op_dghm_def dghm_field_simps by (auto simp: nat_omega_simps)


subsubsection‹Further properties›

lemma (in is_dghm) is_dghm_op: "op_dghm 𝔉 : op_dg 𝔄 ↦↦DGαop_dg 𝔅"
proof(intro is_dghmI, unfold dg_op_simps)
  show "vfsequence (op_dghm 𝔉)" unfolding op_dghm_def by simp
  show "vcard (op_dghm 𝔉) = 4"
    unfolding op_dghm_def by (auto simp: nat_omega_simps)
qed 
  (
    cs_concl cs_shallow 
      cs_intro: dghm_ObjMap_vrange dg_cs_intros dg_op_intros V_cs_intros 
      cs_simp: dg_cs_simps dg_op_simps
  )+

lemma (in is_dghm) is_dghm_op'[dg_op_intros]:  
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅" and "α' = α"
  shows "op_dghm 𝔉 : 𝔄' ↦↦DGα'𝔅'"
  unfolding assms by (rule is_dghm_op)

lemmas is_dghm_op[dg_op_intros] = is_dghm.is_dghm_op'

lemma (in is_dghm) dghm_op_dghm_op_dghm[dg_op_simps]: "op_dghm (op_dghm 𝔉) = 𝔉" 
  using is_dghm_axioms
  by 
    (
      cs_concl cs_shallow 
        cs_simp: dg_op_simps 
        cs_intro: dg_op_intros dghm_eqI[where 𝔉=𝔉]
    )

lemmas dghm_op_dghm_op_dghm[dg_op_simps] = is_dghm.dghm_op_dghm_op_dghm

lemma eq_op_dghm_iff[dg_op_simps]: 
  assumes "𝔊 : 𝔄 ↦↦DGα𝔅" and "𝔉 :  ↦↦DGα𝔇"
  shows "op_dghm 𝔊 = op_dghm 𝔉  𝔊 = 𝔉"
proof
  interpret L: is_dghm α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret R: is_dghm α  𝔇 𝔉 by (rule assms(2))
  assume prems: "op_dghm 𝔊 = op_dghm 𝔉"
  show "𝔊 = 𝔉"
  proof(rule dghm_eqI[OF assms])
    from prems R.dghm_op_dghm_op_dghm L.dghm_op_dghm_op_dghm show 
      "𝔊ObjMap = 𝔉ObjMap" and "𝔊ArrMap = 𝔉ArrMap"
      by metis+
    from prems R.dghm_op_dghm_op_dghm L.dghm_op_dghm_op_dghm have 
      "𝔊HomDom = 𝔉HomDom" "𝔊HomCod = 𝔉HomCod"
      by auto
    then show "𝔄 = " "𝔅 = 𝔇" by (auto simp: dg_cs_simps)
  qed
qed auto



subsection‹Composition of covariant digraph homomorphisms›


subsubsection‹Definition and elementary properties›


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

definition dghm_comp :: "V  V  V" (infixl DGHM 55)
  where "𝔊 DGHM 𝔉 =
    [𝔊ObjMap  𝔉ObjMap, 𝔊ArrMap  𝔉ArrMap, 𝔉HomDom, 𝔊HomCod]"


text‹Components.›

lemma dghm_comp_components:
  shows "(𝔊 DGHM 𝔉)ObjMap = 𝔊ObjMap  𝔉ObjMap"
    and "(𝔊 DGHM 𝔉)ArrMap = 𝔊ArrMap  𝔉ArrMap"
    and [dg_shared_cs_simps, dg_cs_simps]: "(𝔊 DGHM 𝔉)HomDom = 𝔉HomDom"
    and [dg_shared_cs_simps, dg_cs_simps]: "(𝔊 DGHM 𝔉)HomCod = 𝔊HomCod"
  unfolding dghm_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

lemma dghm_comp_ObjMap_vsv[dg_cs_intros]: 
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "vsv ((𝔊 DGHM 𝔉)ObjMap)"
proof-
  interpret L: is_dghm α 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis by (cs_concl cs_simp: dghm_comp_components cs_intro: V_cs_intros)
qed

lemma dghm_comp_ObjMap_vdomain[dg_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "𝒟 ((𝔊 DGHM 𝔉)ObjMap) = 𝔄Obj"
  using assms 
  by 
    (
      cs_concl 
        cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
        cs_intro: is_dghm.dghm_ObjMap_vrange
    )

lemma dghm_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows " ((𝔊 DGHM 𝔉)ObjMap)  Obj"
  using assms 
  by 
    (
      cs_concl cs_shallow
        cs_simp: dghm_comp_components 
        cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros
    )

lemma dghm_comp_ObjMap_app[dg_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅" and "a  𝔄Obj"
  shows "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
proof-
  interpret L: is_dghm α 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  from assms(3) show "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa" 
    by 
      (
        cs_concl  
          cs_simp: dghm_comp_components dg_cs_simps V_cs_simps 
          cs_intro: V_cs_intros dg_cs_intros
      )
qed


subsubsection‹Arrow map›

lemma dghm_comp_ArrMap_vsv[dg_cs_intros]: 
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "vsv ((𝔊 DGHM 𝔉)ArrMap)"
proof-
  interpret L: is_dghm α 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by (cs_concl cs_simp: dghm_comp_components cs_intro: V_cs_intros)
qed

lemma dghm_comp_ArrMap_vdomain[dg_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "𝒟 ((𝔊 DGHM 𝔉)ArrMap) = 𝔄Arr"
  using assms 
  by 
    (
      cs_concl 
        cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
        cs_intro: is_dghm.dghm_ArrMap_vrange
    )

lemma dghm_comp_ArrMap_vrange[dg_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows " ((𝔊 DGHM 𝔉)ArrMap)  Arr"
  using assms 
  by 
    (
      cs_concl cs_shallow
        cs_simp: dghm_comp_components 
        cs_intro: is_dghm.dghm_ArrMap_vrange V_cs_intros
    )

lemma dghm_comp_ArrMap_app[dg_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅" and "f  𝔄Arr"
  shows "(𝔊 DGHM 𝔉)ArrMapf = 𝔊ArrMap𝔉ArrMapf"
proof-
  interpret L: is_dghm α 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  from assms(3) show "(𝔊 DGHM 𝔉)ArrMapf = 𝔊ArrMap𝔉ArrMapf"
    by 
      (
        cs_concl 
          cs_simp: dghm_comp_components dg_cs_simps V_cs_simps 
          cs_intro: V_cs_intros dg_cs_intros
      )
qed


subsubsection‹Opposite of the composition of covariant digraph homomorphisms›

lemma op_dghm_dghm_comp[dg_op_simps]: 
  "op_dghm (𝔊 DGHM 𝔉) = op_dghm 𝔊 DGHM op_dghm 𝔉"
  unfolding dghm_comp_def op_dghm_def dghm_field_simps
  by (simp add: nat_omega_simps)


subsubsection‹Further properties›

lemma dghm_comp_is_dghm[dg_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 ↦↦DGα"
proof-
  interpret L: is_dghm α 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
  proof(intro is_dghmI is_dghmI, unfold dg_cs_simps)  
    show "vfsequence (𝔊 DGHM 𝔉)" unfolding dghm_comp_def by simp
    show "vcard (𝔊 DGHM 𝔉) = 4" 
      unfolding dghm_comp_def by (simp add: nat_omega_simps)
    fix f a b assume "f : a 𝔄b"
    with assms show "(𝔊 DGHM 𝔉)ArrMapf : 
      (𝔊 DGHM 𝔉)ObjMapa (𝔊 DGHM 𝔉)ObjMapb"
      by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed 
    (
      use assms in 
        cs_concl cs_shallow
            cs_intro: dg_cs_intros dghm_comp_ObjMap_vrange 
            cs_simp: dg_cs_simps
    )+
qed

lemma dghm_comp_assoc[dg_cs_simps]:
  assumes " :  ↦↦DGα𝔇" and "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "( DGHM 𝔊) DGHM 𝔉 =  DGHM (𝔊 DGHM 𝔉)"
proof(rule dghm_eqI [of α 𝔄 𝔇 _ 𝔄 𝔇])
  show "( DGHM 𝔊 DGHM 𝔉)ObjMap = ( DGHM (𝔊 DGHM 𝔉))ObjMap"
  proof(rule vsv_eqI)
    show "( DGHM 𝔊 DGHM 𝔉)ObjMapa = ( DGHM (𝔊 DGHM 𝔉))ObjMapa"
      if "a  𝒟 (( DGHM 𝔊 DGHM 𝔉)ObjMap)" for a 
      using that assms
      by 
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed (use assms in cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
  show "( DGHM 𝔊 DGHM 𝔉)ArrMap = ( DGHM (𝔊 DGHM 𝔉))ArrMap"
  proof(rule vsv_eqI)
    show "( DGHM 𝔊 DGHM 𝔉)ArrMapa = ( DGHM (𝔊 DGHM 𝔉))ArrMapa"
      if "a  𝒟 (( DGHM 𝔊 DGHM 𝔉)ArrMap)" for a 
      using that assms
      by 
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  qed 
    (
      use assms in 
        cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros
    )+
qed (use assms in cs_concl cs_shallow cs_intro: dg_cs_intros)+



subsection‹Composition of contravariant digraph homomorphisms›


subsubsection‹Definition and elementary properties›


text‹See section 1.2 in cite"bodo_categories_1970".›

definition dghm_cn_comp :: "V  V  V" (infixl DGHM 55)
  where "𝔊 DGHM 𝔉 =
    [
      𝔊ObjMap  𝔉ObjMap,
      𝔊ArrMap  𝔉ArrMap,
      op_dg (𝔉HomDom), 
      𝔊HomCod
    ]"


text‹Components.›

lemma dghm_cn_comp_components:
  shows "(𝔊 DGHM 𝔉)ObjMap = 𝔊ObjMap  𝔉ObjMap"
    and "(𝔊 DGHM 𝔉)ArrMap = 𝔊ArrMap  𝔉ArrMap"
    and [dg_cn_cs_simps]: "(𝔊 DGHM 𝔉)HomDom = op_dg (𝔉HomDom)"
    and [dg_cn_cs_simps]: "(𝔊 DGHM 𝔉)HomCod = 𝔊HomCod"
  unfolding dghm_cn_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map: two contravariant digraph homomorphisms›

lemma dghm_cn_comp_ObjMap_vsv[dg_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows "vsv ((𝔊 DGHM 𝔉)ObjMap)"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α op_dg 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed

lemma dghm_cn_comp_ObjMap_vdomain[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows "𝒟 ((𝔊 DGHM 𝔉)ObjMap) = 𝔄Obj"
  using assms 
  by 
    (
      cs_concl  
        cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
        cs_intro: is_dghm.dghm_ObjMap_vrange 
    )

lemma dghm_cn_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows " ((𝔊 DGHM 𝔉)ObjMap)  Obj"
  using assms 
  by 
    (
      cs_concl cs_shallow
        cs_simp: dghm_cn_comp_components
        cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros 
    )

lemma dghm_cn_comp_ObjMap_app[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅" and "a  𝔄Obj"
  shows "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α op_dg 𝔄 𝔅 𝔉 by (rule assms(2))
  from assms(3) show "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
    by 
      (
        cs_concl 
          cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps 
          cs_intro: V_cs_intros dg_cs_intros
      )
qed


subsubsection‹Arrow map: two contravariant digraph homomorphisms›

lemma dghm_cn_comp_ArrMap_vsv[dg_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows "vsv ((𝔊 DGHM 𝔉)ArrMap)"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α op_dg 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed

lemma dghm_cn_comp_ArrMap_vdomain[dg_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows "𝒟 ((𝔊 DGHM 𝔉)ArrMap) = 𝔄Arr"
  using assms 
  by 
    (
      cs_concl  
        cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
        cs_intro: is_dghm.dghm_ArrMap_vrange 
    )

lemma dghm_cn_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows " ((𝔊 DGHM 𝔉)ArrMap)  Arr"
  using assms 
  by 
    (
      cs_concl cs_shallow 
        cs_simp: dghm_cn_comp_components
        cs_intro: is_dghm.dghm_ArrMap_vrange V_cs_intros 
    )

lemma dghm_cn_comp_ArrMap_app[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅" and "a  𝔄Arr"
  shows "(𝔊 DGHM 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α op_dg 𝔄 𝔅 𝔉 by (rule assms(2))
  from assms(3) show "(𝔊 DGHM 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa"
    by 
      (
        cs_concl 
          cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps 
          cs_intro: V_cs_intros dg_cs_intros
      )
qed


subsubsection‹Object map: contravariant and covariant digraph homomorphisms›

lemma dghm_cn_cov_comp_ObjMap_vsv[dg_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "vsv ((𝔊 DGHM 𝔉)ObjMap)"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed

lemma dghm_cn_cov_comp_ObjMap_vdomain[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "𝒟 ((𝔊 DGHM 𝔉)ObjMap) = 𝔄Obj"
  using assms 
  by 
    (
      cs_concl  
        cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
        cs_intro: is_dghm.dghm_ObjMap_vrange 
    )

lemma dghm_cn_cov_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows " ((𝔊 DGHM 𝔉)ObjMap)  Obj"
  using assms
  by
    (
      cs_concl cs_shallow
        cs_simp: dghm_cn_comp_components
        cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros 
    )

lemma dghm_cn_cov_comp_ObjMap_app[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅" and "a  𝔄Obj"
  shows "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  from assms show "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa" 
    by 
      (
        cs_concl  
          cs_simp: dghm_cn_comp_components dg_cs_simps V_cs_simps 
          cs_intro: V_cs_intros dg_op_intros dg_cs_intros
      )
qed


subsubsection‹Arrow map: contravariant and covariant digraph homomorphisms›

lemma dghm_cn_cov_comp_ArrMap_vsv[dg_cn_cs_intros]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "vsv ((𝔊 DGHM 𝔉)ArrMap)"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by (cs_concl cs_simp: dghm_cn_comp_components cs_intro: V_cs_intros)
qed

lemma dghm_cn_cov_comp_ArrMap_vdomain[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "𝒟 ((𝔊 DGHM 𝔉)ArrMap) = 𝔄Arr"
  using assms 
  by 
    (
      cs_concl  
        cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
        cs_intro: is_dghm.dghm_ArrMap_vrange 
    )

lemma dghm_cn_cov_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows " ((𝔊 DGHM 𝔉)ArrMap)  Arr"
  using assms 
  by 
    (
      cs_concl cs_shallow 
        cs_simp: dghm_cn_comp_components
        cs_intro: is_dghm.dghm_ArrMap_vrange V_cs_intros 
    )

lemma dghm_cn_cov_comp_ArrMap_app[dg_cn_cs_simps]:
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅" and "a  𝔄Arr"
  shows "(𝔊 DGHM 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  from assms(3) show "(𝔊 DGHM 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa" 
    by 
      (
        cs_concl  
          cs_simp: dghm_cn_comp_components dg_cs_simps V_cs_simps 
          cs_intro: V_cs_intros dg_op_intros dg_cs_intros
      )
qed


subsubsection‹
Opposite of the contravariant composition of the digraph homomorphisms
›

lemma op_dghm_dghm_cn_comp[dg_op_simps]: 
  "op_dghm (𝔊 DGHM 𝔉) = op_dghm 𝔊 DGHM op_dghm 𝔉"
  unfolding op_dghm_def dghm_cn_comp_def dghm_field_simps
  by (auto simp: nat_omega_simps)


subsubsection‹Further properties›

lemma dghm_cn_comp_is_dghm[dg_cn_cs_intros]:
  ―‹See section 1.2 in \cite{bodo_categories_1970}.›
  assumes "digraph α 𝔄" and "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 ↦↦DGα"
proof-
  interpret 𝔄: digraph α 𝔄 by (rule assms(1))
  interpret L: is_dghm α op_dg 𝔅  𝔊 using assms(2) by auto
  interpret R: is_dghm α op_dg 𝔄 𝔅 𝔉 using assms(3) by auto
  show ?thesis
  proof(intro is_dghmI, unfold dg_op_simps dg_cs_simps dg_cn_cs_simps)
    show "vfsequence (𝔊 DGHM 𝔉)" unfolding dghm_cn_comp_def by auto
    show "vcard (𝔊 DGHM 𝔉) = 4"
      unfolding dghm_cn_comp_def by (simp add: nat_omega_simps)
    fix f a b assume "f : a 𝔄b"
    with assms show "(𝔊 DGHM 𝔉)ArrMapf :
      (𝔊 DGHM 𝔉)ObjMapa (𝔊 DGHM 𝔉)ObjMapb"
      by 
        (
          cs_concl   
            cs_simp: dg_cn_cs_simps  
            cs_intro: dg_cs_intros dg_op_intros
        )
  qed 
    ( 
      cs_concl 
        cs_simp: dg_cs_simps dg_cn_cs_simps 
        cs_intro: dghm_cn_comp_ObjMap_vrange dg_cs_intros dg_cn_cs_intros
    )+
qed

lemma dghm_cn_cov_comp_is_dghm[dg_cn_cs_intros]:
  ―‹See section 1.2 in \cite{bodo_categories_1970}.›
  assumes "𝔊 : 𝔅 DG↦↦α" and "𝔉 : 𝔄 ↦↦DGα𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 DG↦↦α"
proof-
  interpret L: is_dghm α op_dg 𝔅  𝔊 by (rule assms(1))
  interpret R: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
  proof(intro is_dghmI, unfold dg_op_simps dg_cs_simps)
    show "vfsequence (𝔊 DGHM 𝔉)" unfolding dghm_cn_comp_def by simp
    show "vcard (𝔊 DGHM 𝔉) = 4" 
      unfolding dghm_cn_comp_def by (auto simp: nat_omega_simps)
    fix f b a assume "f : b 𝔄a"
    with assms show "(𝔊 DGHM 𝔉)ArrMapf : 
      (𝔊 DGHM 𝔉)ObjMapa (𝔊 DGHM 𝔉)ObjMapb"
      by (cs_concl cs_simp: dg_cn_cs_simps dg_op_simps cs_intro: dg_cs_intros)
  qed
    ( 
      cs_concl cs_shallow
        cs_simp: dg_cs_simps dg_cn_cs_simps
        cs_intro:
          dghm_cn_cov_comp_ObjMap_vrange 
          dg_cs_intros dg_cn_cs_intros dg_op_intros 
    )+
qed

lemma dghm_cov_cn_comp_is_dghm:
  ―‹See section 1.2 in \cite{bodo_categories_1970}›
  assumes "𝔊 : 𝔅 ↦↦DGα" and "𝔉 : 𝔄 DG↦↦α𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 DG↦↦α"
  using assms by (rule dghm_comp_is_dghm)



subsection‹Identity digraph homomorphism›


subsubsection‹Definition and elementary properties›


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

definition dghm_id :: "V  V"
  where "dghm_id  = [vid_on (Obj), vid_on (Arr), , ]"


text‹Components.›

lemma dghm_id_components:
  shows "dghm_id ObjMap = vid_on (Obj)" 
    and "dghm_id ArrMap = vid_on (Arr)" 
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_id HomDom = "
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_id HomCod = " 
  unfolding dghm_id_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda dghm_id_components(1)[folded VLambda_vid_on]
  |vsv dghm_id_ObjMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
  |vdomain dghm_id_ObjMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
  |app dghm_id_ObjMap_app[dg_shared_cs_simps, dg_cs_simps]|

lemma dghm_id_ObjMap_vrange[dg_shared_cs_simps, dg_cs_simps]: 
  " (dghm_id ObjMap) = Obj"
  unfolding dghm_id_components by simp


subsubsection‹Arrow map›

mk_VLambda dghm_id_components(2)[folded VLambda_vid_on]
  |vsv dghm_id_ArrMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
  |vdomain dghm_id_ArrMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
  |app dghm_id_ArrMap_app[dg_shared_cs_simps, dg_cs_simps]|

lemma dghm_id_ArrMap_vrange[dg_shared_cs_simps, dg_cs_simps]: 
  " (dghm_id ArrMap) = Arr"
  unfolding dghm_id_components by simp


subsubsection‹Opposite identity digraph homomorphism›

lemma op_dghm_dghm_id[dg_op_simps]: "op_dghm (dghm_id ) = dghm_id (op_dg )"
  unfolding dghm_id_def op_dg_def op_dghm_def dghm_field_simps dg_field_simps
  by (auto simp: nat_omega_simps)


subsubsection‹An identity digraph homomorphism is a digraph homomorphism›

lemma (in digraph) dg_dghm_id_is_dghm: "dghm_id  :  ↦↦DGα"
proof(intro is_dghmI, unfold dg_cs_simps)
  show "vfsequence (dghm_id )" unfolding dghm_id_def by simp
  show "vcard (dghm_id ) = 4"
    unfolding dghm_id_def by (simp add: nat_omega_simps)
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+

lemma (in digraph) dg_dghm_id_is_dghm': 
  assumes "𝔄 = " and "𝔅 = "
  shows "dghm_id  : 𝔄 ↦↦DGα𝔅"
  unfolding assms by (rule dg_dghm_id_is_dghm)

lemmas [dg_cs_intros] = digraph.dg_dghm_id_is_dghm'


subsubsection‹Further properties›

lemma (in is_dghm) dghm_dghm_comp_dghm_id_left: "dghm_id 𝔅 DGHM 𝔉 = 𝔉"
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}).›
proof(rule dghm_eqI [of α 𝔄 𝔅 _ 𝔄 𝔅])
  show "(dghm_id 𝔅 DGHM 𝔉)ObjMap = 𝔉ObjMap"
  proof(rule vsv_eqI)
    show "(dghm_id 𝔅 DGHM 𝔉)ObjMapa = 𝔉ObjMapa"
      if "a  𝒟 ((dghm_id 𝔅 DGHM 𝔉)ObjMap)" for a 
      using that 
      by 
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (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 V_cs_intros)+
  show "(dghm_id 𝔅 DGHM 𝔉)ArrMap = 𝔉ArrMap"
  proof(rule vsv_eqI)
    show "(dghm_id 𝔅 DGHM 𝔉)ArrMapa = 𝔉ArrMapa"
      if "a  𝒟 ((dghm_id 𝔅 DGHM 𝔉)ArrMap)" for a 
      using that 
      by 
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (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 V_cs_intros)+
qed (cs_concl cs_shallow cs_simp: cs_intro: dg_cs_intros)+

lemmas [dg_cs_simps] = is_dghm.dghm_dghm_comp_dghm_id_left

lemma (in is_dghm) dghm_dghm_comp_dghm_id_right: "𝔉 DGHM dghm_id 𝔄 = 𝔉"
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}).›
proof(rule dghm_eqI [of α 𝔄 𝔅 _ 𝔄 𝔅])
  show "(𝔉 DGHM dghm_id 𝔄)ObjMap = 𝔉ObjMap"
  proof(rule vsv_eqI)
    show "(𝔉 DGHM dghm_id 𝔄)ObjMapa = 𝔉ObjMapa"
      if "a  𝒟 ((𝔉 DGHM dghm_id 𝔄)ObjMap)" for a 
      using that 
      by 
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (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 V_cs_intros)+
  show "(𝔉 DGHM dghm_id 𝔄)ArrMap = 𝔉ArrMap"
  proof(rule vsv_eqI)
    show "(𝔉 DGHM dghm_id 𝔄)ArrMapa = 𝔉ArrMapa"
      if "a  𝒟 ((𝔉 DGHM dghm_id 𝔄)ArrMap)" for a 
      using that 
      by 
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (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 V_cs_intros)+
qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+

lemmas [dg_cs_simps] = is_dghm.dghm_dghm_comp_dghm_id_right



subsection‹Constant digraph homomorphism›


subsubsection‹Definition and elementary properties›


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

definition dghm_const :: "V  V  V  V  V"
  where "dghm_const  𝔇 a f =
    [vconst_on (Obj) a, vconst_on (Arr) f, , 𝔇]"


text‹Components.›

lemma dghm_const_components:
  shows "dghm_const  𝔇 a fObjMap = vconst_on (Obj) a" 
    and "dghm_const  𝔇 a fArrMap = vconst_on (Arr) f" 
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_const  𝔇 a fHomDom = "
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_const  𝔇 a fHomCod = 𝔇" 
  unfolding dghm_const_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda dghm_const_components(1)[folded VLambda_vconst_on]
  |vsv dghm_const_ObjMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
  |vdomain dghm_const_ObjMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
  |app dghm_const_ObjMap_app[dg_shared_cs_simps, dg_cs_simps]|


subsubsection‹Arrow map›

mk_VLambda dghm_const_components(2)[folded VLambda_vconst_on]
  |vsv dghm_const_ArrMap_vsv[dg_shared_cs_intros, dg_cs_intros]|
  |vdomain dghm_const_ArrMap_vdomain[dg_shared_cs_simps, dg_cs_simps]|
  |app dghm_const_ArrMap_app[dg_shared_cs_simps, dg_cs_simps]|


subsubsection‹Opposite constant digraph homomorphism›

lemma op_dghm_dghm_const[dg_op_simps]:
  "op_dghm (dghm_const  𝔇 a f) = dghm_const (op_dg ) (op_dg 𝔇) a f"
  unfolding dghm_const_def op_dg_def op_dghm_def dghm_field_simps dg_field_simps
  by (auto simp: nat_omega_simps)


subsubsection‹A constant digraph homomorphism is a digraph homomorphism›

lemma dghm_const_is_dghm: 
  assumes "digraph α " and "digraph α 𝔇" and "f : a 𝔇a"
  shows "dghm_const  𝔇 a f :  ↦↦DGα𝔇"
proof-
  interpret 𝔇: digraph α 𝔇 by (rule assms(2))
  show ?thesis
  proof(intro is_dghmI)
    show "vfsequence (dghm_const  𝔇 a f)"
      unfolding dghm_const_def by simp
    show "vcard (dghm_const  𝔇 a f) = 4"
      unfolding dghm_const_def by (simp add: nat_omega_simps)
  qed 
    (
      use assms in 
        cs_concl 
            cs_simp: dghm_const_components(1) dg_cs_simps
            cs_intro: V_cs_intros dg_cs_intros
    )+
qed

lemma dghm_const_is_dghm'[dg_cs_intros]: 
  assumes "digraph α " 
    and "digraph α 𝔇" 
    and "f : a 𝔇a"
    and "𝔄 = "
    and "𝔅 = 𝔇"
  shows "dghm_const  𝔇 a f : 𝔄 ↦↦DGα𝔅"
  using assms(1-3) unfolding assms(4,5) by (rule dghm_const_is_dghm)


subsubsection‹Further properties›

lemma (in is_dghm) dghm_dghm_comp_dghm_const[dg_cs_simps]:
  assumes "digraph α " and "f : a a"
  shows "dghm_const 𝔅  a f DGHM 𝔉 = dghm_const 𝔄  a f"
proof(rule dghm_eqI)
  interpret: digraph α  by (rule assms(1))
  from assms(2) show "dghm_const 𝔅  a f DGHM 𝔉 : 𝔄 ↦↦DGα"
    by (cs_concl cs_shallow cs_intro: dg_cs_intros)
  with assms(2) have ObjMap_dom_lhs: 
    "𝒟 ((dghm_const 𝔅  a f DGHM 𝔉)ObjMap) = 𝔄Obj"
    and ArrMap_dom_lhs: "𝒟 ((dghm_const 𝔅  a f DGHM 𝔉)ArrMap) = 𝔄Arr"
    by (cs_concl cs_simp: dg_cs_simps)+
  from assms(2) show "dghm_const 𝔄  a f : 𝔄 ↦↦DGα"
    by (cs_concl cs_shallow cs_intro: dg_cs_intros)
  with assms(2) have ObjMap_dom_rhs: "𝒟 (dghm_const 𝔄  a fObjMap) = 𝔄Obj"
    and ArrMap_dom_rhs: "𝒟 (dghm_const 𝔄  a fArrMap) = 𝔄Arr"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps)+
  show "(dghm_const 𝔅  a f DGHM 𝔉)ObjMap = dghm_const 𝔄  a fObjMap"
    by (rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      (
        use assms(2) in 
          cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros
      )+
  show "(dghm_const 𝔅  a f DGHM 𝔉)ArrMap = dghm_const 𝔄  a fArrMap"
    by (rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      (
        use assms(2) in 
          cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros
      )+
qed simp_all

lemmas [dg_cs_simps] = is_dghm.dghm_dghm_comp_dghm_const



subsection‹Faithful digraph homomorphism›


subsubsection‹Definition and elementary properties›


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

locale is_ft_dghm = is_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
  assumes ft_dghm_v11_on_Hom: 
    " a  𝔄Obj; b  𝔄Obj   v11 (𝔉ArrMap l Hom 𝔄 a b)"

syntax "_is_ft_dghm" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦DG.faithfulı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦DG.faithfulα𝔅"  "CONST is_ft_dghm α 𝔄 𝔅 𝔉"


text‹Rules.›

lemma (in is_ft_dghm) is_ft_dghm_axioms'[dghm_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦DG.faithfulα'𝔅'"
  unfolding assms by (rule is_ft_dghm_axioms)

mk_ide rf is_ft_dghm_def[unfolded is_ft_dghm_axioms_def]
  |intro is_ft_dghmI|
  |dest is_ft_dghmD[dest]|
  |elim is_ft_dghmE[elim]|

lemmas [dghm_cs_intros] = is_ft_dghmD(1)

lemma is_ft_dghmI'':
  assumes "𝔉 : 𝔄 ↦↦DGα𝔅"
    and "a b g f.
       g : a 𝔄b; f : a 𝔄b; 𝔉ArrMapg = 𝔉ArrMapf   g = f"
  shows "𝔉 : 𝔄 ↦↦DG.faithfulα𝔅"
proof(intro is_ft_dghmI assms)
  interpret 𝔉: is_dghm α 𝔄 𝔅 𝔉 by (rule assms(1))
  fix a b assume prems: "a  𝔄Obj" "b  𝔄Obj"
  have dom_def: "𝒟 (𝔉ArrMap l Hom 𝔄 a b) = Hom 𝔄 a b"
    by (intro vdomain_vlrestriction_vsubset vsubsetI) (auto simp: dg_cs_simps)
  show "v11 (𝔉ArrMap l Hom 𝔄 a b)"
  proof(intro vsv.vsv_valeq_v11I, unfold dom_def dg_cs_simps)
    from prems show "vsv (𝔉ArrMap l Hom 𝔄 a b)" by auto
    fix g f assume prems:
      "g : a 𝔄b"
      "f : a 𝔄b"
      "(𝔉ArrMap l Hom 𝔄 a b)g = (𝔉ArrMap l Hom 𝔄 a b)f"
    from prems(3,1,2) have 𝔉g_𝔉f: "𝔉ArrMapg = 𝔉ArrMapf"
      by
        (
          cs_prems
            cs_simp: V_cs_simps dg_cs_simps
            cs_intro: V_cs_intros dg_cs_intros
        )
    show "g = f" by (rule assms(2)[OF prems(1,2) 𝔉g_𝔉f])
  qed
qed


subsubsection‹Opposite faithful digraph homomorphism›

lemma (in is_ft_dghm) ft_dghm_op_dghm_is_ft_dghm: 
  "op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.faithfulαop_dg 𝔅"
  by 
    (
      rule is_ft_dghmI, 
      unfold dg_op_simps, 
      cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros
    )
    (auto simp: ft_dghm_v11_on_Hom)

lemma (in is_ft_dghm) ft_dghm_op_dghm_is_ft_dghm'[dg_op_intros]: 
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
  shows "op_dghm 𝔉 : 𝔄' ↦↦DG.faithfulα𝔅'"
  unfolding assms by (rule ft_dghm_op_dghm_is_ft_dghm)

lemmas ft_dghm_op_dghm_is_ft_dghm[dg_op_intros] = 
  is_ft_dghm.ft_dghm_op_dghm_is_ft_dghm'


subsubsection‹
The composition of faithful digraph homomorphisms is a faithful
digraph homomorphism.
›

lemma dghm_comp_is_ft_dghm[dghm_cs_intros]:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}.›
  assumes "𝔊 : 𝔅 ↦↦DG.faithfulα" and "𝔉 : 𝔄 ↦↦DG.faithfulα𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 ↦↦DG.faithfulα"
proof- 
  interpret L: is_ft_dghm α 𝔅  𝔊 using assms(1) by auto
  interpret R: is_ft_dghm α 𝔄 𝔅 𝔉 using assms(2) by auto 
  have inj: 
    " a  𝔄Obj ; b  𝔄Obj   v11 ((𝔊 DGHM 𝔉)ArrMap l Hom 𝔄 a b)"
    for a b
  proof-
    assume prems: "a  𝔄Obj" "b  𝔄Obj"
    then have 𝔊_hom_𝔅: 
      "v11 (𝔊ArrMap l Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb))" 
      by (intro L.ft_dghm_v11_on_Hom) 
        (cs_concl cs_shallow cs_intro: dg_cs_intros)+
    have "v11 (𝔊ArrMap l (𝔉ArrMap ` Hom 𝔄 a b))"
    proof(intro v11_vlrestriction_vsubset[OF 𝔊_hom_𝔅] vsubsetI)
      fix g assume "g  𝔉ArrMap ` Hom 𝔄 a b" 
      then obtain f where f: "f : a 𝔄b" and g_def: "g = 𝔉ArrMapf" 
        by auto
      from f show "g  Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
        by (cs_concl cs_shallow cs_simp: g_def cs_intro: dg_cs_intros)
    qed
    then show "v11 ((𝔊 DGHM 𝔉)ArrMap l Hom 𝔄 a b)"
      unfolding dghm_comp_components
      by (intro v11_vlrestriction_vcomp) (auto simp: R.ft_dghm_v11_on_Hom prems)
  qed
  then show "𝔊 DGHM 𝔉 : 𝔄 ↦↦DG.faithfulα"
    by (intro is_ft_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros) auto
qed


subsubsection‹Further properties›

lemma (in is_ft_dghm) ft_dghm_ArrMap_eqD:
  assumes "g : a 𝔄b" and "f : a 𝔄b" and "𝔉ArrMapg = 𝔉ArrMapf"
  shows "g = f"
proof- 
  from assms(1) have a: "a  𝔄Obj" and b: "b  𝔄Obj" by auto
  interpret ArrMap: v11 𝔉ArrMap l Hom 𝔄 a b 
    by (rule ft_dghm_v11_on_Hom[OF a b])
  have dom_def: "𝒟 (𝔉ArrMap l Hom 𝔄 a b) = Hom 𝔄 a b"
    by (intro vdomain_vlrestriction_vsubset vsubsetI) (auto simp: dg_cs_simps)
  show ?thesis
  proof(rule ArrMap.v11_injective[unfolded dom_def dg_cs_simps, OF assms(1,2)])
    from assms(1,2) show 
      "(𝔉ArrMap l Hom 𝔄 a b)g = (𝔉ArrMap l Hom 𝔄 a b)f"
      by 
        (
          cs_concl 
            cs_simp: dg_cs_simps assms(3) vsv.vlrestriction_atI 
            cs_intro: V_cs_intros dg_cs_intros
        )
  qed
qed



subsection‹Full digraph homomorphism›


subsubsection‹Definition and elementary properties›


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

locale is_fl_dghm = is_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
  assumes fl_dghm_surj_on_Hom: 
    " a  𝔄Obj; b  𝔄Obj  
      𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"

syntax "_is_fl_dghm" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦DG.fullı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦DG.fullα𝔅"  "CONST is_fl_dghm α 𝔄 𝔅 𝔉"


text‹Rules.›

lemma (in is_fl_dghm) is_fl_dghm_axioms'[dghm_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦DG.fullα'𝔅'"
  unfolding assms by (rule is_fl_dghm_axioms)

mk_ide rf is_fl_dghm_def[unfolded is_fl_dghm_axioms_def]
  |intro is_fl_dghmI|
  |dest is_fl_dghmD[dest]|
  |elim is_fl_dghmE[elim]|

lemmas [dghm_cs_intros] = is_fl_dghmD(1)


subsubsection‹Opposite full digraph homomorphism›

lemma (in is_fl_dghm) fl_dghm_op_dghm_is_fl_dghm:
  "op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.fullαop_dg 𝔅"  
  by 
    (
      rule is_fl_dghmI,
      unfold dg_op_simps, 
      cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros
    )
    (auto simp: fl_dghm_surj_on_Hom)

lemma (in is_fl_dghm) fl_dghm_op_dghm_is_fl_dghm'[dg_op_intros]:
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
  shows "op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.fullαop_dg 𝔅"
  unfolding assms by (rule fl_dghm_op_dghm_is_fl_dghm)

lemmas fl_dghm_op_dghm_is_fl_dghm[dg_op_intros] = 
  is_fl_dghm.fl_dghm_op_dghm_is_fl_dghm'


subsubsection‹
The composition of full digraph homomorphisms is a full digraph homomorphism
›

lemma dghm_comp_is_fl_dghm[dghm_cs_intros]:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}.›
  assumes "𝔊 : 𝔅 ↦↦DG.fullα" and "𝔉 : 𝔄 ↦↦DG.fullα𝔅" 
  shows "𝔊 DGHM 𝔉 : 𝔄 ↦↦DG.fullα"
proof- 
  interpret L: is_fl_dghm α 𝔅  𝔊 by (rule assms(1))
  interpret R: is_fl_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  have surj: 
    " a  𝔄Obj; b  𝔄Obj   
      (𝔊 DGHM 𝔉)ArrMap ` (Hom 𝔄 a b) = 
        Hom  ((𝔊 DGHM 𝔉)ObjMapa) ((𝔊 DGHM 𝔉)ObjMapb)"
    for a b
  proof-
    assume prems: "a  𝔄Obj" "b  𝔄Obj"
    have surj_𝔉: "𝔉ArrMap ` Hom 𝔄 a b = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)" 
      by (rule R.fl_dghm_surj_on_Hom[OF prems])
    from prems L.is_dghm_axioms R.is_dghm_axioms have comp_Obj:
      "(𝔊 DGHM 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
      "(𝔊 DGHM 𝔉)ObjMapb = 𝔊ObjMap𝔉ObjMapb"
      by (auto simp: dg_cs_simps)
    have "(𝔊 DGHM 𝔉)ArrMap ` Hom 𝔄 a b = 𝔊ArrMap ` 𝔉ArrMap ` Hom 𝔄 a b"
      unfolding dghm_comp_components by (simp add: vcomp_vimage)
    also from prems have 
      " = Hom  ((𝔊 DGHM 𝔉)ObjMapa) ((𝔊 DGHM 𝔉)ObjMapb)"
      unfolding surj_𝔉 comp_Obj
      by 
        (
          simp add: 
            prems(2) L.fl_dghm_surj_on_Hom R.dghm_ObjMap_app_in_HomCod_Obj
        )
    finally show "(𝔊 DGHM 𝔉)ArrMap ` (Hom 𝔄 a b) =
      Hom  ((𝔊 DGHM 𝔉)ObjMapa) ((𝔊 DGHM 𝔉)ObjMapb)"
      by simp
  qed
  show ?thesis  
    by (rule is_fl_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros)
      (auto simp: surj)
qed



subsection‹Fully faithful digraph homomorphism›


subsubsection‹Definition and elementary properties›


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

locale is_ff_dghm = is_ft_dghm α 𝔄 𝔅 𝔉 + is_fl_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉

syntax "_is_ff_dghm" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦DG.ffı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦DG.ffα𝔅"  "CONST is_ff_dghm α 𝔄 𝔅 𝔉"


text‹Rules.›

lemma (in is_ff_dghm) is_ff_dghm_axioms'[dghm_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦DG.ffα'𝔅'"
  unfolding assms by (rule is_ff_dghm_axioms)

mk_ide rf is_ff_dghm_def
  |intro is_ff_dghmI|
  |dest is_ff_dghmD[dest]|
  |elim is_ff_dghmE[elim]|

lemmas [dghm_cs_intros] = is_ff_dghmD


subsubsection‹Opposite fully faithful digraph homomorphism.›

lemma (in is_ff_dghm) ff_dghm_op_dghm_is_ff_dghm: 
  "op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.ffαop_dg 𝔅"  
  by (rule is_ff_dghmI) (cs_concl cs_shallow cs_intro: dg_op_intros)+

lemma (in is_ff_dghm) ff_dghm_op_dghm_is_ff_dghm'[dg_op_intros]: 
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
  shows "op_dghm 𝔉 : 𝔄' ↦↦DG.ffα𝔅'" 
  unfolding assms by (rule ff_dghm_op_dghm_is_ff_dghm)

lemmas ff_dghm_op_dghm_is_ff_dghm[dg_op_intros] = 
  is_ff_dghm.ff_dghm_op_dghm_is_ff_dghm


subsubsection‹
The composition of fully faithful digraph homomorphisms is 
a fully faithful digraph homomorphism.
›

lemma dghm_comp_is_ff_dghm[dghm_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦DG.ffα" and "𝔉 : 𝔄 ↦↦DG.ffα𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 ↦↦DG.ffα"
  using assms 
  by (intro is_ff_dghmI, elim is_ff_dghmE) (cs_concl cs_intro: dghm_cs_intros)



subsection‹Isomorphism of digraphs›


subsubsection‹Definition and elementary properties›


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

locale is_iso_dghm = is_dghm α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
  assumes iso_dghm_ObjMap_v11: "v11 (𝔉ObjMap)"
    and iso_dghm_ArrMap_v11: "v11 (𝔉ArrMap)"
    and iso_dghm_ObjMap_vrange[dghm_cs_simps]: " (𝔉ObjMap) = 𝔅Obj"
    and iso_dghm_ArrMap_vrange[dghm_cs_simps]: " (𝔉ArrMap) = 𝔅Arr"

syntax "_is_iso_dghm" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦DG.isoı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦DG.isoα𝔅"  "CONST is_iso_dghm α 𝔄 𝔅 𝔉"

sublocale is_iso_dghm  ObjMap: v11 𝔉ObjMap
  rewrites "𝒟 (𝔉ObjMap) = 𝔄Obj" and " (𝔉ObjMap) = 𝔅Obj"
  by
    (
      cs_concl cs_shallow 
        cs_simp: dghm_cs_simps dg_cs_simps cs_intro: iso_dghm_ObjMap_v11
    )+

sublocale is_iso_dghm  ArrMap: v11 𝔉ArrMap
  rewrites "𝒟 (𝔉ArrMap) = 𝔄Arr" and " (𝔉ArrMap) = 𝔅Arr"
  by 
    (
      cs_concl cs_shallow 
        cs_simp: dghm_cs_simps dg_cs_simps cs_intro: iso_dghm_ArrMap_v11
    )+

lemmas [dghm_cs_simps] = 
  is_iso_dghm.iso_dghm_ObjMap_vrange
  is_iso_dghm.iso_dghm_ArrMap_vrange


text‹Rules.›

lemma (in is_iso_dghm) is_iso_dghm_axioms'[dghm_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦DG.isoα'𝔅'"
  unfolding assms by (rule is_iso_dghm_axioms)

mk_ide rf is_iso_dghm_def[unfolded is_iso_dghm_axioms_def]
  |intro is_iso_dghmI|
  |dest is_iso_dghmD[dest]|
  |elim is_iso_dghmE[elim]|


text‹Elementary properties.›

lemma (in is_iso_dghm) iso_dghm_Obj_HomDom_if_Obj_HomCod[elim]:
  assumes "b  𝔅Obj"
  obtains a where "a  𝔄Obj" and "b = 𝔉ObjMapa"
  using assms ObjMap.vrange_atD iso_dghm_ObjMap_vrange by blast

lemma (in is_iso_dghm) iso_dghm_Arr_HomDom_if_Arr_HomCod[elim]:
  assumes "g  𝔅Arr"
  obtains f where "f  𝔄Arr" and "g = 𝔉ArrMapf"
  using assms ArrMap.vrange_atD iso_dghm_ArrMap_vrange by blast

lemma (in is_iso_dghm) iso_dghm_ObjMap_eqE[elim]:
  assumes "𝔉ObjMapa = 𝔉ObjMapb" 
    and "a  𝔄Obj" 
    and "b  𝔄Obj" 
    and "a = b  P"
  shows P
  using assms ObjMap.v11_eq_iff by auto

lemma (in is_iso_dghm) iso_dghm_ArrMap_eqE[elim]:
  assumes "𝔉ArrMapf = 𝔉ArrMapg"
    and "f  𝔄Arr"
    and "g  𝔄Arr"
    and "f = g  P"
  shows P
  using assms ArrMap.v11_eq_iff by auto

sublocale is_iso_dghm  is_ft_dghm 
  by (intro is_ft_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros) auto

sublocale is_iso_dghm  is_fl_dghm
proof
  fix a b assume [intro]: "a  𝔄Obj" "b  𝔄Obj" 
  show "𝔉ArrMap ` Hom 𝔄 a b = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  proof(intro vsubset_antisym vsubsetI)
    fix g assume prems: "g  Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
    then have g: "g : 𝔉ObjMapa 𝔅𝔉ObjMapb" by auto
    then have dom_g: "𝔅Domg = 𝔉ObjMapa" 
      and cod_g: "𝔅Codg = 𝔉ObjMapb" 
      by blast+
    from prems obtain f 
      where [intro, simp]: "f  𝔄Arr" and g_def: "g = 𝔉ArrMapf" 
      by auto
    then obtain a' b' where f: "f : a' 𝔄b'"  by blast
    then have "g : 𝔉ObjMapa' 𝔅𝔉ObjMapb'" 
      by (cs_concl cs_shallow cs_simp: g_def dg_cs_simps cs_intro: dg_cs_intros)
    with g have "𝔉ObjMapa = 𝔉ObjMapa'" and "𝔉ObjMapb = 𝔉ObjMapb'"
      by (metis HomCod.dg_is_arrE cod_g)+
    with f have "a = 𝔄Domf" "b = 𝔄Codf" by auto (*slow*)
    with f show "g  𝔉ArrMap ` Hom 𝔄 a b"  
      by (auto simp: g_def HomDom.dg_is_arrD(4,5) ArrMap.vsv_vimageI1)
  qed (metis ArrMap.vsv_vimageE dghm_ArrMap_is_arr' in_Hom_iff)
qed

sublocale is_iso_dghm  is_ff_dghm by unfold_locales

lemmas (in is_iso_dghm) iso_dghm_is_ff_dghm = is_ff_dghm_axioms
lemmas [dghm_cs_intros] = is_iso_dghm.iso_dghm_is_ff_dghm


subsubsection‹Opposite digraph isomorphisms›

lemma (in is_iso_dghm) is_iso_dghm_op: 
  "op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.isoαop_dg 𝔅"
  by (intro is_iso_dghmI, unfold dg_op_simps)
    (
      cs_concl cs_shallow
        cs_simp: dghm_cs_simps cs_intro: V_cs_intros dg_cs_intros dg_op_intros
    )+

lemma (in is_iso_dghm) is_iso_dghm_op': 
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅"
  shows "op_dghm 𝔉 : 𝔄' ↦↦DG.isoα𝔅'"
  unfolding assms by (rule is_iso_dghm_op)
  
lemmas is_iso_dghm_op[dg_op_intros] = is_iso_dghm.is_iso_dghm_op'


subsubsection‹
The composition of isomorphisms of digraphs is an isomorphism of digraphs
›
 
lemma dghm_comp_is_iso_dghm[dghm_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦DG.isoα" and "𝔉 : 𝔄 ↦↦DG.isoα𝔅"
  shows "𝔊 DGHM 𝔉 : 𝔄 ↦↦DG.isoα"
proof- 
  interpret 𝔉: is_iso_dghm α 𝔄 𝔅 𝔉 using assms by auto
  interpret 𝔊: is_iso_dghm α 𝔅  𝔊 using assms by auto
  show ?thesis
    by (intro is_iso_dghmI, unfold dghm_comp_components)
      (
        cs_concl 
          cs_simp: V_cs_simps dg_cs_simps dghm_cs_simps 
          cs_intro: dg_cs_intros V_cs_intros
      )+
qed


subsubsection‹An identity digraph homomorphism is an isomorphism of digraphs.›

lemma (in digraph) dg_dghm_id_is_iso_dghm: "dghm_id  :  ↦↦DG.isoα"
  by (rule is_iso_dghmI) (simp_all add: dg_dghm_id_is_dghm dghm_id_components)

lemma (in digraph) dg_dghm_id_is_iso_dghm'[dghm_cs_intros]:
  assumes "𝔄' = " and "𝔅' = "
  shows "dghm_id  : 𝔄' ↦↦DG.isoα𝔅'"
  unfolding assms by (rule dg_dghm_id_is_iso_dghm)

lemmas [dghm_cs_intros] = digraph.dg_dghm_id_is_iso_dghm'



subsection‹Inverse digraph homomorphism›


subsubsection‹Definition and elementary properties›

definition inv_dghm :: "V  V"
  where "inv_dghm 𝔉 = [(𝔉ObjMap)¯, (𝔉ArrMap)¯, 𝔉HomCod, 𝔉HomDom]"


text‹Components.›

lemma inv_dghm_components:
  shows "inv_dghm 𝔉ObjMap = (𝔉ObjMap)¯" 
    and "inv_dghm 𝔉ArrMap = (𝔉ArrMap)¯" 
    and [dghm_cs_simps]: "inv_dghm 𝔉HomDom = 𝔉HomCod"
    and [dghm_cs_simps]: "inv_dghm 𝔉HomCod = 𝔉HomDom" 
  unfolding inv_dghm_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

lemma (in is_iso_dghm) inv_dghm_ObjMap_v11[dghm_cs_intros]:
  "v11 (inv_dghm 𝔉ObjMap)"
  unfolding inv_dghm_components by (cs_concl cs_shallow cs_intro: V_cs_intros)

lemmas [dghm_cs_intros] = is_iso_dghm.inv_dghm_ObjMap_v11

lemma (in is_iso_dghm) inv_dghm_ObjMap_vdomain[dghm_cs_simps]:
  "𝒟 (inv_dghm 𝔉ObjMap) = 𝔅Obj"
  unfolding inv_dghm_components by (cs_concl cs_simp: dghm_cs_simps V_cs_simps)

lemmas [dghm_cs_simps] = is_iso_dghm.inv_dghm_ObjMap_vdomain

lemma (in is_iso_dghm) inv_dghm_ObjMap_app[dghm_cs_simps]:
  assumes "a' = 𝔉ObjMapa" and "a  𝔄Obj"
  shows "inv_dghm 𝔉ObjMapa' = a" 
  unfolding inv_dghm_components
  by (metis assms ObjMap.vconverse_atI ObjMap.vsv_vconverse vsv.vsv_appI)

lemmas [