Theory CZH_DG_Small_TDGHM

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for transformations of digraph homomorphisms›
theory CZH_DG_Small_TDGHM
  imports 
    CZH_DG_Small_DGHM
    CZH_DG_TDGHM
begin



subsection‹Transformation of digraph homomorphisms with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_tdghm = 
  𝒵 α + 
  NTDom: is_tm_dghm α 𝔄 𝔅 𝔉 +
  NTCod: is_tm_dghm α 𝔄 𝔅 𝔊 +
  is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑
  for α 𝔄 𝔅 𝔉 𝔊 𝔑

syntax "_is_tm_tdghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦DGHM.tm _ :/ _ ↦↦DG.tmı _)› [51, 51, 51, 51, 51] 51)
translations "𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅" ⇌
  "CONST is_tm_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑"

abbreviation all_tm_tdghms :: "V ⇒ V"
  where "all_tm_tdghms α ≡
    set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}"

abbreviation tm_tdghms :: "V ⇒ V ⇒ V ⇒ V"
  where "tm_tdghms α 𝔄 𝔅 ≡
    set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}"

abbreviation these_tm_tdghms :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "these_tm_tdghms α 𝔄 𝔅 𝔉 𝔊 ≡ 
    set {𝔑. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}"


text‹Rules.›

lemma (in is_tm_tdghm) is_tm_tdghm_axioms'[dg_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "𝔑 : 𝔉' ↦DGHM.tm 𝔊' : 𝔄' ↦↦DG.tm⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tm_tdghm_axioms)

mk_ide rf is_tm_tdghm_def
  |intro is_tm_tdghmI|
  |dest is_tm_tdghmD[dest]|
  |elim is_tm_tdghmE[elim]|

lemmas [dg_small_cs_intros] = is_tm_tdghmD(2,3,4)


text‹Size.›

lemma (in is_tm_tdghm) tm_tdghm_NTMap_in_Vset: "𝔑⦇NTMap⦈ ∈∘ Vset α"
proof-
  show ?thesis
  proof(rule vbrelation.vbrelation_Limit_in_VsetI)
    have "(⋃∘a∈∘ℛ∘ (𝔉⦇ObjMap⦈). ⋃∘b∈∘ℛ∘ (𝔊⦇ObjMap⦈). Hom 𝔅 a b) ∈∘ Vset α"
      by 
        (
          intro 
            NTDom.HomCod.dg_Hom_vifunion_in_Vset
            NTDom.dghm_ObjMap_vrange 
            NTDom.tm_dghm_ObjMap_in_Vset 
            NTCod.dghm_ObjMap_vrange 
            NTCod.tm_dghm_ObjMap_in_Vset
            vrange_in_VsetI
        )+
    moreover have 
      "ℛ∘ (𝔑⦇NTMap⦈) ⊆∘ (⋃∘a∈∘ℛ∘ (𝔉⦇ObjMap⦈). ⋃∘b∈∘ℛ∘ (𝔊⦇ObjMap⦈). Hom 𝔅 a b)"
      by (rule tdghm_NTMap_vrange_vifunion)
    ultimately show "ℛ∘ (𝔑⦇NTMap⦈) ∈∘ Vset α" by (auto simp: dg_cs_simps)
  qed 
    (
      insert NTCod.tm_dghm_HomDom_is_tiny_digraph, 
      auto intro!: NTMap.vbrelation_axioms simp: dg_cs_simps
    )
qed

lemma small_all_tm_tdghms[simp]: 
  "small {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}"
proof(rule down)
  show "{𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅} ⊆
    elts (set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_tdghms if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔑 assume "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
    then obtain 𝔉 𝔊 𝔄 𝔅 where 𝔑: "𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
      by clarsimp
    interpret is_tm_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule 𝔑)
    have "𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘α⇙ 𝔅" by (auto intro: dg_cs_intros)
    then show "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘α⇙ 𝔅" by auto
  qed
qed

lemma small_tm_tdghms[simp]: 
  "small {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}"
  by 
    (
      rule 
        down[
          of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}›
          ]
    )
    auto

lemma small_these_tm_tdghms[simp]: 
  "small {𝔑. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}"
  by 
    (
      rule 
        down[
          of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅}›
          ]
    ) 
    auto


text‹Further elementary results.›

lemma these_tm_tdghms_iff: (*not simp*)
  "𝔑 ∈∘ these_tm_tdghms α 𝔄 𝔅 𝔉 𝔊 ⟷
    𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
  by auto


subsubsection‹
Opposite transformation of digraph homomorphisms with tiny maps
›

lemma (in is_tm_tdghm) is_tm_tdghm_op:
  "op_tdghm 𝔑 : op_dghm 𝔊 ↦DGHM.tm op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.tm⇘α⇙ op_dg 𝔅"
  by (intro is_tm_tdghmI)
    (cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros)+

lemma (in is_tm_tdghm) is_tm_tdghm_op'[dg_op_intros]: 
  assumes "𝔊' = op_dghm 𝔊"
    and "𝔉' = op_dghm 𝔉"
    and "𝔄' = op_dg 𝔄"
    and "𝔅' = op_dg 𝔅"
  shows "op_tdghm 𝔑 : 𝔊' ↦DGHM.tm 𝔉' : 𝔄' ↦↦DG.tm⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_tdghm_op)

lemmas is_tm_tdghm_op[dg_op_intros] = is_tm_tdghm.is_tm_tdghm_op'


subsubsection‹
Composition of a transformation of digraph homomorphisms with tiny
maps and a digraph homomorphism with tiny maps
›

lemma tdghm_dghm_comp_is_tm_tdghm:
  assumes "𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔅 ↦↦DG.tm⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
  shows "𝔑 ∘TDGHM-DGHM ℌ : 𝔉 ∘DGHM ℌ ↦DGHM.tm 𝔊 ∘DGHM ℌ : 𝔄 ↦↦DG.tm⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_tm_tdghm α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_tm_dghm α 𝔄 𝔅 ℌ by (rule assms(2))
  show ?thesis
    by (rule is_tm_tdghmI)
      (
        cs_concl 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_small_cs_intros
      )+
qed

lemma tdghm_dghm_comp_is_tm_tdghm'[dg_small_cs_intros]:
  assumes "𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔅 ↦↦DG.tm⇘α⇙ ℭ" 
    and "ℌ : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
    and "𝔉' = 𝔉 ∘DGHM ℌ"
    and "𝔊' = 𝔊 ∘DGHM ℌ"
  shows "𝔑 ∘TDGHM-DGHM ℌ : 𝔉' ↦DGHM.tm 𝔊' : 𝔄 ↦↦DG.tm⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule tdghm_dghm_comp_is_tm_tdghm)


subsubsection‹
Composition of a digraph homomorphism with tiny maps and a  
transformation of digraph homomorphisms with tiny maps
›

lemma dghm_tdghm_comp_is_tm_tdghm:
  assumes "ℌ : 𝔅 ↦↦DG.tm⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
  shows "ℌ ∘DGHM-TDGHM 𝔑 : ℌ ∘DGHM 𝔉 ↦DGHM.tm ℌ ∘DGHM 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ ℭ"
proof-
  interpret ℌ: is_tm_dghm α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_tm_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
    by (rule is_tm_tdghmI)
      (
        cs_concl 
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_small_cs_intros
      )+
qed

lemma dghm_tdghm_comp_is_tm_tdghm'[dg_small_cs_intros]:
  assumes "ℌ : 𝔅 ↦↦DG.tm⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦DGHM.tm 𝔊 : 𝔄 ↦↦DG.tm⇘α⇙ 𝔅"
    and "𝔉' = ℌ ∘DGHM 𝔉"
    and "𝔊' = ℌ ∘DGHM 𝔊"
  shows "ℌ ∘DGHM-TDGHM 𝔑 : 𝔉' ↦DGHM.tm 𝔊' : 𝔄 ↦↦DG.tm⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule dghm_tdghm_comp_is_tm_tdghm)



subsection‹Transformation of homomorphisms of tiny digraphs›


subsubsection‹Definition and elementary properties›

locale is_tiny_tdghm = 
  𝒵 α + 
  NTDom: is_tiny_dghm α 𝔄 𝔅 𝔉 +
  NTCod: is_tiny_dghm α 𝔄 𝔅 𝔊 +
  is_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑
  for α 𝔄 𝔅 𝔉 𝔊 𝔑

syntax "_is_tiny_tdghm" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦DGHM.tiny _ :/ _ ↦↦DG.tinyı _)› [51, 51, 51, 51, 51] 51)
translations "𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅" ⇌
  "CONST is_tiny_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑"

abbreviation all_tiny_tdghms :: "V ⇒ V"
  where "all_tiny_tdghms α ≡ 
    set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}"

abbreviation tiny_tdghms :: "V ⇒ V ⇒ V ⇒ V"
  where "tiny_tdghms α 𝔄 𝔅 ≡ 
    set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}"

abbreviation these_tiny_tdghms :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "these_tiny_tdghms α 𝔄 𝔅 𝔉 𝔊 ≡ 
    set {𝔑. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}"


text‹Rules.›

lemmas (in is_tiny_tdghm) [dg_small_cs_intros] = is_tiny_tdghm_axioms

mk_ide rf is_tiny_tdghm_def
  |intro is_tiny_tdghmI[intro]|
  |dest is_tiny_tdghmD[dest]|
  |elim is_tiny_tdghmE[elim]|

lemmas [dg_small_cs_intros] = is_tiny_tdghmD(2,3,4)


text‹Elementary properties.›

sublocale is_tiny_tdghm ⊆ is_tm_tdghm
  by (rule is_tm_tdghmI) 
    (auto simp: vfsequence_axioms dg_cs_intros dg_small_cs_intros)

lemmas (in is_tiny_tdghm) tiny_tdghm_is_tm_tdghm = is_tm_tdghm_axioms

lemmas [dg_small_cs_intros] = is_tiny_tdghm.tiny_tdghm_is_tm_tdghm


text‹Size.›

lemma (in is_tiny_tdghm) tiny_tdghm_in_Vset: "𝔑 ∈∘ Vset α"
proof-
  note [dg_cs_intros] =
    tm_tdghm_NTMap_in_Vset
    NTDom.tiny_dghm_in_Vset
    NTCod.tiny_dghm_in_Vset
    NTDom.HomDom.tiny_dg_in_Vset
    NTDom.HomCod.tiny_dg_in_Vset
  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 small_all_tiny_tdghms[simp]:
  "small {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}"
proof(rule down)
  show "{𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅} ⊆ 
    elts (set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_tdghms if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔑 assume "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅"
    then obtain 𝔉 𝔊 𝔄 𝔅 where 𝔑: "𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅"
      by clarsimp
    interpret is_tiny_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule 𝔑)
    have "𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘α⇙ 𝔅" by (auto intro: dg_cs_intros)
    then show "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘α⇙ 𝔅" by auto
  qed
qed

lemma small_tiny_tdghms[simp]: 
  "small {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}"
  by 
    (
      rule 
        down[
          of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}›
          ]
    )
    auto

lemma small_these_tiny_tdghms[simp]: 
  "small {𝔑. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}"
  by 
    (
      rule 
        down[
          of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅}›
          ]
    ) 
    auto

lemma tiny_tdghms_vsubset_Vset[simp]: 
  "set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅} ⊆∘ Vset α"
  (is ‹set ?tdghms ⊆∘ _›)
proof(cases ‹tiny_digraph α 𝔄 ∧ tiny_digraph α 𝔅›)
  case True
  then have "tiny_digraph α 𝔄" and "tiny_digraph α 𝔅" by auto
  show ?thesis 
  proof(rule vsubsetI)
    fix 𝔑 assume "𝔑 ∈∘ set ?tdghms"
    then obtain 𝔉 𝔊 where 𝔉: "𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅" 
      by clarsimp
    interpret is_tiny_tdghm α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule 𝔉)
    from tiny_tdghm_in_Vset show "𝔑 ∈∘ Vset α" by simp
  qed
next
  case False
  then have "set ?tdghms = 0" by fastforce
  then show ?thesis by simp
qed

lemma (in is_tdghm) tdghm_is_tiny_tdghm_if_ge_Limit:
  assumes "𝒵 β" and "α ∈∘ β"
  shows "𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘β⇙ 𝔅" 
proof(intro is_tiny_tdghmI)
  interpret β: 𝒵 β by (rule assms(1))
  show "𝔑 : 𝔉 ↦DGHM 𝔊 : 𝔄 ↦↦DG⇘β⇙ 𝔅"
    by (intro tdghm_is_tdghm_if_ge_Limit)
      (use assms(2) in ‹cs_concl cs_shallow cs_intro: dg_cs_intros›)+
  show "𝔉 : 𝔄 ↦↦DG.tiny⇘β⇙ 𝔅" "𝔊 : 𝔄 ↦↦DG.tiny⇘β⇙ 𝔅"
    by 
      (
        simp_all add:
          NTDom.dghm_is_tiny_dghm_if_ge_Limit
          NTCod.dghm_is_tiny_dghm_if_ge_Limit
          β.𝒵_axioms 
          assms(2)
      )
qed (rule assms(1))


text‹Further elementary results.›

lemma these_tiny_tdghms_iff: (*not simp*)
  "𝔑 ∈∘ these_tiny_tdghms α 𝔄 𝔅 𝔉 𝔊 ⟷
    𝔑 : 𝔉 ↦DGHM.tiny 𝔊 : 𝔄 ↦↦DG.tiny⇘α⇙ 𝔅"
  by auto


subsubsection‹Opposite transformation of homomorphisms of tiny digraphs›

lemma (in is_tiny_tdghm) is_tm_tdghm_op: "op_tdghm 𝔑 :
  op_dghm 𝔊 ↦DGHM.tiny op_dghm 𝔉 : op_dg 𝔄 ↦↦DG.tiny⇘α⇙ op_dg 𝔅"
  by (intro is_tiny_tdghmI)
   (cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros)+

lemma (in is_tiny_tdghm) is_tiny_tdghm_op'[dg_op_intros]: 
  assumes "𝔊' = op_dghm 𝔊"
    and "𝔉' = op_dghm 𝔉"
    and "𝔄' = op_dg 𝔄"
    and "𝔅' = op_dg 𝔅"
  shows "op_tdghm 𝔑 : 𝔊' ↦DGHM.tiny 𝔉' : 𝔄' ↦↦DG.tiny⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_tdghm_op)

lemmas is_tiny_tdghm_op[dg_op_intros] = is_tiny_tdghm.is_tiny_tdghm_op'

text‹\newpage›

end