Theory CZH_DG_Small_DGHM

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for digraph homomorphisms›
theory CZH_DG_Small_DGHM
  imports 
    CZH_DG_Small_Digraph
    CZH_DG_DGHM
begin



subsection‹Digraph homomorphism with tiny maps›


subsubsection‹Definition and elementary properties›


text‹
The following construction is based on the concept
of a ‹small functor› used in \<^cite>‹"shulman_set_2008"›
in the context of the presentation of the set theory ‹ZFC/S›.
›

locale is_tm_dghm =
  is_dghm α 𝔄 𝔅 𝔉 +
  HomDom: digraph α 𝔄 + 
  HomCod: digraph α 𝔅
  for α 𝔄 𝔅 𝔉 +
  assumes tm_dghm_ObjMap_in_Vset[dg_small_cs_intros]: "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and tm_dghm_ArrMap_in_Vset[dg_small_cs_intros]: "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"

syntax "_is_tm_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (‹(_ :/ _ ↦↦⇩D⇩G⇩.⇩t⇩mı _)› [51, 51, 51] 51)
syntax_consts "_is_tm_dghm" ⇌ is_tm_dghm
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅" ⇌ "CONST is_tm_dghm α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_tm_dghm :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_tm_dghm α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅"

syntax "_is_cn_tm_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (‹(_ :/ _ ⇩D⇩G⇩.⇩t⇩m↦↦ı _)› [51, 51, 51] 51)
syntax_consts "_is_cn_tm_dghm" ⇌ is_cn_tm_dghm
translations "𝔉 : 𝔄 ⇩D⇩G⇩.⇩t⇩m↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_tm_dghm α 𝔄 𝔅 𝔉"

abbreviation all_tm_dghms :: "V ⇒ V"
  where "all_tm_dghms α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅}"

abbreviation small_tm_dghms :: "V ⇒ V ⇒ V ⇒ V"
  where "small_tm_dghms α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅}"

lemmas [dg_small_cs_intros] =
  is_tm_dghm.tm_dghm_ObjMap_in_Vset
  is_tm_dghm.tm_dghm_ArrMap_in_Vset


text‹Rules.›

lemma (in is_tm_dghm) is_tm_dghm_axioms'[dg_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩m⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tm_dghm_axioms)

mk_ide rf is_tm_dghm_def[unfolded is_tm_dghm_axioms_def]
  |intro is_tm_dghmI|
  |dest is_tm_dghmD[dest]|
  |elim is_tm_dghmE[elim]|

lemmas [dg_small_cs_intros] = is_tm_dghmD(1)


text‹Elementary properties.›

sublocale is_tm_dghm ⊆ HomDom: tiny_digraph α 𝔄 
proof(rule tiny_digraphI')
  show "𝔄⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_dghm_ObjMap_in_Vset, simplified dg_cs_simps])
  show "𝔄⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_dghm_ArrMap_in_Vset, simplified dg_cs_simps])
qed (cs_concl cs_shallow cs_intro: dg_cs_intros)

lemmas (in is_tm_dghm) 
  tm_dghm_HomDom_is_tiny_digraph = HomDom.tiny_digraph_axioms

lemmas [dg_small_cs_intros] = is_tm_dghm.tm_dghm_HomDom_is_tiny_digraph


text‹Further rules.›

lemma is_tm_dghmI':
  assumes "𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅"
    and [simp]: "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and [simp]: "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
  shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret is_dghm α 𝔄 𝔅 𝔉 by (rule assms(1))
  from assms show ?thesis
    by (intro is_tm_dghmI) (auto simp: vfsequence_axioms dghm_ObjMap_vrange)
qed


text‹Size.›

lemma small_all_tm_dghms[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_dghms if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅"
    then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅" by clarsimp
    interpret is_tm_dghm α 𝔄 𝔅 𝔉 by (rule 𝔉)
    from is_dghm_axioms' show "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" by blast
  qed
qed


subsubsection‹Opposite digraph homomorphism with tiny maps›

lemma (in is_tm_dghm) is_tm_dghm_op: "op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ op_dg 𝔅"
  by (intro is_tm_dghmI', unfold dg_op_simps)
    (cs_concl cs_intro: dg_cs_intros dg_small_cs_intros dg_op_intros)

lemma (in is_tm_dghm) is_tm_dghm_op'[dg_op_intros]:  
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅" and "α' = α"
  shows "op_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩m⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tm_dghm_op)

lemmas is_tm_dghm_op[dg_op_intros] = is_tm_dghm.is_tm_dghm_op'


subsubsection‹Composition of a digraph homomorphism with tiny maps›

lemma dghm_comp_is_tm_dghm[dg_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret 𝔉: is_tm_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tm_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
  show ?thesis
  proof(intro is_tm_dghmI')
    from assms show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ObjMap⦈ ∈⇩∘ Vset α"
      by 
        (
          cs_concl cs_shallow
            cs_simp: dghm_comp_components 
            cs_intro: dg_small_cs_intros Limit_vcomp_in_VsetI 𝔉.Limit_α 
        )+
    from assms show "(𝔊 ∘⇩D⇩G⇩H⇩M 𝔉)⦇ArrMap⦈ ∈⇩∘ Vset α"
      by 
        (
          cs_concl cs_shallow
            cs_simp: dghm_comp_components 
            cs_intro: dg_small_cs_intros Limit_vcomp_in_VsetI 𝔉.Limit_α 
        )+
  qed (auto intro: dg_cs_intros)
qed


subsubsection‹Finite digraphs and digraph homomorphisms with tiny maps›

lemma (in is_dghm) dghm_is_tm_dghm_if_HomDom_finite_digraph:
  assumes "finite_digraph α 𝔄"
  shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔅"
proof(intro is_tm_dghmI')
  interpret 𝔄: finite_digraph α 𝔄 by (rule assms(1))
  show "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
  proof(rule ObjMap.vsv_Limit_vsv_in_VsetI)
    show "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ Vset α"
    proof-
      have "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 𝔅⦇Obj⦈" by (simp add: dghm_ObjMap_vrange)
      moreover have "𝔅⦇Obj⦈ ⊆⇩∘ Vset α"
        by (simp add: HomCod.dg_Obj_vsubset_Vset)
      ultimately show ?thesis by auto
    qed
  qed (auto simp: dg_cs_simps dg_small_cs_intros)
  show "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
  proof(rule ArrMap.vsv_Limit_vsv_in_VsetI)
    show "ℛ⇩∘ (𝔉⦇ArrMap⦈) ⊆⇩∘ Vset α"
    proof-
      have "ℛ⇩∘ (𝔉⦇ArrMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈" by (simp add: dghm_ArrMap_vrange)
      moreover have "𝔅⦇Arr⦈ ⊆⇩∘ Vset α"
        by (simp add: HomCod.dg_Arr_vsubset_Vset)
      ultimately show ?thesis by auto
    qed
  qed (auto simp: dg_cs_simps dg_small_cs_intros)
qed (simp add: dg_cs_intros)


subsubsection‹Constant digraph homomorphism›

lemma dghm_const_is_tm_dghm: 
  assumes "tiny_digraph α ℭ" and "digraph α 𝔇" and "f : a ↦⇘𝔇⇙ a"
  shows "dghm_const ℭ 𝔇 a f : ℭ ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔇"
proof(intro is_tm_dghmI')
  interpret ℭ: tiny_digraph α ℭ by (rule assms(1))
  interpret 𝔇: digraph α 𝔇 by (rule assms(2))
  from assms show "dghm_const ℭ 𝔇 a f : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
  show "dghm_const ℭ 𝔇 a f⦇ObjMap⦈ ∈⇩∘ Vset α"
    unfolding dghm_const_components
  proof(rule vbrelation.vbrelation_Limit_in_VsetI)
    from assms(3) have "a ∈⇩∘ set {a}" 
      by (cs_concl cs_shallow cs_intro: V_cs_intros)
    with assms(3) show "ℛ⇩∘ (vconst_on (ℭ⦇Obj⦈) a) ∈⇩∘ Vset α"
      by 
        (
          cs_concl cs_intro: 
            dg_cs_intros 
            V_cs_intros
            𝔇.dg_in_Obj_in_Vset 
            vsubset_in_VsetI 
            Limit_vsingleton_in_VsetI 
        )
    show "𝒟⇩∘ (vconst_on (ℭ⦇Obj⦈) a) ∈⇩∘ Vset α"
      by (cs_concl cs_simp: V_cs_simps cs_intro: V_cs_intros dg_small_cs_intros)
  qed simp_all
  show "dghm_const ℭ 𝔇 a f⦇ArrMap⦈ ∈⇩∘ Vset α"
    unfolding dghm_const_components
  proof(rule vbrelation.vbrelation_Limit_in_VsetI)
    from assms(3) 𝔇.dg_Arr_vsubset_Vset show
      "ℛ⇩∘ (vconst_on (ℭ⦇Arr⦈) f) ∈⇩∘ Vset α"
      by (cases ‹ℭ⦇Arr⦈=0›)
        (
          auto 
            simp: dg_cs_simps 𝔇.dg_is_arrD(1) 
            intro!: Limit_vsingleton_in_VsetI
        ) 
  qed (auto simp: ℭ.tiny_dg_Arr_in_Vset)
qed

lemma dghm_const_is_tm_dghm'[dg_small_cs_intros]:
  assumes "tiny_digraph α ℭ"
    and "digraph α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "dghm_const ℭ 𝔇 a f : ℭ' ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ 𝔇'"
  using assms(1-3) unfolding assms(4,5) by (rule dghm_const_is_tm_dghm)



subsection‹Tiny digraph homomorphism›


subsubsection‹Definition and elementary properties›

locale is_tiny_dghm = 
  is_dghm α 𝔄 𝔅 𝔉 +
  HomDom: tiny_digraph α 𝔄 + 
  HomCod: tiny_digraph α 𝔅 
  for α 𝔄 𝔅 𝔉

syntax "_is_tiny_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (‹(_ :/ _ ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩yı _)› [51, 51, 51] 51)
syntax_consts "_is_tiny_dghm" ⇌ is_tiny_dghm
translations "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" ⇌ "CONST is_tiny_dghm α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_tiny_dghm :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_tiny_dghm α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"

syntax "_is_cn_tiny_dghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (‹(_ :/ _ ⇩D⇩G⇩.⇩t⇩i⇩n⇩y↦↦ı _)› [51, 51, 51] 51)
syntax_consts "_is_cn_tiny_dghm" ⇌ is_cn_tiny_dghm
translations "𝔉 : 𝔄 ⇩D⇩G⇩.⇩t⇩i⇩n⇩y↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_tiny_dghm α 𝔄 𝔅 𝔉"

abbreviation all_tiny_dghms :: "V ⇒ V"
  where "all_tiny_dghms α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"

abbreviation small_dghms :: "V ⇒ V ⇒ V ⇒ V"
  where "small_dghms α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"


text‹Rules.›

lemma (in is_tiny_dghm) is_tiny_dghm_axioms'[dg_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tiny_dghm_axioms)

mk_ide rf is_tiny_dghm_def
  |intro is_tiny_dghmI|
  |dest is_tiny_dghmD[dest]|
  |elim is_tiny_dghmE[elim]|

lemmas [dg_small_cs_intros] = is_tiny_dghmD(2,3)


text‹Size.›

lemma (in is_tiny_dghm) tiny_dghm_ObjMap_in_Vset[dg_small_cs_intros]: 
  "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
proof-
  have "𝒟⇩∘ (𝔉⦇ObjMap⦈) ∈⇩∘ Vset α" 
    by (simp add: dghm_ObjMap_vdomain HomDom.tiny_dg_Obj_in_Vset)
  moreover from dghm_ObjMap_vrange have "ℛ⇩∘ (𝔉⦇ObjMap⦈) ∈⇩∘ Vset α"
    by (simp add: vsubset_in_VsetI HomCod.tiny_dg_Obj_in_Vset)
  ultimately show "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α" 
    by 
      (
        cs_concl cs_shallow cs_intro: 
          V_cs_intros dg_small_cs_intros ObjMap.vbrelation_Limit_in_VsetI 
      )
qed

lemmas [dg_small_cs_intros] = is_tiny_dghm.tiny_dghm_ObjMap_in_Vset

lemma (in is_tiny_dghm) tiny_dghm_ArrMap_in_Vset[dg_small_cs_intros]: 
  "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
proof-
  have "𝒟⇩∘ (𝔉⦇ArrMap⦈) ∈⇩∘ Vset α"
    by (simp add: dghm_ArrMap_vdomain HomDom.tiny_dg_Arr_in_Vset)
  moreover from HomCod.tiny_dg_Arr_in_Vset dghm_ArrMap_vrange have 
    "ℛ⇩∘ (𝔉⦇ArrMap⦈) ∈⇩∘ Vset α"
    by auto
  ultimately show "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α" 
    by 
      (
        cs_concl cs_shallow cs_intro:  
          V_cs_intros dg_small_cs_intros ArrMap.vbrelation_Limit_in_VsetI
      )
qed

lemmas [dg_small_cs_intros] = is_tiny_dghm.tiny_dghm_ArrMap_in_Vset

lemma (in is_tiny_dghm) tiny_dghm_in_Vset: "𝔉 ∈⇩∘ Vset α"
proof-
  note [dg_cs_intros] = 
    tiny_dghm_ObjMap_in_Vset 
    tiny_dghm_ArrMap_in_Vset
    HomDom.tiny_dg_in_Vset 
    HomCod.tiny_dg_in_Vset 
  show ?thesis
    by (subst dghm_def) 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros
      )
qed

sublocale is_tiny_dghm ⊆ is_tm_dghm
  by (intro is_tm_dghmI') (auto simp: dg_cs_intros dg_small_cs_intros)

lemmas (in is_tiny_dghm) tiny_dghm_is_tm_dghm = is_tm_dghm_axioms

lemmas [dg_small_cs_intros] = is_tiny_dghm.tiny_dghm_is_tm_dghm

lemma small_all_tiny_dghms[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_dghms if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" by clarsimp
    interpret is_tiny_dghm α 𝔄 𝔅 𝔉 by (rule 𝔉)
    from is_dghm_axioms show "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇘α⇙ 𝔅" by auto
  qed
qed

lemma tiny_dghms_vsubset_Vset[simp]: 
  "set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆⇩∘ Vset α"
proof(rule vsubsetI) 
  fix 𝔉 assume "𝔉 ∈⇩∘ all_tiny_dghms α"
  then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" by clarsimp
  then show "𝔉 ∈⇩∘ Vset α" by (auto simp: is_tiny_dghm.tiny_dghm_in_Vset)
qed

lemma (in is_dghm) dghm_is_tiny_dghm_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅"
proof(intro is_tiny_dghmI)
  interpret β: 𝒵 β by (rule assms(1))
  show "𝔉 : 𝔄 ↦↦⇩D⇩G⇘β⇙ 𝔅"
    by (intro dghm_is_dghm_if_ge_Limit)
      (use assms(2) in ‹cs_concl cs_shallow cs_intro: dg_cs_intros›)+
  show "tiny_digraph β 𝔄" "tiny_digraph β 𝔅"
    by 
      (
        simp_all add: 
          assms 
          HomDom.dg_tiny_digraph_if_ge_Limit 
          HomCod.dg_tiny_digraph_if_ge_Limit
      )
qed


subsubsection‹Opposite tiny digraph homomorphism›

lemma (in is_tiny_dghm) is_tiny_dghm_op: 
  "op_dghm 𝔉 : op_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ op_dg 𝔅"
  by (intro is_tiny_dghmI) 
    (cs_concl cs_shallow cs_intro: dg_small_cs_intros dg_cs_intros dg_op_intros)+

lemma (in is_tiny_dghm) is_tiny_dghm_op'[dg_op_intros]:  
  assumes "𝔄' = op_dg 𝔄" and "𝔅' = op_dg 𝔅" and "α' = α"
  shows "op_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tiny_dghm_op)

lemmas is_tiny_dghm_op[dg_op_intros] = is_tiny_dghm.is_tiny_dghm_op'


subsubsection‹Composition of tiny digraph homomorphisms›

lemma dghm_comp_is_tiny_dghm[dg_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩D⇩G⇩H⇩M 𝔉 : 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ ℭ"
proof-
  interpret 𝔉: is_tiny_dghm α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tiny_dghm α 𝔅 ℭ 𝔊 by (rule assms(1))
  show ?thesis 
    by (intro is_tiny_dghmI) 
      (auto simp: dg_small_cs_intros dg_cs_simps intro: dg_cs_intros)
qed


subsubsection‹Tiny constant digraph homomorphism›

lemma dghm_const_is_tiny_dghm:
  assumes "tiny_digraph α ℭ" and "tiny_digraph α 𝔇" and "f : a ↦⇘𝔇⇙ a"
  shows "dghm_const ℭ 𝔇 a f : ℭ ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔇"
proof(intro is_tiny_dghmI)
  from assms show "dghm_const ℭ 𝔇 a f : ℭ ↦↦⇩D⇩G⇘α⇙ 𝔇"
    by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_small_cs_intros)
qed (auto simp: assms(1,2))

lemma dghm_const_is_tiny_dghm'[dg_small_cs_intros]:
  assumes "tiny_digraph α ℭ"
    and "tiny_digraph α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "dghm_const ℭ 𝔇 a f : ℭ' ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔇'"
  using assms(1-3) unfolding assms(4,5) by (rule dghm_const_is_tiny_dghm)

text‹\newpage›

end